gitignore and shortened cs predicate name

LPCIC · Jan 26, 2024 · ed96e69 · ed96e69
1 parent f8e854f
commit ed96e69
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 110 deletions.
diff --git a/.gitignore b/.gitignore
@@ -48,3 +48,4 @@ META
 apps/coercion/src/coq_elpi_coercion_hook.ml
 .filestoinstall
 apps/tc/src/coq_elpi_tc_hook.ml
+apps/cs/src/coq_elpi_cs_hook.ml
diff --git a/apps/cs/TODOREADME.md → apps/cs/README.md b/apps/cs/TODOREADME.md → apps/cs/README.md
@@ -4,16 +4,16 @@ The `canonical_solution` app enables to program Coq canonical structure solution
 
 This app is experimental.
 
-## The canonical-solution predicate
+## The cs predicate
 
-The `canonical-solution` predicate lives in the database `cs.db`
+The `cs` predicate lives in the database `cs.db`
 
 ```elpi
-% predicate [canonical-solution Ctx Lhs Rhs] used to unify Lhs with Rhs, with
+% predicate [cs Ctx Lhs Rhs] used to unify Lhs with Rhs, with
 % - [Ctx] is the context
 % - [Lhs] and [Rhs] are the terms to unify
 :index (0 6 6)
-pred canonical-solution i:goal-ctx, o:term, o:term.
+pred cs i:goal-ctx, o:term, o:term.
 ```
 
 By addings rules for this predicate one can recover from a CS instance search failure
@@ -34,7 +34,7 @@ Structure S : Type :=
 
 Elpi Accumulate cs.db lp:{{
 
-canonical-solution _ {{ sort lp:Sol }} {{ nat }} :-
+cs _ {{ sort lp:Sol }} {{ nat }} :-
   Sol = {{ Build_S nat }}.
 
 }}.

diff --git a/apps/cs/src/coq_elpi_cs_hook.ml b/apps/cs/src/coq_elpi_cs_hook.ml
diff --git a/apps/cs/tests/test_cs.v b/apps/cs/tests/test_cs.v
@@ -8,7 +8,7 @@ Structure S : Type :=
 
 Elpi Accumulate cs.db lp:{{
 
-canonical-solution _ {{ sort lp:Sol }} {{ nat }} :-
+cs _ {{ sort lp:Sol }} {{ nat }} :-
   Sol = {{ Build_S nat }}.
 
 }}.
@@ -28,7 +28,7 @@ Check eq_refl _ : (sort1 _) = nat1.
 
 Elpi Accumulate cs.db lp:{{
 
-canonical-solution _ {{ sort lp:Sol }} {{ bool }} :-
+cs _ {{ sort lp:Sol }} {{ bool }} :-
   % typing is wired in, do we want this?
   std.spy(Sol = {{ Prop }}).
 

diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v
@@ -7,7 +7,7 @@ Elpi Db cs.db lp:{{
 % - [Ctx] is the context
 % - [Lhs] and [Rhs] are the terms to unify
 :index (0 6 6)
-pred canonical-solution i:goal-ctx, o:term, o:term.
+pred cs i:goal-ctx, o:term, o:term.
 
 }}.
 
@@ -17,8 +17,8 @@ Elpi Tactic canonical_solution.
 Elpi Accumulate lp:{{
 
 solve (goal Ctx _ {{ @eq lp:T lp:Lhs lp:Rhs }} _P []) _ :-
-  canonical-solution Ctx Lhs Rhs,
-  % std.assert! (P = {{ eq_refl lp:Lhs }}) "canonical-solution wrong solution".
+  cs Ctx Lhs Rhs,
+  % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution".
   true.
 
 }}.