From b49675050810a62f3a3024a174ce8fac42867df0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Oct 2023 15:37:34 +0200 Subject: [PATCH 1/2] fix separation parsing/execution --- src/coq_elpi_programs.ml | 95 +++++++++++++++++++----------- src/coq_elpi_programs.mli | 9 ++- src/coq_elpi_vernacular.ml | 28 ++++++--- src/coq_elpi_vernacular.mli | 9 ++- src/coq_elpi_vernacular_syntax.mlg | 27 ++++++--- 5 files changed, 117 insertions(+), 51 deletions(-) diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index e5476157e..f2793efb4 100644 --- a/src/coq_elpi_programs.ml +++ b/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 = diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 951e7733d..63879f2fe 100644 --- a/src/coq_elpi_programs.mli +++ b/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 diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 6fb16636c..5a1f86503 100644 --- a/src/coq_elpi_vernacular.ml +++ b/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 diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index ac3ca1eef..64a132d82 100644 --- a/src/coq_elpi_vernacular.mli +++ b/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 diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index a81d1a39a..08bd601ef 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/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" ] -> { From a3388dc3bbcf585ced12db0784ec9549f7167ee2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Oct 2023 15:42:06 +0200 Subject: [PATCH 2/2] Update doc.yml --- .github/workflows/doc.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index cdd57bf5a..21d39c19d 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -16,6 +16,9 @@ jobs: runs-on: ubuntu-latest steps: + - name: workaround bug + run: sudo apt-get update + - name: checkout uses: actions/checkout@v2