[TC] perf: fold-map fully implemented in precompile goal

Author: FissoreD

apps/tc/elpi/ho_compile.elpi

@@ -342,8 +342,6 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
-
       % 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.
@@ -352,43 +350,52 @@ namespace tc {
         prune Y S.
 
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
-        prune V S, fold-map T L T' L2.
+        prune V S, decompile-problematic-term T L T' L2.
 
       decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        fold-map 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 fold-map Tl L',
+        std.fold-map NPF L decompile-problematic-term Tl L',
         NL = tc.link.llam Z (app[Y | Tl]).
 
-      % TODO: complete this fold
       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 A L A L :- var A, !.
-
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
-        (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      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,
-        fold-map Ty L Ty' L2,
+        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\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      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,
-        fold-map Ty L Ty' L2,
+        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' :-
-        (pi t l t' l'\ fold-map t l t' l' :- decompile-problematic-term t l t' l', !) =>
-          fold-map T L T' L'.
+      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.

apps/tc/elpi/ho_precompile.elpi

@@ -236,28 +236,26 @@ namespace tc {
         close-term-prune-safe-fun Xs Ty Xs'.
 
       pred precompile-aux i:term, i:list term, o:term, o:list term.
-      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux (global _ as C) A C A :- !.
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
       precompile-aux (primitive _ as C) A C A :- !.
 
-      precompile-aux T A (tc.coercion T Scope) A :- 
-        coq.safe-dest-app T HD _, tc.coercion-unify HD, !, names Scope.
+      precompile-aux (app [HD | _] as T) A (tc.coercion T Scope) A :- 
+        tc.coercion-unify HD, !, names Scope.
       precompile-aux (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) A :- 
         coq.env.projection? C N, !, names Scope.
       precompile-aux (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) A :- 
         coq.env.primitive-projection? P _, !, names Scope.
 
-
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
         names Scope,
         std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
-      % Detect maybe-beta term
+      % Detect maybe-llam term
       precompile-aux (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope1) [X|M] :-
         var X _ Scope, split-pf XS Scope PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
@@ -281,7 +279,8 @@ namespace tc {
       precompile-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
         precompile-aux T A T1 A1, precompile-aux Rty A1 Rty1 A2, std.fold-map B A2 precompile-aux B1 A3.
       precompile-aux (primitive _ as C) A C A :- !.
-      precompile-aux X A X [X|A] :- var X, !.
+      precompile-aux (uvar _ _ as X) A X [X|A] :- !.
+      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
     }
 
     pred goal i:term, o:term, o:list term.