synthesize with elpi

.gitattributes

@@ -0,0 +1 @@
+*.elpi linguist-language=prolog

.vscode/settings.json

@@ -0,0 +1,13 @@
+{
+    "files.exclude": {
+        "**/*.d": true,
+        "**/*.vo": true,
+        "**/*.vok": true,
+        "**/*.vos": true,
+        "**/*.glob": true,
+        "**/*.aux": true,
+        "**/Makefile.coq": true,
+        "**/Makefile.coq.conf": true
+    },
+    "coqtop.binPath": "/nix/store/bfygibqxf976p49svngbkzkls6fqwywz-coq-8.14.0/bin/"
+}

Makefile.coq.local

@@ -0,0 +1,5 @@
+src/tag.vo : src/tag.elpi
+src/fields.vo : src/fields.elpi
+src/eqb.vo : src/eqb.elpi src/fields.elpi
+src/eqbcorrect.vo : src/eqbcorrect.elpi src/fields.elpi src/eqb.elpi
+src/eqbP.vo : src/eqbP.elpi src/eqbcorrect.elpi src/fields.elpi src/eqb.elpi

_CoqProject

@@ -17,4 +17,10 @@ src/option_defs.v
 src/list_defs.v
 src/nested_defs.v
 src/nested_list_defs.v
-src/large_defs.v
+src/large_defs.v
+src/large_defs2.v
+src/tag.v
+src/fields.v
+src/eqb.v
+src/eqbcorrect.v
+src/eqbP.v

coqword.nix

@@ -0,0 +1,49 @@
+{ stdenv, lib, fetchFromGitHub, coqPackages, ocaml, dune_2 }:
+
+let inherit (coqPackages) coq; in
+
+let mathcomp =
+ (if coqPackages ? mathcomp_
+  then coqPackages.mathcomp_ "1.12.0"
+  else coqPackages.mathcomp.override { version = "1.12.0"; }
+ ).algebra
+; in
+
+let rev = "e39e96d51aa96f386222fd1b38776f2117f325c5"; in
+
+stdenv.mkDerivation rec {
+  version = "1.0-git-${builtins.substring 0 8 rev}";
+  name = "coq${coq.coq-version}-coqword-${version}";
+
+  src = fetchFromGitHub {
+    owner = "jasmin-lang";
+    repo = "coqword";
+    inherit rev;
+    sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg";
+  };
+
+  buildInputs = [ coq ocaml dune_2 ];
+
+  propagatedBuildInputs = [ mathcomp ];
+
+  buildPhase = ''
+    runHook preBuild
+    dune build -p coq-mathcomp-word
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix=$out
+    mkdir -p $out/lib/coq/${coq.coq-version}/
+    mv $out/lib/coq/user-contrib $out/lib/coq/${coq.coq-version}/
+    runHook postInstall
+  '';
+
+  meta = {
+    description = "Yet Another Coq Library on Machine Words";
+    license = lib.licenses.cecill-b;
+    inherit (src.meta) homepage;
+    inherit (coq.meta) platforms;
+  };
+}

default.nix

@@ -11,7 +11,7 @@ with pkgs;
 
 let inherit (lib) optionals; in
 
-let coqPackages = coqPackages_8_12; in
+let coqPackages = coqPackages_8_14; in
 
 let coqword = callPackage ./coqword.nix { inherit coqPackages; }; in
 
