From 23803338b26bb833e9e5254d5b7ce36ce832ee59 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 26 Oct 2015 19:41:51 +0100 Subject: Two test-suite files for bugs 3974 and 3975 --- test-suite/bugs/closed/3974.v | 7 +++++++ test-suite/bugs/closed/3975.v | 8 ++++++++ 2 files changed, 15 insertions(+) create mode 100644 test-suite/bugs/closed/3974.v create mode 100644 test-suite/bugs/closed/3975.v diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v new file mode 100644 index 0000000000..b6be159595 --- /dev/null +++ b/test-suite/bugs/closed/3974.v @@ -0,0 +1,7 @@ +Module Type S. +End S. + +Module Type M (X : S). + Fail Module P (X : S). + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather say now: Error: X already exists. *) \ No newline at end of file diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v new file mode 100644 index 0000000000..95851c8137 --- /dev/null +++ b/test-suite/bugs/closed/3975.v @@ -0,0 +1,8 @@ +Module Type S. End S. + +Module M (X:S). End M. + +Module Type P (X : S). + Print M. + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather : print something :-) *) \ No newline at end of file -- cgit v1.2.3 From d4edd135e7cb8b6f86d9d5a0d320e0b29ee20148 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Oct 2015 17:57:24 +0200 Subject: Preserving goal name in revert/bring_hyps. --- tactics/tactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0d6a26a113..1437b24625 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2480,11 +2480,13 @@ let bring_hyps hyps = else Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in + let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (instance_from_named_context hyps) in Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar env sigma newcl in + let (sigma, ev) = + Evarutil.new_evar env sigma ~principal:true ~store newcl in (sigma, (mkApp (ev, args))) end end -- cgit v1.2.3 From d1114c5f55fcb96a99a1a5562b014414ad8217ba Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Oct 2015 18:10:24 +0200 Subject: Documenting a bit more interpretation functions in passing. --- interp/constrintern.mli | 8 +++++--- pretyping/pretyping.mli | 24 +++++++++++++++++------- 2 files changed, 22 insertions(+), 10 deletions(-) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4d2c994679..b671c98815 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -95,7 +95,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** {6 Composing internalization with type inference (pretyping) } *) -(** Main interpretation functions expecting evars to be all resolved *) +(** Main interpretation functions, using type class inference, + expecting evars and pending problems to be all resolved *) val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context @@ -106,9 +107,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context -(** Main interpretation function expecting evars to be all resolved *) +(** Main interpretation function expecting all postponed problems to + be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index a6aa086579..5f0e19cf2b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -66,9 +66,12 @@ val all_and_fail_flags : inference_flags (** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref -(** Generic call to the interpreter from glob_constr to open_constr, leaving - unresolved holes as evars and returning the typing contexts of - these evars. Work as [understand_gen] for the rest. *) +(** Generic calls to the interpreter from glob_constr to open_constr; + by default, inference_flags tell to use type classes and + heuristics (but no external tactic solver hooks), as well as to + ensure that conversion problems are all solved and expand evars, + but unresolved evars can remain. The difference is in whether the + evar_map is modified explicitly or by side-effect. *) val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> open_constr @@ -92,7 +95,12 @@ val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> typing_constraint -> glob_constr -> pure_open_constr -(** Standard call to get a constr from a glob_constr, resolving implicit args *) +(** Standard call to get a constr from a glob_constr, resolving + implicit arguments and coercions, and compiling pattern-matching; + the default inference_flags tells to use type classes and + heuristics (but no external tactic solver hook), as well as to + ensure that conversion problems are all solved and that no + unresolved evar remains, expanding evars. *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context @@ -102,12 +110,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> val understand_judgment : env -> evar_map -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context -(** Idem but do not fail on unresolved evars *) +(** Idem but do not fail on unresolved evars (type cl*) val understand_judgment_tcc : env -> evar_map ref -> glob_constr -> unsafe_judgment (** Trying to solve remaining evars and remaining conversion problems - with type classes, heuristics, and possibly an external solver *) + possibly using type classes, heuristics, external tactic solver + hook depending on given flags. *) (* For simplicity, it is assumed that current map has no other evars with candidate and no other conversion problems that the one in [pending], however, it can contain more evars than the pending ones. *) @@ -115,7 +124,8 @@ val understand_judgment_tcc : env -> evar_map ref -> val solve_remaining_evars : inference_flags -> env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map -(** Checking evars are all solved and reporting an appropriate error message *) +(** Checking evars and pending conversion problems are all solved, + reporting an appropriate error message *) val check_evars_are_solved : env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit -- cgit v1.2.3 From ee72fb2936a4ff5032aa6b8fba3165cdb6ca448e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Oct 2015 15:20:28 +0100 Subject: Preventing using OCaml 4.02.0 for compiling Coq as compilation times are redhibitory. --- INSTALL | 10 ++++++---- configure.ml | 7 ++++++- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/INSTALL b/INSTALL index 955e605c39..83c1b9f3f1 100644 --- a/INSTALL +++ b/INSTALL @@ -55,10 +55,12 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.12.1 (or later) - installed on your computer and that "ocamlc" (or its native code version - "ocamlc.opt") lie in a directory which is present in your $PATH environment - variable. +1- Check that you have the Objective Caml compiler installed on your + computer and that "ocamlc" (or, better, its native code version + "ocamlc.opt") lies in a directory which is present in your $PATH + environment variable. At the time of writing this sentence, all + versions of Objective Caml later or equal to 3.12.1 are + supported to the exception of Objective Caml 4.02.0. To get Coq in native-code, (it runs 4 to 10 times faster than bytecode, but it takes more time to get compiled and the binary is diff --git a/configure.ml b/configure.ml index 806ac381b2..0573cced63 100644 --- a/configure.ml +++ b/configure.ml @@ -513,7 +513,12 @@ let caml_version_nums = let check_caml_version () = if caml_version_nums >= [3;12;1] then - printf "You have OCaml %s. Good!\n" caml_version + if caml_version_nums = [4;2;0] && not !Prefs.force_caml_version then + die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ + "very slow compilation times. If you still want to use it, use \n" ^ + "option -force-caml-version.\n") + else + printf "You have OCaml %s. Good!\n" caml_version else let () = printf "Your version of OCaml is %s.\n" caml_version in if !Prefs.force_caml_version then -- cgit v1.2.3 From 032f1a4ba8b5655b4f2396671061613aa8e2cf48 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Oct 2015 15:22:30 +0100 Subject: Fixing bugs in options of the configure. - usage ill-formed for -native-compiler - compatibility with the configure of 8.4 (-force-caml-version), though e.g. its force-ocaml-version alias is no longer supported (but at the same time not documented either, so...) --- configure.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/configure.ml b/configure.ml index 0573cced63..1945167168 100644 --- a/configure.ml +++ b/configure.ml @@ -332,11 +332,11 @@ let args_options = Arg.align [ "-makecmd", Arg.Set_string Prefs.makecmd, " Name of GNU Make command"; "-native-compiler", arg_bool Prefs.nativecompiler, - " (yes|no) Compilation to native code for conversion and normalization"; + "(yes|no) Compilation to native code for conversion and normalization"; "-coqwebsite", Arg.Set_string Prefs.coqwebsite, " URL of the coq website"; - "-force-caml-version", arg_bool Prefs.force_caml_version, - " Force OCaml version"; + "-force-caml-version", Arg.Set Prefs.force_caml_version, + "Force OCaml version"; ] let parse_args () = -- cgit v1.2.3 From 7bf9bbe2968802b48230d35d34c585201ee9e9b4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Oct 2015 15:24:43 +0100 Subject: Seeing configure as a static resolution of path, hence hardwiring long paths for ocaml* executables in the generated config/Makefile. Hoping I'm not doing something wrong. E.g., I don't see why it would not be ok for windows or macosx too, since e.g. camlp5o was already with a full path. --- configure.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 1945167168..37c45f3e62 100644 --- a/configure.ml +++ b/configure.ml @@ -476,7 +476,10 @@ let camlbin, caml_version, camllib = rebase_camlexec dir camlexec; Filename.dirname camlexec.byte, camlexec.byte | None -> - try let camlc = which camlexec.byte in Filename.dirname camlc, camlc + try let camlc = which camlexec.byte in + let dir = Filename.dirname camlc in + rebase_camlexec dir camlexec; + dir, camlc with Not_found -> die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^ "Please adjust your path or use the -camldir option of ./configure") -- cgit v1.2.3 From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Oct 2015 13:55:45 -0400 Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names structure. --- library/declare.ml | 93 +++++++++++++++++++++++++------------------ library/declare.mli | 4 +- library/lib.ml | 39 ++++++++++++------ library/lib.mli | 2 +- library/universes.ml | 3 +- test-suite/bugs/closed/4390.v | 37 +++++++++++++++++ toplevel/command.ml | 4 +- toplevel/command.mli | 5 ++- toplevel/vernacentries.ml | 25 ++++++++---- 9 files changed, 147 insertions(+), 65 deletions(-) create mode 100644 test-suite/bugs/closed/4390.v diff --git a/library/declare.ml b/library/declare.ml index 16803b3bfa..0004f45a29 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -27,7 +27,7 @@ open Decls open Decl_kinds (** flag for internal message display *) -type internal_flag = +type internal_flag = | UserAutomaticRequest (* kernel action, a message is displayed *) | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) @@ -63,7 +63,7 @@ let cache_variable ((sp,_),o) = add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> + | Inr (id,_) -> if variable_polymorphic id then None else Some (Inl (variable_context id)) | Inl _ -> Some o @@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = +let dummy_constant_entry = ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { @@ -185,7 +185,7 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c -let definition_entry ?(opaque=false) ?(inline=false) ?types +let definition_entry ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; @@ -212,11 +212,11 @@ let declare_sideff env fix_exn se = in let ty_of cb = match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t + | Declarations.RegularArity t -> Some t | Declarations.TemplateArity _ -> None in let cst_of cb pt = let pt, opaque = pt_opaque_of cb pt in - let univs, subst = + let univs, subst = if cb.const_polymorphic then let univs = Univ.instantiate_univ_context cb.const_universes in univs, Vars.subst_instance_constr (Univ.UContext.instance univs) @@ -240,7 +240,7 @@ let declare_sideff env fix_exn se = } in let exists c = try ignore(Environ.lookup_constant c env); true - with Not_found -> false in + with Not_found -> false in let knl = CList.map_filter (fun (c,cb,pt) -> if exists c then None @@ -287,7 +287,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = - let cb = + let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id @@ -383,12 +383,12 @@ let inInductive : inductive_obj -> obj = let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, pjs)) -> + Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) + IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true | Some None | None -> false @@ -442,52 +442,69 @@ let assumption_message id = (** Global universe names, in a different summary *) -type universe_names = +type universe_names = (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) -let input_universes : universe_names -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi); - load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi); - discharge_function = (fun (_, a) -> Some a); - classify_function = (fun a -> Keep a) } +(* Discharged or not *) +type universe_decl = polymorphic * (Id.t * Univ.universe_level) list -let do_universe l = +let cache_universes (p, l) = let glob = Universes.global_universe_names () in - let glob', ctx = - List.fold_left (fun ((idl,lid),ctx) (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + let glob', ctx = + List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + ((Idmap.add id lev idl, Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set false ctx; - Lib.add_anonymous_leaf (input_universes glob') + if p then Lib.add_section_context ctx; + Universes.set_global_universe_names glob' + +let input_universes : universe_decl -> Libobject.obj = + declare_object + { (default_object "Global universe name state") with + cache_function = (fun (na, pi) -> cache_universes pi); + load_function = (fun _ (_, pi) -> cache_universes pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let do_universe poly l = + let l = + List.map (fun (l, id) -> + let lev = Universes.new_univ_level (Global.current_dirpath ()) in + (id, lev)) l + in + Lib.add_anonymous_leaf (input_universes (poly, l)) + +type constraint_decl = polymorphic * Univ.constraints + +let cache_constraints (na, (p, c)) = + Global.add_constraints c; + if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) +let discharge_constraints (_, (p, c as a)) = + if p then None else Some a -let input_constraints : Univ.constraints -> Libobject.obj = - let open Libobject in +let input_constraints : constraint_decl -> Libobject.obj = + let open Libobject in declare_object { (default_object "Global universe constraints") with - cache_function = (fun (na, c) -> Global.add_constraints c); - load_function = (fun _ (_, c) -> Global.add_constraints c); - discharge_function = (fun (_, a) -> Some a); + cache_function = cache_constraints; + load_function = (fun _ -> cache_constraints); + discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint l = - let u_of_id = +let do_constraint poly l = + let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> + fun (loc, id) -> try Idmap.find id names with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) in let constraints = List.fold_left (fun acc (l, d, r) -> let lu = u_of_id l and ru = u_of_id r in Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints constraints) - + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 76538a6248..7ed451c3f1 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -85,5 +85,5 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -val do_universe : Id.t Loc.located list -> unit -val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/lib.ml b/library/lib.ml index f4f52db53b..cdc8889037 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) + | Context of Univ.universe_context_set + let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.universe_context_set) list * - Opaqueproof.work_list * abstr_list) list) + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = @@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r - | ((_,_,poly,ctx)::idl,hyps) -> + | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context sign = - let rec inst_rec = function | (id,b,None,_) :: sign -> id :: inst_rec sign | _ :: sign -> inst_rec sign @@ -437,7 +448,8 @@ let add_section_replacement f g hyps = let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + g (sechyps,subst,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn = let section_instance = function | VarRef id -> - if List.exists (fun (id',_,_,_) -> Names.id_eq id id') - (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + let eq = function + | Variable (id',_,_,_) -> Names.id_eq id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5b2..b67b2b873f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit - +val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> Names.constant -> Context.named_context -> unit val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit diff --git a/library/universes.ml b/library/universes.ml index 0656188eb5..30d38eb2a4 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -16,7 +16,8 @@ open Univ type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t -let global_universes = Summary.ref ~name:"Global universe names" +let global_universes = + Summary.ref ~name:"Global universe names" ((Idmap.empty, Univ.LMap.empty) : universe_names) let global_universe_names () = !global_universes diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v new file mode 100644 index 0000000000..a96a137001 --- /dev/null +++ b/test-suite/bugs/closed/4390.v @@ -0,0 +1,37 @@ +Module A. +Set Printing All. +Set Printing Universes. + +Module M. +Section foo. +Universe i. +End foo. +End M. + +Check Type@{i}. +(* Succeeds *) + +Fail Check Type@{j}. +(* Error: Undeclared universe: j *) + +Definition foo@{j} : Type@{i} := Type@{j}. +(* ok *) +End A. + +Set Universe Polymorphism. +Fail Universes j. +Monomorphic Universe j. +Section foo. + Universes i. + Constraint i < j. + Definition foo : Type@{j} := Type@{i}. + Definition foo' : Type@{j} := Type@{i}. +End foo. + +Check eq_refl : foo@{i} = foo'@{i}. + +Definition bar := foo. +Monomorphic Definition bar'@{k} := foo@{k}. + +Fail Constraint j = j. +Monomorphic Constraint i = i. diff --git a/toplevel/command.ml b/toplevel/command.ml index 7c86d2d059..3995c4b1bc 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -38,8 +38,8 @@ open Indschemes open Misctypes open Vernacexpr -let do_universe l = Declare.do_universe l -let do_constraint l = Declare.do_constraint l +let do_universe poly l = Declare.do_universe poly l +let do_constraint poly l = Declare.do_constraint poly l let rec under_binders env sigma f n c = if Int.equal n 0 then snd (f env sigma c) else diff --git a/toplevel/command.mli b/toplevel/command.mli index b1e1d7d060..b400f0fde2 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -20,8 +20,9 @@ open Pfedit (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) -val do_universe : Id.t Loc.located list -> unit -val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> + (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit (** {6 Hooks for Pcoq} *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d04d6c9eda..2879947a91 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -552,12 +552,12 @@ let vernac_inductive poly lo finite indl = Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class true -> Class false | _ -> b) - poly finite id bl c oc fs + poly finite id bl c oc fs | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in - (((coe', AssumExpr ((loc, Name id), ce)), None), []) + (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) poly finite id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Errors.error "Definitional classes must have a single method" @@ -602,8 +602,19 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l -let vernac_universe l = do_universe l -let vernac_constraint l = do_constraint l +let vernac_universe loc poly l = + if poly && not (Lib.sections_are_opened ()) then + user_err_loc (loc, "vernac_universe", + str"Polymorphic universes can only be declared inside sections, " ++ + str "use Monomorphic Universe instead"); + do_universe poly l + +let vernac_constraint loc poly l = + if poly && not (Lib.sections_are_opened ()) then + user_err_loc (loc, "vernac_constraint", + str"Polymorphic universe constraints can only be declared" + ++ str " inside sections, use Monomorphic Constraint instead"); + do_constraint poly l (**********************) (* Modules *) @@ -1870,8 +1881,8 @@ let interp ?proof ~loc locality poly c = | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l - | VernacUniverse l -> vernac_universe l - | VernacConstraint l -> vernac_constraint l + | VernacUniverse l -> vernac_universe loc poly l + | VernacConstraint l -> vernac_constraint loc poly l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> @@ -2034,7 +2045,7 @@ let check_vernac_supports_polymorphism c p = | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacHints _ | VernacContext _ - | VernacExtend _ ) -> () + | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () | Some _, _ -> Errors.error "This command does not support Polymorphism" let enforce_polymorphism = function -- cgit v1.2.3 From 1235c6c3cfc6770920f46de30b1c4b0f5cb44b19 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Oct 2015 12:49:03 +0100 Subject: Do not pause globing in funind. (Fix bug #4382) Since the functions of this plugin exit by raising exceptions, globing was never restarted. This prevented coqdoc from generating a proper output whenever some feature of this plugin was used. There does not seem to be any parsing of dynamic expressions, so pausing globing does not make much sense in the first place. --- plugins/funind/functional_principles_types.ml | 7 +------ plugins/funind/indfun.ml | 9 ++------- 2 files changed, 3 insertions(+), 13 deletions(-) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 64284c6fe7..9e27ddf2e9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -594,9 +594,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in const::other_result - let build_scheme fas = - Dumpglob.pause (); let evd = (ref (Evd.from_env (Global.env ()))) in let pconstants = (List.map (fun (_,f,sort) -> @@ -626,10 +624,7 @@ let build_scheme fas = Declare.definition_message princ_id ) fas - bodies_types; - Dumpglob.continue () - - + bodies_types let build_case_scheme fa = let env = Global.env () diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eadeebd38e..47c67ed2aa 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -27,7 +27,6 @@ let choose_dest_or_ind scheme_info = Tactics.induction_destruct (is_rec_info scheme_info) false let functional_induction with_clean c princl pat = - Dumpglob.pause (); let res = let f,args = decompose_app c in fun g -> @@ -123,9 +122,7 @@ let functional_induction with_clean c princl pat = (args_as_induction_constr,princ'))) subst_and_reduce g' - in - Dumpglob.continue (); - res + in res let rec abstract_glob_constr c = function | [] -> c @@ -831,7 +828,6 @@ let make_graph (f_ref:global_reference) = end | _ -> raise (UserError ("", str "Not a function reference") ) in - Dumpglob.pause (); (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" | Some body -> @@ -883,8 +879,7 @@ let make_graph (f_ref:global_reference) = (* We register the infos *) List.iter (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) - expr_list); - Dumpglob.continue () + expr_list) let do_generate_principle = do_generate_principle [] warning_error true -- cgit v1.2.3 From 38aacaa96abee65edb64bf88f15016d54ce31568 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 27 Oct 2015 18:13:55 +0100 Subject: Seeing configure as a static resolution of path continued (not yet on windows). This makes sense probably on Windows too, to be evaluated, maybe .exe suffix should be added. --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 37c45f3e62..173429ba8e 100644 --- a/configure.ml +++ b/configure.ml @@ -478,7 +478,7 @@ let camlbin, caml_version, camllib = | None -> try let camlc = which camlexec.byte in let dir = Filename.dirname camlc in - rebase_camlexec dir camlexec; + if not arch_win32 then rebase_camlexec dir camlexec; (* win32: TOCHECK *) dir, camlc with Not_found -> die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^ -- cgit v1.2.3 From e3ec13976d39909ac6f1a82bf1b243ba8a895190 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Oct 2015 12:42:27 +0100 Subject: Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" After all, let's target 8.6. --- pretyping/constr_matching.ml | 19 +++---------------- test-suite/success/ltac.v | 26 -------------------------- 2 files changed, 3 insertions(+), 42 deletions(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 3fa037ffdd..5e99521a12 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -413,25 +413,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in let sub = (env, c1) :: subargs env lc in try_aux sub mk_ctx next - | Case (ci,p,c,brs) -> - (* Warning: this assumes predicate and branches to be - in canonical form using let and fun of the signature *) - let nardecls = List.length ci.ci_pp_info.ind_tags in - let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in - let env_p = Environ.push_rel_context sign_p env in - let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in - let sign_brs = Array.map fst brs in - let f (sign,br) = (Environ.push_rel_context sign env, br) in - let sub_br = Array.map f brs in + | Case (ci,hd,c1,lc) -> let next_mk_ctx = function - | c :: p :: brs -> - let p = it_mkLambda_or_LetIn p sign_p in - let brs = - Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in - mk_ctx (mkCase (ci,p,c,brs)) + | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) | _ -> assert false in - let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in + let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 5bef2e512a..6c4d4ae98f 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,29 +317,3 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. - -(* Check that matching "match" does not look into the invisible - canonically generated binders of the return clause and of the branches *) - -Goal forall n, match n with 0 => true | S _ => false end = true. -intros. unfold nat_rect. -Fail match goal with |- context [nat] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are correctly eta-expanded and hence matchable as seen - from the user point of view *) - -Goal forall a f n, nat_rect (fun _ => nat) a f n = 0. -intros. unfold nat_rect. -match goal with |- context [f _] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are in correct form also in the presence of let-ins *) - -Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a. -Goal forall x, match x with c => 0 end = 1. -intros. -match goal with |- context [0] => idtac end. -Abort. -- cgit v1.2.3 From b5a0e384b405f64fd0854d5e88b55e8c2a159c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 11:02:09 -0400 Subject: Univs: fix bug #4375, accept universe binders on (co)-fixpoints --- plugins/funind/indfun.ml | 2 +- test-suite/bugs/closed/4375.v | 106 ++++++++++++++++++++++++++++++++++++++++++ toplevel/command.ml | 44 +++++++++++------- toplevel/command.mli | 8 ++-- 4 files changed, 139 insertions(+), 21 deletions(-) create mode 100644 test-suite/bugs/closed/4375.v diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 47c67ed2aa..3dbd438061 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -592,7 +592,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in + let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in let fixpoint_exprl_with_new_bl = diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v new file mode 100644 index 0000000000..03af16535b --- /dev/null +++ b/test-suite/bugs/closed/4375.v @@ -0,0 +1,106 @@ + + +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + + +Module A. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End A. + +Module B. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End B. + +Module C. +Fail Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End C. + +Module D. +Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End D. + +Module E. +Fail Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j i} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End E. + +(* +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print g. + +Polymorphic Fixpoint a@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t +with b@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print a. +Print b. +*) + +Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} := +| A : foo T -> foo T. + +Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (cg@{i} t). + +Print cg. + +Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@cb@{i} t) +with cb@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@ca@{i} t). + +Print ca. +Print cb. \ No newline at end of file diff --git a/toplevel/command.ml b/toplevel/command.ml index 3995c4b1bc..d75efeca1e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1037,7 +1037,17 @@ let interp_recursive isfix fixl notations = let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let evdref = ref (Evd.from_env env) in + let all_universes = + List.fold_right (fun sfe acc -> + match sfe.fix_univs , acc with + | None , acc -> acc + | x , None -> x + | Some ls , Some us -> + if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then + error "(co)-recursive definitions should all have the same universe binders"; + Some (ls @ us)) fixl None in + let ctx = Evd.make_evar_universe_context env all_universes in + let evdref = ref (Evd.from_ctx ctx) in let fixctxs, fiximppairs, fixannots = List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in let fixctximpenvs, fixctximps = List.split fiximppairs in @@ -1084,7 +1094,7 @@ let interp_recursive isfix fixl notations = let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in (* Build the fix declaration block *) - (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots + (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env evd (Evd.empty,evd); @@ -1094,16 +1104,16 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = end let interp_fixpoint l ntns = - let (env,_,evd),fix,info = interp_recursive true l ntns in + let (env,_,pl,evd),fix,info = interp_recursive true l ntns in check_recursive true env evd fix; - (fix,Evd.evar_universe_context evd,info) + (fix,pl,Evd.evar_universe_context evd,info) let interp_cofixpoint l ntns = - let (env,_,evd),fix,info = interp_recursive false l ntns in + let (env,_,pl,evd),fix,info = interp_recursive false l ntns in check_recursive false env evd fix; - fix,Evd.evar_universe_context evd,info + (fix,pl,Evd.evar_universe_context evd,info) -let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = +let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1127,10 +1137,10 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in - let ctx = Universes.restrict_universe_context ctx vars in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in - let ctx = Univ.ContextSet.to_context ctx in + let ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) @@ -1139,7 +1149,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns = +let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1158,10 +1168,12 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let vars = Universes.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in - let ctx = Univ.ContextSet.to_context ctx in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) @@ -1197,7 +1209,7 @@ let out_def = function let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in - let (env, rec_sign, evd), fix, info = + let (env, rec_sign, pl, evd), fix, info = interp_recursive isfix fixl ntns in (* Program-specific code *) @@ -1267,9 +1279,9 @@ let do_fixpoint local poly l = if Flags.is_program_mode () then do_program_fixpoint local poly l else let fixl, ntns = extract_fixpoint_components true l in - let fix = interp_fixpoint fixl ntns in + let (_, _, _, info as fix) = interp_fixpoint fixl ntns in let possible_indexes = - List.map compute_possible_guardness_evidences (pi3 fix) in + List.map compute_possible_guardness_evidences info in declare_fixpoint local poly fix possible_indexes ntns let do_cofixpoint local poly l = diff --git a/toplevel/command.mli b/toplevel/command.mli index b400f0fde2..94b4af9dd9 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -136,24 +136,24 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Evd.evar_universe_context * + recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Evd.evar_universe_context * + recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : locality -> polymorphic -> - recursive_preentry * Evd.evar_universe_context * + recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * Evd.evar_universe_context * + recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit -- cgit v1.2.3 From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- dev/vm_printers.ml | 7 +- kernel/byterun/coq_interp.c | 34 ++++-- kernel/byterun/coq_values.h | 17 ++- kernel/cbytecodes.ml | 57 +++++----- kernel/cbytecodes.mli | 31 ++++-- kernel/cbytegen.ml | 250 ++++++++++++++++++++++++++++++++++---------- kernel/cbytegen.mli | 10 +- kernel/cemitcodes.ml | 23 ++-- kernel/cemitcodes.mli | 4 +- kernel/csymtable.ml | 30 +++--- kernel/environ.mli | 2 +- kernel/mod_typing.ml | 10 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 2 +- kernel/term_typing.ml | 39 ++++--- kernel/univ.ml | 7 +- kernel/univ.mli | 3 + kernel/vars.ml | 4 +- kernel/vars.mli | 2 +- kernel/vconv.ml | 50 +++++++-- kernel/vm.ml | 112 ++++++++++++++++---- kernel/vm.mli | 11 +- pretyping/vnorm.ml | 96 ++++++++++++----- 23 files changed, 578 insertions(+), 225 deletions(-) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 802b0f9d80..272df7b421 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -13,7 +13,7 @@ let ppripos (ri,pos) = ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" - | Reloc_getglobal (kn,_) -> + | Reloc_getglobal kn -> print_string ("getglob "^(string_of_con kn)^"\n")); print_flush () @@ -30,7 +30,7 @@ let ppsort = function let print_idkey idk = match idk with - | ConstKey (sp,_) -> + | ConstKey sp -> print_string "Cons("; print_string (string_of_con sp); print_string ")" @@ -61,7 +61,8 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Aind((sp,i),_) -> print_string "Ind("; + | Atype u -> print_string "Type(...)" + | Aind(sp,i) -> print_string "Ind("; print_string (string_of_mind sp); print_string ","; print_int i; print_string ")" diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0553a5ed7e..dc571699ef 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -341,6 +341,7 @@ value coq_interprete /* Fallthrough */ Instruct(ENVACC){ print_instr("ENVACC"); + print_int(*pc); accu = Field(coq_env, *pc++); Next; } @@ -371,6 +372,10 @@ value coq_interprete sp[1] = (value)pc; sp[2] = coq_env; sp[3] = Val_long(coq_extra_args); + print_instr("call stack="); + print_lint(sp[1]); + print_lint(sp[2]); + print_lint(sp[3]); pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; @@ -458,6 +463,7 @@ value coq_interprete sp[0] = arg1; sp[1] = arg2; pc = Code_val(accu); + print_lint(accu); coq_env = accu; coq_extra_args += 1; goto check_stacks; @@ -481,11 +487,18 @@ value coq_interprete print_instr("RETURN"); print_int(*pc); sp += *pc++; + print_instr("stack="); + print_lint(sp[0]); + print_lint(sp[1]); + print_lint(sp[2]); if (coq_extra_args > 0) { + print_instr("extra args > 0"); + print_lint(coq_extra_args); coq_extra_args--; pc = Code_val(accu); coq_env = accu; } else { + print_instr("extra args = 0"); pc = (code_t)(sp[0]); coq_env = sp[1]; coq_extra_args = Long_val(sp[2]); @@ -585,7 +598,10 @@ value coq_interprete Alloc_small(accu, 1 + nvars, Closure_tag); Code_val(accu) = pc + *pc; pc++; - for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i]; + for (i = 0; i < nvars; i++) { + print_lint(sp[i]); + Field(accu, i + 1) = sp[i]; + } sp += nvars; Next; } @@ -720,6 +736,7 @@ value coq_interprete /* Fallthrough */ Instruct(GETGLOBAL){ print_instr("GETGLOBAL"); + print_int(*pc); accu = Field(coq_global_data, *pc); pc++; Next; @@ -732,7 +749,7 @@ value coq_interprete tag_t tag = *pc++; mlsize_t i; value block; - print_instr("MAKEBLOCK"); + print_instr("MAKEBLOCK, tag="); Alloc_small(block, wosize, tag); Field(block, 0) = accu; for (i = 1; i < wosize; i++) Field(block, i) = *sp++; @@ -743,7 +760,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK1"); + print_instr("MAKEBLOCK1, tag="); + print_int(tag); Alloc_small(block, 1, tag); Field(block, 0) = accu; accu = block; @@ -753,7 +771,8 @@ value coq_interprete tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK2"); + print_instr("MAKEBLOCK2, tag="); + print_int(tag); Alloc_small(block, 2, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -764,7 +783,8 @@ value coq_interprete Instruct(MAKEBLOCK3) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK3"); + print_instr("MAKEBLOCK3, tag="); + print_int(tag); Alloc_small(block, 3, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -776,7 +796,8 @@ value coq_interprete Instruct(MAKEBLOCK4) { tag_t tag = *pc++; value block; - print_instr("MAKEBLOCK4"); + print_instr("MAKEBLOCK4, tag="); + print_int(tag); Alloc_small(block, 4, tag); Field(block, 0) = accu; Field(block, 1) = sp[0]; @@ -940,6 +961,7 @@ value coq_interprete /* Fallthrough */ Instruct(CONSTINT) { print_instr("CONSTINT"); + print_int(*pc); accu = Val_int(*pc); pc++; Next; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 80100da719..bb0f0eb5e4 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -17,22 +17,17 @@ #define Default_tag 0 #define Accu_tag 0 - - #define ATOM_ID_TAG 0 #define ATOM_INDUCTIVE_TAG 1 -#define ATOM_PROJ_TAG 2 -#define ATOM_FIX_TAG 3 -#define ATOM_SWITCH_TAG 4 -#define ATOM_COFIX_TAG 5 -#define ATOM_COFIXEVALUATED_TAG 6 - - +#define ATOM_TYPE_TAG 2 +#define ATOM_PROJ_TAG 3 +#define ATOM_FIX_TAG 4 +#define ATOM_SWITCH_TAG 5 +#define ATOM_COFIX_TAG 6 +#define ATOM_COFIXEVALUATED_TAG 7 /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #endif /* _COQ_VALUES_ */ - - diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 448bf85444..b13b0607b3 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -19,13 +19,12 @@ type tag = int let accu_tag = 0 -let max_atom_tag = 1 -let proj_tag = 2 -let fix_app_tag = 3 -let switch_tag = 4 -let cofix_tag = 5 -let cofix_evaluated_tag = 6 - +let max_atom_tag = 2 +let proj_tag = 3 +let fix_app_tag = 4 +let switch_tag = 5 +let cofix_tag = 6 +let cofix_evaluated_tag = 7 (* It would be great if OCaml exported this value, So fixme if this happens in a new version of OCaml *) @@ -33,10 +32,12 @@ let last_variant_tag = 245 type structured_constant = | Const_sorts of sorts - | Const_ind of pinductive + | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array + | Const_univ_level of Univ.universe_level + | Const_type of Univ.universe type reloc_table = (tag * int) array @@ -71,7 +72,8 @@ type instruction = | Kclosure of Label.t * int | Kclosurerec of int * int * Label.t array * Label.t array | Kclosurecofix of int * int * Label.t array * Label.t array - | Kgetglobal of pconstant + (* nb fv, init, lbl types, lbl bodies *) + | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag | Kmakeprod @@ -127,7 +129,10 @@ type instruction = and bytecodes = instruction list -type fv_elem = FVnamed of Id.t | FVrel of int +type fv_elem = + | FVnamed of Id.t + | FVrel of int + | FVuniv_var of int type fv = fv_elem array @@ -145,18 +150,17 @@ type vm_env = { type comp_env = { - nb_stack : int; (* nbre de variables sur la pile *) - in_stack : int list; (* position dans la pile *) - nb_rec : int; (* nbre de fonctions mutuellement *) - (* recursives = nbr *) + nb_uni_stack : int ; (* number of universes on the stack, *) + (* universes are always at the bottom. *) + nb_stack : int; (* number of variables on the stack *) + in_stack : int list; (* position in the stack *) + nb_rec : int; (* number of mutually recursive functions *) pos_rec : instruction list; (* instruction d'acces pour les variables *) (* de point fix ou de cofix *) offset : int; - in_env : vm_env ref + in_env : vm_env ref (* The free variables of the expression *) } - - (* --- Pretty print *) open Pp open Util @@ -169,14 +173,24 @@ let pp_sort s = let rec pp_struct_const = function | Const_sorts s -> pp_sort s - | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i + | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) + | Const_univ_level l -> Univ.Level.pr l + | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let pp_lbl lbl = str "L" ++ int lbl +let pp_pcon (id,u) = + pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" + +let pp_fv_elem = function + | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" + | FVrel i -> str "Rel(" ++ int i ++ str ")" + | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" + let rec pp_instr i = match i with | Klabel _ | Ksequence _ -> assert false @@ -210,8 +224,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,u) -> - str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" + | Kgetglobal idu -> str "getglobal " ++ pr_con idu | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> @@ -269,10 +282,6 @@ and pp_bytecodes c = | i :: c -> tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c -let dump_bytecode c = - pperrnl (pp_bytecodes c); - flush_all() - (*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) type block = diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 03d6383057..c35ef6920f 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -22,14 +22,18 @@ val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag -val last_variant_tag : tag +val last_variant_tag : tag type structured_constant = | Const_sorts of sorts - | Const_ind of pinductive + | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array + | Const_univ_level of Univ.universe_level + | Const_type of Univ.universe + +val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array @@ -64,9 +68,11 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of pconstant (** accu = coq_global_data[c] *) + | Kgetglobal of constant | Kconst of structured_constant - | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *) + | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 + ** is accu, all others are popped from + ** the top of the stack *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int | Kswitch of Label.t array * Label.t array (** consts,blocks *) @@ -120,7 +126,10 @@ type instruction = and bytecodes = instruction list -type fv_elem = FVnamed of Id.t | FVrel of int +type fv_elem = + FVnamed of Id.t +| FVrel of int +| FVuniv_var of int type fv = fv_elem array @@ -129,26 +138,28 @@ type fv = fv_elem array closed terms. *) exception NotClosed -(*spiwack: both type have been moved from Cbytegen because I needed then +(*spiwack: both type have been moved from Cbytegen because I needed them for the retroknowledge *) type vm_env = { - size : int; (** longueur de la liste [n] *) + size : int; (** length of the list [n] *) fv_rev : fv_elem list (** [fvn; ... ;fv1] *) } type comp_env = { + nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) nb_rec : int; (** number of mutually recursive functions *) - (** recursives = nbr *) + (** (= nbr) *) pos_rec : instruction list; (** instruction d'acces pour les variables *) (** de point fix ou de cofix *) offset : int; - in_env : vm_env ref + in_env : vm_env ref (** the variables that are accessed *) } -val dump_bytecode : bytecodes -> unit +val pp_bytecodes : bytecodes -> Pp.std_ppcmds +val pp_fv_elem : fv_elem -> Pp.std_ppcmds (*spiwack: moved this here because I needed it for retroknowledge *) type block = diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3462694d61..f9f72efdb9 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -96,13 +96,14 @@ let empty_fv = { size= 0; fv_rev = [] } let fv r = !(r.in_env) -let empty_comp_env ()= - { nb_stack = 0; +let empty_comp_env ?(univs=0) ()= + { nb_uni_stack = univs; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; offset = 0; - in_env = ref empty_fv; + in_env = ref empty_fv } (*i Creation functions for comp_env *) @@ -110,8 +111,9 @@ let empty_comp_env ()= let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) -let comp_env_fun arity = - { nb_stack = arity; +let comp_env_fun ?(univs=0) arity = + { nb_uni_stack = univs ; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; pos_rec = []; @@ -120,8 +122,9 @@ let comp_env_fun arity = } -let comp_env_fix_type rfv = - { nb_stack = 0; +let comp_env_fix_type rfv = + { nb_uni_stack = 0; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; @@ -134,7 +137,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_stack = arity; + { nb_uni_stack = 0; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; pos_rec = !prec; @@ -143,7 +147,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_stack = 0; + { nb_uni_stack = 0; + nb_stack = 0; in_stack = []; nb_rec = 0; pos_rec = []; @@ -156,7 +161,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_stack = arity; + { nb_uni_stack = 0; + nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; pos_rec = !prec; @@ -168,7 +174,7 @@ let comp_env_cofix ndef arity rfv = let push_param n sz r = { r with nb_stack = r.nb_stack + n; - in_stack = add_param n sz r.in_stack } + in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack } (* [push_local sz r] add a new variable on the stack at position [sz] *) let push_local sz r = @@ -176,8 +182,6 @@ let push_local sz r = nb_stack = r.nb_stack + 1; in_stack = (sz + 1) :: r.in_stack } - - (*i Compilation of variables *) let find_at f l = let rec aux n = function @@ -214,6 +218,37 @@ let pos_rel i r sz = r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; Kenvacc(r.offset + pos) +(* +let pos_poly_inst idu r = + let env = !(r.in_env) in + let f = function + | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i + | _ -> false + in + try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + with Not_found -> + let pos = env.size in + let db = FVpoly_inst idu in + r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + Kenvacc(r.offset + pos) +*) + +let pos_universe_var i r sz = + if i < r.nb_uni_stack then + Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + else + let env = !(r.in_env) in + let f = function + | FVuniv_var u -> Int.equal i u + | _ -> false + in + try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + with Not_found -> + let pos = env.size in + let db = FVuniv_var i in + r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ; + Kenvacc(r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -459,7 +494,8 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind ind -> Bstrconst (Const_ind ind) + | Ind (ind,_) -> + Bstrconst (Const_ind ind) | Construct (((kn,j),i),u) -> begin (* spiwack: tries first to apply the run-time compilation @@ -513,6 +549,7 @@ let compile_fv_elem reloc fv sz cont = match fv with | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont + | FVuniv_var i -> pos_universe_var i reloc sz :: cont let rec compile_fv reloc l sz cont = match l with @@ -524,18 +561,21 @@ let rec compile_fv reloc l sz cont = (* Compiling constants *) -let rec get_alias env (kn,u as p) = +let rec get_alias env kn = let cb = lookup_constant kn env in let tps = cb.const_body_code in match tps with - | None -> p + | None -> kn | Some tps -> (match Cemitcodes.force tps with - | BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u') - | _ -> p) + | BCalias kn' -> get_alias env kn' + | _ -> kn) (* Compiling expressions *) +type ('a,'b) sum = Inl of 'a | Inr of 'b + +(* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" @@ -552,9 +592,40 @@ let rec compile_constr reloc c sz cont = | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont | Const (kn,u) -> compile_const reloc kn u [||] sz cont - | Sort _ | Ind _ | Construct _ -> + | Ind (i,u) -> + if Univ.Instance.is_empty u then compile_str_cst reloc (str_const c) sz cont - + else + comp_app compile_str_cst compile_universe reloc + (str_const c) + (Univ.Instance.to_array u) + sz + cont + | Sort (Prop _) | Construct _ -> + compile_str_cst reloc (str_const c) sz cont + | Sort (Type u) -> + begin + let levels = Univ.Universe.levels u in + if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels + then + (** TODO(gmalecha): Fix this **) + (** NOTE: This relies on the order of iteration to be consistent + **) + let level_vars = + List.map_filter (fun x -> Univ.Level.var_index x) + (Univ.LSet.elements levels) + in + let compile_get_univ reloc idx sz cont = + compile_fv_elem reloc (FVuniv_var idx) sz cont + in + comp_app compile_str_cst compile_get_univ reloc + (Bstrconst (Const_type u)) + (Array.of_list level_vars) + sz + cont + else + compile_str_cst reloc (str_const c) sz cont + end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz (Kpush :: @@ -663,7 +734,9 @@ let rec compile_constr reloc c sz cont = let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = match branch1 with - | Kreturn k -> assert (Int.equal k sz); sz, branch1, true + | Kreturn k -> + assert (Int.equal k sz) ; + sz, branch1, true | _ -> sz+3, Kjump, false in let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in @@ -745,6 +818,19 @@ and compile_str_cst reloc sc sz cont = (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) +and compile_get_global reloc (kn,u) sz cont = + let kn = get_alias !global_env kn in + if Univ.Instance.is_empty u then + Kgetglobal kn :: cont + else + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_universe reloc () (Univ.Instance.to_array u) sz cont + +and compile_universe reloc uni sz cont = + match Univ.Level.var_index uni with + | None -> Kconst (Const_univ_level uni) :: cont + | Some idx -> pos_universe_var idx reloc sz :: cont + and compile_const = fun reloc-> fun kn u -> fun args -> fun sz -> fun cont -> let nargs = Array.length args in @@ -756,31 +842,83 @@ and compile_const = (mkConstU (kn,u)) reloc args sz cont with Not_found -> if Int.equal nargs 0 then - Kgetglobal (get_alias !global_env (kn, u)) :: cont + compile_get_global reloc (kn,u) sz cont else - comp_app (fun _ _ _ cont -> - Kgetglobal (get_alias !global_env (kn,u)) :: cont) - compile_constr reloc () args sz cont - -let compile fail_on_error env c = + if Univ.Instance.is_empty u then + (* normal compilation *) + comp_app (fun _ _ sz cont -> + compile_get_global reloc (kn,u) sz cont) + compile_constr reloc () args sz cont + else + let compile_either reloc constr_or_uni sz cont = + match constr_or_uni with + | Inl cst -> compile_constr reloc cst sz cont + | Inr uni -> compile_universe reloc uni sz cont + in + (** TODO(gmalecha): This can be more efficient **) + let all = + Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @ + List.map (fun x -> Inl x) (Array.to_list args)) + in + comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) + compile_either reloc () all sz cont + +let is_univ_copy max u = + let u = Univ.Instance.to_array u in + if Array.length u = max then + Array.fold_left_i (fun i acc u -> + if acc then + match Univ.Level.var_index u with + | None -> false + | Some l -> l = i + else false) true u + else + false + +let dump_bytecodes init code fvs = + let open Pp in + (str "code =" ++ fnl () ++ + pp_bytecodes init ++ fnl () ++ + pp_bytecodes code ++ fnl () ++ + str "fv = " ++ + prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ + fnl ()) + +let compile fail_on_error ?universes:(universes=0) env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); - let reloc = empty_comp_env () in - try - let init_code = compile_constr reloc c 0 [Kstop] in - let fv = List.rev (!(reloc.in_env).fv_rev) in - let pp_v v = - match v with - | FVnamed id -> Pp.str (Id.to_string id) - | FVrel i -> Pp.str (string_of_int i) + let cont = [Kstop] in + try + let reloc, init_code = + if Int.equal universes 0 then + let reloc = empty_comp_env () in + reloc, compile_constr reloc c 0 cont + else + (* We are going to generate a lambda, but merge the universe closure + * with the function closure if it exists. + *) + let reloc = empty_comp_env () in + let arity , body = + match kind_of_term c with + | Lambda _ -> + let params, body = decompose_lam c in + List.length params , body + | _ -> 0 , c + in + let full_arity = arity + universes in + let r_fun = comp_env_fun ~univs:universes arity in + let lbl_fun = Label.create () in + let cont_fun = + compile_constr r_fun body full_arity [Kreturn full_arity] + in + fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + let fv = fv r_fun in + reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont) in - let open Pp in - if !Flags.dump_bytecode then - (dump_bytecode init_code; - dump_bytecode !fun_code; - Pp.msg_debug (Pp.str "fv = " ++ - Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ())); + let fv = List.rev (!(reloc.in_env).fv_rev) in + (if !Flags.dump_bytecode then + Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in @@ -789,28 +927,33 @@ let compile fail_on_error env c = Id.print tname ++ str str_max_constructors)); None) -let compile_constant_body fail_on_error env = function +let compile_constant_body fail_on_error env univs = function | Undef _ | OpaqueDef _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in + let instance_size = + match univs with + | None -> 0 + | Some univ -> Univ.UContext.size univ + in match kind_of_term body with - | Const (kn',u) -> + | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in - Some (BCalias (get_alias env (con,u))) + Some (BCalias (get_alias env con)) | _ -> - let res = compile fail_on_error env body in + let res = compile fail_on_error ~universes:instance_size env body in Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) -let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u) +let compile_alias kn = BCalias (constant_of_kn (canonical_con kn)) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) let make_areconst n else_lbl cont = - if n <=0 then + if n <= 0 then cont else Kareconst (n, else_lbl)::cont @@ -902,14 +1045,14 @@ let op2_compilation op = 3/ if at least one is not, branches to the normal behavior: Kgetglobal (get_alias !global_env kn) *) let op_compilation n op = - let code_construct kn cont = + let code_construct reloc kn sz cont = let f_cont = let else_lbl = Label.create () in Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: op:: Kreturn 0:: Klabel else_lbl:: (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - Kgetglobal (get_alias !global_env kn):: - Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *) + compile_get_global reloc kn sz ( + Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) in let lbl = Label.create () in fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; @@ -926,12 +1069,11 @@ let op_compilation n op = (*Kaddint31::escape::Klabel else_lbl::Kpush::*) (op::escape::Klabel else_lbl::Kpush:: (* works as comp_app with nargs = n and non-tailcall cont*) - Kgetglobal (get_alias !global_env kn):: - Kapply n::labeled_cont))) + compile_get_global reloc kn sz (Kapply n::labeled_cont)))) else if Int.equal nargs 0 then - code_construct kn cont + code_construct reloc kn sz cont else - comp_app (fun _ _ _ cont -> code_construct kn cont) + comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont) compile_constr reloc () args sz cont let int31_escape_before_match fc cont = diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 1128f0d0b7..c0f48641ce 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -4,17 +4,17 @@ open Term open Declarations open Pre_env - +(** Should only be used for monomorphic terms *) val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *) - env -> constr -> (bytecodes * bytecodes * fv) option + ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option (** init, fun, fv *) -val compile_constant_body : bool -> - env -> constant_def -> body_code option +val compile_constant_body : bool -> + env -> constant_universes option -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) -val compile_alias : pconstant -> body_code +val compile_alias : Names.constant -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9b275cb6c3..2a70d0b1b7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of pconstant + | Reloc_getglobal of Names.constant type patch = reloc_info * int @@ -127,11 +127,11 @@ let slot_for_const c = enter (Reloc_const c); out_int 0 -and slot_for_annot a = +let slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal p = +let slot_for_getglobal p = enter (Reloc_getglobal p); out_int 0 @@ -190,7 +190,7 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q - | Kconst((Const_b0 i)) -> + | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 then out (opCONST0 + i) else (out opCONSTINT; out_int i) @@ -310,7 +310,7 @@ let rec subst_strcst s sc = | Const_sorts _ | Const_b0 _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_patch s (ri,pos) = match ri with @@ -319,7 +319,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -328,12 +328,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) type body_code = | BCdefined of to_patch - | BCalias of pconstant + | BCalias of Names.constant | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of pconstant substituted +| PBCalias of Names.constant substituted | PBCconstant let from_val = function @@ -343,7 +343,7 @@ let from_val = function let force = function | PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCalias cu -> BCalias (force subst_pconstant cu) +| PBCalias cu -> BCalias (force subst_constant cu) | PBCconstant -> BCconstant let subst_to_patch_subst s = function @@ -373,8 +373,3 @@ let to_memory (init_code, fun_code, fv) = | Label_undefined patchlist -> assert (patchlist = []))) !label_table; (code, reloc, fv) - - - - - diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 54b92b9121..10f3a6087a 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant Univ.puniverses + | Reloc_getglobal of constant type patch = reloc_info * int @@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCalias of constant Univ.puniverses + | BCalias of constant | BCconstant diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index b3f0ba5b58..28f0fa4f28 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -58,7 +58,7 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 | Const_sorts _, _ -> false -| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 | Const_proj _, _ -> false @@ -67,18 +67,24 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 | Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2 +| Const_univ_level _ , _ -> false +| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type _ , _ -> false let rec hash_structured_constant c = let open Hashset.Combine in match c with | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u)) + | Const_ind i -> combinesmall 2 (ind_hash i) | Const_proj p -> combinesmall 3 (Constant.hash p) | Const_b0 t -> combinesmall 4 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in let h = Array.fold_left fold 0 a in combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + | Const_type u -> combinesmall 7 (Univ.Universe.hash u) module SConstTable = Hashtbl.Make (struct type t = structured_constant @@ -124,7 +130,7 @@ exception NotEvaluated let key rk = match !rk with | None -> raise NotEvaluated - | Some k -> (*Pp.msgnl (str"found at: "++int k);*) + | Some k -> try Ephemeron.get k with Ephemeron.InvalidKey -> raise NotEvaluated @@ -148,23 +154,22 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n -let rec slot_for_getglobal env (kn,u) = +let rec slot_for_getglobal env kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = match cb.const_body_code with - | None -> set_global (val_of_constant (kn,u)) + | None -> set_global (val_of_constant kn) | Some code -> match Cemitcodes.force code with | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) + let v = eval_to_patch env (code,pl,fv) in + set_global v | BCalias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + | BCconstant -> set_global (val_of_constant kn) + in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -197,6 +202,8 @@ and slot_for_fv env fv = fill_fv_cache rv i val_of_rel env_of_rel b | Some (v, _) -> v end + | FVuniv_var idu -> + assert false and eval_to_patch env (buff,pl,fv) = (* copy code *before* patching because of nested evaluations: @@ -214,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) = List.iter patch pl; let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in -(*Pp.msgnl (str"execute code");*) eval_tcode tc vm_env and val_of_constr env c = @@ -232,5 +238,3 @@ and val_of_constr env c = let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) - - diff --git a/kernel/environ.mli b/kernel/environ.mli index 9f6ea522a7..dfe6cc85b1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -250,7 +250,7 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c03c5175fd..bd7ee7b339 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -126,11 +126,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in +(* let ctx' = Univ.UContext.make (newus, cst) in *) + let univs = + if cb.const_polymorphic then Some cb.const_universes + else None + in let cb' = { cb with const_body = def; - const_universes = univs; - const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) } + const_universes = ctx ; + const_body_code = Option.map Cemitcodes.from_val + (compile_constant_body env' univs def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index f0cb65c967..cbb7963315 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -335,7 +335,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) } + const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 263befd213..4d033bc999 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) = | None -> p | Some tps -> match Cemitcodes.force tps with - | Cemitcodes.BCalias kn' -> get_alias env kn' + | Cemitcodes.BCalias kn' -> get_alias env (kn', u) | _ -> p (*i Global environment *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b6df8f454b..cab99077f0 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -258,33 +258,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in let tps = - (* FIXME: incompleteness of the bytecode vm: we compile polymorphic - constants like opaque definitions. *) - if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant) - else - let res = - match proj with - | None -> compile_constant_body env def - | Some pb -> + let res = + let comp_univs = if poly then Some univs else None in + match proj with + | None -> compile_constant_body env comp_univs def + | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => Proj(p,c)). We break the cycle by building an ad-hoc compilation environment. A cleaner solution would be that kernel projections are simply Proj(i,c) with i an int and c a constr, but we would have to get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = proj; - const_body_code = None; - const_polymorphic = poly; - const_universes = univs; - const_inline_code = inline_code } - in - let env = add_constant kn cb env in - compile_constant_body env def - in Option.map Cemitcodes.from_val res + let cb = + { const_hyps = hyps; + const_body = def; + const_type = typ; + const_proj = proj; + const_body_code = None; + const_polymorphic = poly; + const_universes = univs; + const_inline_code = inline_code } + in + let env = add_constant kn cb env in + compile_constant_body env comp_univs def + in Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/univ.ml b/kernel/univ.ml index c0bd3bacd7..064dde3a64 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1754,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' (** A context of universe levels with universe constraints, - representiong local universe variables and constraints *) + representing local universe variables and constraints *) module UContext = struct @@ -1778,8 +1778,11 @@ struct let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' - + let dest x = x + + let size (x,_) = Instance.length x + end type universe_context = UContext.t diff --git a/kernel/univ.mli b/kernel/univ.mli index cbaf7e546a..c926c57bd8 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -343,6 +343,9 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t + (* the number of universes in the context *) + val size : t -> int + end type universe_context = UContext.t diff --git a/kernel/vars.ml b/kernel/vars.ml index 88c1e1038c..a800e25315 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -337,5 +337,5 @@ let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx -type id_key = pconstant tableKey -let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y +type id_key = constant tableKey +let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index fdd4603b5b..c0fbeeb6e6 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -88,5 +88,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_ val subst_instance_constr : universe_instance -> constr -> constr val subst_instance_context : universe_instance -> rel_context -> rel_context -type id_key = pconstant tableKey +type id_key = constant tableKey val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2f6be06011..e0d9688486 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 cu = else conv_whd env pb k (whd_val v1) (whd_val v2) cu and conv_whd env pb k whd1 whd2 cu = +(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *) match whd1, whd2 with | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu + | Vuniv_level _ , _ + | _ , Vuniv_level _ -> + (** Both of these are invalid since universes are handled via + ** special cases in the code. + **) + assert false | Vprod p1, Vprod p2 -> let cu = conv_val env CONV k (dom p1) (dom p2) cu in conv_fun env pb k (codom p1) (codom p2) cu @@ -81,26 +88,53 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = +(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ind1, Aind ind2 -> - if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2 + | Aind ((mi,i) as ind1) , Aind ind2 -> + if eq_ind ind1 ind2 && compare_stack stk1 stk2 then - conv_stack env k stk1 stk2 cu + if Environ.polymorphic_ind ind1 env + then + let mib = Environ.lookup_mind mi env in + let ulen = Univ.UContext.size mib.Declarations.mind_universes in + match stk1 , stk2 with + | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> + assert (ulen <= nargs args1) ; + assert (ulen <= nargs args2) ; + for i = 0 to ulen - 1 do + let a1 = uni_lvl_val (arg args1 i) in + let a2 = uni_lvl_val (arg args2 i) in + let result = Univ.Level.equal a1 a2 in + if not result + then raise NotConvertible + done ; + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) + | _ -> raise NotConvertible + else + conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible + | Atype u1 , Atype u2 -> + let u1 = Vm.instantiate_universe u1 stk1 in + let u2 = Vm.instantiate_universe u2 stk2 in + sort_cmp_universes env pb (Type u1) (Type u2) cu + | Atype _ , Aid _ + | Atype _ , Aind _ + | Aid _ , Atype _ | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env k stk1 stk2 cu = +and conv_stack env ?from:(from=0) k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in @@ -144,13 +178,13 @@ and conv_cofix env k cf1 cf2 cu = conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible -and conv_arguments env k args1 args2 cu = +and conv_arguments env ?from:(from=0) k args1 args2 cu = if args1 == args2 then cu else let n = nargs args1 in if Int.equal n (nargs args2) then let rcu = ref cu in - for i = 0 to n - 1 do + for i = from to n - 1 do rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu done; !rcu diff --git a/kernel/vm.ml b/kernel/vm.ml index eacd803fd4..858f546c60 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -121,12 +121,12 @@ type vswitch = { (* *) (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) (* - representation of [accu] : tag_[....] *) -(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *) -(* -- 3_[accu|proj name] : a projection blocked by an accu *) -(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 5_[accu|vswitch] : a match blocked by an accu *) -(* -- 6_[fcofix] : a cofix function *) -(* -- 7_[fcofix|val] : a cofix function, val represent the value *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[fcofix|val] : a cofix function, val represent the value *) (* of the function applied to arg1 ... argn *) (* The [arguments] type, which is abstracted as an array, represents : *) (* tag[ _ | _ |v1|... | vn] *) @@ -136,7 +136,8 @@ type vswitch = { type atom = | Aid of Vars.id_key - | Aind of pinductive + | Aind of inductive + | Atype of Univ.universe (* Zippers *) @@ -159,6 +160,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack + | Vuniv_level of Univ.universe_level (*************************************************) (* Destructors ***********************************) @@ -199,7 +201,9 @@ let rec whd_accu a stk = | [Zapp args] -> Vcofix(vcofix, res, Some args) | _ -> assert false end - | _ -> assert false + | tg -> + Errors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -212,22 +216,45 @@ let whd_val : values -> whd = if tag = accu_tag then ( if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else + else if is_accumulate (fun_code o) then whd_accu o [] - else (Vprod(Obj.obj o))) + else Vprod(Obj.obj o)) else if tag = Obj.closure_tag || tag = Obj.infix_tag then - ( match kind_of_closure o with + (match kind_of_closure o with | 0 -> Vfun(Obj.obj o) | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) - else - Vconstr_block(Obj.obj o) - + else + Vconstr_block(Obj.obj o) + +let uni_lvl_val : values -> Univ.universe_level = + fun v -> + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + (************************************************) -(* Abstrct machine ******************************) +(* Abstract machine *****************************) (************************************************) (* gestion de la pile *) @@ -299,6 +326,8 @@ let rec obj_of_str_const str = Obj.set_field res i (obj_of_str_const args.(i)) done; res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) let val_of_obj o = ((Obj.obj o) : values) @@ -317,11 +346,11 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = pconstant tableKey - let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal) + type t = constant tableKey + let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function - | ConstKey (c,u) -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end @@ -606,3 +635,50 @@ let apply_whd k whd = interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v + | Vuniv_level lvl -> assert false + +let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = + match stk with + | [] -> u + | [Zapp args] -> + assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; + let _,mp = Univ.LSet.fold (fun key (i,mp) -> + let u = uni_lvl_val (arg args i) in + (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) + (Univ.Universe.levels u) + (0,Univ.LMap.empty) in + let subst = Univ.make_subst mp in + Univ.subst_univs_universe subst u + | _ -> + Errors.anomaly Pp.(str "ill-formed universe") + + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Names.pr_con c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index 045d02333c..bc19786632 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -22,7 +22,8 @@ type arguments type atom = | Aid of Vars.id_key - | Aind of pinductive + | Aind of inductive + | Atype of Univ.universe (** Zippers *) @@ -45,19 +46,25 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack + | Vuniv_level of Univ.universe_level + +val pr_atom : atom -> Pp.std_ppcmds +val pr_whd : whd -> Pp.std_ppcmds (** Constructors *) val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : pconstant -> values +val val_of_constant : constant -> values external val_of_annot_switch : annot_switch -> values = "%identity" (** Destructors *) val whd_val : values -> whd +val uni_lvl_val : values -> Univ.universe_level +val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 46af784dda..b9c1a5a1c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -let constr_type_of_idkey env idkey = - match idkey with - | ConstKey cst -> - let const_type = Typeops.type_of_constant_in env cst in - mkConstU cst, const_type - | VarKey id -> - let (_,_,ty) = lookup_named id env in - mkVar id, ty - | RelKey i -> - let n = (nb_rel env - i) in - let (_,_,ty) = lookup_rel n env in - mkRel n, lift n ty - let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) @@ -164,9 +151,11 @@ and nf_whd env whd typ = let t = ta.(i) in let _, args = nf_args env vargs t in mkApp(cfd,args) - | Vconstr_const n -> construct_of_constr_const env n typ + | Vconstr_const n -> + construct_of_constr_const env n typ | Vconstr_block b -> let tag = btag b in + let x = tag in let (tag,ofs) = if tag = Cbytecodes.last_variant_tag then match whd_val (bfield b 0) with @@ -177,22 +166,80 @@ and nf_whd env whd typ = let args = nf_bargs env b ofs ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> - let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk - | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkIndU ind) (type_of_ind env ind) stk + constr_type_of_idkey env idkey stk nf_stk +(*let c,typ = constr_type_of_idkey env idkey in + nf_stk env c typ stk *) + | Vatom_stk(Aind ((mi,i) as ind), stk) -> + if Environ.polymorphic_ind ind env then + let mib = Environ.lookup_mind mi env in + let ulen = Univ.UContext.size mib.mind_universes in + match stk with + | Zapp args :: stk' -> + assert (ulen <= nargs args) ; + let inst = + Array.init ulen (fun i -> Vm.uni_lvl_val (arg args i)) + in + let pind = (ind, Univ.Instance.of_array inst) in + nf_stk ~from:ulen env (mkIndU pind) (type_of_ind env pind) stk + | _ -> assert false + else + let pind = (ind, Univ.Instance.empty) in + nf_stk env (mkIndU pind) (type_of_ind env pind) stk + | Vatom_stk(Atype u, stk) -> + mkSort (Type (Vm.instantiate_universe u stk)) + | Vuniv_level lvl -> + assert false + +and constr_type_of_idkey env (idkey : Vars.id_key) stk cont = + match idkey with + | ConstKey cst -> + if Environ.polymorphic_constant cst env then + let cbody = Environ.lookup_constant cst env in + match stk with + | Zapp vargs :: stk' -> + let uargs = Univ.UContext.size cbody.const_universes in + assert (Vm.nargs vargs >= uargs) ; + let uary = Array.init uargs (fun i -> Vm.uni_lvl_val (Vm.arg vargs i)) in + let ui = Univ.Instance.of_array uary in + let ucst = (cst, ui) in + let const_type = Typeops.type_of_constant_in env ucst in + if uargs < Vm.nargs vargs then + let t, args = nf_args env vargs ~from:uargs const_type in + cont env (mkApp (mkConstU ucst, args)) t stk' + else + cont env (mkConstU ucst) const_type stk' + | _ -> assert false + else + begin + let ucst = (cst, Univ.Instance.empty) in + let const_type = Typeops.type_of_constant_in env ucst in + cont env (mkConstU ucst) const_type stk + end + | VarKey id -> + let (_,_,ty) = lookup_named id env in + cont env (mkVar id) ty stk + | RelKey i -> + let n = (nb_rel env - i) in + let (_,_,ty) = lookup_rel n env in + cont env (mkRel n) (lift n ty) stk -and nf_stk env c t stk = +and nf_stk ?from:(from=0) env c t stk = match stk with | [] -> c | Zapp vargs :: stk -> - let t, args = nf_args env vargs t in - nf_stk env (mkApp(c,args)) t stk + if nargs vargs >= from then + let t, args = nf_args ~from:from env vargs t in + nf_stk env (mkApp(c,args)) t stk + else + let rest = from - nargs vargs in + nf_stk ~from:rest env c t stk | Zfix (f,vargs) :: stk -> + assert (from = 0) ; let fa, typ = nf_fix_app env f vargs in let _,_,codom = decompose_prod env typ in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> + assert (from = 0) ; let ((mind,_ as ind), u), allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in @@ -215,6 +262,7 @@ and nf_stk env c t stk = let ci = case_info sw in nf_stk env (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> + assert (from = 0) ; let p' = Projection.make p true in let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in nf_stk env (mkProj(p',c)) ty stk @@ -240,14 +288,14 @@ and nf_predicate env ind mip params v pT = true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type -and nf_args env vargs t = +and nf_args env vargs ?from:(f=0) t = let t = ref t in - let len = nargs vargs in + let len = nargs vargs - f in let args = Array.init len (fun i -> let _,dom,codom = decompose_prod env !t in - let c = nf_val env (arg vargs i) dom in + let c = nf_val env (arg vargs (f+i)) dom in t := subst1 c codom; c) in !t,args -- cgit v1.2.3 From 95669265239c4da7f5cfcf134825f6801e52391f Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 21 Oct 2015 09:13:18 -0700 Subject: test cases. --- test-suite/kernel/vm-univ.v | 145 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 test-suite/kernel/vm-univ.v diff --git a/test-suite/kernel/vm-univ.v b/test-suite/kernel/vm-univ.v new file mode 100644 index 0000000000..1bdba3c68d --- /dev/null +++ b/test-suite/kernel/vm-univ.v @@ -0,0 +1,145 @@ +(* Basic tests *) +Polymorphic Definition pid {T : Type} (x : T) : T := x. +(* +Definition _1 : pid true = true := + @eq_refl _ true <: pid true = true. + +Polymorphic Definition a_type := Type. + +Definition _2 : a_type@{i} = Type@{i} := + @eq_refl _ Type@{i} <: a_type@{i} = Type@{i}. + +Polymorphic Definition FORALL (T : Type) (P : T -> Prop) : Prop := + forall x : T, P x. + +Polymorphic Axiom todo : forall {T:Type}, T -> T. + +Polymorphic Definition todo' (T : Type) := @todo T. + +Definition _3 : @todo'@{Set} = @todo@{Set} := + @eq_refl _ (@todo@{Set}) <: @todo'@{Set} = @todo@{Set}. +*) + +(* Inductive Types *) +Inductive sumbool (A B : Prop) : Set := +| left : A -> sumbool A B +| right : B -> sumbool A B. + +Definition x : sumbool True False := left _ _ I. + +Definition sumbool_copy {A B : Prop} (H : sumbool A B) : sumbool A B := + match H with + | left _ _ x => left _ _ x + | right _ _ x => right _ _ x + end. + +Definition _4 : sumbool_copy x = x := + @eq_refl _ x <: sumbool_copy x = x. + +(* Polymorphic Inductive Types *) +Polymorphic Inductive poption (T : Type@{i}) : Type@{i} := +| PSome : T -> poption@{i} T +| PNone : poption@{i} T. + +Polymorphic Definition poption_default {T : Type@{i}} (p : poption@{i} T) (x : T) : T := + match p with + | @PSome _ y => y + | @PNone _ => x + end. + +Polymorphic Inductive plist (T : Type@{i}) : Type@{i} := +| pnil +| pcons : T -> plist@{i} T -> plist@{i} T. + +Arguments pnil {_}. +Arguments pcons {_} _ _. + +Section pmap. + Context {T : Type@{i}} {U : Type@{j}} (f : T -> U). + + Polymorphic Fixpoint pmap (ls : plist@{i} T) : plist@{j} U := + match ls with + | @pnil _ => @pnil _ + | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls) + end. +End pmap. + +Universe Ubool. +Inductive tbool : Type@{Ubool} := ttrue | tfalse. + + +Eval vm_compute in pmap pid (pcons true (pcons false pnil)). +Eval vm_compute in pmap (fun x => match x with + | pnil => true + | pcons _ _ => false + end) (pcons pnil (pcons (pcons false pnil) pnil)). +Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) pnil)). + +Polymorphic Inductive Tree (T : Type@{i}) : Type@{i} := +| Empty +| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. + +Section pfold. + Context {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U). + + Polymorphic Fixpoint pfold (acc : U) (ls : plist@{i} T) : U := + match ls with + | pnil => acc + | pcons a b => pfold (f a acc) b + end. +End pfold. + +Polymorphic Inductive nat : Type@{i} := +| O +| S : nat -> nat. + +Fixpoint nat_max (a b : nat) : nat := + match a , b with + | O , b => b + | a , O => a + | S a , S b => S (nat_max a b) + end. + +Polymorphic Fixpoint height {T : Type@{i}} (t : Tree@{i} T) : nat := + match t with + | Empty _ => O + | Branch _ ls => S (pfold nat_max O (pmap height ls)) + end. + +Polymorphic Fixpoint repeat {T : Type@{i}} (n : nat) (v : T) : plist@{i} T := + match n with + | O => pnil + | S n => pcons v (repeat n v) + end. + +Polymorphic Fixpoint big_tree (n : nat) : Tree@{i} nat := + match n with + | O => @Empty nat + | S n' => Branch _ (repeat n' (big_tree n')) + end. + +Eval compute in height (big_tree (S (S (S O)))). + +Let big := S (S (S (S (S O)))). +Polymorphic Definition really_big := (S@{i} (S (S (S (S (S (S (S (S (S O)))))))))). + +Time Definition _5 : height (@Empty nat) = O := + @eq_refl nat O <: height (@Empty nat) = O. + +Time Definition _6 : height@{Set} (@Branch nat pnil) = S O := + @eq_refl nat@{Set} (S@{Set} O@{Set}) <: height@{Set} (@Branch nat pnil) = S O. + +Time Definition _7 : height (big_tree big) = big := + @eq_refl nat big <: height (big_tree big) = big. + +Time Definition _8 : height (big_tree really_big) = really_big := + @eq_refl nat@{Set} (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} (S@{Set} (S@{Set} (S@{Set} (S@{Set} O@{Set})))))))))) + <: + @eq nat@{Set} + (@height nat@{Set} (big_tree really_big@{Set})) + really_big@{Set}. -- cgit v1.2.3 From 9ce6802ea563437b15e45198f4d8d0f716a576bb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Oct 2015 23:27:50 +0100 Subject: Fix minor typo in native compiler. --- kernel/nativevalues.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e4a7799933..40bef4bc67 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -10,7 +10,7 @@ open Names open Errors open Util -(** This modules defines the representation of values internally used by +(** This module defines the representation of values internally used by the native compiler *) type t = t -> t -- cgit v1.2.3 From 90dfacaacfec8265b11dc9291de9510f515c0081 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Oct 2015 23:59:05 +0100 Subject: Conversion of polymorphic inductive types was incomplete in VM and native. Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with a polymorphic prod. --- kernel/nativeconv.ml | 10 ++++++---- kernel/reduction.ml | 14 ++++++++------ kernel/reduction.mli | 7 ++++++- kernel/vconv.ml | 35 ++++++++++------------------------- pretyping/reductionops.ml | 2 +- 5 files changed, 31 insertions(+), 37 deletions(-) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 7ae66c485a..0242fd461c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -63,10 +63,12 @@ and conv_atom env pb lvl a1 a2 cu = | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Aind ind1, Aind ind2 -> - if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible - | Aconstant c1, Aconstant c2 -> - if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible + | Aind (ind1,u1), Aind (ind2,u2) -> + if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + else raise NotConvertible + | Aconstant (c1,u1), Aconstant (c2,u2) -> + if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2c111a55b5..892557ac6c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -173,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -185,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) -let convert_instances flex u u' (s, check) = - (check.compare_instances flex u u' s, check) +(* [flex] should be true for constants, false for inductive types and + constructors. *) +let convert_instances ~flex u u' (s, check) = + (check.compare_instances ~flex u u' s, check) let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -196,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv = else let flex = evaluable_constant cst (info_env infos) && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) - in convert_instances flex u u' cuniv + in convert_instances ~flex u u' cuniv | VarKey id, VarKey id' when Id.equal id id' -> cuniv | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible @@ -590,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs = let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances _flex u u' univs = +let check_convert_instances ~flex u u' univs = if Univ.Instance.check_eq univs u u' then univs else raise NotConvertible @@ -630,7 +632,7 @@ let infer_cmp_universes env pb s0 s1 univs = | CONV -> infer_eq univs u1 u2) else univs -let infer_convert_instances flex u u' (univs,cstrs) = +let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c3cc7b2b69..0df26d6276 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool (* Instance of a flexible constant? *) -> + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(* [flex] should be true for constants, false for inductive types and +constructors. *) +val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> + 'a * 'a universe_compare -> 'a * 'a universe_compare + val checked_universes : Univ.universes universe_compare val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare diff --git a/kernel/vconv.ml b/kernel/vconv.ml index e0d9688486..2e519789e1 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -99,17 +99,15 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let ulen = Univ.UContext.size mib.Declarations.mind_universes in match stk1 , stk2 with | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> - assert (ulen <= nargs args1) ; - assert (ulen <= nargs args2) ; - for i = 0 to ulen - 1 do - let a1 = uni_lvl_val (arg args1 i) in - let a2 = uni_lvl_val (arg args2 i) in - let result = Univ.Level.equal a1 a2 in - if not result - then raise NotConvertible - done ; - conv_arguments env ~from:ulen k args1 args2 - (conv_stack env k stk1' stk2' cu) + assert (ulen <= nargs args1); + assert (ulen <= nargs args2); + let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in + let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in + let u1 = Univ.Instance.of_array u1 in + let u2 = Univ.Instance.of_array u2 in + let cu = convert_instances ~flex:false u1 u2 cu in + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) | _ -> raise NotConvertible else conv_stack env k stk1 stk2 cu @@ -118,13 +116,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype u1 , Atype u2 -> - let u1 = Vm.instantiate_universe u1 stk1 in - let u2 = Vm.instantiate_universe u2 stk2 in - sort_cmp_universes env pb (Type u1) (Type u2) cu - | Atype _ , Aid _ - | Atype _ , Aind _ - | Aid _ , Atype _ + | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env ?from:(from=0) k stk1 stk2 cu = @@ -190,13 +182,6 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu = !rcu else raise NotConvertible -let rec eq_puniverses f (x,l1) (y,l2) cu = - if f x y then conv_universes l1 l2 cu - else raise NotConvertible - -and conv_universes l1 l2 cu = - if Univ.Instance.equal l1 l2 then cu else raise NotConvertible - let vm_conv_gen cv_pb env univs t1 t2 = try let v1 = val_of_constr env t1 in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bb1bc7d2ea..0714c93b4f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1282,7 +1282,7 @@ let sigma_compare_sorts env pb s0 s1 sigma = | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 -let sigma_compare_instances flex i0 i1 sigma = +let sigma_compare_instances ~flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 with Evd.UniversesDiffer | Univ.UniverseInconsistency _ -> -- cgit v1.2.3 From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 11:16:24 +0100 Subject: Refine Gregory Malecha's patch on VM and universe polymorphism. - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. --- dev/vm_printers.ml | 1 + kernel/cbytecodes.ml | 1 + kernel/cbytecodes.mli | 1 + kernel/cbytegen.ml | 92 ++++++++++++--------------- kernel/cemitcodes.ml | 2 +- kernel/vconv.ml | 3 +- kernel/vm.ml | 167 ++++++++++++++++++++++++-------------------------- kernel/vm.mli | 1 - pretyping/vnorm.ml | 85 ++++++++++++------------- 9 files changed, 163 insertions(+), 190 deletions(-) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 272df7b421..1c501df808 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -79,6 +79,7 @@ and ppwhd whd = | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s + | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl) and ppvblock b = open_hbox(); diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index b13b0607b3..0a24a75d68 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -19,6 +19,7 @@ type tag = int let accu_tag = 0 +let type_atom_tag = 2 let max_atom_tag = 2 let proj_tag = 3 let fix_app_tag = 4 diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index c35ef6920f..03ae6b9cdc 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -15,6 +15,7 @@ type tag = int val accu_tag : tag +val type_atom_tag : tag val max_atom_tag : tag val proj_tag : tag val fix_app_tag : tag diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index f9f72efdb9..1f7cc3c7a6 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -91,6 +91,7 @@ open Pre_env (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = [] } @@ -218,21 +219,6 @@ let pos_rel i r sz = r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; Kenvacc(r.offset + pos) -(* -let pos_poly_inst idu r = - let env = !(r.in_env) in - let f = function - | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i - | _ -> false - in - try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) - with Not_found -> - let pos = env.size in - let db = FVpoly_inst idu in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; - Kenvacc(r.offset + pos) -*) - let pos_universe_var i r sz = if i < r.nb_uni_stack then Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) @@ -494,9 +480,9 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind (ind,_) -> + | Ind (ind,u) when Univ.Instance.is_empty u -> Bstrconst (Const_ind ind) - | Construct (((kn,j),i),u) -> + | Construct (((kn,j),i),_) -> begin (* spiwack: tries first to apply the run-time compilation behavior of the constructor, as in 2/ above *) @@ -571,10 +557,6 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> kn) -(* Compiling expressions *) - -type ('a,'b) sum = Inl of 'a | Inr of 'b - (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = match kind_of_term c with @@ -592,39 +574,43 @@ let rec compile_constr reloc c sz cont = | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont | Const (kn,u) -> compile_const reloc kn u [||] sz cont - | Ind (i,u) -> + | Ind (ind,u) -> + let bcst = Bstrconst (Const_ind ind) in if Univ.Instance.is_empty u then - compile_str_cst reloc (str_const c) sz cont + compile_str_cst reloc bcst sz cont else comp_app compile_str_cst compile_universe reloc - (str_const c) + bcst (Univ.Instance.to_array u) sz cont | Sort (Prop _) | Construct _ -> compile_str_cst reloc (str_const c) sz cont | Sort (Type u) -> - begin - let levels = Univ.Universe.levels u in - if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels - then - (** TODO(gmalecha): Fix this **) - (** NOTE: This relies on the order of iteration to be consistent - **) - let level_vars = - List.map_filter (fun x -> Univ.Level.var_index x) - (Univ.LSet.elements levels) - in - let compile_get_univ reloc idx sz cont = + (* We separate global and local universes in [u]. The former will be part + of the structured constant, while the later (if any) will be applied as + arguments. *) + let open Univ in begin + let levels = Universe.levels u in + let global_levels = + LSet.filter (fun x -> Level.var_index x = None) levels + in + let local_levels = + List.map_filter (fun x -> Level.var_index x) + (LSet.elements levels) + in + (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let uglob = + LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m + in + if local_levels = [] then + compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont + else + let compile_get_univ reloc idx sz cont = compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) - (Array.of_list level_vars) - sz - cont - else - compile_str_cst reloc (str_const c) sz cont + (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz @@ -831,8 +817,7 @@ and compile_universe reloc uni sz cont = | None -> Kconst (Const_univ_level uni) :: cont | Some idx -> pos_universe_var idx reloc sz :: cont -and compile_const = - fun reloc-> fun kn u -> fun args -> fun sz -> fun cont -> +and compile_const reloc kn u args sz cont = let nargs = Array.length args in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function @@ -850,18 +835,19 @@ and compile_const = compile_get_global reloc (kn,u) sz cont) compile_constr reloc () args sz cont else - let compile_either reloc constr_or_uni sz cont = + let compile_arg reloc constr_or_uni sz cont = match constr_or_uni with - | Inl cst -> compile_constr reloc cst sz cont - | Inr uni -> compile_universe reloc uni sz cont - in - (** TODO(gmalecha): This can be more efficient **) - let all = - Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @ - List.map (fun x -> Inl x) (Array.to_list args)) + | ArgConstr cst -> compile_constr reloc cst sz cont + | ArgUniv uni -> compile_universe reloc uni sz cont in + let u = Univ.Instance.to_array u in + let lu = Array.length u in + let all = + Array.init (lu + Array.length args) + (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu)) + in comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) - compile_either reloc () all sz cont + compile_arg reloc () all sz cont let is_univ_copy max u = let u = Univ.Instance.to_array u in diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2a70d0b1b7..ef0c9af4ff 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -307,7 +307,7 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2e519789e1..4610dbcb07 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -98,6 +98,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = Univ.UContext.size mib.Declarations.mind_universes in match stk1 , stk2 with + | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> assert (ulen <= nargs args1); assert (ulen <= nargs args2); @@ -108,7 +109,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let cu = convert_instances ~flex:false u1 u2 cu in conv_arguments env ~from:ulen k args1 args2 (conv_stack env k stk1' stk2' cu) - | _ -> raise NotConvertible + | _, _ -> assert false (* Should not happen if problem is well typed *) else conv_stack env k stk1 stk2 cu else raise NotConvertible diff --git a/kernel/vm.ml b/kernel/vm.ml index 858f546c60..64ddc43766 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -162,16 +162,96 @@ type whd = | Vatom_stk of atom * stack | Vuniv_level of Univ.universe_level +(************************************************) +(* Abstract machine *****************************) +(************************************************) + +(* gestion de la pile *) +external push_ra : tcode -> unit = "coq_push_ra" +external push_val : values -> unit = "coq_push_val" +external push_arguments : arguments -> unit = "coq_push_arguments" +external push_vstack : vstack -> unit = "coq_push_vstack" + + +(* interpreteur *) +external interprete : tcode -> values -> vm_env -> int -> values = + "coq_interprete_ml" + + + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i)) + +(* Apply a value to arguments contained in [vargs] *) +let apply_arguments vf vargs = + let n = nargs vargs in + if Int.equal n 0 then vf + else + begin + push_ra stop; + push_arguments vargs; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + +(* Apply value [vf] to an array of argument values [varray] *) +let apply_varray vf varray = + let n = Array.length varray in + if Int.equal n 0 then vf + else + begin + push_ra stop; + push_vstack varray; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + (*************************************************) (* Destructors ***********************************) (*************************************************) +let uni_lvl_val (v : values) : Univ.universe_level = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + let rec whd_accu a stk = let stk = if Int.equal (Obj.size a) 2 then stk else Zapp (Obj.obj a) :: stk in let at = Obj.field a 1 in match Obj.tag at with + | i when Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end | i when i <= max_atom_tag -> Vatom_stk(Obj.magic at, stk) | i when Int.equal i proj_tag -> @@ -230,77 +310,6 @@ let whd_val : values -> whd = else Vconstr_block(Obj.obj o) -let uni_lvl_val : values -> Univ.universe_level = - fun v -> - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - Errors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) - -(************************************************) -(* Abstract machine *****************************) -(************************************************) - -(* gestion de la pile *) -external push_ra : tcode -> unit = "coq_push_ra" -external push_val : values -> unit = "coq_push_val" -external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" - - -(* interpreteur *) -external interprete : tcode -> values -> vm_env -> int -> values = - "coq_interprete_ml" - - - -(* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) - -(* Apply a value to arguments contained in [vargs] *) -let apply_arguments vf vargs = - let n = nargs vargs in - if Int.equal n 0 then vf - else - begin - push_ra stop; - push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - -(* Apply value [vf] to an array of argument values [varray] *) -let apply_varray vf varray = - let n = Array.length varray in - if Int.equal n 0 then vf - else - begin - push_ra stop; - push_vstack varray; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - (**********************************************) (* Constructors *******************************) (**********************************************) @@ -637,22 +646,6 @@ let apply_whd k whd = apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = - match stk with - | [] -> u - | [Zapp args] -> - assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; - let _,mp = Univ.LSet.fold (fun key (i,mp) -> - let u = uni_lvl_val (arg args i) in - (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) - (Univ.Universe.levels u) - (0,Univ.LMap.empty) in - let subst = Univ.make_subst mp in - Univ.subst_univs_universe subst u - | _ -> - Errors.anomaly Pp.(str "ill-formed universe") - - let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with diff --git a/kernel/vm.mli b/kernel/vm.mli index bc19786632..43a42eb9c4 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity" val whd_val : values -> whd val uni_lvl_val : values -> Univ.universe_level -val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b9c1a5a1c7..c4c85a62ed 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -155,7 +155,6 @@ and nf_whd env whd typ = construct_of_constr_const env n typ | Vconstr_block b -> let tag = btag b in - let x = tag in let (tag,ofs) = if tag = Cbytecodes.last_variant_tag then match whd_val (bfield b 0) with @@ -166,62 +165,54 @@ and nf_whd env whd typ = let args = nf_bargs env b ofs ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> - constr_type_of_idkey env idkey stk nf_stk -(*let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk *) + constr_type_of_idkey env idkey stk | Vatom_stk(Aind ((mi,i) as ind), stk) -> - if Environ.polymorphic_ind ind env then - let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size mib.mind_universes in - match stk with - | Zapp args :: stk' -> - assert (ulen <= nargs args) ; - let inst = - Array.init ulen (fun i -> Vm.uni_lvl_val (arg args i)) - in - let pind = (ind, Univ.Instance.of_array inst) in - nf_stk ~from:ulen env (mkIndU pind) (type_of_ind env pind) stk - | _ -> assert false - else - let pind = (ind, Univ.Instance.empty) in - nf_stk env (mkIndU pind) (type_of_ind env pind) stk - | Vatom_stk(Atype u, stk) -> - mkSort (Type (Vm.instantiate_universe u stk)) + let mib = Environ.lookup_mind mi env in + let nb_univs = + if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes + else 0 + in + let mk u = + let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) + in + nf_univ_args ~nb_univs mk env stk + | Vatom_stk(Atype u, stk) -> assert false | Vuniv_level lvl -> assert false -and constr_type_of_idkey env (idkey : Vars.id_key) stk cont = +and nf_univ_args ~nb_univs mk env stk = + let u = + if Int.equal nb_univs 0 then Univ.Instance.empty + else match stk with + | Zapp args :: _ -> + let inst = + Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i)) + in + Univ.Instance.of_array inst + | _ -> assert false + in + let (t,ty) = mk u in + nf_stk ~from:nb_univs env t ty stk + +and constr_type_of_idkey env (idkey : Vars.id_key) stk = match idkey with | ConstKey cst -> - if Environ.polymorphic_constant cst env then - let cbody = Environ.lookup_constant cst env in - match stk with - | Zapp vargs :: stk' -> - let uargs = Univ.UContext.size cbody.const_universes in - assert (Vm.nargs vargs >= uargs) ; - let uary = Array.init uargs (fun i -> Vm.uni_lvl_val (Vm.arg vargs i)) in - let ui = Univ.Instance.of_array uary in - let ucst = (cst, ui) in - let const_type = Typeops.type_of_constant_in env ucst in - if uargs < Vm.nargs vargs then - let t, args = nf_args env vargs ~from:uargs const_type in - cont env (mkApp (mkConstU ucst, args)) t stk' - else - cont env (mkConstU ucst) const_type stk' - | _ -> assert false - else - begin - let ucst = (cst, Univ.Instance.empty) in - let const_type = Typeops.type_of_constant_in env ucst in - cont env (mkConstU ucst) const_type stk - end - | VarKey id -> + let cbody = Environ.lookup_constant cst env in + let nb_univs = + if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes + else 0 + in + let mk u = + let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) + in + nf_univ_args ~nb_univs mk env stk + | VarKey id -> let (_,_,ty) = lookup_named id env in - cont env (mkVar id) ty stk + nf_stk env (mkVar id) ty stk | RelKey i -> let n = (nb_rel env - i) in let (_,_,ty) = lookup_rel n env in - cont env (mkRel n) (lift n ty) stk + nf_stk env (mkRel n) (lift n ty) stk and nf_stk ?from:(from=0) env c t stk = match stk with -- cgit v1.2.3 From f1dd27ae0e6082b111770fa74cba6abda30f3b89 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 12:51:51 +0100 Subject: Fix bug in native compiler with universe polymorphism. Universe instances for constructors were not always correct, for instance in: [cons _ list (nil _)] with a polymorphic [list] type, [nil] was receiving an empty instance. --- pretyping/nativenorm.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index dafe88d8db..de988aa2cd 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -53,8 +53,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib typ params = - let s = ind_subst mind mib Univ.Instance.empty (* FIXME *)in +let type_constructor mind mib u typ params = + let s = ind_subst mind mib u in let ctyp = substl s typ in let nparams = Array.length params in if Int.equal nparams 0 then ctyp @@ -68,13 +68,13 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let params = Array.sub allargs 0 nparams in try if const then - let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in + let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp else raise Not_found with Not_found -> let i = invert_tag const tag mip.mind_reloc_tbl in - let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in + let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in (mkApp(mkConstructU((ind,i),u), params), ctyp) @@ -90,12 +90,12 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -let build_branches_type env (mind,_ as _ind) mib mip params dep p = +let build_branches_type env (mind,_ as _ind) mib mip u params dep p = let rtbl = mip.mind_reloc_tbl in (* [build_one_branch i cty] construit le type de la ieme branche (commence a 0) et les lambda correspondant aux realargs *) let build_one_branch i cty = - let typi = type_constructor mind mib cty params in + let typi = type_constructor mind mib u cty params in let decl,indapp = Reductionops.splay_prod env Evd.empty typi in let decl_with_letin,_ = decompose_prod_assum typi in let ind,cargs = find_rectype_a env indapp in @@ -292,7 +292,7 @@ and nf_atom_type env atom = let pT = whd_betadeltaiota env pT in let dep, p = nf_predicate env ind mip params p pT in (* Calcul du type des branches *) - let btypes = build_branches_type env (fst ind) mib mip params dep p in + let btypes = build_branches_type env (fst ind) mib mip u params dep p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) ans bs in let mkbranch i v = -- cgit v1.2.3 From 110f7b41eca9c3e22fff0df67419b57d9c2ef612 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 16:56:41 +0100 Subject: Fix test suite after Matthieu's ed7af646f2e486b. --- test-suite/success/univnames.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 31d264f645..048b53d26c 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,6 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. -Universe g. +Monomorphic Universe g. Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'. \ No newline at end of file -- cgit v1.2.3 From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 10:03:17 +0100 Subject: lib_stack: API to reorder the libstack For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api. --- library/lib.ml | 3 +++ library/lib.mli | 1 + 2 files changed, 4 insertions(+) diff --git a/library/lib.ml b/library/lib.ml index cdc8889037..297441e6e2 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -198,6 +198,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index b67b2b873f..bb88317591 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- kernel/declarations.mli | 6 - kernel/declareops.ml | 18 +-- kernel/declareops.mli | 12 +- kernel/entries.mli | 25 +++- kernel/opaqueproof.ml | 5 +- kernel/safe_typing.ml | 103 +++++++++++--- kernel/safe_typing.mli | 41 +++++- kernel/term_typing.ml | 188 ++++++++++++++++++++++--- kernel/term_typing.mli | 33 ++++- library/declare.ml | 151 +++++++++----------- library/declare.mli | 10 +- library/global.mli | 5 +- library/heads.ml | 5 +- library/libobject.ml | 3 + plugins/derive/derive.ml | 4 +- plugins/funind/functional_principles_types.ml | 14 +- plugins/funind/functional_principles_types.mli | 10 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 4 +- pretyping/evd.ml | 26 +--- pretyping/evd.mli | 4 +- proofs/pfedit.ml | 10 +- proofs/pfedit.mli | 6 +- proofs/proof_global.ml | 9 +- proofs/proof_global.mli | 4 +- proofs/proofview.mli | 2 +- stm/lemmas.ml | 5 +- tactics/elimschemes.ml | 20 +-- tactics/eqschemes.ml | 17 +-- tactics/eqschemes.mli | 4 +- tactics/equality.ml | 2 +- tactics/tactics.ml | 6 +- toplevel/auto_ind_decl.ml | 23 ++- toplevel/classes.ml | 2 +- toplevel/command.ml | 8 +- toplevel/command.mli | 10 +- toplevel/discharge.ml | 4 +- toplevel/ind_tables.ml | 22 +-- toplevel/ind_tables.mli | 10 +- toplevel/indschemes.ml | 4 +- toplevel/obligations.ml | 12 +- toplevel/obligations.mli | 4 +- toplevel/record.ml | 6 +- 43 files changed, 547 insertions(+), 312 deletions(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7def963e73..dc5c17a75b 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -79,12 +79,6 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] - -type side_effect = - | SEsubproof of constant * constant_body * seff_env - | SEscheme of (inductive * constant * constant_body * seff_env) list * string - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c13..248504c1b1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +let string_of_side_effect { Entries.eff } = match eff with + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEscheme (cl,_) -> + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af975e..1b87009589 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d355..e058519e96 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -54,11 +54,11 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects -type const_entry_body = proof_output Future.computation +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation -type definition_entry = { - const_entry_body : const_entry_body; +type 'a definition_entry = { + const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) @@ -78,8 +78,8 @@ type projection_entry = { proj_entry_ind : mutual_inductive; proj_entry_arg : int } -type constant_entry = - | DefinitionEntry of definition_entry +type 'a constant_entry = + | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -96,3 +96,16 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_eff = + | SEsubproof of constant * Declarations.constant_body * seff_env + | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + +type side_effect = { + from_env : Declarations.structure_body Ephemeron.key; + eff : side_eff; +} + +type side_effects = side_effect list diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 9f4361f401..badb15b561 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f) let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with - | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") + | Indirect (_,_,i) -> + if not (Int.Map.mem i prfs) + then Errors.anomaly (Pp.str "Indirect in a different table") + else Errors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in let id = Int.Map.cardinal prfs in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ec245b0648..b71cd31b5c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -207,15 +207,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -let sideff_of_con env c = +type private_constant = Entries.side_effect +type private_constants = private_constant list + +type private_constant_role = Term_typing.side_effect_role = + | Subproof + | Schema of inductive * string + +let empty_private_constants = [] +let add_private x xs = x :: xs +let concat_private xs ys = xs @ ys +let mk_pure_proof = Term_typing.mk_pure_proof +let inline_private_constants_in_constr = Term_typing.handle_side_effects +let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects +let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) + +let constant_entry_of_private_constant = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.map (fun (_,kn,cb,eff_env) -> + kn, Term_typing.constant_entry_of_side_effect cb eff_env) l + +let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - SEsubproof (c, cbo, get_opaque_body env.env cbo) -let sideff_of_scheme kind env cl = - SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + +let private_con_of_scheme ~kind env cl = + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEscheme( + List.map (fun (i,c) -> + let cbo = Environ.lookup_constant c env.env in + i, c, cbo, get_opaque_body env.env cbo) cl, + kind) } + +let universes_of_private eff = + let open Declarations in + List.fold_left (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc in + if cb.const_polymorphic then acc + else (Univ.ContextSet.of_context cb.const_universes) :: acc) + acc l + | Entries.SEsubproof _ -> acc) + [] eff let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe -let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in - let cb = match decl with - | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe senv.env kn r in - if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb - in +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +let add_constant_aux no_section senv (kn, cb) = + let l = pi3 (Constant.repr3 kn) in let cb, otab = match cb.const_body with - | OpaqueDef lc when DirPath.is_empty dir -> + | OpaqueDef lc when no_section -> (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) let od, otab = @@ -471,7 +508,33 @@ let add_constant dir l decl senv = (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' | _ -> senv' in - kn, senv'' + senv'' + +let add_constant dir l decl senv = + let kn = make_con senv.modpath dir l in + let no_section = DirPath.is_empty dir in + let seff_to_export, decl = + match decl with + | ConstantEntry (true, ce) -> + let exports, ce = + Term_typing.validate_side_effects_for_export + senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce) + | _ -> [], decl + in + let senv = + List.fold_left (add_constant_aux no_section) senv + (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in + let senv = + let cb = + match decl with + | ConstantEntry (export_seff,ce) -> + Term_typing.translate_constant senv.revstruct senv.env kn ce + | GlobalRecipe r -> + let cb = Term_typing.translate_recipe senv.env kn r in + if no_section then Declareops.hcons_const_body cb else cb in + add_constant_aux no_section senv (kn, cb) in + (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index eac08eb834..2214cf8bb8 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -val sideff_of_con : safe_environment -> constant -> Declarations.side_effect -val sideff_of_scheme : - string -> safe_environment -> (inductive * constant) list -> - Declarations.side_effect +type private_constant +type private_constants + +type private_constant_role = + | Subproof + | Schema of inductive * string + +val side_effects_of_private_constants : + private_constants -> Entries.side_effects + +val empty_private_constants : private_constants +val add_private : private_constant -> private_constants -> private_constants +val concat_private : private_constants -> private_constants -> private_constants + +val private_con_of_con : safe_environment -> constant -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant + +val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output +val inline_private_constants_in_constr : + Environ.env -> Constr.constr -> private_constants -> Constr.constr +val inline_private_constants_in_definition_entry : + Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + +val universes_of_private : private_constants -> Univ.universe_context_set list val is_curmod_library : safe_environment -> bool @@ -63,16 +83,23 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + (* bool: export private constants *) + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +(** returns the main constant plus a list of auxiliary constants (empty + unless one requires the side effects to be exported) *) val add_constant : - DirPath.t -> Label.t -> global_declaration -> constant safe_transformer + DirPath.t -> Label.t -> global_declaration -> + (constant * exported_private_constant list) safe_transformer (** Adding an inductive type *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cab99077f0..d75bd73fb6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff +let mk_pure_proof c = (c, Univ.ContextSet.empty), [] + +let equal_eff e1 e2 = + let open Entries in + match e1, e2 with + | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> + Names.Constant.equal c1 c2 + | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> + CList.for_all2eq + (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) + cl1 cl2 + | _ -> false + +let rec uniq_seff = function + | [] -> [] + | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) +(* The list of side effects is in reverse order (most recent first). + * To keep the "tological" order between effects we have to uniqize from the + * tail *) +let uniq_seff l = List.rev (uniq_seff (List.rev l)) let handle_side_effects env body ctx side_eff = - let handle_sideff (t,ctx) se = + let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = let cbl = match se with | SEsubproof (c,cb,b) -> [c,cb,b] | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in @@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff = let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> Vars.subst_instance_constr u' b - | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in + | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in let fix_body (c,cb,b) (t,ctx) = match cb.const_body, b with | Def b, _ -> @@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff = let t = sub c 1 (Vars.lift 1 t) in mkApp (mkLambda (cname c, b_ty, t), [|b|]), Univ.ContextSet.union ctx - (Univ.ContextSet.of_context cb.const_universes) + (Univ.ContextSet.of_context cb.const_universes) else let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx | _ -> assert false in - List.fold_right fix_body cbl (t,ctx) + let t, ctx = List.fold_right fix_body cbl (t,ctx) in + t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - Declareops.fold_side_effects handle_sideff (body,ctx) - (Declareops.uniquize_side_effects side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + +let check_signatures curmb sl = + let is_direct_ancestor (sl, curmb) (mb, how_many) = + match curmb with + | None -> None, None + | Some curmb -> + try + let mb = Ephemeron.get mb in + match sl with + | None -> sl, None + | Some n -> + if List.length mb >= how_many && CList.skipn how_many mb == curmb + then Some (n + how_many), Some mb + else None, None + with Ephemeron.InvalidKey -> None, None in + let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in + sl + +let trust_seff sl b e = + let rec aux sl b e acc = + match sl, kind_of_term b with + | (None|Some 0), _ -> b, e, acc + | Some sl, LetIn (n,c,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc) + | Some sl, App(hd,arg) -> + begin match kind_of_term hd with + | Lambda (n,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc) + | _ -> assert false + end + | _ -> assert false + in + aux sl b e [] + +let rec unzip ctx j = + match ctx with + | [] -> j + | `Let (n,c,ty) :: ctx -> + unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) } + | `Cut (n,ty,arg) :: ctx -> + unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} @@ -105,7 +167,7 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration env kn dcl = +let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -124,9 +186,14 @@ let infer_declaration env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> - let body,ctx = handle_side_effects env body ctx side_eff in + let body, ctx, signatures = + handle_side_effects env body ctx side_eff in + let trusted_signatures = check_signatures trust signatures in let env' = push_context_set ctx env in - let j = infer env' body in + let j = + let body, env', zip_ctx = trust_seff trusted_signatures body env' in + let j = infer env' body in + unzip zip_ctx j in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,7 +210,7 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx = handle_side_effects env body + let body, ctx, _ = handle_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in @@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant mb env kn ce = + build_constant_declaration kn env + (infer_declaration ~trust:mb env (Some kn) ce) + +let constant_entry_of_side_effect cb u = + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, []); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = + (match cb.const_type with RegularArity t -> Some t | _ -> None); + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = cb.const_universes; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } +;; + +let turn_direct (kn,cb,u,r as orig) = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b,c) -> + let pt = Future.from_val (b,c) in + kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r + | _ -> orig +;; + +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +let validate_side_effects_for_export mb env ce = + match ce with + | ParameterEntry _ | ProjectionEntry _ -> [], ce + | DefinitionEntry c -> + let { const_entry_body = body } = c in + let _, eff = Future.force body in + let ce = DefinitionEntry { c with + const_entry_body = Future.chain ~greedy:true ~pure:true body + (fun (b_ctx, _) -> b_ctx, []) } in + let not_exists (c,_,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = match se with + | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] + | SEscheme (cl,k) -> + List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in + let cbl = List.filter not_exists cbl in + if cbl = [] then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let trusted = check_signatures mb signatures in + let push_seff env = function + | kn, cb, `Nothing, _ -> + Environ.add_constant kn cb env + | kn, cb, `Opaque(_, ctx), _ -> + let env = Environ.add_constant kn cb env in + Environ.push_context_set + ~strict:(not cb.const_polymorphic) ctx env in + let rec translate_seff sl seff acc env = + match sl, seff with + | _, [] -> List.rev acc, ce + | (None | Some 0), cbs :: rest -> + let env, cbs = + List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + let ce = constant_entry_of_side_effect ocb u in + let cb = translate_constant mb env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (env,[]) cbs in + translate_seff sl rest (cbs @ acc) env + | Some sl, cbs :: rest -> + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map (fun (kn,cb,u,r) -> + kn, cb, constant_entry_of_side_effect cb u, r) cbs in + translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env +;; let translate_local_assum env t = let j = infer env t in @@ -305,9 +457,9 @@ let translate_local_assum env t = let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with @@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx' = handle_side_effects env body ctx side_eff in - (body, ctx'), Declareops.no_seff); + let body, ctx',_ = handle_side_effects env body ctx side_eff in + (body, ctx'), []); } let handle_side_effects env body side_eff = - fst (handle_side_effects env body Univ.ContextSet.empty side_eff) + pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8d92bcc68f..509160ccc7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,23 +12,42 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> proof_output +val mk_pure_proof : constr -> side_effects proof_output -val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +val handle_side_effects : env -> constr -> side_effects -> constr (** Returns the term where side effects have been turned into let-ins or beta redexes. *) -val handle_entry_side_effects : env -> definition_entry -> definition_entry +val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry (** Same as {!handle_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : env -> constant -> constant_entry -> constant_body +val uniq_seff : side_effects -> side_effects + +val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body + +(* Checks weather the side effects in constant_entry can be trusted. + * Returns the list of effects to be exported. + * Note: It forces the Future.computation. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +val validate_side_effects_for_export : + structure_body -> env -> side_effects constant_entry -> + exported_side_effect list * side_effects constant_entry + +val constant_entry_of_side_effect : + constant_body -> seff_env -> side_effects constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> - constant_entry -> Cooking.result +val infer_declaration : trust:structure_body -> env -> constant option -> + side_effects constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body diff --git a/library/declare.ml b/library/declare.ml index 0004f45a29..63e5a72245 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -35,7 +35,7 @@ type internal_flag = (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -93,9 +93,13 @@ type constant_obj = { cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; + mutable cst_exported : Safe_typing.exported_private_constant list; + (* mutable: to avoid change the libobject API, since cache_function + * does not return an updated object *) + mutable cst_was_seff : bool } -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -131,8 +135,17 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - let () = check_exists sp in - let kn' = Global.add_constant dir id obj.cst_decl in + let kn' = + if obj.cst_was_seff then begin + obj.cst_was_seff <- false; + if Global.exists_objlabel (Label.of_id (basename sp)) + then constant_of_kn kn + else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + end else + let () = check_exists sp in + let kn', exported = Global.add_constant dir id obj.cst_decl in + obj.cst_exported <- exported; + kn' in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in @@ -156,20 +169,23 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) +let dummy_constant_entry = + ConstantEntry + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; + cst_exported = []; + cst_was_seff = cst.cst_was_seff; } let classify_constant cst = Substitute (dummy_constant cst) -let inConstant : constant_obj -> obj = - declare_object { (default_object "CONSTANT") with +let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -177,16 +193,40 @@ let inConstant : constant_obj -> obj = subst_function = ident_subst_function; discharge_function = discharge_constant } +let declare_scheme = ref (fun _ _ -> assert false) +let set_declare_scheme f = declare_scheme := f + let declare_constant_common id cst = - let (sp,kn) = add_leaf id (inConstant cst) in + let update_tables c = +(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) in + let o = inConstant cst in + let _, kn as oname = add_leaf id o in + List.iter (fun (c,ce,role) -> + (* handling of private_constants just exported *) + let o = inConstant { + cst_decl = ConstantEntry (false, ce); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_exported = []; + cst_was_seff = true; } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) + (outConstant o).cst_exported; + pull_to_head oname; let c = Global.constant_of_delta_kn kn in - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c); + update_tables c; c let definition_entry ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -196,90 +236,25 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f -let declare_sideff env fix_exn se = - let cbl, scheme = match se with - | SEsubproof (c, cb, pt) -> [c, cb, pt], None - | SEscheme (cbl, k) -> - List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in - let id_of c = Names.Label.to_id (Names.Constant.label c) in - let pt_opaque_of cb pt = - match cb, pt with - | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false - | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true - | _ -> assert false - in - let ty_of cb = - match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t - | Declarations.TemplateArity _ -> None in - let cst_of cb pt = - let pt, opaque = pt_opaque_of cb pt in - let univs, subst = - if cb.const_polymorphic then - let univs = Univ.instantiate_univ_context cb.const_universes in - univs, Vars.subst_instance_constr (Univ.UContext.instance univs) - else cb.const_universes, fun x -> x - in - let pt = (subst (fst pt), snd pt) in - let ty = Option.map subst (ty_of cb) in - { cst_decl = ConstantEntry (DefinitionEntry { - const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); - const_entry_secctx = Some cb.Declarations.const_hyps; - const_entry_type = ty; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = univs; - }); - cst_hyps = [] ; - cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; - cst_locl = true; - } in - let exists c = - try ignore(Environ.lookup_constant c env); true - with Not_found -> false in - let knl = - CList.map_filter (fun (c,cb,pt) -> - if exists c then None - else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in - match scheme with - | None -> () - | Some (inds_consts,kind) -> - !declare_scheme kind (Array.of_list - (List.map (fun (c,kn) -> - CList.find_map (fun (x,c',_,_) -> - if Constant.equal c c' then Some (x,kn) else None) inds_consts) - knl)) - let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let cd = (* We deal with side effects *) + let export = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry de -> - if export_seff || - not de.const_entry_opaque || - de.const_entry_polymorphic then + | DefinitionEntry de when + export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic -> let bo = de.const_entry_body in let _, seff = Future.force bo in - if Declareops.side_effects_is_empty seff then cd - else begin - let seff = Declareops.uniquize_side_effects seff in - Declareops.iter_side_effects - (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; - Entries.DefinitionEntry { de with - const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> - pt, Declareops.no_seff) } - end - else cd - | _ -> cd + Safe_typing.empty_private_constants <> seff + | _ -> false in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; + cst_exported = []; + cst_was_seff = false; } in let kn = declare_constant_common id cst in kn diff --git a/library/declare.mli b/library/declare.mli index 7ed451c3f1..fdbd235614 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -22,7 +22,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -49,8 +49,8 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> - constr -> definition_entry + ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant @@ -60,7 +60,7 @@ val declare_definition : ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant -(** Since transparent constant's side effects are globally declared, we +(** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : (string -> (inductive * constant) array -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index ac231f7fd8..03469bea41 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive diff --git a/library/heads.ml b/library/heads.ml index 5c153b0676..73d2aa053f 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -68,7 +68,10 @@ let kind_of_head env t = | None -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) - with Not_found -> assert false) + with Not_found -> + Errors.anomaly + Pp.(str "constant not found in kind_of_head: " ++ + str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/libobject.ml b/library/libobject.ml index 2ee57baf9c..85c830ea2c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -108,6 +108,9 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index c232ae31ad..d6c29283f1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = +let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) + : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9e27ddf2e9..c439323243 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (Entries.DefinitionEntry ce, + (DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -447,7 +447,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = +let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = - (Future.from_val (Term_typing.mk_pure_proof princ_body)); - Entries.const_entry_type = Some scheme_type + const_entry_body = + (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + const_entry_type = Some scheme_type } ) other_fun_princ_types @@ -620,7 +620,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index f6e5578d2e..bc082f0730 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* sorts array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Entries.definition_entry list + (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36da..aa47e26192 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 10daf6e848..23f1da1ba7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> unit Lemmas.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and @@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind) + (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1107c2951e..0593bbca8a 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -579,7 +579,7 @@ type evar_map = { (** Metas *) metas : clbinding Metamap.t; (** Interactive proofs *) - effects : Declareops.side_effects; + effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -768,7 +768,7 @@ let empty = { conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; - effects = Declareops.no_seff; + effects = Safe_typing.empty_private_constants; evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -1041,22 +1041,8 @@ let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) let emit_universe_side_effects eff u = - Declareops.fold_side_effects - (fun acc eff -> - match eff with - | Declarations.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx - in if cb.Declarations.const_polymorphic then acc - else - merge_uctx true univ_rigid acc - (Univ.ContextSet.of_context cb.Declarations.const_universes)) - acc l - | Declarations.SEsubproof _ -> acc) - u eff + let uctxs = Safe_typing.universes_of_private eff in + List.fold_left (merge_uctx true univ_rigid) u uctxs let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) @@ -1399,11 +1385,11 @@ let e_eq_constr_univs evdref t u = (* Side effects *) let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; + { evd with effects = Safe_typing.concat_private eff evd.effects; universes = emit_universe_side_effects eff evd.universes } let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } + { evd with effects = Safe_typing.empty_private_constants; } let eval_side_effects evd = evd.effects diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 52d7d42120..9379b50b52 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -261,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Declareops.side_effects +val eval_side_effects : evar_map -> Safe_typing.private_constants (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 00ef8ecafd..02dbd1fdcb 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -150,10 +150,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in + let ce = + if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce + else { ce with + const_entry_body = Future.chain ~pure:true ce.const_entry_body + (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in let (cb, ctx), se = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Declareops.side_effects_is_empty se); + assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = @@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) - let ans = Term_typing.handle_side_effects env ans neff in + let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma (**********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index b1fba132d9..fc521ea432 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -69,11 +69,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) val cook_proof : unit -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -152,7 +152,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a0ead42ef3..809ed41c7e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -67,7 +67,7 @@ type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -315,13 +315,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let open Universes in let body = c in let typ = - if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then + if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then + if keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in let ctx = Evd.evar_universe_context_set initunivs universes in (* For vi2vo compilation proofs are computed now but we need to @@ -365,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, fun pr_ending -> Ephemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fcb706cc8d..f8615e8499 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -58,7 +58,7 @@ type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -97,7 +97,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f0..927df33a0c 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -336,7 +336,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Declareops.side_effects -> unit tactic +val tclEFFECTS : Safe_typing.private_constants -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c49ddfd8ec..6c18326882 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function try ignore(Environ.lookup_constant c e); true with Not_found -> false in if exists c e then e else Environ.add_constant c cb e in - let env = Declareops.fold_side_effects (fun env -> function + let env = List.fold_left (fun env { eff } -> + match eff with | SEsubproof (c, cb,_) -> add c cb env | SEscheme (l,_) -> List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Declareops.uniquize_side_effects eff) in + env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard Loc.ghost env possible_indexes fixdecls in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e6a8cbe3ad..8a6d93cf7c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in - (c, Evd.evar_universe_context sigma), Declareops.no_seff + (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0a..b2603315d5 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -193,7 +193,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Declareops.no_seff) + (c, ctx), Safe_typing.empty_private_constants) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff + in (c, Evd.evar_universe_context_of ctx), + Safe_typing.concat_private eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -704,7 +705,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) (* End of rewriting schemes *) @@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 6bb84808a9..3fe3307308 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val build_r2l_forward_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index bc711b81ef..674c85af79 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = assert false in let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Declareops.no_seff + sigma, elim, Safe_typing.empty_private_constants else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1437b24625..0b920066fd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac = (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in - let open Declareops in - let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 8ac273c84f..7a89b9f54e 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -179,12 +179,12 @@ let build_beq_scheme mode kn = let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with - | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff + | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants else begin try let eq, eff = @@ -193,9 +193,8 @@ let build_beq_scheme mode kn = let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - Declareops.union_side_effects - (Declareops.flatten_side_effects (List.rev effs)) - eff in + List.fold_left Safe_typing.concat_private eff (List.rev effs) + in let args = Array.append (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in @@ -238,7 +237,7 @@ let build_beq_scheme mode kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (Lazy.force ff) in @@ -256,7 +255,7 @@ let build_beq_scheme mode kn = (nb_cstr_args+ndx+1) cc in - eff := Declareops.union_side_effects eff' !eff; + eff := Safe_typing.concat_private eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -288,7 +287,7 @@ let build_beq_scheme mode kn = let names = Array.make nb_ind Anonymous and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); @@ -296,7 +295,7 @@ let build_beq_scheme mode kn = (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Declareops.union_side_effects eff' !eff + eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in @@ -875,7 +874,7 @@ let compute_dec_tact ind lnamesparrec nparrec = Not_found -> Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in + let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -942,7 +941,7 @@ let make_eq_decidability mode mind = (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Declareops.no_seff + ([|ans|], ctx), Safe_typing.empty_private_constants let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 805a29e396..e750f0ca26 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro Evarutil.check_evars env Evd.empty !evars termtype; let ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (Entries.ParameterEntry + (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id end diff --git a/toplevel/command.ml b/toplevel/command.ml index d75efeca1e..433ef4dccd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k imps in - Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r + Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r let _ = Obligations.declare_definition_ref := declare_definition @@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Declareops.side_effects_is_empty sideff); + assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t @@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); @@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let vars = Universes.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in diff --git a/toplevel/command.mli b/toplevel/command.mli index 94b4af9dd9..a031677b47 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -26,17 +26,17 @@ val do_constraint : polymorphic -> (** {6 Hooks for Pcoq} *) -val set_declare_definition_hook : (definition_entry -> unit) -> unit -val get_declare_definition_hook : unit -> (definition_entry -> unit) +val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit +val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit) (** {6 Definitions/Let} *) val interp_definition : lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> - definition_entry -> Impargs.manual_implicits -> + Safe_typing.private_constants definition_entry -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> @@ -170,4 +170,4 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 7d5d61fb8b..b6da21e5ae 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -20,8 +20,8 @@ open Cooking (* Discharging mutual inductive *) let detype_param = function - | (Name id,None,p) -> id, Entries.LocalAssum p - | (Name id,Some p,_) -> id, Entries.LocalDef p + | (Name id,None,p) -> id, LocalAssum p + | (Name id,Some p,_) -> id, LocalDef p | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 218c47b28d..dde801a7fb 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -29,9 +29,9 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants type 'a scheme_kind = string @@ -124,7 +124,9 @@ let define internal id c p univs = let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in let entry = { - const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); + const_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), + Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = None; const_entry_polymorphic = p; @@ -148,8 +150,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; - const, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff + const, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -168,8 +170,8 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -181,10 +183,10 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + s, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind, s]) - Declareops.no_seff + Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd946..abd951c313 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -20,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants (** Main functions to register a scheme builder *) @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Declareops.side_effects + Id.t option -> inductive -> constant * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ae8ee7670a..0b021254e2 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -469,7 +469,7 @@ let do_combined_scheme name schemes = schemes in let body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 665926922f..e488f84f8a 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -541,7 +541,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff) +let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) let declare_mutual_definition l = let len = List.length l in @@ -619,7 +619,7 @@ let declare_obligation prg obl body ty uctx = shrink_body body else [], body, [||] in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); + { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; @@ -796,12 +796,12 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_entry_side_effects env entry in - let body, eff = Future.force entry.Entries.const_entry_body in - assert(Declareops.side_effects_is_empty eff); + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, eff = Future.force entry.const_entry_body in + assert(Safe_typing.empty_private_constants = eff); let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' + (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 40f124ca36..61a8ee520f 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -17,11 +17,11 @@ open Decl_kinds (** Forward declaration. *) val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : (Id.t -> definition_kind -> - Entries.definition_entry -> Impargs.manual_implicits + Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits -> global_reference Lemmas.declaration_hook -> global_reference) ref val check_evars : env -> evar_map -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 60fe76bb82..b1be4c92a6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -160,8 +160,8 @@ let degenerate_decl (na,b,t) = | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) + | None -> (id, LocalAssum t) + | Some b -> (id, LocalDef b) type record_error = | MissingProj of Id.t * Id.t list @@ -297,7 +297,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field try let entry = { const_entry_body = - Future.from_val (Term_typing.mk_pure_proof proj); + Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; -- cgit v1.2.3 From 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 11:16:47 -0400 Subject: Printing of @{} instances for polymorphic references in Print and About. --- printing/prettyp.ml | 14 +++++++++++--- printing/printer.ml | 4 ++++ printing/printer.mli | 1 + printing/printmod.ml | 6 +++++- 4 files changed, 21 insertions(+), 4 deletions(-) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b8c5fd4cfc..7e625af0de 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,11 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ + let inst = + if Global.is_polymorphic ref then Printer.pr_universe_instance univs + else mt () + in + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ Printer.pr_universe_ctx univs) (********************************) @@ -473,6 +477,10 @@ let print_typed_body (val_0,typ) = let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t +let print_instance cb = + if cb.const_polymorphic then pr_universe_instance cb.const_universes + else mt() + let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in @@ -485,11 +493,11 @@ let print_constant with_values sep sp = match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx univs | _ -> - print_basename sp ++ str sep ++ cut () ++ + print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ Printer.pr_universe_ctx univs) diff --git a/printing/printer.ml b/printing/printer.ml index 18e4902255..f4852b1089 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -825,3 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () +let pr_universe_instance ctx = + let inst = Univ.UContext.instance ctx in + str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + diff --git a/printing/printer.mli b/printing/printer.mli index 5f56adbe6f..25a4aa166b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,6 +84,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds +val pr_universe_instance : Univ.universe_context -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 53d0508c7f..8031de27d4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -94,8 +94,12 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in + let inst = + if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + else mt () + in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- library/universes.ml | 16 +++++ library/universes.mli | 10 ++- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/merge.ml | 4 +- plugins/funind/recdef.ml | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- pretyping/evd.ml | 30 ++++++--- pretyping/evd.mli | 6 +- printing/prettyp.ml | 38 +++++++----- printing/printer.ml | 8 +-- printing/printer.mli | 4 +- printing/printmod.ml | 38 +++++++----- tactics/leminv.ml | 3 +- tactics/rewrite.ml | 4 +- toplevel/class.ml | 2 +- toplevel/classes.ml | 4 +- toplevel/command.ml | 89 +++++++++++++++------------ toplevel/command.mli | 13 ++-- toplevel/indschemes.ml | 2 +- toplevel/record.ml | 11 ++-- toplevel/vernacentries.ml | 4 +- 21 files changed, 180 insertions(+), 112 deletions(-) diff --git a/library/universes.ml b/library/universes.ml index 30d38eb2a4..6cccb10efb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -12,7 +12,9 @@ open Names open Term open Environ open Univ +open Globnames +(** Global universe names *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -27,6 +29,20 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + (* To disallow minimization to Set *) let set_minimization = ref true diff --git a/library/universes.mli b/library/universes.mli index 4ff21d45c9..45672ef460 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -14,9 +14,10 @@ open Univ val set_minimization : bool ref val is_set_minimization : unit -> bool - + (** Universes *) +(** Global universe name <-> level mapping *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t @@ -25,6 +26,13 @@ val set_global_universe_names : universe_names -> unit val pr_with_global_universes : Level.t -> Pp.std_ppcmds +(** Local universe name <-> level mapping *) + +type universe_binders = (Id.t * Univ.universe_level) list + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +val universe_binders_of_global : Globnames.global_reference -> universe_binders + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c439323243..c47602bda0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 60c58730a3..e3455e7702 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie impls) + ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca0b9c5feb..5d41ec7237 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1509,7 +1509,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 1c4ba88237..c7185ff25e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd + Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0593bbca8a..36d9c25fdd 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -356,6 +356,16 @@ let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_loca let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } let evar_universe_context_subst ctx = ctx.uctx_univ_variables +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let evar_universe_context_of_binders b = + let ctx = empty_evar_universe_context in + let names = + List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) + ctx.uctx_names b + in { ctx with uctx_names = names } + let instantiate_variable l b v = v := Univ.LMap.add l (Some b) !v @@ -965,19 +975,19 @@ let pr_uctx_level uctx = let universe_context ?names evd = match names with - | None -> Univ.ContextSet.to_context evd.universes.uctx_local + | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local | Some pl -> let levels = Univ.ContextSet.levels evd.universes.uctx_local in - let newinst, left = + let newinst, map, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun (loc,id) (newinst, map, acc) -> let l = try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names) with Not_found -> user_err_loc (loc, "universe_context", str"Universe " ++ pr_id id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) - pl ([], levels) + in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) + pl ([], [], levels) in if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in @@ -985,8 +995,11 @@ let universe_context ?names evd = (str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level evd.universes) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") - else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), - Univ.ContextSet.constraints evd.universes.uctx_local) + else + let inst = Univ.Instance.of_array (Array.of_list newinst) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints evd.universes.uctx_local) + in map, ctx let restrict_universe_context evd vars = let uctx = evd.universes in @@ -1044,9 +1057,6 @@ let emit_universe_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in List.fold_left (merge_uctx true univ_rigid) u uctxs -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) - let uctx_new_univ_variable rigid name predicative ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9379b50b52..3c16b27ad9 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -487,6 +487,9 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst +val evar_universe_context_of_binders : + Universes.universe_binders -> evar_universe_context + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map (** Raises Not_found if not a name for a universe in this map. *) @@ -534,7 +537,8 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> + (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> Univ.universes diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7e625af0de..84649e6ebf 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,12 +73,15 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let env = Global.env () in + let bl = Universes.universe_binders_of_global ref in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance univs + if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ - Printer.pr_universe_ctx univs) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + Printer.pr_universe_ctx sigma univs) (********************************) (** Printing implicit arguments *) @@ -467,18 +470,19 @@ let gallina_print_section_variable id = print_named_decl id ++ with_line_skip (print_name_infos (VarRef id)) -let print_body = function - | Some c -> pr_lconstr c +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c | None -> (str"") -let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t -let print_instance cb = - if cb.const_polymorphic then pr_universe_instance cb.const_universes +let print_instance sigma cb = + if cb.const_polymorphic then + pr_universe_instance sigma cb.const_universes else mt() let print_constant with_values sep sp = @@ -489,17 +493,23 @@ let print_constant with_values sep sp = let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in + let ctx = + Evd.evar_universe_context_of_binders + (Universes.universe_binders_of_global (ConstRef sp)) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx univs + Printer.pr_universe_ctx sigma univs | _ -> - print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx univs) + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ diff --git a/printing/printer.ml b/printing/printer.ml index f4852b1089..202b4f2bc7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -208,10 +208,10 @@ let safe_pr_constr t = let (sigma, env) = get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx c = +let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context Universes.pr_with_global_universes c)) c + (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c else mt() @@ -825,7 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance ctx = +let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" diff --git a/printing/printer.mli b/printing/printer.mli index 25a4aa166b..0a44e4f103 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,8 +84,8 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_universe_instance : Univ.universe_context -> std_ppcmds -val pr_universe_ctx : Univ.universe_context -> std_ppcmds +val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 8031de27d4..1d275c1aa6 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -72,10 +72,10 @@ let print_params env sigma params = if List.is_empty params then mt () else Printer.pr_rel_context env sigma params ++ brk(1,2) -let print_constructors envpar names types = +let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -83,7 +83,7 @@ let print_constructors envpar names types = let build_ind_type env mip = Inductive.type_of_inductive env mip -let print_one_inductive env mib ((_,i) as ind) = +let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in @@ -95,13 +95,14 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + if mib.mind_polymorphic then + Printer.pr_universe_instance sigma mib.mind_universes else mt () in hov 0 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ - brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -113,11 +114,13 @@ let print_mutual_inductive env mind mib = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in + let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env mib) inds ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -146,6 +149,8 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = let open Decl_kinds in match mib.mind_finite with @@ -157,16 +162,16 @@ let print_record env mind mib = hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -267,6 +272,7 @@ let print_body is_impl env mp (l,body) = if cb.const_polymorphic then Univ.UContext.instance cb.const_universes else Univ.Instance.empty in + let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -275,17 +281,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) + hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty + Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 42d22bc3c4..8ca622171f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -229,7 +229,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in + let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) + ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 0811708695..e8a7c0f600 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1806,9 +1806,9 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in + let pl, ctx = Evd.universe_context sigma in let cst = - Declare.definition_entry ~types:typ ~poly - ~univs:(Evd.universe_context sigma) term + Declare.definition_entry ~types:typ ~poly ~univs:ctx term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) diff --git a/toplevel/class.ml b/toplevel/class.ml index f925a2d07e..da6624032f 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -225,7 +225,7 @@ let build_id_coercion idf_opt source poly = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(Evd.universe_context sigma) + (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index e750f0ca26..c354c7d32f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -185,7 +185,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro nf t in Evarutil.check_evars env Evd.empty !evars termtype; - let ctx = Evd.universe_context !evars in + let pl, ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) @@ -381,7 +381,7 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, !uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) in let () = uctx := Univ.ContextSet.empty in diff --git a/toplevel/command.ml b/toplevel/command.ml index 433ef4dccd..73fd3d1a4a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -83,7 +83,7 @@ let interp_definition pl bl p red_option c ctypopt = let evdref = ref (Evd.from_ctx ctx) in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in let nb_args = List.length ctx in - let imps,ce = + let imps,pl,ce = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -94,8 +94,8 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Universes.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl evd in - imps1@(Impargs.lift_implicits nb_args imps2), + let pl, uctx = Evd.universe_context ?names:pl evd in + imps1@(Impargs.lift_implicits nb_args imps2), pl, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -120,14 +120,14 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl ctx in - imps1@(Impargs.lift_implicits nb_args impsty), + let pl, uctx = Evd.universe_context ?names:pl ctx in + imps1@(Impargs.lift_implicits nb_args impsty), pl, definition_entry ~types:typ ~poly:p ~univs:uctx body in - red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, imps + red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps -let check_definition (ce, evd, imps) = +let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce @@ -140,11 +140,12 @@ let get_locality id = function | Local -> true | Global -> false -let declare_global_definition ident ce local k imps = +let declare_global_definition ident ce local k pl imps = let local = get_locality ident local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in let () = definition_message ident in gr @@ -152,7 +153,7 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ident (local, p, k) ce imps hook = +let declare_definition ident (local, p, k) ce pl imps hook = let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -168,13 +169,14 @@ let declare_definition ident (local, p, k) ce imps hook = in gr | Discharge | Local | Global -> - declare_global_definition ident ce local k imps in + declare_global_definition ident ce local k pl imps in Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r -let _ = Obligations.declare_definition_ref := declare_definition +let _ = Obligations.declare_definition_ref := + (fun i k c imps hook -> declare_definition i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = - let (ce, evd, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in + let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in @@ -192,13 +194,14 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ident k ce imps + ignore(declare_definition ident k ce pl imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = +match local with | Discharge when Lib.sections_are_opened () -> let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -225,6 +228,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr local p in @@ -241,11 +245,11 @@ let interp_assumption evdref env impls bl c = let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) -let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = +let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = List.fold_left (fun (refs,status,ctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in + declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in (ref',u')::refs, status' && status, Univ.ContextSet.empty) ([],true,ctx) idl in @@ -277,7 +281,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 (nf_evar evd)) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs @@ -293,9 +297,9 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Universes.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in st let do_assumptions kind nl l = match l with @@ -314,7 +318,8 @@ let do_assumptions kind nl l = match l with | None -> id | Some _ -> let loc = fst id in - let msg = Pp.str "Assumptions with bound universes can only be defined once at a time." in + let msg = + Pp.str "Assumptions with bound universes can only be defined one at a time." in user_err_loc (loc, "", msg) in (coe, (List.map map idl, c)) @@ -587,7 +592,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = map_rel_context nf ctx_params in let evd = !evdref in - let uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.universe_context ?names:pl evd in List.iter (check_evars env_params Evd.empty evd) arities; iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -616,7 +621,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = uctx }, - impls + pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -665,7 +670,7 @@ let is_recursive mie = List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc | _ -> false -let declare_mutual_inductive_with_eliminations mie impls = +let declare_mutual_inductive_with_eliminations mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) begin match mie.mind_entry_finite with @@ -680,12 +685,15 @@ let declare_mutual_inductive_with_eliminations mie impls = let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - maybe_declare_manual_implicits false (IndRef ind) indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) - constrimpls) + let ind = (mind,i) in + let gr = IndRef ind in + maybe_declare_manual_implicits false gr indimpls; + Universes.register_universe_binders gr pl; + List.iteri + (fun j impls -> + maybe_declare_manual_implicits false + (ConstructRef (ind, succ j)) impls) + constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in if_verbose msg_info (minductive_message warn_prim names); @@ -700,14 +708,14 @@ type one_inductive_impls = let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie impls); + ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes - + (* 3c| Fixpoints and co-fixpoints *) (* An (unoptimized) function that maps preorders to partial orders... @@ -811,11 +819,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in - declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) + declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) -let _ = Obligations.declare_fix_ref := declare_fix +let _ = Obligations.declare_fix_ref := + (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1003,7 +1012,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let hook l gr = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in - let univs = Evd.universe_context !evdref in + let pl, univs = Evd.universe_context !evdref in (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in (** FIXME: include locality *) @@ -1140,8 +1149,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) + let pl, ctx = Evd.universe_context ?names:pl evd in + ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1173,8 +1182,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) + let pl, ctx = Evd.universe_context ?names:pl evd in + ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames diff --git a/toplevel/command.mli b/toplevel/command.mli index a031677b47..8e2d9c6fc3 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -33,10 +33,11 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit val interp_definition : lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * + Universes.universe_binders * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> - Safe_typing.private_constants definition_entry -> Impargs.manual_implicits -> + Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> @@ -53,7 +54,7 @@ val do_definition : Id.t -> definition_kind -> lident list option -> nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> - Impargs.manual_implicits -> + Universes.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool @@ -92,13 +93,13 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> - mutual_inductive_entry * one_inductive_impls list + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its associated schemes *) val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> one_inductive_impls list -> + mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> mutual_inductive (** Entry points for the vernacular commands Inductive and CoInductive *) @@ -169,5 +170,5 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 0b021254e2..f16e6e3f3f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -129,7 +129,7 @@ let define id internal ctx c t = const_entry_secctx = None; const_entry_type = t; const_entry_polymorphic = true; - const_entry_universes = Evd.universe_context ctx; + const_entry_universes = snd (Evd.universe_context ctx); const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/toplevel/record.ml b/toplevel/record.ml index b1be4c92a6..dc2c9264b8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -153,7 +153,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); - Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs + Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs let degenerate_decl (na,b,t) = let id = match na with @@ -376,7 +376,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx } in - let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in @@ -532,11 +532,11 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) - let ctx, arity, template, implpars, params, implfs, fields = + let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + let gr = match kind with | Class def -> let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in @@ -549,3 +549,6 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind + in + Universes.register_universe_binders gr pl; + gr diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2879947a91..31bfc004a8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1527,7 +1527,7 @@ let vernac_check_may_eval redexp glopt rc = let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = @@ -1542,7 +1542,7 @@ let vernac_check_may_eval redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx uctx) + Printer.pr_universe_ctx sigma uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in -- cgit v1.2.3 From 78378ba9a79b18a658828d7a110414ad18b9a732 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Oct 2015 07:39:36 +0100 Subject: Accept option -compat 8.5. (Fix bug #4393) --- toplevel/coqinit.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 19d4363ab8..eca344b27c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -130,6 +130,7 @@ let init_ocaml_path () = [ "grammar" ]; [ "ide" ] ] let get_compat_version = function + | "8.5" -> Flags.Current | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 -- cgit v1.2.3