From 8f910a13f1b0aa954a00a2b0e6da071ef3a80953 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Date: Thu, 15 Feb 2024 17:44:01 +0100
Subject: [PATCH] Simplify.

---
 apps/derive/elpi/derive_synterp.elpi | 77 ++++++----------------------
 1 file changed, 15 insertions(+), 62 deletions(-)

diff --git a/apps/derive/elpi/derive_synterp.elpi b/apps/derive/elpi/derive_synterp.elpi
index f6dee5795..4185daa7e 100644
--- a/apps/derive/elpi/derive_synterp.elpi
+++ b/apps/derive/elpi/derive_synterp.elpi
@@ -4,15 +4,6 @@
 
 namespace derive {
 
-pred exists-indc i:inductive, i:(constructor -> prop).
-exists-indc I P :-
-  coq.env.indt I _ _ _ _ KL _,
-  std.exists KL P.
-
-pred if-verbose i:prop.
-if-verbose P :- (get-option "verbose" tt ; get-option "recursive" tt), !, P.
-if-verbose _.
-
 pred dep o:string, o:string.
 dep X Y :- dep1 X Y.
 dep X Y :- dep1 X Z, dep Z Y.
@@ -22,36 +13,20 @@ selected Name :- get-option "only" Map, !,
   Map => (get-option Name _; (get-option X _, dep X Name)).
 selected _.
 
-pred validate-only i:string, i:list derive.
-validate-only T LD :- get-option "only" Map, !, std.forall Map (known-option T LD).
-validate-only _ _.
-
-pred known-option i:string, i:list derive, i:prop.
-known-option T L (get-option X _) :-
-  if (std.mem! L (derive X _ _)) true
-     (coq.error "Derivation" X "unknown or not applicable to input" T).
-
-pred chain i:string, i:list derive, o:list prop.
-chain _ [] [].
-chain T [derive Name _ _|FS] CL :- not(selected Name), !,
-  if-verbose (coq.say "Skipping derivation" Name "on" T "since the user did not select it"),
-  chain T FS CL.
-chain T [derive Name _ AlreadyDone|FS] CL :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
-  if-verbose (coq.say "Skipping derivation" Name "on" T "since it has been already run"),
-  chain T FS CL.
-chain T [derive Name F _|FS] CL :- get-option "only" _, !, % request this one
-  if-verbose (coq.say "Derivation" Name "on" T),
-  std.time (F C) Time,
-  if-verbose (coq.say "Derivation" Name "on" T "took" Time),
-  chain T FS CS.
-chain T [derive Name F _|FS] CL :- % all are selected, we can fail
-  if-verbose (coq.say "Derivation" Name "on" T),
-  (pi x\ stop x :- !, fail) => std.time (F C) Time, !,
-  if-verbose (coq.say "Derivation" Name "on" T "took" Time),
-  chain T FS CS.
-chain T [derive F _ _|FS] CL :-
-  if-verbose (coq.say "Derivation" F "on" T "failed, continuing"),
-  chain T FS CL.
+pred chain i:string, i:list derive.
+chain _ [].
+chain T [derive Name _ _|FS] :- not(selected Name), !,
+  chain T FS.
+chain T [derive Name _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+  chain T FS.
+chain T [derive Name F _|FS] :- get-option "only" _, !, % request this one
+  F _,
+  chain T FS.
+chain T [derive Name F _|FS] :- % all are selected, we can fail
+  (pi x\ stop x :- !, fail) => F _, !,
+  chain T FS.
+chain T [derive F _ _|FS] :-
+  chain T FS.
 
 pred toposort i:list derive, o:list derive.
 toposort L SL :-
@@ -80,37 +55,15 @@ topo L Deps SL :-
   topo Other NewDeps SOther,
   std.append LNoDeps SOther SL.
 
-pred export? i:prop, o:prop.
-export? (export M) (coq.env.export-module M).
-
-% pred indt-or-const i:gref.
-% indt-or-const (indt _).
-% indt-or-const (const _).
-
 pred main i:string, i:bool, o:list prop.
 main T P CL :- main1 T P CL.
 
-pred main.aux i:list string, i:list prop, o:list prop.
-main.aux [] X X.
-main.aux [T|TS] Acc CL :-
-  (pi X\get-option "only" X :- !, fail) => Acc => main T tt CL1,
-  main.aux TS {std.append CL1 Acc} CL.
-
 pred main1 i:string, i:bool, o:list prop.
 main1 T P CL :-
   if (P = tt) (Prefix is T ^ "_") (Prefix = ""),
   std.findall (derivation T Prefix _) L,
   std.map L (x\r\ x = derivation _ _ r) DL,
   toposort DL SortedDL,
-  chain T SortedDL CL.
-
-pred short-alias i:id, i:term.
-short-alias ID T :- @global! => coq.notation.add-abbreviation ID 0 T ff _.
-
-pred indt-decl-name i:indt-decl, o:string.
-indt-decl-name (parameter _ _ _ Decl) Name :-
-  pi x\ indt-decl-name (Decl x) Name.
-indt-decl-name (inductive Name _ _ _) Name.
-indt-decl-name (record Name _ _ _) Name.
+  chain T SortedDL.
 
 }