fix separation parsing/execution

src/coq_elpi_programs.ml

@@ -237,17 +237,19 @@ type program = {
   sources_rev : qualified_name Code.t;
   units : Names.KNset.t;
   dbs : SLSet.t;
-  nature : nature;
 }
 
+let program_name : nature SLMap.t ref =
+  Summary.ref ~stage:Summary.Stage.Synterp ~name:"elpi-programs-synterp" SLMap.empty
+
 let program_src : program SLMap.t ref =
   Summary.ref ~name:"elpi-programs" SLMap.empty
-let program_exists name = SLMap.mem name !program_src
 
+let program_exists name = SLMap.mem name !program_name
 
-let db_name_src : db SLMap.t ref =
-  Summary.ref ~name:"elpi-db" SLMap.empty
-let db_exists name = SLMap.mem name !db_name_src
+let db_name : SLSet.t ref = Summary.ref ~stage:Summary.Stage.Synterp  ~name:"elpi-db-synterp" SLSet.empty
+let db_name_src : db SLMap.t ref = Summary.ref ~name:"elpi-db" SLMap.empty
+let db_exists name = SLSet.mem name !db_name
 
 (* Setup called *)
 let elpi = Stdlib.ref None
@@ -350,10 +352,17 @@ let document_builtins () =
   API.BuiltIn.document_file ~header:"% Generated file, do not edit" elpi_builtins
 
 (* We load pervasives and coq-lib once and forall at the beginning *)
+let get_nature p =
+  try SLMap.find p !program_name
+  with Not_found ->
+    CErrors.user_err
+      Pp.(str "No Elpi Program named " ++ pr_qualified_name p)
+
 let get ?(fail_if_not_exists=false) p =
   let _elpi = ensure_initialized () in
+  let nature = get_nature p in
   try
-  let { sources_rev; units; dbs; nature } = SLMap.find p !program_src in
+  let { sources_rev; units; dbs } = SLMap.find p !program_src in
   units, dbs, Some nature, Some sources_rev
   with Not_found ->
   if fail_if_not_exists then
@@ -374,18 +383,16 @@ let code n : Chunk.t Code.t =
     Not_found ->
       CErrors.user_err Pp.(str "Unknown Db " ++ str (show_qualified_name name)))
 
-
-let nature_max old_nature nature =
-  match old_nature with
-  | Some x -> x
-  | None ->
-    match nature with
-    | None -> CErrors.anomaly Pp.(str "nature_max")
-    | Some x -> x
-
-let append_to_prog name nature src =
-  let units, dbs, old_nature, prog = get name in
-  let nature = nature_max old_nature nature in
+let in_program_name : qualified_name * nature -> Libobject.obj =
+  let open Libobject in
+  declare_object @@ { (superglobal_object_nodischarge "ELPI_synterp"
+  ~cache:(fun (name,nature) ->
+    program_name := SLMap.add name nature !program_name)
+  ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))))
+  with object_stage = Summary.Stage.Synterp }
+
+let append_to_prog name src =
+  let units, dbs, _, prog = get name in
   let units, dbs, prog =
     match src with
     (* undup *)
@@ -398,23 +405,28 @@ let append_to_prog name nature src =
     | Database n ->  units, SLSet.add n dbs, Some (Code.snoc_db_opt n prog)
     in
   let prog = Option.get prog in
-  { units; dbs; nature; sources_rev = prog }
+  { units; dbs; sources_rev = prog }
 
-let in_program : qualified_name * nature option * src -> Libobject.obj =
+let in_program : qualified_name * src -> Libobject.obj =
   let open Libobject in
   declare_object @@ superglobal_object_nodischarge "ELPI"
-  ~cache:(fun (name,nature,src_ast) ->
+  ~cache:(fun (name,src_ast) ->
     program_src :=
-      SLMap.add name (append_to_prog name nature src_ast) !program_src)
+      SLMap.add name (append_to_prog name src_ast) !program_src)
   ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))
 
-let init_program name nature u =
-  let obj = in_program (name, Some nature, u) in
+
+let declare_program name nature =
+  let obj = in_program_name (name,nature) in
+  Lib.add_leaf obj
+
+let init_program name u =
+  let obj = in_program (name, u) in
   Lib.add_leaf obj
 ;;
 
 let add_to_program name v =
-  let obj = in_program (name, None, v) in
+  let obj = in_program (name, v) in
   Lib.add_leaf obj
 ;;
 
@@ -458,6 +470,18 @@ let in_db : Names.Id.t -> snippet -> Libobject.obj =
       else Some o);
   }
 
+let in_db_name : qualified_name -> Libobject.obj =
+  let open Libobject in
+  declare_object @@ {
+    (superglobal_object_nodischarge "ELPI-DB_synterp"
+       ~cache:(fun name -> db_name := SLSet.add name !db_name)
+       ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))))
+      with
+        object_stage = Summary.Stage.Synterp }
+
+let declare_db program =
+  ignore @@ Lib.add_leaf (in_db_name program)
+
 let accum = ref 0
 let add_to_db program code vars scope =
   ignore @@ Lib.add_leaf
@@ -501,18 +525,26 @@ let tactic_init () =
   | None -> CErrors.user_err Pp.(str "Elpi TacticTemplate was not called")
   | Some ast -> ast
 
-let create_program (loc,qualid) nature (init : src) =
+let declare_program (loc,qualid) nature =
   if program_exists qualid || db_exists qualid then
     CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists")
-  else if Global.sections_are_opened () then
+  else
+    declare_program qualid nature
+
+let init_program (loc,qualid) (init : src) =
+  if Global.sections_are_opened () then
     CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections")
   else
-    init_program qualid nature init
+    init_program qualid init
 
