From 8cab3c1ec3c676318af652b7d8ad9deeb377cd99 Mon Sep 17 00:00:00 2001 From: Enrico Date: Thu, 18 Oct 2018 14:43:04 +0200 Subject: [PATCH 1/5] Update README.md --- README.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index a1a1b397e..0123eaa36 100644 --- a/README.md +++ b/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 From 667a7c2a4824cc2a3c099a84c9b1244ca5f2cbb4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Oct 2018 14:54:55 +0200 Subject: [PATCH 2/5] cleanup --- derive/derive.elpi | 9 --------- 1 file changed, 9 deletions(-) diff --git a/derive/derive.elpi b/derive/derive.elpi index 7c671fcd4..c9bebdee7 100644 --- a/derive/derive.elpi +++ b/derive/derive.elpi @@ -10,10 +10,6 @@ chain []. chain [F|FS] :- (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 +22,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 +34,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_")}, From 6d65cf90755ae444c1395eff1180b787ee9723f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Oct 2018 08:07:25 +0200 Subject: [PATCH 3/5] Elpi Trace "easy" "opts" / "low" "level" "opts" In this was one can debug elpi itself. Obviously the / and the options after that are optional. --- src/coq_elpi_vernacular.ml | 4 ++-- src/coq_elpi_vernacular.mli | 2 +- src/coq_elpi_vernacular_syntax.ml4 | 12 +++++++++--- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 139ced271..469a77f7f 100644 --- a/src/coq_elpi_vernacular.ml +++ b/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 = diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 8b55c55c3..b316061d3 100644 --- a/src/coq_elpi_vernacular.mli +++ b/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 diff --git a/src/coq_elpi_vernacular_syntax.ml4 b/src/coq_elpi_vernacular_syntax.ml4 index dc29c5945..eb531b3c1 100644 --- a/src/coq_elpi_vernacular_syntax.ml4 +++ b/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 ] From af6608688a315c165e996350a4c603ecfca7f0ff Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Oct 2018 08:09:44 +0200 Subject: [PATCH 4/5] cleanup map --- derive/map.elpi | 31 ++++++++++++------------------- theories/derive/tests/test_map.v | 3 ++- 2 files changed, 14 insertions(+), 20 deletions(-) diff --git a/derive/map.elpi b/derive/map.elpi index fb6f16dd2..ec001e1aa 100644 --- a/derive/map.elpi +++ b/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 diff --git a/theories/derive/tests/test_map.v b/theories/derive/tests/test_map.v index 5788949ab..26c8336b8 100644 --- a/theories/derive/tests/test_map.v +++ b/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. From e1b50a35252910de1033258cb9d0c589345af7dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Oct 2018 08:10:07 +0200 Subject: [PATCH 5/5] derive: a bit more verbose --- derive/derive.elpi | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/derive/derive.elpi b/derive/derive.elpi index c9bebdee7..c11513b47 100644 --- a/derive/derive.elpi +++ b/derive/derive.elpi @@ -7,7 +7,10 @@ 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. param1p T N C :-