correct rule ho-test in makefile

LPCIC · May 15, 2024 · 5b2a2e3 · 5b2a2e3
1 parent 19bc702
commit 5b2a2e3
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/apps/tc/Makefile b/apps/tc/Makefile
@@ -40,4 +40,4 @@ install:
 	@$(MAKE) -f Makefile.coq $@
 
 ho-test:
-	make tests/test.vo tests/HO_unif.vo tests/pattern_fragment.vo
+	make tests/test.vo tests/test_HO.vo tests/patternFragment.vo
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
@@ -130,16 +130,19 @@ namespace tc {
         pi x\ is-uvar x => main N [x|L] Ty ProofHd (Clause x).
 
       pred make-eta-link-aux i:term, i:term, i:pair term name, i:list term, o:prop, o:term, o:(term -> term), o:term.
-      make-eta-link-aux A (tc.maybe-beta-tm Prod _) BN L Link1 Ty' Bo B :- !,
-        make-eta-link-aux A Prod BN L Link1 Ty' Bo B.
       make-eta-link-aux A (prod _ Ty Bo) (pr B Name) L Link1 Ty' Bo B :- !,
         clean-term Ty Ty',
         name A' A {std.rev L},
         Link1 = tc.link.eta A' (fun Name Ty' B'),
         pi x\ sigma L'\ std.rev [x|L] L', name (B' x) B L'.
-      make-eta-link-aux A T BN L Link1 Ty' Bo B :- !,
+      % Going under maybe-beta-tm
+      make-eta-link-aux A (tc.maybe-beta-tm Prod _) BN L Link1 Ty' Bo B :- !,
+        make-eta-link-aux A Prod BN L Link1 Ty' Bo B.
+      % Unfold definition if 
+      make-eta-link-aux A T BN L Link1 Ty' Bo B :-
         coq.safe-dest-app T Hd Ag,
         @redflags! coq.redflags.delta => coq.reduction.lazy.whd Hd Hd',
+        not (Hd = Hd'), !,
         coq.mk-app Hd' Ag TT',
         make-eta-link-aux A TT' BN L Link1 Ty' Bo B.
       make-eta-link-aux _ T _ _ _ _ _ _ :- coq.error "[TC] make-eta-link-aux of" T.
@@ -299,6 +302,7 @@ namespace tc {
         std.fold-map NPF L fold-map 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',