kill fprop

Author: gares

apps/tc/elpi/ho_link.elpi

@@ -71,7 +71,7 @@ namespace tc {
         (copy Y X :- !) => relocate Xs Ys T T'.
 
       pred collect-store o:list prop.
-      pred collect-store-aux i:list prop, o:list prop.
+      func collect-store-aux list prop -> list prop.
 
       collect-store L :- collect-store-aux [] L.
       collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_].

builtin-doc/coq-builtin-synterp.elpi

@@ -11,29 +11,29 @@ kind upoly-decl-cumul type.
 % -- Misc ---------------------------------------------------------
 
 % [coq.info ...] Prints an info message
-external type coq.info variadic any fprop.
+external type coq.info variadic any (func).
 
 % [coq.notice ...] Prints a notice message
-external type coq.notice variadic any fprop.
+external type coq.notice variadic any (func).
 
 % [coq.say ...] Prints a notice message
-external type coq.say variadic any fprop.
+external type coq.say variadic any (func).
 
 % [coq.debug ...] Prints a debug message
-external type coq.debug variadic any fprop.
+external type coq.debug variadic any (func).
 
 % [coq.warn ...] Prints a generic warning message
-external type coq.warn variadic any fprop.
+external type coq.warn variadic any (func).
 
 % [coq.warning Category Name ...] 
 % Prints a warning message with a Name and Category which can be used
 % to silence this warning or turn it into an error. See coqc -w command
 % line option
-external type coq.warning string -> string -> variadic any fprop.
+external type coq.warning string -> string -> variadic any (func).
 
 % [coq.error ...] Prints and *aborts* the program. It is a fatal error for
 % Elpi and Ltac
