From 5ebf4619f3bd884e460253ea8d492ed7290e6e8f Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 6 Sep 2024 10:00:50 +0200 Subject: [PATCH] Fix file resolution. This includes: - Duplicating [elpi2html.elpi] and [elpi-quoted_syntax.elpi] form elpi. - Always resolving file paths by treating the first component as a Coq directory path, and the rest as a relative path from its mapping. - Require a file path argument in the [Elpi Print] command, resolved in the same way. --- apps/derive/tests/test_derive.v | 2 +- apps/derive/tests/test_param1.v | 2 +- apps/tc/examples/tutorial.v | 4 +- apps/tc/tests/WIP/premisesSort/sort2.v | 4 +- elpi/coq-lib.elpi | 2 +- elpi/elpi-command-template-synterp.elpi | 2 +- elpi/elpi-command-template.elpi | 6 +- elpi/elpi-quoted_syntax.elpi | 26 ++ elpi/elpi-tactic-template.elpi | 8 +- elpi/elpi2html.elpi | 404 ++++++++++++++++++++++++ examples/example_record_expansion.v | 2 +- examples/tutorial_elpi_lang.v | 2 +- src/coq_elpi_programs.ml | 136 ++++---- src/coq_elpi_programs.mli | 15 + src/coq_elpi_vernacular.ml | 40 ++- src/coq_elpi_vernacular.mli | 2 +- src/coq_elpi_vernacular_syntax.mlg | 8 +- src/dune | 2 +- tests/test_link_order1.v | 2 +- tests/test_link_order2.v | 2 +- tests/test_link_order3.v | 2 +- tests/test_link_order4.v | 2 +- tests/test_link_order5.v | 2 +- tests/test_link_order6.v | 2 +- tests/test_link_order7.v | 2 +- tests/test_link_order8.v | 2 +- tests/test_link_order9.v | 2 +- tests/test_link_order_import3.v | 2 +- tests/test_tactic.v | 6 +- theories/elpi.v.in | 8 +- 30 files changed, 578 insertions(+), 123 deletions(-) create mode 100644 elpi/elpi-quoted_syntax.elpi create mode 100644 elpi/elpi2html.elpi diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests/test_derive.v index 055a6c4d9..6810a3131 100644 --- a/apps/derive/tests/test_derive.v +++ b/apps/derive/tests/test_derive.v @@ -68,7 +68,7 @@ Redirect "tmp" Check list_eqb_refl. (* ---------------------------------------------------- *) Require Vector. -Elpi Print derive. +Elpi Print derive "elpi.apps.derive.tests/derive". #[only(eqOK), verbose] derive nat. Module Vector. derive Vector.t. diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v index c82af712e..66fae5c8f 100644 --- a/apps/derive/tests/test_param1.v +++ b/apps/derive/tests/test_param1.v @@ -172,7 +172,7 @@ Definition upair : Set := unit * unit. Elpi derive.param1 upair. Definition uplist := list upair. Elpi derive.param1 uplist. -Elpi Print derive.param1. +Elpi Print derive.param1 "elpi.apps.derive.tests/derive.param1". #[warning="-non-recursive"] Fixpoint bar (pl : uplist) (id : unit) : option unit := None unit. Elpi derive.param1 bar. diff --git a/apps/tc/examples/tutorial.v b/apps/tc/examples/tutorial.v index 359deb6b9..fa780cb10 100644 --- a/apps/tc/examples/tutorial.v +++ b/apps/tc/examples/tutorial.v @@ -55,7 +55,7 @@ Section Foo. context *) - Elpi Print TC.Solver. + Elpi Print TC.Solver "elpi.apps.tc.examples/TC.Solver". End Foo. (* @@ -89,7 +89,7 @@ Module Backtrack. Goal A 3. Fail apply _. Abort. - Elpi Print TC.Solver. + Elpi Print TC.Solver "elpi.apps.tc.examples/TC.Solver". End Backtrack. TC.Print_instances. diff --git a/apps/tc/tests/WIP/premisesSort/sort2.v b/apps/tc/tests/WIP/premisesSort/sort2.v index 31c3730ef..2664f1ba3 100644 --- a/apps/tc/tests/WIP/premisesSort/sort2.v +++ b/apps/tc/tests/WIP/premisesSort/sort2.v @@ -26,7 +26,7 @@ Elpi AddAllInstances. Elpi TC Solver Override TC.Solver All. -Elpi Print TC.Solver. +Elpi Print TC.Solver "elpi.apps.tc.tests/TC.Solver". Goal C bool. apply _. -Qed. \ No newline at end of file +Qed. diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index 1dc6edfaa..ef84a76e0 100644 --- a/elpi/coq-lib.elpi +++ b/elpi/coq-lib.elpi @@ -6,7 +6,7 @@ shorten std.{fatal-error, fatal-error-w-data, debug-print, unsafe-cast}. shorten std.{rev, map, append, appendR, map2, forall-ok, take, do-ok!, lift-ok}. shorten std.{ omap, take-last, intersperse, map-ok, string.concat }. -accumulate elpi/coq-lib-common. +accumulate elpi_elpi/coq-lib-common. :before "stop:begin" stop S :- get-option "ltac:fail" N, !, coq.ltac.fail N S. diff --git a/elpi/elpi-command-template-synterp.elpi b/elpi/elpi-command-template-synterp.elpi index 3db567b21..d044174b1 100644 --- a/elpi/elpi-command-template-synterp.elpi +++ b/elpi/elpi-command-template-synterp.elpi @@ -2,4 +2,4 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -accumulate elpi/coq-lib-common. \ No newline at end of file +accumulate elpi_elpi/coq-lib-common. diff --git a/elpi/elpi-command-template.elpi b/elpi/elpi-command-template.elpi index 7b6258e88..f394b6c7b 100644 --- a/elpi/elpi-command-template.elpi +++ b/elpi/elpi-command-template.elpi @@ -2,7 +2,7 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -accumulate elpi/coq-lib. % basic term manipulation routines -accumulate elpi/elpi-reduction. % whd, hd-beta, ... -accumulate elpi/elpi-ltac. % refine, or, thenl, ... +accumulate elpi_elpi/coq-lib. % basic term manipulation routines +accumulate elpi_elpi/elpi-reduction. % whd, hd-beta, ... +accumulate elpi_elpi/elpi-ltac. % refine, or, thenl, ... diff --git a/elpi/elpi-quoted_syntax.elpi b/elpi/elpi-quoted_syntax.elpi new file mode 100644 index 000000000..e0fb35030 --- /dev/null +++ b/elpi/elpi-quoted_syntax.elpi @@ -0,0 +1,26 @@ +/* elpi: embedded lambda prolog interpreter */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ + +% HOAS for elpi programs + +kind term type. + +type app list term -> term. +type lam (term -> term) -> term. +type const string -> term. + +type cdata ctype "cdata" -> term. % int, string, float.. see also $is_cdata + +type arg (term -> term) -> term. % only to bind the args of a clause + +kind clause type. +type clause (ctype "Loc.t") -> list string -> term -> clause. + +% a program is then a list of clause while +% the query is just one item of the same kind. + +% see elpi-checker.elpi for an example + +% vim: set ft=lprolog: + diff --git a/elpi/elpi-tactic-template.elpi b/elpi/elpi-tactic-template.elpi index c274c6ee1..d278a9551 100644 --- a/elpi/elpi-tactic-template.elpi +++ b/elpi/elpi-tactic-template.elpi @@ -2,11 +2,11 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -accumulate elpi/coq-lib. % basic term manipulation routines -accumulate elpi/elpi-reduction. % whd, hd-beta, ... +accumulate elpi_elpi/coq-lib. % basic term manipulation routines +accumulate elpi_elpi/elpi-reduction. % whd, hd-beta, ... % Since the elaborator written in Elpi is not ready, we fallback to the Coq one % accumulate engine/elaborator. % of, unify -accumulate elpi/coq-elaborator. +accumulate elpi_elpi/coq-elaborator. -accumulate elpi/elpi-ltac. % refine, or, thenl, ... +accumulate elpi_elpi/elpi-ltac. % refine, or, thenl, ... diff --git a/elpi/elpi2html.elpi b/elpi/elpi2html.elpi new file mode 100644 index 000000000..3b40275bc --- /dev/null +++ b/elpi/elpi2html.elpi @@ -0,0 +1,404 @@ +/* elpi: embedded lambda prolog interpreter */ +/* license: GNU Lesser General Public License Version 2.1 or later */ +/* ------------------------------------------------------------------------- */ + +accumulate elpi_elpi/elpi-quoted_syntax. + +shorten std.{spy, rev, exists}. + +pred iter i:(A -> prop), o:list A. +iter _ []. +iter P [X|XS] :- P X, iter P XS. + +pred iter-sep i:list string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string. +iter-sep _ _ _ [] _. +iter-sep _ S P [X] A :- !, P [] X A. +iter-sep B S P [X|XS] A :- P B X [], write S, iter-sep [] S P XS A. + +pred iter-sep2 i:list string, i:string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string. +iter-sep2 _ _ _ _ [] _. +iter-sep2 _ S _ P [X] A :- !, P [] X A. +iter-sep2 B S S1 P [X|XS] A :- P B X [S1], write S, iter-sep2 [] S S1 P XS A. + +pred monad i:list (S -> S -> prop), i:S, o:S. +monad [] X X. +monad [P|PS] X R :- P X X1, monad PS X1 R. + +pred len i:list A, o:int. +len uvar 0. +len [] 0. +len [_|XS] N :- len XS M, N is M + 1. + +pred write-to o:ctype "out_stream". +pred write i:string. +write S :- write-to OC, output OC S. + +pred sanitize i:string, o:string. +sanitize X Y :- + monad [ + rex_replace "&" "&", + rex_replace "<" "<", + rex_replace ">" ">", + rex_replace "\"" """, + rex_replace "'" "'" ] + X Y. + +pred mk-name i:string, i:A, o:string. +mk-name S1 I Y :- + Y is "" ^ S1 ^ "". + +pred cur-int o:int. +pred incr-int i:prop. +incr-int P :- cur-int J, I is J + 1, (cur-int I :- !) => P. + +pred var-to-string i:A, i:B, o:string. +var-to-string X I Y :- + cur-int J, S1 is "x" ^ {term_to_string J} ^ "", + mk-name S1 I Y. +pred uvar-to-string i:A, i:B, o:string. +uvar-to-string X I Y :- + cur-int J, S1 is "X" ^ {term_to_string J} ^ "", + mk-name S1 I Y. +pred name-to-string i:string, i:B, o:string. +name-to-string X0 I Y :- + if (rex_match "^_" X0) (X = "_") (X = X0), + rex_replace "^\\([A-Za-z]+\\)_?\\([0-9]+\\)_?$" "\\1\\2" X S1, + mk-name S1 I Y. + +pred concat i:list string, o:string. +concat [] "". +concat [X|XS] S :- concat XS Res, S is X ^ Res. + +pred par? i:int, i:int, i:list string, i:list string, o:list string, o:list string. +par? CL PL Open Close Open1 Close1 :- + if (CL =< PL) + (Open1 = Open, Close1 = Close) + (Open1 = ["("|Open], Close1 = [")"|Close]). + +kind option type -> type. +type some A -> option A. +type none option A. + +pred grab-list i:term, o:list term, o:option term. +grab-list (const "[]") [] none. +grab-list (app [ const "::", X, XS]) [ X | R ] T :- grab-list XS R T. +grab-list X [] (some X). + + +pred infx i:string, o:int, o:string, o:int, o:int. +% TODO: fix precendences +infx "<" 60 " < " 60 60. +infx "=>" 60 " ⇒ " 59 59. +infx "=" 60 " = " 70 70. +infx "^" 60 " ^ " 60 60. +infx "is" 60 " is " 60 60. +infx ";" 50 " ; " 50 50. +infx "+" 60 " + " 60 60. +infx "*" 60 " * " 60 60. +infx "as" 0 " as " 60 60. + +%@log (pp _ _ _ _). + +pred pp-compound i:prop. +pp-compound P :- write "
", P, write "
". + +% pp Level ParensBefore Term ParensAfter +pred pp i:int, i:list string, i:term, i:list string. +pp L B (app [ const OP, Left, Right ]) A :- infx OP LOP S PL PR, !, + par? L LOP B A B1 A1, + pp-compound (pp PL B1 Left [S]), + pp-compound (pp PR [] Right A1). + +pp L B (app [ const ":-" , Hd , Hyps ]) A :- + par? L 60 B A B1 A1, + if (Hyps = app [ const "," , const "!" | Rest]) + (Hyps2 = app [ const "," | Rest], NeckCut = " neckcut") + (Hyps2 = Hyps, NeckCut = ""), + write "
", + pp 59 B1 Hyps2 [], + write "
", + Concl is "
", + write Concl, + pp 59 [] Hd A1, + write "
". + +pp L B (app [ const C, lam _ ] as T) A :- (C = "pi"; C = "sigma"), !, + par? L 60 B A B1 A1, + pp-quantifier-block B1 C T [] A1. + +pred pp-quantifier-block i:list string, i:string, i:term, i:list string, i:list string. +pp-quantifier-block B C (app [ const C, lam F ]) Args A :- !, incr-int ( + new_int I, + pi x\ if (C = "pi") (var-to-string x I X) (uvar-to-string x I X), + is-name x X => pp-quantifier-block B C (F x) [X|Args] A). +pp-quantifier-block B C T Args A :- + write "
", + write-math-quantifier B C, + iter-sep [] " " (b\ x\ a\ write x) {rev Args} [], + write ".
", + pp 60 [] T A, + write "
". + +pred write-math-quantifier i:list string, i:string. +write-math-quantifier B "pi" :- write {concat B}, write "∀". +write-math-quantifier B "sigma" :- write {concat B}, write "∃". + +pp L B (app [ const "," | Args ]) A :- + par? L 60 B A B1 A1, + write "
", + iter-sep2 B1 "
" "," (pp 59) Args A1, + write "
". + +pp L B (app [ const "::", HD, TL ]) A :- + par? L 99 B A B1 A1, + grab-list TL Args Last, + write "
[
", + iter-sep2 B1 "
" "," (pp 61) [HD|Args] [], + if (Last = some X) (write " | ", pp 0 [] X []) (true), + write "
]
", write {concat A1}. + +pp L B (app Args) A :- + par? L 65 B A B1 A1, + iter-sep B1 " " (pp 66) Args A1. + +pp L B (lam F) A :- incr-int ( + par? L 70 B A B1 A1, + new_int I, + pi x\ + write "
λ", + write {concat B1}, + var-to-string x I X, write X, + write ".
", + is-name x X => pp 10 [] (F x) A1, + write "
"). + +pp _ B (const "!") A :- !, + write {concat B}, + write "!", + write {concat A}. + +pp _ B (const "discard") A :- + write {concat B}, + write "_", + write {concat A}. + +pp _ B (const X) A :- + write {concat B}, + write {sanitize X}, + write {concat A}. + +pp _ B X A :- is-name X Y, !, + write {concat B}, write Y, write {concat A}. + +pp _ B (cdata S) A :- is_cdata S _, !, + term_to_string S Y, + write {concat B}, + write Y, + write {concat A}. + +pp _ B X A :- write "ERROR". + +pred hd-symbol i:term. +hd-symbol (app [ const ":-", H, _ ]) :- hd-symbol H. +hd-symbol (app [ const S | _ ]) :- write S. +hd-symbol (const S) :- write S. + +type is-name term -> string -> prop. +pred write-clause i:clause. +write-clause (clause Loc [] (arg Body)) :- + new_int I, + (pi x\ X is "X" ^ {term_to_string I}), + name-to-string X I A1, + pi x\ is-name x A1 => write-clause (clause Loc [] (Body x)). +write-clause (clause Loc [A|Args] (arg Body)) :- + new_int I, name-to-string A I A1, + pi x\ is-name x A1 => write-clause (clause Loc Args (Body x)). +write-clause (clause Loc [] C) :- !, + write "
", + write "
", + term_to_string Loc LocS, write LocS, + write "
", + cur-int 0 => + if (C = app [const ":-"|_]) + (pp 0 [] C []) + (write "
", + pp 0 [] C [], + write "
"), + write "
\n". + +pred write-preamble i:string. +write-preamble F :- + write " + + + + ", + write F, + write " + + + + + + + +

