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..2fa848bb2 --- /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/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index 480038bca..aa38ad72f 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -631,67 +631,67 @@ let coq_synterp_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 file_resolver ?cwd:_ ~unit:file () = + (* Handle absolute paths, as bound by "Extra Dependency". *) + if not (Filename.is_relative file) then file else + (* Split filename into a logical path, and a remaining relative path. *) + let (logpath, path) = + (* 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 () -;; + match String.split_on_char '/' path with + | loadpath :: ((_ :: _) as path) -> + let path = String.concat "/" path in + let has_ext = Filename.check_suffix path ".elpi" in + let path = if has_ext then path else path ^ ".elpi" in + (loadpath, path) + | _ -> + let msg = + "File reference " ^ file ^ " is ill-formed, and cannot be resolved." + in + CErrors.user_err (Pp.str msg) + in + 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 + (* 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) path in + if 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) + (***********************************************************************) module Synterp : Programs = struct @@ -747,4 +747,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/theories/elpi.v.in b/theories/elpi.v.in index 4379d648d..b25e1b4f2 100644 --- a/theories/elpi.v.in +++ b/theories/elpi.v.in @@ -8,7 +8,7 @@ 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 Printer "elpi2html.elpi" "elpi2html.elpi". (* this one is from elpi *) +Elpi Printer "coq://elpi_elpi/elpi2html.elpi" "coq://elpi_elpi/elpi2html.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".