From 889bd3fc16c31f35c850edf5a0df2f70ea9c655a Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 8 Jul 2024 16:27:42 +0200 Subject: [PATCH] [TC] premise w/solution add comment --- apps/tc/elpi/tc_aux.elpi | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index fc7a90631..0ee71c442 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -109,6 +109,16 @@ pred get-mode i:gref, o:list string. get-mode ClassGR M :- class ClassGR _ _ M, !. get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class". +/* +[make-tc.aux B Sol Head Body Rule] builds the rule with the given Head and body + paying attention to the positivity of the + clause +Note: if the Rule being constructed is negative (B = ff), then Rules returns a + solution Sol used inside the proof. If the solution is already given, we + do not run the premise. This would ask Sol to be ground (ground_term S). + Here, for performance issues, we simply check that the solution is not a + flexible term +*/ pred make-tc.aux i:bool, i:term, i:prop, i:list prop, o:prop. make-tc.aux tt _ Head [] Head :- !. make-tc.aux ff Sol Head [] P :- !, P = if (var Sol) Head true.