", + write F, + write "

+ +

Filter predicate:

+". + +pred write-end. +write-end :- + write "". + +pred filter-out i:list A, i:(A -> prop), o:list A. +filter-out [] _ []. +filter-out [X|XS] P R :- + if (P X) (R = [X | RS]) (R = RS), + filter-out XS P RS. + +pred write-html i:list clause, i:string, i:(string -> prop). +write-html P F R :- + filter-out P (c\ + sigma Loc LocS \ c = (clause Loc _ _), + term_to_string Loc LocS, not(R LocS)) PF, + write-preamble F, + iter write-clause PF, + write-end. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred main-quoted i:list clause, i:string, i:list string. + +% entry point from a software having the program in compiled form +main-quoted P OUT FILTERS :- + open_out OUT OC, + R = (x\exists FILTERS (y\ rex_match y x)), + write-to OC => write-html P OUT R, + close_out OC. + +pred main i:list string. +type main prop. + +% entry point from the command line +main [IN,OUT|FILTERS] :- !, + quote_syntax IN "main" P _, + main-quoted P OUT FILTERS. + +main _ :- usage. +main. + +usage :- + halt "usage: elpi elpi2html.elpi -exec main -- in out [filter]". + +% vim: set ft=lprolog: diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index 64e192b3b..72e348ab1 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -195,7 +195,7 @@ Print f. Print expanded_f. (* so that we can see the new "copy" clause *) -Elpi Print record.expand. +Elpi Print record.expand "elpi_examples/record.expand". Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. diff --git a/examples/tutorial_elpi_lang.v b/examples/tutorial_elpi_lang.v index 3fc5c79a2..fbc5ee915 100644 --- a/examples/tutorial_elpi_lang.v +++ b/examples/tutorial_elpi_lang.v @@ -1443,7 +1443,7 @@ predicate. |*) -Elpi Print stlc. +Elpi Print stlc "elpi_examples/stlc". (*| diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index 480038bca..def9e3a57 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -630,68 +630,82 @@ let coq_synterp_builtins = Coq_elpi_builtins.coq_misc_builtins @ Coq_elpi_builtins_synterp.coq_synterp_builtins end - -let file_resolver = - let error_cannot_resolve dp file = - raise (Failure ( - "Cannot resolve " ^ Names.DirPath.to_string dp ^ - " in loadpath:\n" ^ String.concat "\n" (List.map (fun t -> - "- " ^ Names.DirPath.to_string (Loadpath.logical t) ^ - " -> " ^ Loadpath.physical t) (Loadpath.get_load_paths ())))) in - let error_found_twice logpath file abspath other = - raise (Failure ( - "File " ^ file ^ " found twice in loadpath " ^ logpath ^ ":\n" ^ - "- " ^ abspath ^ "\n- " ^ other ^ "\n")) in - let error_file_not_found logpath file paths = - raise (Failure ( - "File " ^ file ^ " not found in loadpath " ^ logpath ^ ", mapped to:\n" ^ - String.concat "\n" (List.map (fun t -> "- " ^ t) paths))) in - let ensure_only_one_path_contains logpath file (paths as allpaths) = - let rec aux found paths = - match paths, found with - | [], None -> error_file_not_found logpath file allpaths - | [], Some abspath -> abspath - | x :: xs, None -> - let abspath = x ^ "/" ^ file in - if Sys.file_exists abspath then aux (Some abspath) xs - else aux None xs - | x :: xs, Some other -> - let abspath = x ^ "/" ^ file in - if Sys.file_exists abspath then error_found_twice logpath file abspath other - else aux found xs +let resolve_file_path ~must_exist ~allow_absolute ~only_elpi file = + (* Handle absolute paths, as bound by "Extra Dependency". *) + if allow_absolute && not (Filename.is_relative file) then + if not must_exist || Sys.file_exists file then file else + let msg = "The referenced absolute path " ^ file ^ " does not exist." in + CErrors.user_err (Pp.str msg) + else + (* Split filename into a logical path, and a remaining relative path. *) + let (logpath, relpath) = + (* Remove "coq://" prefix for backward compatibility. *) + let path = + if String.length file >= 6 && String.sub file 0 6 = "coq://" then + String.sub file 6 (String.length file - 6) + else file in - aux None paths in - let legacy_paths = - let build_dir = Filename.dirname Coq_elpi_config.elpi2html in - let installed_dirs = - let valid_dir d = try Sys.is_directory d with Sys_error _ -> false in - let user_contrib = - if Sys.backend_type = Sys.Other "js_of_ocaml" then "../.." - else - let env = Boot.Env.init () in - Boot.Env.(user_contrib env |> Path.to_string) in - user_contrib :: Envars.coqpath - |> List.map (fun p -> p ^ "/elpi/") - |> ((@) [".";".."]) (* Hem, this sucks *) - |> List.filter valid_dir - in - "." :: build_dir :: installed_dirs in - let legacy_resolver = API.Parse.std_resolver ~paths:legacy_paths () in -fun ?cwd ~unit:file () -> - if Str.(string_match (regexp_string "coq://") file 0) then - let logpath_file = String.(sub file 6 (length file - 6)) in - match string_split_on_char '/' logpath_file with - | [] -> assert false - | logpath :: rest -> - let dp = string_split_on_char '.' logpath |> CList.rev_map Names.Id.of_string_soft |> Names.DirPath.make in - match Loadpath.find_with_logical_path dp with - | _ :: _ as paths -> - let paths = List.map Loadpath.physical paths in - ensure_only_one_path_contains logpath (String.concat "/" rest) paths - | [] -> error_cannot_resolve dp file - else legacy_resolver ?cwd ~unit:file () -;; + (* Remove ".elpi" extension if applicable. *) + let path = + if only_elpi && Filename.check_suffix path ".elpi" then + String.sub path 0 (String.length path - 5) + else path + in + match String.split_on_char '/' path with + | logpath :: ((_ :: _) as relpath) -> + let logpath = + let logpath = String.split_on_char '.' logpath in + let logpath = List.rev_map Names.Id.of_string logpath in + Names.DirPath.make logpath + in + let relpath = + let relpath = String.concat "/" relpath in + if only_elpi then relpath ^ ".elpi" else relpath + in + (logpath, relpath) + | _ -> + let msg = + "File reference " ^ file ^ " is ill-formed, and cannot be resolved." + in + CErrors.user_err (Pp.str msg) + in + (* Lookup the directory path in Coq's state. *) + let loadpath = + match Loadpath.find_with_logical_path logpath with + | p :: [] -> p + | [] -> + let msg = + "No loadpath found with logical name " ^ + Names.DirPath.to_string logpath ^ + ", cannot resolve file reference " ^ file ^ "." + in + CErrors.user_err (Pp.str msg) + | ps -> + let msg = + "Multiple loadpaths found with logical name " ^ + Names.DirPath.to_string logpath ^ + ", while resolving file reference " ^ file ^ ":\n" ^ + String.concat "\n" (List.map (fun lp -> + Printf.sprintf "- %s -> %s" + (Names.DirPath.to_string (Loadpath.logical lp)) + (Loadpath.physical lp) + ) ps) + in + CErrors.user_err (Pp.str msg) + in + (* Assemble the file path. *) + let resolved = Filename.concat (Loadpath.physical loadpath) relpath in + if not must_exist || Sys.file_exists resolved then resolved else + let msg = + "File reference " ^ file ^ " was resolved to " ^ resolved ^ + " but the file does not exist." + in + CErrors.user_err (Pp.str msg) + +let file_resolver ?cwd:_ ~unit:file () = + resolve_file_path ~must_exist:true ~allow_absolute:true ~only_elpi:true file + (***********************************************************************) module Synterp : Programs = struct @@ -747,4 +761,4 @@ let document_builtins () = API.BuiltIn.document_file coq_interp_builtins; API.BuiltIn.document_file coq_synterp_builtins; API.BuiltIn.document_file ~header:"% Generated file, do not edit" elpi_builtins - \ No newline at end of file + diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 2512754ac..4cf72e8ba 100644 --- a/src/coq_elpi_programs.mli +++ b/src/coq_elpi_programs.mli @@ -110,6 +110,21 @@ module type Programs = sig val db_inspect : qualified_name -> int end +(** [resolve_file_path ~must_exist ~allow_absolute ~only_elpi file] interprets + file path [file] according to the Coq directory path configuration (taking + into account the -Q and -R Coq options. If [file] is an absolute path, the + functions returns [file] unchanged if [allow_absolute] is set, and gives a + user error otherwise. Otherwise, [file] is expected to be of the following + form: /. The part is expected to be + a logical Coq directory, as mapped with -Q or -R. The part is a + relative part from the corresponding directory. When [must_exist] is true, + a user error is given when the resolved file does not exist (even if it is + handled as an absolute path). When [only_elpi] is true, the function gives + a path to a file with the ".elpi" extension, even in the case where [file] + does not have an extension. *) +val resolve_file_path : + must_exist:bool -> allow_absolute:bool -> only_elpi:bool -> string -> string + module Synterp : Programs module Interp : Programs diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index f18d76286..454a0d3dc 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -433,25 +433,20 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc, Pp.(strbrk "Now click \"Start watching\" in the Elpi Trace Browser panel and then execute the Command/Tactic/Query you want to trace. Also try \"F1 Elpi\".") let trace_browser ~atts opts = skip ~ph:atts trace_browser opts - let print name args = + let print ~name ~args output = let elpi = P.ensure_initialized () in - get_and_compile name |> Option.iter (fun (program, _) -> - let args, fname, fname_txt = - let default_fname = String.concat "." name ^ ".html" in - let default_fname_txt = String.concat "." name ^ ".txt" in - let default_blacklist = [ - "elaborator.elpi";"reduction.elpi"; - "coq-builtin.elpi";"coq-lib.elpi";"coq-HOAS.elpi" - ] in - match args with - | [] -> default_blacklist, default_fname, default_fname_txt - | [x] -> default_blacklist, x ^ ".html", x ^ ".txt" - | x :: xs -> xs, x ^ ".html", x ^ ".txt" in - let args = List.map API.RawOpaqueData.of_string args in - let query_ast = Interp.parse_goal ~elpi (API.Ast.Loc.initial "(print)") "true." in - let query = EC.query program query_ast in - let oc = open_out fname_txt in - let fmt = Format.formatter_of_out_channel oc in + get_and_compile name |> Option.iter @@ fun (program, _) -> + let fname = + Coq_elpi_programs.resolve_file_path + ~must_exist:false ~allow_absolute:false ~only_elpi:false output + in + let fname_html = fname ^ ".html" in + let fname_txt = fname ^ ".txt" in + let args = List.map API.RawOpaqueData.of_string args in + let query_ast = Interp.parse_goal ~elpi (API.Ast.Loc.initial "(print)") "true." in + let query = EC.query program query_ast in + let oc = open_out fname_txt in + let fmt = Format.formatter_of_out_channel oc in EPP.program fmt query; Format.pp_print_flush fmt (); close_out oc; @@ -466,11 +461,12 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc, assert(depth=0); (* else, we should lift the terms down here *) let q = ET.mkApp main_quotedc (EU.list_to_lp_list quotedP) - [API.RawOpaqueData.of_string fname; EU.list_to_lp_list args] in + [API.RawOpaqueData.of_string fname_html; EU.list_to_lp_list args] in state, (loc,q), [] in ignore @@ run_and_print ~print:false ~static_check:false ["Elpi";"Print"] - (P.assemble_units ~elpi [P.printer ()]) (`Fun q)) - let print ~atts name args = skip ~ph:atts (print name) args + (P.assemble_units ~elpi [P.printer ()]) (`Fun q) + let print ~atts ~name ~args output = + skip ~ph:atts (print ~name ~args) output let create_command ~atts:(raw_args) n = @@ -546,7 +542,7 @@ module type Common = sig val trace : atts:phase option -> int -> int -> string list -> string list -> unit val trace_browser : atts:phase option -> string list -> unit val bound_steps : atts:phase option -> int -> unit - val print : atts:phase option -> qualified_name -> string list -> unit + val print : atts:phase option -> name:qualified_name -> args:string list -> string -> unit val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_command : atts:bool option -> program_name -> unit diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index ce7c05310..eb8f95ad3 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -42,7 +42,7 @@ module type Common = sig val trace : atts:phase option -> int -> int -> string list -> string list -> unit val trace_browser : atts:phase option -> string list -> unit val bound_steps : atts:phase option -> int -> unit - val print : atts:phase option -> qualified_name -> string list -> unit + val print : atts:phase option -> name:qualified_name -> args:string list -> string -> unit val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_command : atts:bool option -> program_name -> unit diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 1e81644ca..9d7d314ba 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -48,7 +48,7 @@ let () = Coq_elpi_glob_quotation.get_elpi_code_appArg := let rec inlogpath q = function | [] -> [] - | x :: xs -> ("coq://" ^ Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs + | x :: xs -> (Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs let warning_legacy_accumulate_gen = CWarnings.create ~default:CWarnings.AsError ~name:"elpi.accumulate-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun has_from -> @@ -290,12 +290,12 @@ VERNAC COMMAND EXTEND ElpiUnnamed CLASSIFIED AS SIDEFF } -> { EV.Interp.bound_steps ~atts steps } -| #[ atts = any_attribute ] [ "Elpi" "Print" qualified_name(p) string_list(s) ] SYNTERP AS atts { +| #[ atts = any_attribute ] [ "Elpi" "Print" qualified_name(p) string(output) string_list(args) ] SYNTERP AS atts { let atts = validate_attributes synterp_attribute atts in - EV.Synterp.print ~atts (snd p) s; + EV.Synterp.print ~atts ~name:(snd p) ~args output; atts } -> { - EV.Interp.print ~atts (snd p) s } + EV.Interp.print ~atts ~name:(snd p) ~args output; } | #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] SYNTERP AS _ { diff --git a/src/dune b/src/dune index ef9a8d9de..53531cca9 100644 --- a/src/dune +++ b/src/dune @@ -8,7 +8,7 @@ (rule (target coq_elpi_builtins_arg_HOAS.ml) - (deps ../elpi/coq-arg-HOAS.elpi) + (deps ../elpi/coq-arg-HOAS.elpi (package elpi)) (action (with-stdout-to %{target} (progn (echo "(* Automatically generated from %{deps}, don't edit *)\n") diff --git a/tests/test_link_order1.v b/tests/test_link_order1.v index 5d0078ae0..13dcdbcbc 100644 --- a/tests/test_link_order1.v +++ b/tests/test_link_order1.v @@ -24,4 +24,4 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. Elpi add 10. -Elpi Print foo "tests/test_link_order1". +Elpi Print foo "elpi.tests/test_link_order1". diff --git a/tests/test_link_order2.v b/tests/test_link_order2.v index a998a21be..03f3bbca5 100644 --- a/tests/test_link_order2.v +++ b/tests/test_link_order2.v @@ -24,5 +24,5 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. Elpi add 10. -Elpi Print foo "tests/test_link_order2". +Elpi Print foo "elpi.tests/test_link_order2". diff --git a/tests/test_link_order3.v b/tests/test_link_order3.v index 653a8ad0d..4ebdee9fc 100644 --- a/tests/test_link_order3.v +++ b/tests/test_link_order3.v @@ -24,4 +24,4 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. Elpi add 10. -Elpi Print foo "tests/test_link_order3". +Elpi Print foo "elpi.tests/test_link_order3". diff --git a/tests/test_link_order4.v b/tests/test_link_order4.v index e1e48f4f0..6e4a041b7 100644 --- a/tests/test_link_order4.v +++ b/tests/test_link_order4.v @@ -24,5 +24,5 @@ Elpi Accumulate lp:{{ }}. Elpi Typecheck. Elpi add 10. -Elpi Print foo "tests/test_link_order4". +Elpi Print foo "elpi.tests/test_link_order4". diff --git a/tests/test_link_order5.v b/tests/test_link_order5.v index c74142567..a4adc2830 100644 --- a/tests/test_link_order5.v +++ b/tests/test_link_order5.v @@ -25,4 +25,4 @@ Elpi Accumulate lp:{{ Elpi Typecheck. Elpi add 5. Elpi add 5. -Elpi Print foo "tests/test_link_order5". +Elpi Print foo "elpi.tests/test_link_order5". diff --git a/tests/test_link_order6.v b/tests/test_link_order6.v index ad25b09b7..ddc10de5d 100644 --- a/tests/test_link_order6.v +++ b/tests/test_link_order6.v @@ -25,5 +25,5 @@ Elpi Accumulate lp:{{ Elpi Typecheck. Elpi add 5. Elpi add 5. -Elpi Print foo "tests/test_link_order6". +Elpi Print foo "elpi.tests/test_link_order6". diff --git a/tests/test_link_order7.v b/tests/test_link_order7.v index c9e057870..9e4ab34b0 100644 --- a/tests/test_link_order7.v +++ b/tests/test_link_order7.v @@ -25,4 +25,4 @@ Elpi Accumulate lp:{{ Elpi Typecheck. Elpi add 5. Elpi add 5. -Elpi Print foo "tests/test_link_order7". +Elpi Print foo "elpi.tests/test_link_order7". diff --git a/tests/test_link_order8.v b/tests/test_link_order8.v index 406e31b4c..29f0377dc 100644 --- a/tests/test_link_order8.v +++ b/tests/test_link_order8.v @@ -25,5 +25,5 @@ Elpi Accumulate lp:{{ Elpi Typecheck. Elpi add 5. Elpi add 5. -Elpi Print foo "tests/test_link_order8". +Elpi Print foo "elpi.tests/test_link_order8". diff --git a/tests/test_link_order9.v b/tests/test_link_order9.v index b7d66b957..f4d730876 100644 --- a/tests/test_link_order9.v +++ b/tests/test_link_order9.v @@ -2,5 +2,5 @@ From elpi Require Import elpi. From elpi.tests Require Import test_link_order1. From elpi.tests Require Import test_link_order1. -Elpi Print foo "tests/test_link_order9". +Elpi Print foo "elpi.tests/test_link_order9". diff --git a/tests/test_link_order_import3.v b/tests/test_link_order_import3.v index 262b93d88..5be2d76c6 100644 --- a/tests/test_link_order_import3.v +++ b/tests/test_link_order_import3.v @@ -1,3 +1,3 @@ From elpi.tests Require Import test_link_order_import2 test_link_order_import1. -Elpi Print bar "tests/test_link_order_import3". \ No newline at end of file +Elpi Print bar "elpi.tests/test_link_order_import3". diff --git a/tests/test_tactic.v b/tests/test_tactic.v index fb88cf908..dc690a2f0 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -17,9 +17,9 @@ Proof. Abort. Elpi Command foo. -Elpi Print foo. +Elpi Print foo "elpi.tests/foo". Elpi Tactic foobar. -Elpi Print foobar. +Elpi Print foobar "elpi.tests/foobar". @@ -134,7 +134,7 @@ solve (goal Ctx _Ev (prod _ T x\ app[G x,B x,_]) _ _) _ :- . }}. Elpi Typecheck. -Elpi Print test_typecheck_in_ctx. +Elpi Print test_typecheck_in_ctx "elpi.tests/test_typecheck_in_ctx". Section T. Variable a : nat. diff --git a/theories/elpi.v.in b/theories/elpi.v.in index 4379d648d..68cc90484 100644 --- a/theories/elpi.v.in +++ b/theories/elpi.v.in @@ -6,11 +6,11 @@ Declare ML Module "coq-elpi.elpi". Elpi Document Builtins. (* Load once and forall these files in this .vo, to ease redistribution *) -Elpi Checker "coq://elpi_elpi/coq-elpi-checker.elpi" "coq://elpi_elpi/coq-elpi-checker.elpi". +Elpi Checker "elpi_elpi/coq-elpi-checker.elpi" "elpi_elpi/coq-elpi-checker.elpi". -Elpi Printer "elpi2html.elpi" "elpi2html.elpi". (* this one is from elpi *) -Elpi Template Command "coq://elpi_elpi/elpi-command-template-synterp.elpi" "coq://elpi_elpi/elpi-command-template.elpi". -Elpi Template Tactic "coq://elpi_elpi/elpi-tactic-template.elpi". +Elpi Printer "elpi_elpi/elpi2html.elpi" "elpi_elpi/elpi2html.elpi". +Elpi Template Command "elpi_elpi/elpi-command-template-synterp.elpi" "elpi_elpi/elpi-command-template.elpi". +Elpi Template Tactic "elpi_elpi/elpi-tactic-template.elpi". (* Special constant used for HOAS of holes, see coq-bultins.elpi *) Lemma hole : True. Proof. exact I. Qed.