-external type coq.error variadic any fprop.
+external type coq.error variadic any (func).
 
 % [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
 % as a string and as 3 numbers

builtin-doc/coq-builtin.elpi

@@ -546,29 +546,29 @@ external symbol off : coercion-status = "1".
 % -- Misc ---------------------------------------------------------
 
 % [coq.info ...] Prints an info message
-external type coq.info variadic any fprop.
+external type coq.info variadic any (func).
 
 % [coq.notice ...] Prints a notice message
-external type coq.notice variadic any fprop.
+external type coq.notice variadic any (func).
 
 % [coq.say ...] Prints a notice message
-external type coq.say variadic any fprop.
+external type coq.say variadic any (func).
 
 % [coq.debug ...] Prints a debug message
-external type coq.debug variadic any fprop.
+external type coq.debug variadic any (func).
 
 % [coq.warn ...] Prints a generic warning message
-external type coq.warn variadic any fprop.
+external type coq.warn variadic any (func).
 
 % [coq.warning Category Name ...] 
 % Prints a warning message with a Name and Category which can be used
 % to silence this warning or turn it into an error. See coqc -w command
 % line option
-external type coq.warning string -> string -> variadic any fprop.
+external type coq.warning string -> string -> variadic any (func).
 
 % [coq.error ...] Prints and *aborts* the program. It is a fatal error for
 % Elpi and Ltac
-external type coq.error variadic any fprop.
+external type coq.error variadic any (func).
 
 % [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
 % as a string and as 3 numbers
@@ -1613,7 +1613,7 @@ kind ltac1-tactic type.
 % [coq.ltac.fail Level ...] Interrupts the Elpi program and calls Ltac's
 % fail Level Msg, where Msg is the printing of the remaining arguments.
 % Level can be left unspecified and defaults to 0
-external type coq.ltac.fail int -> variadic any fprop.
+external type coq.ltac.fail int -> variadic any (func).
 
 % [coq.ltac.collect-goals T Goals ShelvedGoals] 
 % Turns the holes in T into Goals.
@@ -1989,7 +1989,7 @@ external func coq.gref.set.cardinal coq.gref.set -> int.
 
 % [coq.gref.set.filter M F M1] Filter M w.r.t. the predicate F
 external func coq.gref.set.filter coq.gref.set, 
-                                 (gref -> prop) -> coq.gref.set.
+                                 (gref -> (func)) -> coq.gref.set.
 
 % [coq.gref.set.map M F M1] Map M w.r.t. the predicate F
 external func coq.gref.set.map coq.gref.set, 
@@ -2002,7 +2002,7 @@ external func coq.gref.set.fold coq.gref.set, A,
 % [coq.gref.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
 % is where F holds
 external func coq.gref.set.partition coq.gref.set, 
-                                    (gref -> prop) -> coq.gref.set, 
+                                    (gref -> (func)) -> coq.gref.set, 
                                     coq.gref.set.
 
 % CAVEAT: the type parameter of coq.gref.map must be a closed term
@@ -2088,7 +2088,7 @@ external func coq.univ.set.cardinal coq.univ.set -> int.
 
 % [coq.univ.set.filter M F M1] Filter M w.r.t. the predicate F
 external func coq.univ.set.filter coq.univ.set, 
-                                 (univ -> prop) -> coq.univ.set.
+                                 (univ -> (func)) -> coq.univ.set.
 
 % [coq.univ.set.map M F M1] Map M w.r.t. the predicate F
 external func coq.univ.set.map coq.univ.set, 
@@ -2101,7 +2101,7 @@ external func coq.univ.set.fold coq.univ.set, A,
 % [coq.univ.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
 % is where F holds
 external func coq.univ.set.partition coq.univ.set, 
-                                    (univ -> prop) -> coq.univ.set, 
+                                    (univ -> (func)) -> coq.univ.set, 
                                     coq.univ.set.
 
 % CAVEAT: the type parameter of coq.univ.map must be a closed term
@@ -2192,7 +2192,7 @@ external func coq.univ.variable.set.cardinal coq.univ.variable.set -> int.
 
 % [coq.univ.variable.set.filter M F M1] Filter M w.r.t. the predicate F
 external func coq.univ.variable.set.filter coq.univ.variable.set, 
-                                          (univ.variable -> prop) -> coq.univ.variable.set.
+                                          (univ.variable -> (func)) -> coq.univ.variable.set.
 
 % [coq.univ.variable.set.map M F M1] Map M w.r.t. the predicate F
 external func coq.univ.variable.set.map coq.univ.variable.set, 
@@ -2205,7 +2205,7 @@ external func coq.univ.variable.set.fold coq.univ.variable.set, A,
 % [coq.univ.variable.set.partition M F M1 M2] Partitions M w.r.t. the
 % predicate F, M1 is where F holds
 external func coq.univ.variable.set.partition coq.univ.variable.set, 
-                                             (univ.variable -> prop) -> coq.univ.variable.set, 
+                                             (univ.variable -> (func)) -> coq.univ.variable.set, 
                                              coq.univ.variable.set.
 
 % CAVEAT: the type parameter of coq.univ.variable.map must be a closed

builtin-doc/elpi-builtin.elpi

@@ -37,23 +37,23 @@ external symbol (;) prop -> prop -> prop.
 
 (_ ; B) :- B.
 
-external symbol (:-)  : fprop -> fprop -> fprop = "core".
+external symbol (:-)  : (func) -> (func) -> (func) = "core".
 
-external symbol (:-)  : fprop -> list prop -> fprop = "core".
+external symbol (:-)  : (func) -> list prop -> (func) = "core".
 
-external symbol (,)   : variadic fprop fprop.
+external symbol (,)   : variadic (func) (func).
 
 external symbol uvar  : A = "core".
 
 external symbol (as)  : A -> A -> A = "core".
 
-external symbol (=>)  : prop -> fprop -> fprop = "core".
+external symbol (=>)  : prop -> (func) -> (func) = "core".
 
-external symbol (=>)  : list prop -> fprop -> fprop = "core".
+external symbol (=>)  : list prop -> (func) -> (func) = "core".
 
-external symbol (==>) : prop -> fprop -> fprop.
+external symbol (==>) : prop -> (func) -> (func).
 
-external symbol (==>) : list prop -> fprop -> fprop.
+external symbol (==>) : list prop -> (func) -> (func).
 
 %  -- Control --
 
@@ -73,7 +73,7 @@ external func declare_constraint (func) -> any .. .
 external func print_constraints.
 
 % [halt ...] halts the program and print the terms
-external type halt variadic any fprop.
+external type halt variadic any (func).
 
 func stop.
 
@@ -294,10 +294,10 @@ external symbol error : string -> diagnostic = "1".  % Failure
 % == Elpi builtins =====================================
 
 % [dprint ...] prints raw terms (debugging)
-external type dprint variadic any fprop.
+external type dprint variadic any (func).
 
 % [print ...] prints terms
-external type print variadic any fprop.
+external type print variadic any (func).
 
 % Deprecated, use trace.counter
 func counter string -> int.
@@ -341,7 +341,7 @@ rex_split Rx S L :- rex.split Rx S L.
 
 % [var V ...] checks if the term V is a variable. When used with tree
 % arguments it relates an applied variable with its head and argument list.
-external type var any -> variadic any fprop.
+external func var -> any, any.. .
 
 
 % [prune V L] V is pruned to L (V is unified with a variable that only sees
@@ -374,11 +374,11 @@ external func cmp_term any, any -> cmp.
 
 % [name T ...] checks if T is a eigenvariable. When used with tree arguments
 % it relates an applied name with its head and argument list.
-external type name any -> variadic any fprop.
+external func name -> any, any.. .
 
 % [constant T ...] checks if T is a (global) constant.  When used with tree
 % arguments it relates an applied constant with its head and argument list.
-external type constant any -> variadic any fprop.
+external func constant -> any, any.. .
 
 external func names % generates the list of eigenvariable
   -> list any. % list of eigenvariables in order of age (young first)
@@ -428,12 +428,12 @@ external func open_safe safe -> list A.
 
 % [if C T E] picks the first success of C then runs T (never E).
 % if C has no success it runs E.
-func if prop, fprop, fprop.
+func if prop, (func), (func).
 if B T _ :- B, !, T.
 if _ _ E :- E.
 
 % [if2 C1 B1 C2 B2 E] like if but with 2 then branches (and one else branch).
-func if2 prop, fprop, prop, fprop, fprop.
+func if2 prop, (func), prop, (func), (func).
 if2 G1 P1 _  _  _ :- G1, !, P1.
 if2 _  _  G2 P2 _ :- G2, !, P2.
 if2 _  _  _  _  E :- !, E. 
@@ -734,7 +734,7 @@ intersperse Sep [X|XS] [X,Sep|YS] :- intersperse Sep XS YS.
 func flip (func A, B), B, A.
 flip P X Y :- P Y X.
 
-func time fprop -> float.
+func time (func) -> float.
 time P T :- gettimeofday Before, P, gettimeofday After, T is After - Before.
 
 func do! list prop.
@@ -929,7 +929,7 @@ external func std.string.set.cardinal std.string.set -> int.
 
 % [std.string.set.filter M F M1] Filter M w.r.t. the predicate F
 external func std.string.set.filter std.string.set, 
-                                   (string -> prop) -> std.string.set.
+                                   (string -> (func)) -> std.string.set.
 
 % [std.string.set.map M F M1] Map M w.r.t. the predicate F
 external func std.string.set.map std.string.set, 
@@ -942,7 +942,7 @@ external func std.string.set.fold std.string.set, A,
 % [std.string.set.partition M F M1 M2] Partitions M w.r.t. the predicate F,
 % M1 is where F holds
 external func std.string.set.partition std.string.set, 
-                                      (string -> prop) -> std.string.set, 
+                                      (string -> (func)) -> std.string.set, 
                                       std.string.set.
 
 kind std.int.set type.
@@ -991,7 +991,7 @@ external func std.int.set.cardinal std.int.set -> int.
 
 % [std.int.set.filter M F M1] Filter M w.r.t. the predicate F
 external func std.int.set.filter std.int.set, 
-                                (int -> prop) -> std.int.set.
+                                (int -> (func)) -> std.int.set.
 
 % [std.int.set.map M F M1] Map M w.r.t. the predicate F
 external func std.int.set.map std.int.set, 
@@ -1004,7 +1004,7 @@ external func std.int.set.fold std.int.set, A,
 % [std.int.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
 % is where F holds
 external func std.int.set.partition std.int.set, 
-                                   (int -> prop) -> std.int.set, 
+                                   (int -> (func)) -> std.int.set, 
                                    std.int.set.
 
 kind std.loc.set type.
@@ -1053,7 +1053,7 @@ external func std.loc.set.cardinal std.loc.set -> int.
 
 % [std.loc.set.filter M F M1] Filter M w.r.t. the predicate F
 external func std.loc.set.filter std.loc.set, 
-                                (loc -> prop) -> std.loc.set.
+                                (loc -> (func)) -> std.loc.set.
 
 % [std.loc.set.map M F M1] Map M w.r.t. the predicate F
 external func std.loc.set.map std.loc.set, 
@@ -1066,7 +1066,7 @@ external func std.loc.set.fold std.loc.set, A,
 % [std.loc.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
 % is where F holds
 external func std.loc.set.partition std.loc.set, 
-                                   (loc -> prop) -> std.loc.set, 
+                                   (loc -> (func)) -> std.loc.set, 
                                    std.loc.set.
 
 #line 1 "builtin_map.elpi"

elpi/coq-lib.elpi

@@ -630,7 +630,7 @@ coq.bind-ind-parameters.aux I T Vs Ts K O :- I > 0, whd1 T T', !,
 
 % coq.with-TC Class Instance->Clause Code: runs Code under a context augmented with
 % all instances for Class transformed by Instance->Clause.
-func coq.with-TC term, (func tc-instance -> prop), fprop ->.
+func coq.with-TC term, (func tc-instance -> prop), (func) ->.
 coq.with-TC Class Instance->Clause Code :-
   coq.TC.db-for {coq.term->gref Class} Instances,
   map Instances Instance->Clause Hyps, !,

examples/tutorial_elpi_lang.v

@@ -1067,10 +1067,10 @@ kind nat type.
 type z nat.
 type s nat -> nat.
 
-pred sum i:nat, i:nat, o:nat.
+func sum nat, nat -> nat.
 
-sum (s X) Y (s Z) :- sum X Y Z.
-sum z X X.
+sum (s X) Y (s Z) :- !, sum X Y Z.
+sum z X X :- !.
 sum X Y Z :-
   % the head of the rule always unifies with the query, so
   % we double check X is a variable (we could also be
@@ -1137,12 +1137,12 @@ and we would like to be able to fail early.
 
 Elpi Accumulate lp:{{
 
-pred even i:nat.
-pred odd  i:nat.
+func even nat.
+func odd  nat.
 
-even z.
-even (s X) :- odd X.
-odd (s X) :- even X.
+even z :- !.
+even (s X) :- !, odd X.
+odd (s X) :- !, even X.
 
 odd X :- var X, declare_constraint (odd X) [X].
 even X :- var X, declare_constraint (even X) [X].