Elpi File immediately scopes the program

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

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,22 +382,24 @@ 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
   let hash = Digest.(to_hex @@ string x) in
   (* 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))

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

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) =

tests/boom.elpi

@@ -0,0 +1 @@
+p :- X = {{ hd }}.

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 }}.  }}.