Merge branch 'master' into coq-v8.9

README.md

@@ -7,8 +7,9 @@ This software is beta quality, it works but it has rough edges.
 
 ## What is ELPI
 [ELPI](https://github.com/LPCIC/elpi) provides an easy-to-embed 
-implementation of λProlog, a programming language well suited to
-express transformations of abstract syntax trees with binders.  
+implementation of a dialect of λProlog, a programming language well suited to
+express transformations of abstract syntax trees containing
+binders and unification variables.  
 
 ## What is coq-elpi
 Coq-elpi provides a Coq plugin that embeds ELPI.
@@ -25,8 +26,8 @@ notation. Finally it provides a way to define new vernacular commands and
 new tactics.
 
 ## What is the purpose of all that
-Provide a scripting language to Coq well suited to express manipulation
-of terms.  One can use such language to implement new features, like
+Provide an extension language to Coq well suited to express manipulation
+of terms.  One can use such a language to implement new features, like
 code generation "à la derive", or implement new tactics.
 Finally ELPI extends λProlog with a (still under study) language to declare and
 manipulate higher order constraints. The aim is to provide good language support

derive/derive.elpi

@@ -7,13 +7,12 @@ namespace derive {
 pred chain i:list (list prop -> prop).
 :if "DBG:derive" chain [X|_] :- coq.say {counter "run"} X, fail.
 chain [].
-chain [F|FS] :- (stop :- !, fail) => F C, !, C => chain FS.
+chain [F|FS] :-
+  coq.say "Derivation: " F,
+  (stop :- !, fail) => F C, !,
+  C => chain FS.
 chain [F|FS] :- coq.say "Derivation fails: " F, chain FS.
 
-
-begin_ns N [] :- coq.env.begin-module N _.
-end_ns [] :- coq.env.end-module _.
-
 param1p T N C :-
   reali T P, !,
   derive.param1P.main P N C.
@@ -26,10 +25,6 @@ mapR T N C :-
   reali T R, !,
   derive.map.main R N C.
 
-simplify P N C :-
-  P T,
-  derive.eqOK.main T N C.
-
 main T M :- 
   coq.gr->id {term->gr T} Tname,
   Indname is M ^ Tname ^ "_",
@@ -42,7 +37,6 @@ main T M :-
     mapR T {calc (M ^ "is_" ^ Tname ^ "_map")},
     % invert T "",
     derive.induction.main T {calc (Indname ^ "induction")},
-    % simplify (induction-db T) "induction",
     derive.eq.main T {calc (Indname ^ "eq")},
     derive.bcongr.main T {calc (Indname ^ "bcongr_")},
     derive.eqK.main T {calc (Indname ^ "eq_axiom_")},

derive/map.elpi

@@ -22,20 +22,22 @@ pred bo-idx
   i:term, % inductive arity (input)
   i:term, % inductive type (input) applied to params & idx handled so far
   i:term, % inductive type (output) applied to params & idx handled so far
+  i:int,  % current index no
   o:int, % Recno
   i:list term, % rev list of (output) parameters
   o:term, % body
   o:term. % type
 
-bo-idx (prod _ S1 T1) Ity1 Ity2 N Ps (lam `x` S1 Bo) (prod `x` S1 Ty) :-
+bo-idx (prod _ S1 T1) Ity1 Ity2 N M Ps (lam `x` S1 Bo) (prod `x` S1 Ty) :-
   pi x\ sigma Ity1x Ity2x\
     mk-app  Ity1 [x]  Ity1x,
     mk-app  Ity2 [x]  Ity2x,
-    decl x `x` S1 => bo-idx (T1 x) Ity1x Ity2x M Ps (Bo x) (Ty x),
-    N is M + 1.
+    N1 is N + 1,
+    decl x `x` S1 => bo-idx (T1 x) Ity1x Ity2x N1 M Ps (Bo x) (Ty x).
 
-bo-idx (sort _) Ity1 Ity2 0 Ps (lam `x` Ity1 Bo) (prod `_` Ity1 _\ Ity2) :-
-  pi x\ decl x `x` Ity1 => build-match x Ity1 (bo-idx-rty Ps Ity2) (bo-k-args Ps) (Bo x).
+bo-idx (sort _) Ity1 Ity2 N N Ps (lam `x` Ity1 Bo) (prod `_` Ity1 _\ Ity2) :-
+  @pi-decl `x` Ity1 x\
+    build-match x Ity1 (bo-idx-rty Ps Ity2) (bo-k-args Ps) (Bo x).
 
 bo-idx-rty Ps ItyArgs _ Vs _ R :-
   rev Vs [_|IdxsRev],
@@ -47,9 +49,9 @@ bo-k-args ParamsRev K _ Args Tys R :-
   rev ParamsRev Params,
   safe-dest-app K (indc GR) _,
   coq.env.typeof-gr GR T, subst-prod Params T KT,
-  (bo-k-args-aux {mk-app (indc GR) Params} Args Tys KT R), !. % the first combination that typechecks
+  (bo-k-args-aux {mk-app (indc GR) Params} Args Tys KT R),
+  !. % the first combination that typechecks
 
-% We search, since we don't know if we can map or not
 bo-k-args-aux R [] [] _ R :- coq.typecheck R _.
 bo-k-args-aux K [A|As] [T|Ts] (prod _ S Ty) R :-
   map-db T S F,
@@ -72,8 +74,9 @@ pred bo-params
   o:term. % map function
 
 bo-params Lno Lno Ity1 Ity2 A1 _ Ps (fix `f` Recno Fty Bo) :- !,
-  (pi f\ mk-fix-clause A1 Ity1 Ity2 f (Clause f)),
-  pi f\ Clause f => decl f `rec` Fty => bo-idx A1 Ity1 Ity2 Recno Ps (Bo f) Fty.
+  @pi-decl `rec` Fty f\
+    map-db Ity1 Ity2 f =>
+      bo-idx A1 Ity1 Ity2 0 Recno Ps (Bo f) Fty.
 
 bo-params N Lno Ity1 Ity2 (prod A Sty1 Rty1) (prod _ _ Rty2) Ps R :- skip N, !,
   N1 is N + 1,
@@ -133,16 +136,6 @@ mk-map-ty (app[X|XS] as A) _ (app[Y|YS] as B) _ (prod `x` A _\ B) (app [G|GS] as
   mk-app G LF PLF.
 mk-map-ty A _ B _ (prod `x` A _\ B) F 0 [map-db A B F].
 
-pred mk-fix-clause % The fix does not map the indexes
-  i:term, % Arity of input/output type
-  i:term, % input type IT
-  i:term, % output type OT
-  i:term, % function
-  o:prop. % clause (pi xs\ map-db (IT xs) (OT xs) (F xs))
-mk-fix-clause (prod _ _ T) T1 T2 F (pi x\ C x) :-
- pi x\ mk-fix-clause (T x) {mk-app T1 [x]} {mk-app T2 [x]} {mk-app F [x]} (C x).
-mk-fix-clause (sort _) T1 T2 F (map-db T1 T2 F).
-
 % Build a clause %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 pred mk-clause

src/coq_elpi_vernacular.ml

@@ -516,9 +516,9 @@ let mk_trace_opts start stop preds =
   ; "-trace-maxbox"; "30"
   ] @ List.(flatten (map (fun x -> ["-trace-only-pred"; x]) preds))
 
-let trace start stop preds =
+let trace start stop preds opts =
   if start = 0 && stop = 0 then trace_options := []
-  else trace_options := mk_trace_opts start stop preds
+  else trace_options := mk_trace_opts start stop preds @ opts
 
 let print (_,name as prog) args = 
   let args, fname =

src/coq_elpi_vernacular.mli

@@ -15,7 +15,7 @@ val load_files : string list -> unit
 val load_string : Ploc.t * string -> unit
 val load_db : qualified_name -> unit
 val debug : string list -> unit
-val trace : int -> int -> string list -> unit
+val trace : int -> int -> string list -> string list -> unit
 val bound_steps : int -> unit
 val declare_db : qualified_name -> Ploc.t * string -> unit
 

src/coq_elpi_vernacular_syntax.ml4

@@ -111,9 +111,15 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
   [ EV.set_current_program (snd p);EV.load_db (snd d) ]
 
 | [ "Elpi" "Debug" string_list(s) ] -> [ EV.debug s ]
-| [ "Elpi" "Trace" string_list(s) ] -> [ EV.trace 1 max_int s ]
-| [ "Elpi" "Trace" int(start) int(stop) string_list(s) ] -> [ EV.trace start stop s ]
-| [ "Elpi" "Trace" "Off" ] -> [ EV.trace 0 0 [] ]
+| [ "Elpi" "Trace" string_list(s) ] ->
+  [ EV.trace 1 max_int s [] ]
+| [ "Elpi" "Trace" string_list(s) "/" string_list(o) ] ->
+  [ EV.trace 1 max_int s o ]
+| [ "Elpi" "Trace" int(start) int(stop) string_list(s) ] ->
+  [ EV.trace start stop s [] ]
+| [ "Elpi" "Trace" int(start) int(stop) string_list(s) "/" string_list(o) ] ->
+  [ EV.trace start stop s o ]
+| [ "Elpi" "Trace" "Off" ] -> [ EV.trace 0 0 [] [] ]
 | [ "Elpi" "Bound" "Steps" int(steps) ] -> [ EV.bound_steps steps ]
 
 | [ "Elpi" "Print" qualified_name(p) string_list(s) ] -> [ EV.print p s ]

theories/derive/tests/test_map.v

@@ -28,9 +28,10 @@ Elpi derive.map Coverage.is_peano.
 Elpi derive.map Coverage.is_option.
 Elpi derive.map Coverage.is_pair.
 Elpi derive.map Coverage.is_seq.
-Fail Elpi derive.map Coverage.is_tree.
+Elpi derive.map Coverage.is_tree.
 Elpi derive.map Coverage.is_nest.
 Fail Elpi derive.map Coverage.is_w.
+
 Elpi derive.map Coverage.is_vect.
 Elpi derive.map Coverage.is_dyn.
 Fail Elpi derive.map Coverage.is_zeta.