From 23fc6ae1f018c4f162072ff36a6483d053d2d97e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Mar 2021 12:43:04 +0100 Subject: [PATCH] accumulated clauses can survive section if they don't mention variables --- Changelog.md | 8 +++++++ coq-builtin.elpi | 12 +++++++---- src/coq_elpi_HOAS.ml | 17 +++++++++++++-- src/coq_elpi_HOAS.mli | 1 + src/coq_elpi_builtins.ml | 27 ++++++++++-------------- src/coq_elpi_builtins.mli | 4 ++-- src/coq_elpi_utils.ml | 13 +++++++++++- src/coq_elpi_utils.mli | 6 +++++- src/coq_elpi_vernacular.ml | 42 ++++++++++++++++++++++++------------- src/coq_elpi_vernacular.mli | 2 +- tests/test_API.v | 38 ++++++++++++++++++++++++++++----- tests/test_tactic.v | 8 +++---- 12 files changed, 128 insertions(+), 50 deletions(-) diff --git a/Changelog.md b/Changelog.md index 494da4016..41d5d50f4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,14 @@ ## UNRELEASED + +### Vernacular +- Commands, Tactics and Db cannot be declared inside sections or modules + (it never really worked, but now you get an error message). +- Clauses which are accumulated via `coq.elpi.accumulate` and are not `@local!` + survive section closing if they don't mention the section variables being + discharged. + ### Typechecker - Warnings can be turned into errors by passing Coq `-w +elpi.typecheck`. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 59eb16fe1..b68be4e60 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -418,8 +418,8 @@ external type coq.say variadic any prop. external type coq.warn variadic any prop. % [coq.warning Category Name ...] -% Prints a warning message with a Name an Category which can be used -% to silence this warning or turn it into an error. See coqc -w connad +% Prints a warning message with a Name and Category which can be used +% to silence this warning or turn it into an error. See coqc -w commad % line option external type coq.warning string -> string -> variadic any prop. @@ -1032,9 +1032,13 @@ type current scope. % The module being defined (see begin/end-module) % to % the given db (see Elpi Db). Clauses belong to Coq modules: the Scope % argument -% lets one select which module (default is execution-site). +% lets one select which module (default is execution-site). +% A clause that mentions a section variable is automatically discarded at +% the +% end of the section. +% Clauses cannot be accumulated inside functors. % Supported attributes: -% - @local! (default: false) +% - @local! (default: false, discard at the end of section or module) external pred coq.elpi.accumulate i:scope, i:id, i:clause. % -- Utils ------------------------------------------------------------ diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index c05d49d4c..c55d4eb9f 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -206,8 +206,8 @@ let global_constant_of_globref = function | GlobRef.ConstRef x -> Constant x | x -> CErrors.anomaly Pp.(str"not a global constant: " ++ (Printer.pr_global x)) -let constant, inductive, constructor = - let open API.OpaqueData in +let ({ CD.isc = isconstant; cout = constantout },constant), (_,inductive), (_,constructor) = + let open API.RawOpaqueData in declare { name = "constant"; doc = "Global constant name"; @@ -241,6 +241,19 @@ let constant, inductive, constructor = } ;; +let collect_term_variables ~depth t = + let rec aux ~depth acc t = + match E.look ~depth t with + | E.CData c when isconstant c -> + begin match constantout c with + | Variable id -> id :: acc + | _ -> acc + end + | x -> fold_elpi_term aux acc ~depth x + in + aux ~depth [] t + + let gref = let open GlobRef in let open API.AlgebraicData in declare { diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index b650491c6..84d36fcdd 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -146,6 +146,7 @@ val universe : Sorts.t Conversion.t val global_constant_of_globref : Names.GlobRef.t -> global_constant val abbreviation : Globnames.syndef_name Conversion.t val implicit_kind : Glob_term.binding_kind Conversion.t +val collect_term_variables : depth:int -> term -> Names.Id.t list module GRMap : Elpi.API.Utils.Map.S with type key = Names.GlobRef.t module GRSet : Elpi.API.Utils.Set.S with type elt = Names.GlobRef.t diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index c656f21b5..fcd016e6c 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -111,15 +111,6 @@ let on_global_state_does_rewind_env api thunk = (); (fun state -> Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls) let warn_if_contains_univ_levels ~depth t = - let fold f acc ~depth t = - match t with - | E.Const _ | E.Nil | E.CData _ -> acc - | E.App(_,x,xs) -> List.fold_left (f ~depth) (f ~depth acc x) xs - | E.Cons(x,xs) -> f ~depth (f ~depth acc x) xs - | E.Builtin(_,xs) -> List.fold_left (f ~depth) acc xs - | E.Lam x -> f ~depth:(depth+1) acc x - | E.UnifVar(_,xs) -> List.fold_left (f ~depth) acc xs - in let global_univs = UGraph.domain (Environ.universes (Global.env ())) in let is_global u = match Univ.Universe.level u with @@ -128,7 +119,7 @@ let warn_if_contains_univ_levels ~depth t = let rec aux ~depth acc t = match E.look ~depth t with | E.CData c when isuniv c -> let u = univout c in if is_global u then acc else u :: acc - | x -> fold aux acc ~depth x + | x -> Coq_elpi_utils.fold_elpi_term aux acc ~depth x in let univs = aux ~depth [] t in if univs <> [] then @@ -224,7 +215,7 @@ let clauses_for_later = ~init:(fun () -> []) ~start:(fun x -> x) ~pp:(fun fmt l -> - List.iter (fun (dbname, code,local) -> + List.iter (fun (dbname, code,vars,local) -> Format.fprintf fmt "db:%s code:%a local:%b\n" (String.concat "." dbname) Elpi.API.Pp.Ast.program code local) l) @@ -503,7 +494,7 @@ The name and the grafting specification can be left unspecified.|}; } |> CConv.(!<) let set_accumulate_to_db, get_accumulate_to_db = - let f = ref (fun _ _ ~local:_ -> assert false) in + let f = ref (fun _ _ _ ~local:_ -> assert false) in (fun x -> f := x), (fun () -> !f) @@ -2345,22 +2336,26 @@ Supported attributes: Full (global, {| Declare that, once the program is over, the given clause has to be added to the given db (see Elpi Db). Clauses belong to Coq modules: the Scope argument -lets one select which module (default is execution-site). +lets one select which module (default is execution-site). +A clause that mentions a section variable is automatically discarded at the +end of the section. +Clauses cannot be accumulated inside functors. Supported attributes: -- @local! (default: false)|} )))), +- @local! (default: false, discard at the end of section or module)|} )))), (fun scope dbname (name,graft,clause) ~depth ctx _ state -> let loc = API.Ast.Loc.initial "(elpi.add_clause)" in let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in warn_if_contains_univ_levels ~depth clause; + let vars = collect_term_variables ~depth clause in let clause = API.Utils.clause_of_term ?name ?graft ~depth loc clause in let local = ctx.options.local = Some true in match scope with | Unspec | Given ExecutionSite -> State.update clauses_for_later state (fun l -> - (dbname,clause,local) :: l), (), [] + (dbname,clause,vars,local) :: l), (), [] | Given CurrentModule -> let f = get_accumulate_to_db () in - f dbname clause ~local; + f dbname clause vars ~local; state, (), [] )), DocAbove); diff --git a/src/coq_elpi_builtins.mli b/src/coq_elpi_builtins.mli index b070f7f80..4c5e94596 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/coq_elpi_builtins.mli @@ -9,8 +9,8 @@ val coq_builtins : BuiltIn.declaration list (* Clauses to be added to elpi programs when the execution is over *) val clauses_for_later : - (string list * Ast.program * bool) list State.component -val set_accumulate_to_db : ((string list -> Ast.program -> local:bool -> unit)) -> unit + (string list * Ast.program * Names.Id.t list * bool) list State.component +val set_accumulate_to_db : ((string list -> Ast.program -> Names.Id.t list -> local:bool -> unit)) -> unit val attribute : (string * Attributes.vernac_flag_value) Conversion.t diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 5883b0a65..a1c957d2f 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -130,4 +130,15 @@ let float64 : Float64.t Elpi.API.Conversion.t = hash = Float64.hash; hconsed = false; constants = []; - } \ No newline at end of file + } + +let fold_elpi_term f acc ~depth t = + let module E = Elpi.API.RawData in + match t with + | E.Const _ | E.Nil | E.CData _ -> acc + | E.App(_,x,xs) -> List.fold_left (f ~depth) (f ~depth acc x) xs + | E.Cons(x,xs) -> f ~depth (f ~depth acc x) xs + | E.Builtin(_,xs) -> List.fold_left (f ~depth) acc xs + | E.Lam x -> f ~depth:(depth+1) acc x + | E.UnifVar(_,xs) -> List.fold_left (f ~depth) acc xs + diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index f0ab223a4..737684b0c 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -21,5 +21,9 @@ val manual_implicit_of_binding_kind : Names.Name.t -> Glob_term.binding_kind -> val manual_implicit_of_gdecl : Glob_term.glob_decl -> (Names.Name.t * bool) option CAst.t val lookup_inductive : Environ.env -> Names.inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body +val fold_elpi_term : + (depth:int -> 'a -> Elpi.API.Data.term -> 'a) -> + 'a -> depth:int -> Elpi.API.RawData.view -> 'a + val uint63 : Uint63.t Elpi.API.Conversion.t -val float64 : Float64.t Elpi.API.Conversion.t \ No newline at end of file +val float64 : Float64.t Elpi.API.Conversion.t diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index e29291351..13e9c4848 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -326,7 +326,7 @@ and src_string = { val set_current_program : qualified_name -> unit val current_program : unit -> qualified_name val accumulate : qualified_name -> src list -> unit - val accumulate_to_db : qualified_name -> Compile.compilation_unit -> local:bool -> unit + val accumulate_to_db : qualified_name -> Compile.compilation_unit -> Names.Id.t list -> local:bool -> unit val load_checker : string -> unit val load_printer : string -> unit @@ -481,6 +481,7 @@ type snippet = { program : qualified_name; code : EC.compilation_unit; local : bool; + vars : Names.Id.t list; } let in_db : snippet -> Libobject.obj = @@ -488,16 +489,23 @@ let in_db : snippet -> Libobject.obj = db_name_src := SLMap.add name (append_to_db name (kname,p)) !db_name_src in let import i o = if Int.equal i 1 then cache o in Libobject.declare_object @@ { (Libobject.default_object "ELPI-DB") with - Libobject.classify_function = (fun ({ local; _ } as o) -> - if local then Libobject.Dispose else Libobject.Keep o); + Libobject.classify_function = (fun ({ local; program; _ } as o) -> + if local then Libobject.Dispose else Libobject.Keep o); Libobject.cache_function = cache; - Libobject.subst_function = (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")); + Libobject.subst_function = (fun _ -> + CErrors.user_err Pp.(str"elpi: Accumulating clauses in a functor is not supported yet")); Libobject.open_function = Libobject.simple_open import; + Libobject.discharge_function = (fun (_,({ local; program; vars; } as o)) -> + if local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None + else Some o); + } let accum = ref 0 -let add_to_db program code local = - ignore @@ Lib.add_leaf (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) (in_db { program; code; local }) +let add_to_db program code vars local = + ignore @@ Lib.add_leaf + (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) + (in_db { program; code; local; vars }) let lp_command_ast = Summary.ref ~name:"elpi-lp-command" None let in_lp_command_src : src -> Libobject.obj = @@ -538,15 +546,21 @@ let tactic_init () = let create_program (loc,qualid) init = 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 + CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") else add_to_program qualid [init] let create_db (loc,qualid) init = 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 + 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") else match ast_of_src init with - | [`Static,base] -> add_to_db qualid base false + | [`Static,base] -> add_to_db qualid base [] false | _ -> assert false ;; @@ -605,10 +619,10 @@ let accumulate p v = CErrors.user_err Pp.(str "No Elpi Program named " ++ pr_qualified_name p); add_to_program p v -let accumulate_to_db p v ~local = +let accumulate_to_db p v vs ~local = if not (db_exists p) then CErrors.user_err Pp.(str "No Elpi Db " ++ pr_qualified_name p); - add_to_db p v local + add_to_db p v vs local end @@ -670,14 +684,14 @@ let compile name baseul extra = (Summary.Local.(:=) compiler_cache (SLMap.add name (baseul,program) (Summary.Local.(!) compiler_cache))); extend_w_units ~base:program extra -let () = Coq_elpi_builtins.set_accumulate_to_db (fun n x ~local -> +let () = Coq_elpi_builtins.set_accumulate_to_db (fun n x vs ~local -> let elpi = ensure_initialized () in let u = try EC.unit ~elpi ~flags:(cc_flags ()) x with EC.CompileError(oloc, msg) -> let loc = Option.map Coq_elpi_utils.to_coq_loc oloc in CErrors.user_err ?loc ~hdr:"elpi" (Pp.str msg) in - Programs.accumulate_to_db n u ~local) + Programs.accumulate_to_db n u vs ~local) let get_and_compile name = let core_units, extra_units = get name in @@ -745,9 +759,9 @@ let run_and_print ~tactic_mode ~print ~static_check program_ast query_ast = API.State.get Coq_elpi_builtins.clauses_for_later state in let elpi = ensure_initialized () in - List.iter (fun (dbname,ast,local) -> + List.iter (fun (dbname,ast,vs,local) -> let unit = EC.unit ~elpi ~flags:(cc_flags()) ast in - accumulate_to_db dbname unit ~local) clauses_to_add + accumulate_to_db dbname unit vs ~local) clauses_to_add ;; let run_in_program ?(program = current_program ()) (loc, query) = @@ -902,7 +916,7 @@ let accumulate_string ?(program=current_program()) (loc,s) = let elpi = ensure_initialized () in let new_ast = unit_from_string ~elpi loc s in if db_exists program then - accumulate_to_db program new_ast ~local:false + accumulate_to_db program new_ast [] ~local:false else accumulate program [EmbeddedString { sloc = loc; sdata = s; sast = new_ast}] ;; diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index cb63d1a0c..ed928577b 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -18,7 +18,7 @@ val accumulate_files : ?program:qualified_name -> string list -> unit val accumulate_string : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> unit val accumulate_db : ?program:qualified_name -> qualified_name -> unit -val accumulate_to_db : qualified_name -> Elpi.API.Ast.Loc.t * string -> local:bool -> unit +val accumulate_to_db : qualified_name -> Elpi.API.Ast.Loc.t * string -> Names.Id.t list -> local:bool -> unit (* Setup *) diff --git a/tests/test_API.v b/tests/test_API.v index dd5ef6e4b..44cc52142 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -329,9 +329,6 @@ End II. (* inductive *) -Section Dummy. -Variable dummy : nat. - Elpi Command indtest. Elpi Accumulate lp:{{ main _ :- @@ -359,8 +356,6 @@ Check K2 true : myind true true. Check myind1 true false : Prop. Check K21 true : myind1 true true. -End Dummy. - Elpi Query lp:{{ coq.env.add-indt (parameter "X" _ {{Type}} x\ inductive "nuind" _ (parameter "n" _ {{ nat }} _\ arity {{ bool -> Type }}) i\ @@ -757,6 +752,39 @@ Fail Elpi Query lp:{{foo "there"}}. Import test_db_accumulate. Elpi Query lp:{{foo "there"}}. +(********* accumulate *************** *) + +Elpi Db test2.db lp:{{ + type foo gref -> prop. +}}. +Elpi Command test2.use.db. +Elpi Accumulate Db test2.db. +Elpi Accumulate lp:{{ + main [str S] :- coq.locate S GR, coq.elpi.accumulate _ "test2.db" (clause _ _ (foo GR)). + main [str "local", str S] :- coq.locate S GR, @local! => coq.elpi.accumulate _ "test2.db" (clause _ _ (foo GR)). + main [int N] :- std.findall (foo X_) L, coq.say L, std.length L N. +}}. + +Module T2. +Section T2. +Variable X : nat. +Elpi test2.use.db X. +Elpi test2.use.db nat. +Elpi test2.use.db "local" bool. +Elpi test2.use.db 3. +End T2. +Elpi test2.use.db "local" bool. +Elpi test2.use.db 2. +End T2. +Elpi test2.use.db 0. +Import T2. +Elpi test2.use.db 1. + + +Section T3. Fail Elpi Db test3.db lp:{{ }}. End T3. +Module T3. Fail Elpi Db test3.db lp:{{ }}. End T3. + +(********* export *************** *) Elpi Command export.me. Elpi Accumulate lp:{{ main _ :- coq.say "hello". }}. diff --git a/tests/test_tactic.v b/tests/test_tactic.v index 5a8e57b9f..84f080869 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -6,10 +6,6 @@ Elpi Tactic foobar. Elpi Print foobar. -Section foo. - -Variables n m : nat. -Let o := m. Elpi Tactic print.goal. Elpi Accumulate lp:{{ @@ -25,6 +21,10 @@ Elpi Accumulate lp:{{ Elpi Typecheck. +Section foo. + +Variables n m : nat. +Let o := m. Lemma test_print (T : Type) (x : forall y : T, Type) (h : o = m) (w : T) : forall e : x w = Type, forall j : x w, exists a : x w, a = a.