Merge pull request #823 from LPCIC/lettify-master

Lettify master

Author: gares

.github/workflows/nix-action-coq-8.20.yml

@@ -1 +1 @@
-"b598891e5323d9e68fcb1c2483c2e0a046e6de54"
+"0d640bae117cd64fd202e1453613d614b6e29aea"

.github/workflows/nix-action-coq-master.yml

@@ -104,6 +104,11 @@ namespace tc {
         decompile-term-aux (app L) PR (app L') PR' :- !,
           std.fold-map L PR decompile-term-aux L' PR'.
 
+        decompile-term-aux (let N T Ty Bo) PR (let N T' Ty' Bo') PR3 :- !,
+          decompile-term-aux T PR T' PR1,
+          decompile-term-aux Ty PR1 Ty' PR2,
+          (pi x\ is-name x => decompile-term-aux (Bo x) PR2 (Bo' x) PR3).
+
         decompile-term-aux A B _ _ :- coq.error "[TC] cannot decompile-term-aux of" A B.
 
         pred decompile-term i:list term, o:list term, i:term, o:term, o:list prop.
@@ -244,6 +249,16 @@ namespace tc {
             decl p N Ty' =>
             name-pair p p z => E p => add-link-eta-dedup F Arity p Ty [] PremR (C p)
         ].
+      compile-ty L L1 ProofHd IsPositive (let _ Ty T Bo) ProofTlR PremR Clause :- !,
+        if (IsPositive = tt) 
+          (Clause = (pi x\ C x), E = is-uvar) 
+          (clean-term Ty Ty', Clause = (pi x\ decl x N Ty' => C x), E = is-name),
+        pi p\ sigma F NewPrem\
+          (decl p N Ty' :- !) => (E p :- !) => (
+            NewPrem = tc.link.unif-eq T p,
+            compile-premise L L1 p Ty ProofHd IsPositive (Bo p) ProofTlR [NewPrem | PremR] (C p)
+          ).
+
       compile-ty L L2 ProofHd IsPositive Goal ProofTlR PremR Clause :-
         std.do![    
           coq.mk-app ProofHd {std.rev ProofTlR} Proof,

.github/workflows/nix-action-rocq-9.0.yml

@@ -130,6 +130,16 @@ namespace tc {
       }
     }
 
+    namespace unif-eq {
+      pred unif-eq i:term, i:term.
+      unif-eq T1 (uvar as T2) :- !, declare_constraint (unif-eq T1 T2) [_,T2].
+      unif-eq T1 T2 :- !, coq.unify-eq T1 T2 ok.
+    }
+
+    pred unif-eq i:term, i:term.
+    unif-eq T1 T2 :- unif-eq.unif-eq T1 T2.
+
+
     pred eta i:term, i:term.
     eta A B :- eta.eta A B.
 

.nix/coq-nix-toolbox.nix

@@ -94,6 +94,12 @@ namespace tc {
       get-range-arity-aux _ uvar @max-min :- !.
       get-range-arity-aux _ (sort _) @max-min :- !.
       get-range-arity-aux _ (pglobal _ _) @max-min :- !.
+      get-range-arity-aux X (let _ T Ty B) R4 :- !,
+        get-range-arity-aux X Ty R1,
+        get-range-arity-aux X T R2,
+        (pi x\ get-range-arity-aux T (B x) R3),
+        min-max-nat R1 R2 R12,
+        min-max-nat R12 R3 R4.
       get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
 
       pred get-range-arity i:term, i:term, i:term, o:range-arity.
@@ -130,11 +136,17 @@ namespace tc {
 
       % Working with fun
       precompile-aux _ (fun N T F) A (fun N T1 F1) A2 :- !,
-        precompile-aux _ T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
+        precompile-aux is_neg_fix T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
 
       precompile-aux _ (app L) A (app L1) A1 :- !, std.fold-map L A (precompile-aux is_neg_fix) L1 A1.
       precompile-aux _ X A X A :- var X, !.
 
+      precompile-aux _ (let N T Ty Bo) A (let N T' Ty' Bo') A3 :- !,
+        precompile-aux is_neg_fix T A T' A1,
+        precompile-aux is_neg_fix Ty A1 Ty' A2,
+        pi x\ is-name x => precompile-aux is_neg_fix (Bo x) A2 (Bo' x) A3.
+
+
       % TODO: what about the following constructors?
       % precompile-aux IsP (let N T B F) A (let N T1 B1 F1) A3 :- !,
       %   precompile-aux IsP T A T1 A1, precompile-aux IsP B A1 B1 A2, pi x\ is-name x => precompile-aux IsP (F x) A2 (F1 x) A3.

apps/tc/elpi/ho_compile.elpi

@@ -3,6 +3,29 @@
 
 namespace tc {
 
+  namespace lettify {
+    func replace-args term, list term, list term, (func term -> term) -> term.
+    replace-args Hd []     L K R :- std.rev L L1, K (app [Hd|L1]) R.
+    replace-args Hd [X|Xs] L K (let `_` Ty X T') :-
+      coq.typecheck X Ty ok,
+      pi x\ replace-args Hd Xs [x|L] K (T' x).
+
+    func replace-top-level list term, term, list term -> term.
+    replace-top-level []     Hd L (app [Hd | L']) :- std.rev L L'.
+    replace-top-level [app[X|Xs]|As] Hd L R :-
+      replace-args X Xs [] (x\ replace-top-level As Hd [x|L]) R.
+    replace-top-level [(fun _ _ _ as A)|As] Hd L (let `_` Ty A T') :-
+      coq.typecheck A Ty ok,
+      pi x\ replace-top-level As Hd [x|L] (T' x).
+
+    func main term -> term.
+    main (prod N Ty Bo) (prod N Ty Bo') :- !,
+      pi x\ main (Bo x) (Bo' x).
+    main (app [X|Xs]) T :- is-instance-term X, !,
+      replace-top-level Xs X [] T.
+    main T T.
+  }
+
   % return if a gref is an existsing instance
   % TODO: this could be replaced with an API
   % coq.TC.get-class-of-inst i:gref, o:gref
@@ -29,6 +52,8 @@ namespace tc {
   pred get-TC-of-inst-type i:term, o:gref.
   get-TC-of-inst-type (prod _ _ A) ClassGR:- !,
     pi x\ get-TC-of-inst-type (A x) ClassGR.
+  get-TC-of-inst-type (let _ _ _ A) ClassGR:- !,
+    pi x\ get-TC-of-inst-type (A x) ClassGR.
   get-TC-of-inst-type T ClassGR :-
     coq.safe-dest-app T HD _,
     not (var HD), class-gref HD ClassGR.

apps/tc/elpi/ho_link.elpi

@@ -0,0 +1,14 @@
+From elpi Require Import elpi tc.
+
+Class C (T : Type) : Type := {}.
+Axiom t : forall n m : nat, Type.
+
+Instance tC (n : nat) : C (t n n). Qed.
+Set Printing All.
+Goal C (t 0 0). apply _. Qed.
+
+Instance tC1 (n : nat) : let n' := n in C (t n n'). Qed. 
+
+Goal C (t 0 (id 0)). apply _. Qed.
+
+(* Elpi Print TC.Solver "elpi.apps.tc.examples/TC.Solver". *)