TC solver 2 #529

gares · 2023-10-30T13:46:49Z

TODO (before/after merge):

toposort tests and ML api
header in all files (with license)
README (what works, commands available)
maybe add an option to disable TC and instance event register
in tests/patternFragment.v we have Unshelved goals (example at line 15)
find a way to encode modes: since classes are compiled at their creation, we should set modes modes before their creation or we should be able to dinamically modify the modes of the parameters of a predicate in elpi after its creation.

Need of elpi and/or coq update:

bool arith in calc (requires API: expose register_eval in builtins.mli elpi#202)
keep reverse mapping from instance to class, from instance to priority-> need of coq API (get_instance_from_gref)

apps/tc/theories/tc.v

gares · 2023-10-30T13:54:21Z

apps/tc/theories/tc.v

+Elpi Command AddInstances.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate File modes.
+Elpi Accumulate File compiler.
+Elpi Accumulate File parser_addInstances.
+Elpi Accumulate lp:{{
+  % The main of the Command
+  main Arguments :- 
+    std.time (parse Arguments Res, run-command Res) T,
+    if (coq.option.get ["TimeAddInstances"] (coq.option.bool tt))
+      (coq.say "Add instance all Time" T) true.
+}}.
+(* Elpi Typecheck. *)
+Elpi Query lp:{{
+  coq.option.add ["TimeAddInstances"] (coq.option.bool ff) ff.
+}}.
+(* Elpi Typecheck. *)


comment: needed if we don't want to also declare the instance in Coq

AddAllInstances class logpath eg AddAllInstances Decidable Coq.stdpp.file..

apps/tc/theories/tc.v

.vscode/settings.json

_CoqProject

apps/tc/Makefile.coq.local

apps/tc/elpi/alias.elpi

apps/tc/elpi/base.elpi

apps/tc/elpi/compiler.elpi

gares · 2023-10-30T14:28:05Z

apps/tc/theories/tc.v

+      std.forall {coq.TC.db-tc} (x\ add-tc-or-inst-gr [] L1 [x])) T,
+    if (coq.option.get ["TimeAddInstances"] (coq.option.bool tt))
+      (coq.say "Add instance Time" T) true.
+}}.


idealli (or TODO) add #[local] AddAllInstances ...

gares · 2023-10-30T14:29:05Z

apps/tc/elpi/compiler.elpi

+% [add-inst->db IgnoreClassDepL ForceAdd Inst] add the Inst to
+% the database except those depending on at least one 
+% inside IgnoreClassDepL
+pred add-inst->db i:list gref, i:bool, i:gref.
+:name "add-inst->db:start"
+add-inst->db IgnoreClassDepL ForceAdd Inst :-
+  coq.env.current-section-path SectionPath,
+  get-sub-classes Inst Dep,
+  warn-multiple-deps Inst Dep,
+  if ((ForceAdd = tt; not (instance _ Inst _)), 
+    not (std.exists Dep (std.mem IgnoreClassDepL)), not (banned Inst)) 
+  (
+    compile Inst _IsLeaf TC-of-Inst Clause, 
+    % TODO: a clause is flexible if an instance is polimorphic (pglobal)
+    not (var Clause),
+    Graft is after (int_to_string {get-inst-prio Inst}),
+    get-full-path Inst ClauseName,
+    if (is-local) (Visibility = [@local!])
+      (if (has-context-deps Inst) 
+        (@local! => add-tc-db _ Graft (instance SectionPath Inst TC-of-Inst))
+        (@global! => add-tc-db _ Graft (instance [] Inst TC-of-Inst)), Visibility = [@global!]),
+    Visibility => add-tc-db ClauseName Graft Clause
+    )
+  true; @global! => add-tc-db _ _ (banned Inst), 
+  coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal".


simplify assuming one calls #[local] AddAllInstances, call add-inst

if (get-option "local" tt) (P = @local!) true, P =>

apps/tc/elpi/compiler.elpi

gares · 2023-10-30T14:32:42Z

apps/tc/elpi/compiler.elpi

+add-tc-or-inst-gr IgnoreDepClass IgnoreInsts Names :-
+  std.map IgnoreDepClass coq.locate IgnoreDepClassGR,
+  std.map IgnoreInsts coq.locate IgnoreInstsGR,
+  std.forall Names (GR\


maybe we can remove these blacklists, since there is a global one already

apps/tc/elpi/create_tc_predicate.elpi

apps/tc/elpi/modes.elpi

apps/tc/elpi/rewrite_forward.elpi

apps/tc/elpi/solver.elpi

apps/tc/tests/bigTest.v

apps/tc/elpi/tc_aux.elpi

apps/tc/tests/stdppInj.v

apps/tc/tests/stdppInjClassic.v