Change signature of is-option-active

Author: FissoreD

apps/tc/elpi/compiler.elpi

@@ -97,7 +97,7 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
         (L = [NewPremise | RevPremises])) (L = RevPremises),
     compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _.
 compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- 
-  not (is-option-active {oTC-use-pattern-fragment-compiler}), !,
+  not (is-option-active oTC-use-pattern-fragment-compiler), !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
   make-tc IsHead Ty AppInst Premises Clause.

apps/tc/elpi/solver.elpi

@@ -4,7 +4,7 @@
 pred time-solve i:prop.
 time-solve P :-
   std.time P Time,
-  if (is-option-active {oTC-time}) (coq.say "[TC] Total resolution time is:" Time) true.
+  if (is-option-active oTC-time) (coq.say "[TC] Total resolution time is:" Time) true.
 
 msolve L N :- !,
   time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
@@ -28,7 +28,7 @@ tc-recursive-search Ty Sol :-
   std.time (coq.safe-dest-app Ty (global TC) TL',
     std.append TL' [Sol] TL,
     coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
-  if (is-option-active {oTC-time-instance-search}) (coq.say "[TC] Instance search time is:" Time) true.
+  if (is-option-active oTC-time-instance-search) (coq.say "[TC] Instance search time is:" Time) true.
 
 :if "solve-print-goal"
 solve (goal Ctx _ Ty _ _) _ :-
@@ -80,10 +80,10 @@ solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
       % coq.say "Solution " X "end" X' "caio",
       % std.assert! (ground_term X') "solution not complete",
       % (pi F\ (copy (fun _ _ x\ (app [F, x])) F :- !)) => copy X X',
-      if (is-option-active {oTC-ignore-eta-reduction}) 
+      if (is-option-active oTC-ignore-eta-reduction) 
         (Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
       std.time (refine Proof' G GL) Refine-Time, 
-      if (is-option-active {oTC-time-refine}) (coq.say "[TC] Refine time is:" Refine-Time) true;
+      if (is-option-active oTC-time-refine) (coq.say "[TC] Refine time is:" Refine-Time) true;
       coq.error "illtyped solution:" {coq.term->string Proof}
     ) 
     (GL = [seal G]).

apps/tc/elpi/tc_aux.elpi

@@ -69,7 +69,7 @@ get-last (app L) R :-
 % TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name]
 pred gref->pred-name i:gref, o:string.
 gref->pred-name Gr S :-
-  if (is-option-active {oTC-clauseNameShortName})
+  if (is-option-active oTC-clauseNameShortName)
     (Path = "")
     (coq.gref->path Gr [Hd | Tl], 
       std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 

apps/tc/theories/db.v

@@ -39,9 +39,9 @@ Elpi Db tc_options.db lp:{{
     oTC-use-pattern-fragment-compiler
   ].
 
-  pred is-option-active i:list string.
-  is-option-active Opt :- 
-    coq.option.get Opt (coq.option.bool tt).
+  pred is-option-active i:(list string -> prop).
+  is-option-active Opt :-
+    Opt X, coq.option.get X (coq.option.bool tt).
 }}.
 
 Elpi Db tc.db lp:{{

apps/tc/theories/tc.v

@@ -45,9 +45,8 @@ Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
-    all-options Options,
-    std.forall Options (x\ sigma Args\ x Args, 
-      coq.option.add Args (coq.option.bool ff) ff).
+    std.forall {all-options} (x\ sigma L\ x L, 
+      coq.option.add L (coq.option.bool ff) ff).
 }}.
 Elpi Typecheck.