[TC] remove goal precomp and goal compile (all is done in ycompile_goal.elpi)

Author: FissoreD

apps/tc/elpi/compile_goal.elpi

@@ -1,6 +1,4 @@
 namespace tc {
-  shorten tc.{r-ar, range-arity}.
-
   namespace compile {
     namespace goall {
       :index (_ _ 1)
@@ -76,7 +74,7 @@ namespace tc {
       compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
 
       % Link for eta-redex
-      compile-full-aux (fun Name Ty Bo as G) L G' [tc.link.eta G' (fun Name Ty' Bo') | L'] :- maybe-eta G, !,
+      compile-full-aux (fun Name_ Ty Bo as G) L G' [tc.link.eta G' (fun `_` Ty' Bo') | L'] :- maybe-eta G, !,
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
@@ -111,37 +109,16 @@ namespace tc {
       %       a |- Z x y a w =L (app[Y x y a, c w d])  
       %       The returned variable is Z x y a w
 
-      pred free-names i:term, o:list term.
-      free-names T L :-
-        names N,
-        (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
-        undup {std.rev L'} L.
-
-      :index(_ _ _ _ 3)
-      % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-      %                           LHS      Scope      Ty          Names        PF         NPF        OLDLINKS    NEW_VAR
-      pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-      build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
-        std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
-        prune T Names,
-        var T HD _. 
-      build-eta-llam-links LHS SC _Ty       _    [X] []  OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
-        prune V SC, var (V X) HD _. % TODO...
-      build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
-      % TODO: unfold Ty if needed...
-        std.append SC [X] SC',
-        prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
-
       % Link for beta-redex (Uvar in PF)
       % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
       compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
         % By construction the scope of a uvar is a list of distinct name
         std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        % std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
+        coq.typecheck V Ty ok,
         split-pf S' Scope PF NPF,
         free-names T Names,
-        build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
+        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
         prune G' Names,
         var G' G'' Names.
 

apps/tc/elpi/ho_compile.elpi

@@ -59,18 +59,23 @@ namespace tc {
         % This happens when the instance to be compiled comes from the context
         % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
         %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[H | PF] | NPF]) S) A Z (pr XS' [NL | L3]) :-  !,
-          var H _ Scope, !,
-          std.append Scope S S',
-          prune Z S',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for T
-          Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T PF Y),
-          std.fold-map NPF A decompile-term-aux Tl (pr XS' L2), 
-          std.append P L2 L3,
-          NL = tc.link.llam Z (app [Y|Tl]).
+        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
+          var V _ Scope, !,
+          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
+
+        % HO var when H is a hole appearing in the shelved goals
+        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
+          var V _ Scope, !,
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
@@ -96,21 +101,6 @@ namespace tc {
           std.assert! (name-pair H V Len) "[TC] name-pair not found",
           name R V L.
 
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [T|L]) (pr A B) Z (pr A B') :-
-          var T _ Scope,
-          std.forall L is-name,     % Not needed, since decompile for llam leaves only PF
-          distinct_names L, !,      % Not needed, since decompile for llam leaves only PF
-          std.append Scope L Scope',
-          prune Z Scope',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for `T`
-          Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T L Y),
-          var Z Y Scope',
-          std.append P B B'.
-
         decompile-term-aux (app L) PR (app L') PR' :- !,
           std.fold-map L PR decompile-term-aux L' PR'.
 
@@ -174,10 +164,10 @@ namespace tc {
         o:prop,            % Link         : The new eta-link
         o:term,            % Ty'          : The cleaned version of the binder in Ty
         o:(term -> term).  % Bo           : the body of the type of A
-      make-eta-link-aux A (prod _ Ty Bo) (pr B Name) L Link Ty' Bo :- !,
+      make-eta-link-aux A (prod _ Ty Bo) (pr B Name_) L Link Ty' Bo :- !,
         clean-term Ty Ty',
         name A' A {std.rev L},
-        Link = tc.link.eta A' (fun Name Ty' B'),
+        Link = tc.link.eta A' (fun `_` Ty' B'),
         pi x\ sigma L'\ std.rev [x|L] L', name (B' x) B L'.
       % Going under prod-range
       make-eta-link-aux A (tc.prod-range Prod _) BN L Link Ty' Bo :- !,
@@ -313,129 +303,5 @@ namespace tc {
     instance-gr InstGR Clause :-
       coq.env.typeof InstGR Ty,
       tc.compile.instance Ty (global InstGR) Clause.
-    
-    namespace goal {
-      % [uvar-pair V1 Ty V2] List of uvar for link-eta-dedup
-      %                      V1 has arity n and V2 has arity n+1
-      %                      If V1 has type A -> B, then A = Ty
-      pred uvar-pair i:term, o:term, o:term.
-
-      %                    Type     Var    Cnt    uvar-pair-list
-      pred make-pairs-aux i:term, i:term, o:list prop.
-      make-pairs-aux Ty (fun _ _ IBo) L' :- !,
-        pi x\ make-pairs-aux Ty (IBo x) (L x), close-prop-no-prune L L'.
-      make-pairs-aux (prod _ Ty Bo) V [pi x\ uvar-pair x Ty X' :- x == V, ! | L] :- !,
-        pi x\ make-pairs-aux (Bo x) X' L.
-      make-pairs-aux _ _ [].
-
-      pred make-pairs i:list term, o:list prop.
-      make-pairs [] [] :- !.
-      make-pairs [X|Xs] L :- !,
-        coq.typecheck X Ty ok,
-        make-pairs-aux Ty X L',
-        make-pairs Xs L'',
-        std.append L' L'' L.
-
-      pred get-uva-pair-arity i:term, i:list term, o:term.
-      get-uva-pair-arity X [] X :- !.
-      get-uva-pair-arity X [_|L] Z :- uvar-pair X _ Y, !, 
-        get-uva-pair-arity Y L Z.
-
-      pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      % there is no need to decompile T since no precompilation is done inside coercions
-      decompile-problematic-term (tc.coercion T S) L1 Y [tc.link.cs Y T|L1] :- !,
-        prune Y S.
-      % there is no need to decompile T since no precompilation is done inside CS
-      decompile-problematic-term (tc.canonical-projection T S _) L1 Y [tc.link.cs Y T|L1] :- !,
-        prune Y S.
-
-      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
-        prune V S, decompile-problematic-term T L T' L2.
-
-      decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        decompile-problematic-term T A T' A'.
-
-      decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
-        prune Z Sc,
-        get-uva-pair-arity H S Y,
-        std.fold-map NPF L decompile-problematic-term Tl L',
-        NL = tc.link.llam Z (app[Y | Tl]).
-
-      decompile-problematic-term (app[X|S]) L Z L :-
-        var X _ Scope, 
-        std.append Scope S Scope',
-        distinct_names Scope', !,
-        get-uva-pair-arity X S Y,
-        prune Z Scope', var Z Y Scope'.
-      
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (global _ as C) A C A :- !.
-      decompile-problematic-term (pglobal _ _ as C) A C A :- !.
-      decompile-problematic-term (sort _ as C) A C A :- !.
-      decompile-problematic-term (let N T B F) A (let N T1 B1 F1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term B A1 B1 A2, pi x\ decompile-problematic-term (F x) A2 (F1 x) A3.
-      decompile-problematic-term (app L) A (app L1) A1 :- !, std.fold-map L A decompile-problematic-term L1 A1.
-      decompile-problematic-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-        decompile-problematic-term Ty A Ty1 A1, pi x\ decompile-problematic-term (F x) A1 (F1 x) A2.
-      decompile-problematic-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term Rty A1 Rty1 A2, std.fold-map B A2 decompile-problematic-term B1 A3.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
-      decompile-problematic-term (uvar _ _ as V) A V A :- !.
-      decompile-problematic-term X A Y A :- name X, !, X = Y, !.
-
-      pred compile i:term, i:list prop, o:term, o:list prop.
-      compile T L T' L' :- decompile-problematic-term T L T' L'.
-
-      %                                  Uva      Binders      LinkEta 
-      pred build-eta-links-of-vars-aux i:term, i:list term, o:list prop.
-      build-eta-links-of-vars-aux Old L [Hd | Xs] :- 
-        uvar-pair Old Ty Next, !,
-        prune OldScope L,
-        prune Name L,
-        var OldScope Old L,
-        Hd = tc.link.eta OldScope (fun Name Ty (x\ NextScope x)),
-        pi x\ sigma L'\
-          std.append L [x] L',
-          prune (NextScope x) L',
-          var (NextScope x) Next L',
-          build-eta-links-of-vars-aux Next L' (Ys x), !,
-        sigma Closed\ (close-term-no-prune-ty Ys Ty Closed),
-        Xs = Closed.
-      build-eta-links-of-vars-aux _ _ [].
-
-      pred build-eta-links-of-vars i:list term, o:list prop.
-      build-eta-links-of-vars [] [].
-      build-eta-links-of-vars [V|Vars] L :-
-        var V Hd S,
-        build-eta-links-of-vars-aux Hd S L',
-        build-eta-links-of-vars Vars L'',
-        std.append L' L'' L.
-      build-eta-links-of-vars [fun _ Ty Bo|Vars] L :-
-        (pi x\ build-eta-links-of-vars [Bo x] (L' x), close-term-no-prune-ty L' Ty L''),
-        build-eta-links-of-vars Vars L''',
-        std.append L'' L''' L.
-    }
-    
-    %          Goal    Goal'      Links
-    pred goal i:term, o:term, o:list prop.
-    :name "compile-goal"
-    goal Goal Goal' Links :-
-      tc.precomp.goal Goal GoalPrecomp Vars, !,
-      goal.make-pairs Vars Pairs,
-      Pairs => (
-        std.assert!(goal.build-eta-links-of-vars Vars EtaLinks) "[TC] cannot build eta-links",
-        std.assert!(goal.compile GoalPrecomp EtaLinks Goal' Links) "[TC] cannot compile goal"
-      ).
   }
 }

apps/tc/elpi/ho_link.elpi

@@ -9,6 +9,29 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
+    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
+    % Builds the eta/llam links at runtime for a term having the shape 
+    % `app[(uvar X Scope as V) | L]`.
+    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    :index(_ _ _ _ 3)
+    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
+    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
+    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+      std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
+      prune T Names,
+      var T HD _. 
+    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+      prune V SC, var (V X) HD _.
+    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    % TODO: unfold Ty if needed...
+      std.append SC [X] SC',
+      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
+      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
+
+
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -73,7 +96,7 @@ namespace tc {
 
       pred unify-eta i:term, i:term.
       % unify-eta A B :- coq.say "Unify-eta" "A"A"B"B, fail.
-      unify-eta A B :- var A, !, A = B, !.
+      unify-eta (uvar _ _ as A) B :- !, A = B, !.
       unify-eta (fun _ _ A) (fun _ _ B) :- !, pi x\ unify-eta (A x) (B x).
       unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
       unify-eta A B :- A = B.
@@ -103,7 +126,6 @@ namespace tc {
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
       llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
-        coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
         declare_constraint (llam A (app [H|L])) [_,A|Vars].
       llam (fun _ _ _ as F) (app [H | TL]) :- 
         var H _ Scope, !,