-let create_db (loc,qualid) (init : cunit) =
+let declare_db (loc,qualid) =
   if program_exists qualid || db_exists qualid then
     CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists")
-  else if Global.sections_are_opened () then
+  else
+    declare_db qualid
+
+let init_db (loc,qualid) (init : cunit) =
+  if Global.sections_are_opened () then
     CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections")
   else if 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")
@@ -529,9 +561,6 @@ let current_program () =
   | None -> CErrors.user_err Pp.(str "No current Elpi Program")
   | Some x -> x
 
-let get_nature x =
-  let _,_, nature, _ = get ~fail_if_not_exists:true x in
-  Option.get nature
 
 let lp_checker_ast = Summary.ref ~name:"elpi-lp-checker" None
 let in_lp_checker_ast : cunit list -> Libobject.obj =

src/coq_elpi_programs.mli

@@ -24,8 +24,13 @@ and src_string = {
 type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } 
 
 val get_nature : qualified_name -> nature
-val create_program : program_name -> nature -> src -> unit
-val create_db : program_name -> cunit -> unit
+
+val declare_program : program_name -> nature -> unit
+val init_program : program_name -> src -> unit
+
+val declare_db : program_name -> unit
+val init_db : program_name -> cunit -> unit
+
 val set_current_program : qualified_name -> unit
 val current_program : unit -> qualified_name
 val accumulate : qualified_name -> src list -> unit

src/coq_elpi_vernacular.ml

@@ -21,27 +21,39 @@ let load_printer = load_printer
 let load_checker = load_checker
 let document_builtins = document_builtins
 
-let create_command ?(raw_args=false) n =
+module Synterp = struct
+  let create_command ?(raw_args=false) n =
+    declare_program n (Command { raw_args })
+  let create_tactic n =
+    declare_program n Tactic
+
+  let create_program ?(raw_args=false) n =
+    declare_program n (Program { raw_args })
+
+  let create_db n = declare_db n
+end
+
+let create_command n =
   let _ = ensure_initialized () in
-  create_program n (Command { raw_args }) (command_init());
+  init_program n (command_init());
   set_current_program (snd n)
 
 let create_tactic n =
   let _ = ensure_initialized () in
-  create_program n Tactic (tactic_init ());
+  init_program n (tactic_init ());
   set_current_program (snd n)
 
-let create_program ?(raw_args=false) n ~init:(loc,s) =
+let create_program n ~init:(loc,s) =
   let elpi = ensure_initialized () in
   let unit = unit_from_string ~elpi loc s in
   let init = EmbeddedString { sloc = loc; sdata = s; sast = unit} in
-  create_program n (Program { raw_args }) init;
+  init_program n init;
   set_current_program (snd n)
 
 let create_db n ~init:(loc,s) =
   let elpi = ensure_initialized () in
   let unit = unit_from_string ~elpi loc s in
-  create_db n unit
+  init_db n unit
 
 let default_max_step = max_int
 
@@ -481,9 +493,9 @@ let subst_program = function
 
 let in_exported_program : nature * qualified_name * string -> Libobject.obj =
   let open Libobject in
-  declare_object @@ global_object_nodischarge "ELPI-EXPORTED"
+  declare_object @@ { (global_object_nodischarge "ELPI-EXPORTED"
     ~cache:cache_program
-    ~subst:(Some subst_program)
+    ~subst:(Some subst_program)) with object_stage = Summary.Stage.Synterp }
 
 let export_command p =
   let p_str = String.concat "." p in

src/coq_elpi_vernacular.mli

@@ -5,9 +5,16 @@
 open Coq_elpi_utils
 open Coq_elpi_programs
 
-val create_program : ?raw_args:bool -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+module Synterp : sig
+val create_program : ?raw_args:bool -> program_name -> unit
 val create_command : ?raw_args:bool -> program_name -> unit
 val create_tactic : program_name -> unit
+val create_db : program_name -> unit
+end
+
+val create_program : program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+val create_command : program_name -> unit
+val create_tactic : program_name -> unit
 val create_db : program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
 
 val typecheck_program : ?program:qualified_name -> unit -> unit

src/coq_elpi_vernacular_syntax.mlg

@@ -173,17 +173,30 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      EV.print (snd p) s }
 
-| #[ atts = any_attribute ] [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] -> {
+| #[ atts = any_attribute ] [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] SYNTERP AS _ 
+   { 
      let raw_args = validate_attributes raw_args_attribute atts in
-     EV.create_program ?raw_args p ~init:s }
-| #[ atts = any_attribute ] [ "Elpi" "Command" qualified_name(p) ] -> {
+     EV.Synterp.create_program ?raw_args p
+   } -> {
+     EV.create_program p ~init:s
+   }
+| #[ atts = any_attribute ] [ "Elpi" "Command" qualified_name(p) ] SYNTERP AS _ 
+   { 
      let raw_args = validate_attributes raw_args_attribute atts in
-     EV.create_command ?raw_args p }
-| #[ atts = any_attribute ] [ "Elpi" "Tactic" qualified_name(p) ] -> {
-     let () = ignore_unknown_attributes atts in
+     EV.Synterp.create_command ?raw_args p
+   } -> {
+     EV.create_command p }
+| #[ atts = any_attribute ] [ "Elpi" "Tactic" qualified_name(p) ] SYNTERP AS _ 
+   { 
+     let () = ignore_unknown_attributes atts in
+     EV.Synterp.create_tactic p
+   } -> {
      EV.create_tactic p }
-| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] -> {
+| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] SYNTERP AS _ 
+   { 
      let () = ignore_unknown_attributes atts in
+     EV.Synterp.create_db d
+   } -> {
      EV.create_db d ~init:s }
 
 | #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] -> {