From 57aba6531b069288b5e012f5451d93de956aef24 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Nov 2024 14:49:40 +0100 Subject: [PATCH] Elpi File immediately scopes the program --- builtin-doc/elpi-builtin.elpi | 4 +++ src/coq_elpi_programs.ml | 68 +++++++++++++++++++---------------- src/coq_elpi_programs.mli | 14 ++++---- src/coq_elpi_vernacular.ml | 16 ++++----- tests/boom.elpi | 1 + tests/test_quotation.v | 8 +++++ 6 files changed, 65 insertions(+), 46 deletions(-) create mode 100644 tests/boom.elpi diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi index 9ce5701d3..69c5bdee3 100644 --- a/builtin-doc/elpi-builtin.elpi +++ b/builtin-doc/elpi-builtin.elpi @@ -49,6 +49,10 @@ type (=>) prop -> prop -> prop. type (=>) list prop -> prop -> prop. +type (==>) prop -> prop -> prop. + +type (==>) list prop -> prop -> prop. + % -- Control -- external pred !. % The cut operator diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index 0135950a2..f52141727 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -54,7 +54,7 @@ module Chunk = struct type t = | Base of { hash : int; - base : cunit; + base : cunit list; } | Snoc of { source_rev : cunit list; @@ -193,8 +193,8 @@ module type Programs = sig val cc_flags : unit -> API.Compile.flags val unit_from_file : elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string -> cunit val unit_from_string : elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> API.Ast.Loc.t -> string -> cunit - val ast_from_string : elpi:API.Setup.elpi -> loc:Loc.t -> API.Ast.Loc.t -> string -> Digest.t * API.Ast.program - val unit_from_ast : elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string option -> API.Ast.program -> cunit + val ast_from_string : elpi:API.Setup.elpi -> loc:Loc.t -> API.Ast.Loc.t -> string -> Digest.t * API.Compile.scoped_program + val unit_from_ast : elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string option -> API.Compile.scoped_program -> cunit val extend_w_units : base:API.Compile.program -> loc:Loc.t -> cunit list -> API.Compile.program val parse_goal : elpi:API.Setup.elpi -> loc:Loc.t -> API.Ast.Loc.t -> string -> API.Ast.query @@ -206,10 +206,10 @@ module type Programs = sig val get_nature : qualified_name -> nature val init_program : program_name -> src list -> unit - val init_db : program_name -> cunit -> unit - val init_file : program_name -> Digest.t * API.Ast.program -> unit - val header_of_db : qualified_name -> cunit - val ast_of_file : qualified_name -> Digest.t * API.Ast.program + val init_db : program_name -> loc:Loc.t -> (API.Ast.Loc.t * string) -> unit + val init_file : program_name -> Digest.t * API.Compile.scoped_program -> unit + val header_of_db : qualified_name -> cunit list + val ast_of_file : qualified_name -> Digest.t * API.Compile.scoped_program val accumulate : qualified_name -> src list -> unit @@ -382,9 +382,10 @@ let unit_from_file ~elpi ~base ~loc x : cunit = Full (kn,u) with Not_found -> handle_elpi_compiler_errors ~loc (fun () -> - let program = EP.program ~elpi ~files:[x] in + let ast = EP.program ~elpi ~files:[x] in + let ast = EC.scope ~elpi ast in let loc = Loc.initial Loc.ToplevelInput in - unit_from_ast ~elpi ~flags (Some hash) ~base ~loc program) + unit_from_ast ~elpi ~flags (Some hash) ~base ~loc ast) let unit_from_string ~elpi ~base ~loc xloc x : cunit = let flags = cc_flags () in @@ -392,12 +393,13 @@ let unit_from_string ~elpi ~base ~loc xloc x : cunit = (* TODO: ERROR SAME HASH *) handle_elpi_compiler_errors ~loc (fun () -> let ast = EP.program_from ~elpi ~loc:xloc (Lexing.from_string x) in + let ast = EC.scope ~elpi ast in unit_from_ast ~elpi ~flags (Some hash) ~base ~loc ast) -let ast_from_string ~elpi ~loc xloc x : string * API.Ast.program = +let ast_from_string ~elpi ~loc xloc x : string * API.Compile.scoped_program = let hash = Digest.(to_hex @@ string x) in handle_elpi_compiler_errors ~loc (fun () -> - hash, EP.program_from ~elpi ~loc:xloc (Lexing.from_string x)) + hash, EP.program_from ~elpi ~loc:xloc (Lexing.from_string x) |> EC.scope ~elpi) let parse_goal ~elpi ~loc tloc text = handle_elpi_compiler_errors ~loc (fun () -> @@ -417,7 +419,7 @@ let program_src : program SLMap.t ref = let db_name_src : db SLMap.t ref = Summary.ref ~name:("elpi-db-src") SLMap.empty -let file_name_src : (Digest.t * API.Ast.program) SLMap.t ref = +let file_name_src : (Digest.t * API.Compile.scoped_program) SLMap.t ref = Summary.ref ~name:("elpi-file-src") SLMap.empty (* Setup called *) @@ -502,11 +504,7 @@ let get ?(fail_if_not_exists=false) p = if Names.KNset.mem kname db.units then db else { sources_rev = Chunk.snoc c db.sources_rev; units = Names.KNset.add kname db.units } with Not_found -> - match c with - | [] -> assert false - | [base] -> - { sources_rev = Chunk.Base { hash = hash_cunit base; base }; units = Names.KNset.singleton kname } - | _ -> assert false + { sources_rev = Chunk.Base { hash = hash_list hash_cunit 0 c; base = List.rev c }; units = Names.KNset.singleton kname } let is_inside_current_library kn = Names.DirPath.equal @@ -539,7 +537,7 @@ let get ?(fail_if_not_exists=false) p = else Some o); } - let in_file : Names.Id.t -> (program_name * (Digest.t * API.Ast.program)) -> Libobject.obj = + let in_file : Names.Id.t -> (program_name * (Digest.t * API.Compile.scoped_program)) -> Libobject.obj = let open Libobject in let cache ((_,kn),((_,name),p)) = file_name_src := SLMap.add name p !file_name_src in @@ -565,13 +563,6 @@ let get ?(fail_if_not_exists=false) p = (in_file (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) (program, code)) - let init_db qualid cmd_base init = - match cmd_base with - | File { fast = Full(_,base) } -> - add_to_db qualid [init] [] Coq_elpi_utils.SuperGlobal; - add_to_db qualid [Signature (EC.signature base)] [] Coq_elpi_utils.SuperGlobal; - | _ -> assert false - let init_file qualid init = add_to_file qualid init @@ -601,6 +592,21 @@ let get ?(fail_if_not_exists=false) p = match !lp_command_ast with | None -> CErrors.user_err Pp.(str "Elpi CommandTemplate was not called") | Some ast -> ast + + let db_init_base ~loc = + let elpi = ensure_initialized () in + match command_init () with + | File { fast = Full(_,base) } -> + let base = Signature (EC.signature base) in + base, extend_w_units ~loc ~base:EC.(empty_base ~elpi) [base] + | _ -> assert false + + let init_db qualid ~loc (sloc,s) = + let base_sig, base = db_init_base ~loc in + let elpi = ensure_initialized () in + let unit = unit_from_string ~elpi ~base ~loc sloc s in + add_to_db qualid [base_sig;unit] [] Coq_elpi_utils.SuperGlobal + (* add_to_db qualid [base_sig] [] Coq_elpi_utils.SuperGlobal *) let lp_tactic_ast = Summary.ref ~name:("elpi-lp-tactic") None let in_lp_tactic_ast : src -> Libobject.obj = @@ -628,13 +634,13 @@ let get ?(fail_if_not_exists=false) p = else init_program qualid init - let init_db (loc,qualid) (init : cunit) = + let init_db (_,qualid) ~loc header = if stage = Summary.Stage.Interp && Global.sections_are_opened () then CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") else if stage = Summary.Stage.Interp && match Global.current_modpath () with Names.ModPath.MPdot (Names.ModPath.MPfile _,_) -> true | _ -> false then CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside modules") else - init_db qualid (command_init()) init + init_db qualid ~loc header ;; let accumulate p (v : src list) = @@ -783,9 +789,9 @@ let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option = lookup_chunk 0 h src with Not_found -> match src with - | Chunk.Base { base = u } -> + | Chunk.Base { base } -> let elpi = ensure_initialized () in - let prog = extend_w_units ~loc ~base:(EC.empty_base ~elpi) [u] in + let prog = extend_w_units ~loc ~base:(EC.empty_base ~elpi) base in cache_chunk 0 h prog src | Chunk.Snoc { prev; source_rev } -> let base = compile_db ~loc prev in @@ -935,7 +941,7 @@ module Synterp : Programs = struct let clauses_to_add = clauses_to_add |> group_clauses |> List.map (fun (dbname,asts,vs,scope) -> let base = get_and_compile_existing_db ~loc dbname in - let units = List.map (unit_from_ast ~elpi ~base None ~loc) asts in + let units = List.map (fun x -> unit_from_ast ~elpi ~base None ~loc (EC.scope ~elpi x)) asts in dbname,units,vs,scope) in clauses_to_add |> List.iter (fun (dbname,units,vs,scope) -> accumulate_to_db dbname units vs ~scope)) @@ -956,7 +962,7 @@ let () = Coq_elpi_builtins.set_accumulate_to_db_interp (fun ~loc clauses_to_add let clauses_to_add = clauses_to_add |> group_clauses |> List.map (fun (dbname,asts,vs,scope) -> let base = get_and_compile_existing_db ~loc dbname in - let units = List.map (unit_from_ast ~elpi ~base None ~loc) asts in + let units = List.map (fun x -> unit_from_ast ~elpi ~base None ~loc (EC.scope ~elpi x)) asts in dbname,units,vs,scope) in clauses_to_add |> List.iter (fun (dbname,units,vs,scope) -> accumulate_to_db dbname units vs ~scope)) diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 76469d322..a37c27832 100644 --- a/src/coq_elpi_programs.mli +++ b/src/coq_elpi_programs.mli @@ -31,7 +31,7 @@ module Chunk : sig type t = | Base of { hash : int; - base : cunit; + base : cunit list; } | Snoc of { source_rev : cunit list; @@ -81,8 +81,8 @@ module type Programs = sig val cc_flags : unit -> Compile.flags val unit_from_file : elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string -> cunit val unit_from_string : elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> Ast.Loc.t -> string -> cunit - val ast_from_string : elpi:Setup.elpi -> loc:Loc.t -> Ast.Loc.t -> string -> Digest.t * Ast.program - val unit_from_ast : elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string option -> Ast.program -> cunit + val ast_from_string : elpi:Setup.elpi -> loc:Loc.t -> Ast.Loc.t -> string -> Digest.t * Compile.scoped_program + val unit_from_ast : elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string option -> Compile.scoped_program -> cunit val extend_w_units : base:Compile.program -> loc:Loc.t -> cunit list -> Compile.program val parse_goal : elpi:Setup.elpi -> loc:Loc.t -> Ast.Loc.t -> string -> Ast.query @@ -94,11 +94,11 @@ module type Programs = sig val get_nature : qualified_name -> nature val init_program : program_name -> src list -> unit - val init_db : program_name -> cunit -> unit - val init_file : program_name -> Digest.t * Ast.program -> unit + val init_db : program_name -> loc:Loc.t -> (Ast.Loc.t * string) -> unit + val init_file : program_name -> Digest.t * Compile.scoped_program -> unit - val header_of_db : qualified_name -> cunit - val ast_of_file : qualified_name -> Digest.t * Ast.program + val header_of_db : qualified_name -> cunit list + val ast_of_file : qualified_name -> Digest.t * Compile.scoped_program val accumulate : qualified_name -> src list -> unit val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 673ab0468..7f2a8e956 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -204,7 +204,7 @@ let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_ List.map (fun (dbname,asts,vs,scope) -> let base = P.get_and_compile_existing_db ~loc dbname in (* maybe this should be a fold otherwise all clauses have to be independent (the second cannot mention the first one) *) - let units = asts |> List.map (fun ast -> P.unit_from_ast ~elpi None ~base ~loc ast) in + let units = asts |> List.map (fun ast -> P.unit_from_ast ~elpi None ~base ~loc (EC.scope ~elpi ast)) in dbname,units,vs,scope) in clauses_to_add |> List.iter (fun (dbname,units,vs,scope) -> P.accumulate_to_db dbname units vs ~scope); @@ -301,7 +301,8 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) let accumulate_db ~loc ?(program=current_program()) name = let _ = P.ensure_initialized () in - if P.db_exists name then P.accumulate program [DatabaseHeader { dast = P.(header_of_db name) };DatabaseBody name] + let header = P.header_of_db name |> List.map (fun dast -> DatabaseHeader { dast }) in + if P.db_exists name then P.accumulate program (header @ [DatabaseBody name]) else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name name ++ str" not found") let accumulate_db ~atts:((scope,only),ph) ~loc ?program name = warn_scope_not_regular ~loc scope; @@ -310,12 +311,13 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) let accumulate_db_header ~loc ?(program=current_program()) ~scope name = let _ = P.ensure_initialized () in if P.db_exists name then - let unit = P.header_of_db name in + let units = P.header_of_db name in if P.db_exists program then - P.accumulate_to_db program [unit] [] ~scope + P.accumulate_to_db program units [] ~scope else let () = warn_scope_not_regular ~loc scope in - P.accumulate program [DatabaseHeader { dast = unit }] + let units = List.map (fun dast -> DatabaseHeader { dast }) units in + P.accumulate program units else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name name ++ str" not found") let accumulate_db_header ~atts:((scope,only),ph) ~loc ?program name = skip ~only ~ph (accumulate_db_header ~loc ?program ~scope) name @@ -399,11 +401,9 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) match atts with | None -> same_phase Interp P.stage | Some phase -> same_phase phase P.stage in - let elpi = P.ensure_initialized () in if do_init then begin P.declare_db n; - let unit = P.unit_from_string ~elpi ~base:(EC.empty_base ~elpi) ~loc sloc s in - P.init_db n unit + P.init_db n ~loc (sloc,s) end let create_file ~atts ~loc n ~init:(sloc,s) = diff --git a/tests/boom.elpi b/tests/boom.elpi new file mode 100644 index 000000000..655730c03 --- /dev/null +++ b/tests/boom.elpi @@ -0,0 +1 @@ +p :- X = {{ hd }}. \ No newline at end of file diff --git a/tests/test_quotation.v b/tests/test_quotation.v index c30cb0d87..0f1de7764 100644 --- a/tests/test_quotation.v +++ b/tests/test_quotation.v @@ -88,3 +88,11 @@ Fail Elpi Query lp:{{ std.do! [ std.assert-ok! (coq.typecheck T _) "does not typecheck", ] }}. + + +Fail Check hd. +Fail Elpi File boom lp:{{ p :- X = {{ hd }}. }}. +From elpi.tests Extra Dependency "boom.elpi" as boom2. +Import List. +Check hd. +Elpi File boom lp:{{ p :- X = {{ hd }}. }}.