@@ -35,7 +35,7 @@ stdenv.mkDerivation {
   name = "jasmin-0";
   src = null;
   buildInputs = []
-    ++ optionals coqDeps [ coqPackages.coq coqword coqPackages.coq.ocamlPackages.ocaml ]
+    ++ optionals coqDeps [ coqPackages.coq coqPackages.coq-elpi coqword coqPackages.coq.ocamlPackages.ocaml ]
     ++ optionals testDeps ([ ocamlPackages.apron.out ] ++ (with python3Packages; [ python pyyaml ]))
     ++ optionals ocamlDeps ([ mpfr ppl ] ++ (with oP; [
          ocaml findlib ocamlbuild

src/core_defs.v

@@ -14,19 +14,28 @@ Definition eqb_correct_on (eqb : A -> A -> bool) (a1:A) :=
    forall a2, eqb a1 a2 -> a1 = a2.
 
 Definition eqb_refl_on (eqb : A -> A -> bool) (a:A) := 
-  eqb a a.
+  is_true (eqb a a).
+
+Definition eqb_correct (eqb : A -> A -> bool) := 
+  forall (a1:A), eqb_correct_on eqb a1.
+
+Definition eqb_reflexive (eqb : A -> A -> bool) := 
+  forall (a:A), eqb_refl_on eqb a. 
+
+Lemma iffP2 (f : A -> A -> bool) (H1 : eqb_correct f) (H2 : eqb_reflexive f)
+ (x1 x2 : A) : reflect (x1 = x2) (f x1 x2).
+Proof. apply (iffP idP);[ apply H1 | move->; apply H2 ]. Qed.
 
 Definition eqax_on (eqb : A -> A -> bool) (a1:A) := 
    forall a2, reflect (a1 = a2) (eqb a1 a2).
 
-Class obj := 
-  { tag       : A -> positive
-  ; fields_t  : positive -> Type
-  ; fields    : forall a, fields_t (tag a)
-  ; construct : forall t, fields_t t -> option A 
-  ; constructP : forall a, construct (fields a) = Some a }.
+Variable tag       : A -> positive.
+Variable fields_t  : positive -> Type.
+Variable fields    : forall a, fields_t (tag a).
+Variable construct : forall t, fields_t t -> option A.
+Variable constructP : forall a, construct (fields a) = Some a.
 
-Context {o:obj} (eqb_fields : forall t, fields_t t -> fields_t t -> bool).
+Variable eqb_fields : forall t, fields_t t -> fields_t t -> bool.
 
 Definition eqb_body (t1:positive) (f1:fields_t t1) (x2:A) := 
   let t2 := tag x2 in

src/elpi-ltac.elpi

@@ -0,0 +1,111 @@
+/* elpi-ltac: building blocks for tactics                                    */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+typeabbrev tactic (sealed-goal -> (list sealed-goal -> prop)).
+typeabbrev open-tactic (goal -> (list sealed-goal -> prop)).
+
+% The one tactic ------------------------------------------------------------
+pred refine i:term, i:goal, o:list sealed-goal.
+refine T G GS :- refine.elaborate T G GS.
+
+pred refine.elaborate i:term, i:goal, o:list sealed-goal.
+refine.elaborate T (goal _ RawEv _ Ev _) GS :-
+  RawEv = T, coq.ltac.collect-goals Ev GS _.
+
+pred refine.typecheck i:term, i:goal, o:list sealed-goal.
+refine.typecheck T (goal _ _ Ty Ev _) GS :-
+  coq.typecheck T Ty ok,
+  Ev = T, coq.ltac.collect-goals Ev GS _.
+
+pred refine.no_check i:term, i:goal, o:list sealed-goal.
+refine.no_check T (goal _ _ _ Ev _) GS :-
+  Ev = T, coq.ltac.collect-goals Ev GS _.
+
+% calling other tactics, with arguments ---------------------------------------
+
+pred coq.ltac i:string, i:sealed-goal, o:list sealed-goal.
+coq.ltac Tac G GS :- coq.ltac.open (coq.ltac.call-ltac1 Tac) G GS.
+
+namespace coq.ltac {
+
+pred call i:string, i:list argument, i:goal, o:list sealed-goal.
+call Tac Args G GS :-
+  set-goal-arguments Args G (seal G) (seal G1),
+  coq.ltac.call-ltac1 Tac G1 GS.
+
+pred set-goal-arguments i:list argument, i:goal, i:sealed-goal, o:sealed-goal.
+set-goal-arguments A G (nabla SG) (nabla R) :- pi x\ set-goal-arguments A G (SG x) (R x).
+set-goal-arguments A (goal Ctx1 _ _ _ _) (seal (goal Ctx2 REv2 Ty2 Ev2 _)) (seal (goal Ctx2 REv2 Ty2 Ev2 I)) :-
+  std.map A (private.move-goal-argument Ctx1 Ctx2) I.
+
+% Tacticals ----------------------------------------------------------------
+
+pred try i:tactic, i:sealed-goal, o:list sealed-goal.
+try T G GS :- T G GS.
+try _ G [G].
+
+:index(_ 1)
+pred all i:tactic, i:list sealed-goal, o:list sealed-goal.
+all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O.
+all _ [] [].
+
+pred thenl i:list tactic, i:sealed-goal, o:list sealed-goal.
+thenl [] G [G].
+thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
+
+pred repeat i:tactic, i:sealed-goal, o:list sealed-goal.
+repeat T G GS :- T G GS1, all (repeat T) GS1 GS.
+repeat _ G [G].
+
+pred repeat! i:tactic, i:sealed-goal, o:list sealed-goal.
+repeat! T G GS :- T G GS1, !, all (repeat T) GS1 GS.
+repeat! _ G [G].
+
+pred or i:list tactic, i:sealed-goal, o:list sealed-goal.
+or TL G GS :- std.exists TL (t\ t G GS).
+
+:index(_ 1)
+pred open i:open-tactic, i:sealed-goal, o:list sealed-goal.
+open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O.
+open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect
+open T (seal (goal Ctx _ _ _ _ as G)) O :-
+  std.filter Ctx private.not-already-assumed Ctx1,
+  Ctx1 => T G O,
+  if (var O)
+     (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
+     true.
+
+% helper code ---------------------------------------------------------------
+
+namespace private {
+
+:index(_ _ 1)
+pred move-goal-argument i:list prop, i:list prop, i:argument, o:argument.
+move-goal-argument _ _ (int _ as A) A.
+move-goal-argument _ _ (str _ as A) A.
+move-goal-argument C D (trm T) (trm T1) :-
+  std.rev C Cr, std.rev D Dr,
+  std.assert! (move-term Cr Dr T T1) "cannot move goal argument to the right context", !.
+
+:index(2)
+pred move-term i:list prop, i:list prop, i:term, o:term.
+move-term [] _ T T1 :- copy T T1.
+move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY ], !,
+  copy X Y => move-term C1 C2 T T1.
+move-term [def X _ TX BX|C1] [def Y _ TY BY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY, copy BX BX1, same_term BX1 BY ], !,
+  copy X Y => move-term C1 C2 T T1.
+move-term [decl X _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term [def X _ _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term C1 [_|C2] T T1 :- move-term C1 C2 T T1.
+
+pred distribute-nabla i:(term -> list sealed-goal), o:list sealed-goal.
+distribute-nabla (_\ []) [].
+distribute-nabla (x\ [X x| XS x]) [nabla X|R] :- (pi x\ occurs x (X x)), !,
+  distribute-nabla XS R.
+distribute-nabla (x\ [X| XS x]) [X|R] :- distribute-nabla XS R.
+
+pred not-already-assumed i:prop.
+not-already-assumed (decl X _ _Ty) :- not(decl X _ _ ; def X _ _ _).
+not-already-assumed (def X _ _Ty _Bo) :- not(decl X _ _ ; def X _ _ _).
+
+}}

src/eqb.elpi

@@ -0,0 +1,128 @@
+
+pred eqb.main i:inductive, i:string, o:list prop.
+eqb.main I Prefix CL :- std.do! [
+  coq.env.indt I _ _ N Arity _ _,
+  Ind = global (indt I),
+
+  % the non recursive code comparing all fields according to their types
+  eqbf.do-params N Arity Ind R,
+  std.assert-ok! (coq.typecheck R Rty) "eqbf generates illtyped term",
+  Name is Prefix ^ "eqb_fields",
+  coq.env.add-const Name R Rty ff C,
+  EQBF = global (const C),
+
+  % the fix
+  eqb.do-params N Arity Ind EQBF R1,
+  std.assert-ok! (coq.typecheck R1 R1ty) "eqb generates illtyped term",
+  Name1 is Prefix ^ "eqb",
+  coq.env.add-const Name1 R1 R1ty ff C1,
+  EQB = global (const C1),
+
+  % populate dbs
+  eqbf.do-clause N Arity Ind EQBF [] CL1,
+  eqb.do-clause N Arity Ind EQB [] CL2,
+  CL = [CL1,CL2],
+  std.forall CL (x\ coq.elpi.accumulate _ "eqb.db" (clause _ _ x)),
+].
+
+namespace eqb {
+
+pred do-params i:int, i:term, i:term, i:term, o:term.
+do-params N {{ forall x : lp:T, lp:(F x) }} I EF {{ fun (x : lp:T) (eqx : x -> x -> bool) => lp:(R x eqx) }}  :- N > 0, !, M is N - 1,
+  @pi-decl `x` T x\
+  @pi-decl `eqx` {{ lp:x -> lp:x -> bool }} eqx\
+    do-params M (F x) {coq.mk-app I [x]} {coq.mk-app EF [x,eqx]} (R x eqx).
+do-params 0 _ I EF {{ fix rec (x1 x2 : lp:I) {struct x1} : bool := lp:(R rec x1 x2) }} :-
+  @pi-decl `rec` {{ lp:I -> lp:I -> bool }} rec\
+  @pi-decl `x1` I x1\
+  @pi-decl `x2` I x2\
+    do-match x1 I x2 {coq.mk-app EF [rec]} (R rec x1 x2).
+
+pred do-match i:term, i:term, i:term, i:term, o:term.
+do-match X1 I X2 F R :-
+  coq.build-match X1 I
+    (_\_\_\r\ r = {{ bool }})
+    (do-branch X2 F)
+    R.
+
+pred do-branch i:term, i:term, i:term, i:term, i:list term, i:A, o:term.
+do-branch X2 F K KTY Vars _ {{ @eqb_body _ _ _ lp:FLDP lp:F lp:TAG lp:X lp:X2 }} :- std.do! [
+  coq.safe-dest-app KTY (global (indt I)) Params,
+  fields-for I _ FLD _ _,
+  tag-for I T,
+  coq.mk-app (global (const FLD)) Params FLDP,
+  coq.mk-app (global (const T)) Params TA,
+  coq.mk-app TA [{coq.mk-app K Vars}] TAG,
+  to-tuple Vars X,
+].
+
+pred to-tuple i:list term, o:term.
+to-tuple [] {{ tt }}.
+to-tuple [X] X.
+to-tuple [X|XS] {{ ( lp:X, lp:R ) }} :- to-tuple XS R.
+
+% example: eqb-for {{ list lp:A }} {{ @list_eqb lp:A lp:F }} :- eqb-for A F.
+pred do-clause i:int, i:term, i:term, i:term, i:list prop, o:prop.
+do-clause N {{ forall p, lp:(A p) }} I F Todo (pi a ea\ C a ea) :- N > 0, !, M is N - 1,
+  pi a ea\
+    do-clause M (A a) {coq.mk-app I [a]} {coq.mk-app F [a,ea]} [eqb-for a ea|Todo] (C a ea).
+do-clause 0 _ I F Todo (eqb-for I F :- Todo).
+
+}
+
+% -----------------------------------------------------------------------------
+
+namespace eqbf {
+
+pred do-params i:int, i:term, i:term, o:term.
+do-params J {{ forall p : lp:T, lp:(F p) }} I {{ fun (p : lp:T) (eqp : p -> p -> bool) => lp:(R p eqp) }} :- J > 0, !, K is J - 1,
+  @pi-decl `P` T p\
+  @pi-decl `eqP` {{ lp:p -> lp:p -> bool }} eqP\
+    eqb-for p eqP =>
+    do-params K (F p) {coq.mk-app I [p]} (R p eqP).
+do-params 0 _ Ind {{ fun (rec : lp:Ind -> lp:Ind -> bool) (x : positive) => lp:(R rec x) }} :- std.do! [
+  coq.safe-dest-app Ind (global (indt I)) Params,
+  coq.env.indt I _ _ _ _ _ KT,
+  std.map KT (coq.subst-prod Params) L,
+  fields-for I F_t _ _ _,
+  coq.mk-app (global (const F_t)) Params Fields_t,
+  (@pi-decl `rec` {{ lp:Ind -> lp:Ind -> bool }} rec\
+   @pi-decl `x` {{ positive }} x\
+   eqb-for Ind rec =>
+     fields.splay-over-positive x L {{ fun x => lp:Fields_t x -> lp:Fields_t x -> bool }}
+       {{ fun _ _ => true }}
+       do-fields
+       (R rec x)),
+].  
+pred do-fields i:term, o:term.
+do-fields Ty {{ fun a b => lp:(R a b) }} :-
+  @pi-decl `x` _ x\
+  @pi-decl `y` _ y\
+  do-fields.aux Ty x y (R x y).
+
+pred do-fields.aux i:term, i:term, i:term, o:term.
+do-fields.aux {{ forall p : lp:T, lp:(F p) }} P1 P2 {{ lp:X && lp:R }} :- F = (x\prod _ _ _), !, % not the last one
+  eqb-for T EQB,
+  X = {{ lp:EQB (fst lp:P1) (fst lp:P2) }},
+  (pi x\ if (occurs x (F x)) (coq.error "dependent type not supported yet") true),
+  @pi-decl `p` T n\
+    do-fields.aux (F n) {{ snd lp:P1 }} {{ snd lp:P2 }} R.
+do-fields.aux {{ lp:T -> _ }} P1 P2 X :-
+  eqb-for T EQB,
+  coq.mk-app EQB [P1, P2] X.
+do-fields.aux _ _ _ {{ true }}.
+
+% example:
+%   eqb-fields {{ list lp:A }} {{ @list_eqb_fields lp:A lp:EA lp:ELA }} :-
+%      eqb-for A EA, eqb-for {{ list lp:A }} ELA.
+pred do-clause i:int, i:term, i:term, i:term, i:list prop, o:prop.
+do-clause N (prod _ _ A) I F Todo (pi a ea\ C a ea) :- N > 0, !, M is N - 1,
+  pi a ea\
+    do-clause M (A a) {coq.mk-app I [a]} {coq.mk-app F [a,ea]} [eqb-for a ea|Todo] (C a ea).
+do-clause 0 _ I F Todo (pi ela\ eqb-fields I (F1 ela) :- [C ela|Todo]) :-
+  pi ela\
+    (coq.mk-app F [ela] (F1 ela),
+     C ela = eqb-for I ela).
+
+
+}