From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- checker/check.ml | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index c835cec824..2bc470aead 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -271,20 +271,10 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) +(*s Low-level interning of libraries from files *) -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) - -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) @@ -312,7 +302,7 @@ let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in + let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in -- cgit v1.2.3 From c1630c9dcdf91dc965b3c375d68e3338fb737531 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 13:32:47 +0200 Subject: Univs: update checker --- checker/cic.mli | 2 +- checker/environ.ml | 19 +++++++++++++------ checker/environ.mli | 2 ++ checker/mod_checking.ml | 2 +- checker/modops.ml | 7 ++++--- checker/safe_typing.ml | 4 ++-- checker/univ.ml | 47 +++++++++++++++++++++++++++++++++++++++++++---- checker/univ.mli | 15 ++++++++++++++- checker/values.ml | 6 +++--- 9 files changed, 83 insertions(+), 21 deletions(-) (limited to 'checker') diff --git a/checker/cic.mli b/checker/cic.mli index 881d3ca797..bd75111a2c 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -380,7 +380,7 @@ and module_body = (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; mod_retroknowledge : action list } diff --git a/checker/environ.ml b/checker/environ.ml index 6dbc44d6b8..f8f5c29b79 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -84,13 +84,20 @@ let push_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) -let add_constraints c env = - if c == Univ.Constraint.empty then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if c == Univ.Constraint.empty then env + else map_universes (Univ.merge_constraints c) env + +let push_context ?(strict=false) ctx env = + map_universes (Univ.merge_context strict ctx) env + +let push_context_set ?(strict=false) ctx env = + map_universes (Univ.merge_context_set strict ctx) env let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes diff --git a/checker/environ.mli b/checker/environ.mli index f3b2dd839a..87f143d1bb 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 998e23c6e8..78fff1bbe6 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -69,7 +69,7 @@ let mk_mtb mp sign delta = mod_expr = Abstract; mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.Constraint.empty; + mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = []; } diff --git a/checker/modops.ml b/checker/modops.ml index 8ccf118d3b..7f07f8bf84 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - (* let con = constant_of_delta resolver con in*) let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + Univ.make_abstract_instance cb.const_universes else Univ.Instance.empty in - { cb with const_body = Def (Declarations.from_val (Const (con,u))) } + { cb with + const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index dd94823135..d3bc8373a5 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -27,7 +27,7 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb univs digest = let env = !genv in - let env = add_constraints mb.mod_constraints env in + let env = push_context_set ~strict:true mb.mod_constraints env in let env = add_constraints univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest @@ -84,7 +84,7 @@ let import file clib univs digest = let mb = clib.comp_mod in Mod_checking.check_module (add_constraints univs - (add_constraints mb.mod_constraints env)) mb.mod_mp mb; + (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest diff --git a/checker/univ.ml b/checker/univ.ml index 3bcb3bc950..50c0367bb6 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -244,7 +244,8 @@ module Level = struct let set = make Set let prop = make Prop - + let var i = make (Var i) + let is_small x = match data x with | Level _ -> false @@ -281,8 +282,8 @@ module Level = struct end (** Level sets and maps *) -module LSet = Set.Make (Level) -module LMap = Map.Make (Level) +module LMap = HMap.Make (Level) +module LSet = LMap.Set type 'a universe_map = 'a LMap.t @@ -559,6 +560,8 @@ let repr g u = in repr_rec u +let get_set_arc g = repr g Level.set + (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -573,6 +576,24 @@ let safe_repr g u = let can = terminal u in enter_arc can g, can +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -970,7 +991,7 @@ module Constraint = Set.Make(UConstraintOrd) let empty_constraint = Constraint.empty let merge_constraints c g = Constraint.fold enforce_constraint c g - + type constraints = Constraint.t (** A value with universe constraints. *) @@ -1158,6 +1179,7 @@ struct type t = LSet.t constrained let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst + let levels (ctx, _) = ctx end type universe_context_set = ContextSet.t @@ -1207,6 +1229,9 @@ let subst_instance_constraints s csts = (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) csts Constraint.empty +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + (** Substitute instance inst for ctx in csts *) let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) @@ -1238,6 +1263,20 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst +let merge_context strict ctx g = + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and + constraints due to includes *) + (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + g (UContext.instance ctx) + in merge_constraints (UContext.constraints ctx) g + +let merge_context_set strict ctx g = + let g = LSet.fold + (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) + (ContextSet.levels ctx) g + in merge_constraints (ContextSet.constraints ctx) g + (** Pretty-printing *) let pr_arc = function diff --git a/checker/univ.mli b/checker/univ.mli index 742ef91aed..459adfcd6d 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -74,6 +74,13 @@ val check_eq : universe check_function (** The initial graph of universes: Prop < Set *) val initial_universes : universes +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq @@ -117,7 +124,7 @@ type univ_inconsistency = constraint_type * universe * universe exception UniverseInconsistency of univ_inconsistency val merge_constraints : constraints -> universes -> universes - + val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) @@ -193,6 +200,9 @@ module ContextSet : type universe_context = UContext.t type universe_context_set = ContextSet.t +val merge_context : bool -> universe_context -> universes -> universes +val merge_context_set : bool -> universe_context_set -> universes -> universes + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool @@ -219,6 +229,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints val instantiate_univ_context : universe_context -> universe_context val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +(** Build the relative instance corresponding to the context *) +val make_abstract_instance : universe_context -> universe_instance + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/checker/values.ml b/checker/values.ml index 45220bd051..34de511c8a 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli +MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli *) @@ -307,10 +307,10 @@ and v_impl = and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) (** kernel/safe_typing *) -- cgit v1.2.3 From de648c72a79ae5ba35db166575669ca465b11770 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 18:41:49 +0200 Subject: Univs: fix checker generating undeclared universes. --- checker/mod_checking.ml | 20 ++++++++++++++------ checker/reduction.ml | 2 +- checker/univ.ml | 42 ++++++++++++++++-------------------------- checker/univ.mli | 5 +++-- 4 files changed, 34 insertions(+), 35 deletions(-) (limited to 'checker') diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 78fff1bbe6..3ea5ed0d34 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,19 +18,27 @@ let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in match hd with Sort (Type u) when not (Univ.is_univ_variable u) -> - let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in - mkArity (ctxt,Prop Null), - Univ.enforce_leq u u' Univ.empty_constraint - | _ -> ar, Univ.empty_constraint + let ul = Univ.Level.make empty_dirpath 1 in + let u' = Univ.Universe.make ul in + let cst = Univ.enforce_leq u u' Univ.empty_constraint in + let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in + mkArity (ctxt,Prop Null), ctx + | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); - let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + let env' = + if cb.const_polymorphic then + let inst = Univ.make_abstract_instance cb.const_universes in + let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in + push_context ~strict:false ctx env + else push_context ~strict:true cb.const_universes env + in let envty, ty = match cb.const_type with RegularArity ty -> let ty', cu = refresh_arity ty in - let envty = add_constraints cu env' in + let envty = push_context_set cu env' in let _ = infer_type envty ty' in envty, ty | TemplateArity(ctxt,par) -> let _ = check_ctxt env' ctxt in diff --git a/checker/reduction.ml b/checker/reduction.ml index 8ddeea2a20..384d883ea3 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -175,7 +175,7 @@ let sort_cmp env univ pb s0 s1 = then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds + Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() ++ Univ.pr_universes univ)) end; diff --git a/checker/univ.ml b/checker/univ.ml index 50c0367bb6..648e478176 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -562,20 +562,6 @@ let repr g u = let get_set_arc g = repr g Level.set -(* [safe_repr] also search for the canonical representative, but - if the graph doesn't contain the searched universe, we add it. *) - -let safe_repr g u = - let rec safe_repr_rec u = - match UMap.find u g with - | Equiv v -> safe_repr_rec v - | Canonical arc -> arc - in - try g, safe_repr_rec u - with Not_found -> - let can = terminal u in - enter_arc can g, can - exception AlreadyDeclared let add_universe vlev strict g = @@ -760,8 +746,8 @@ let is_lt g arcu arcv = (** First, checks on universe levels *) let check_equal g u v = - let g, arcu = safe_repr g u in - let _, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in arcu == arcv let check_eq_level g u v = u == v || check_equal g u v @@ -770,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ let check_smaller g strict u v = - let g, arcu = safe_repr g u in - let g, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if strict then is_lt g arcu arcv else @@ -921,8 +907,8 @@ let error_inconsistency o u v = (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> error_inconsistency Eq v u @@ -937,8 +923,8 @@ let enforce_univ_eq u v g = (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if is_leq g arcu arcv then g else match fast_compare g arcv arcu with @@ -949,8 +935,8 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u g | FastLE -> fst (setlt g arcu arcv) @@ -962,7 +948,10 @@ let enforce_univ_lt u v g = | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = + let g = enter_arc (terminal Level.set) UMap.empty in + let g = enter_arc (terminal Level.prop) g in + enforce_univ_lt Level.prop Level.set g (* Constraints and sets of constraints. *) @@ -1167,7 +1156,7 @@ struct (** Universe contexts (variables as a list) *) let empty = (Instance.empty, Constraint.empty) - + let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst end @@ -1180,6 +1169,7 @@ struct let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst let levels (ctx, _) = ctx + let make ctx cst = (ctx, cst) end type universe_context_set = ContextSet.t diff --git a/checker/univ.mli b/checker/univ.mli index 459adfcd6d..02c1bbdb91 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -131,7 +131,7 @@ val check_constraints : constraints -> universes -> bool (** Polymorphic maps from universe levels to 'a *) module LMap : Map.S with type key = universe_level - +module LSet : CSig.SetS with type elt = universe_level type 'a universe_map = 'a LMap.t (** {6 Substitution} *) @@ -184,7 +184,7 @@ sig type t val empty : t - + val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints @@ -193,6 +193,7 @@ end module ContextSet : sig type t + val make : LSet.t -> constraints -> t val empty : t val constraints : t -> constraints end -- cgit v1.2.3 From 42cd40e4edcc29804d1b73d8cb076f8578ce66fa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 4 Nov 2015 19:58:09 -0500 Subject: Checker was forgetting to register global universes introduced by opaque proofs. --- checker/check.ml | 9 ++++----- checker/declarations.ml | 6 ++++-- checker/declarations.mli | 5 +++-- checker/safe_typing.ml | 4 ++-- checker/safe_typing.mli | 4 ++-- 5 files changed, 15 insertions(+), 13 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 2bc470aead..21c8f1c5bb 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -46,7 +46,7 @@ type library_t = { library_opaques : Cic.opaque_table; library_deps : Cic.library_deps; library_digest : Cic.vodigest; - library_extra_univs : Univ.constraints } + library_extra_univs : Univ.ContextSet.t } module LibraryOrdered = struct @@ -97,7 +97,7 @@ let access_opaque_univ_table dp i = let t = LibraryMap.find dp !opaque_univ_tables in assert (i < Array.length t); Future.force t.(i) - with Not_found -> Univ.empty_constraint + with Not_found -> Univ.ContextSet.empty let _ = Declarations.indirect_opaque_access := access_opaque_table @@ -347,9 +347,8 @@ let intern_from_file (dir, f) = LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) opaque_csts; let extra_cst = - Option.default Univ.empty_constraint - (Option.map (fun (_,cs,_) -> - Univ.ContextSet.constraints cs) opaque_csts) in + Option.default Univ.ContextSet.empty + (Option.map (fun (_,cs,_) -> cs) opaque_csts) in mk_library sd md f table digest extra_cst let get_deps (dir, f) = diff --git a/checker/declarations.ml b/checker/declarations.ml index 36e6a7caba..32d1713a88 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -426,7 +426,7 @@ let subst_lazy_constr sub = function let indirect_opaque_access = ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) let indirect_opaque_univ_access = - ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints) + ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t) let force_lazy_constr = function | Indirect (l,dp,i) -> @@ -435,7 +435,7 @@ let force_lazy_constr = function let force_lazy_constr_univs = function | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i - | _ -> Univ.empty_constraint + | _ -> Univ.ContextSet.empty let subst_constant_def sub = function | Undef inl -> Undef inl @@ -457,6 +457,8 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Def _ | Undef _ -> false +let opaque_univ_context cb = force_lazy_constr_univs cb.const_body + let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in diff --git a/checker/declarations.mli b/checker/declarations.mli index 3c6db6ab71..456df83699 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -2,17 +2,18 @@ open Names open Cic val force_constr : constr_substituted -> constr -val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints +val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t val from_val : constr -> constr_substituted val indirect_opaque_access : (DirPath.t -> int -> constr) ref -val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref +val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref (** Constant_body *) val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool +val opaque_univ_context : constant_body -> Univ.ContextSet.t (* Mutual inductives *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index d3bc8373a5..81a3cc035b 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -28,7 +28,7 @@ let set_engagement c = let full_add_module dp mb univs digest = let env = !genv in let env = push_context_set ~strict:true mb.mod_constraints env in - let env = add_constraints univs env in + let env = push_context_set ~strict:true univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest @@ -83,7 +83,7 @@ let import file clib univs digest = check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module - (add_constraints univs + (push_context_set ~strict:true univs (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index e16e64e6a2..892a8d2cc9 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -15,6 +15,6 @@ val get_env : unit -> env val set_engagement : engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit val unsafe_import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit -- cgit v1.2.3 From 3b2c4cb7f53ff664b72e21ca9a653f244624833e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Nov 2015 15:19:05 +0100 Subject: Displaying the object identifier in votour. --- checker/votour.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/votour.ml b/checker/votour.ml index 4aecb28f20..f8264ca684 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -22,6 +22,7 @@ sig val input : in_channel -> obj val repr : obj -> obj repr val size : obj -> int + val oid : obj -> int option end module ReprObj : S = @@ -45,6 +46,7 @@ struct else INT (Obj.magic obj) let size (_, p) = CObj.shared_size_of_pos p + let oid _ = None end module ReprMem : S = @@ -97,6 +99,9 @@ struct let _ = init_size seen obj in obj + let oid = function + | Int _ | Atm _ | Fun _ -> None + | Ptr p -> Some p end module Visit (Repr : S) : @@ -149,9 +154,13 @@ let rec get_details v o = match v, Repr.repr o with |Annot (s,v), _ -> get_details v o |_ -> "" +let get_oid obj = match Repr.oid obj with +| None -> "" +| Some id -> Printf.sprintf " [0x%08x]" id + let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (Repr.size o)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) -- cgit v1.2.3 From 126a3c998c62bfd9f9b570f12b2e29576dd94cdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 13:43:07 +0100 Subject: Factorizing unsafe code by relying on the new Dyn module. --- checker/check.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'checker') diff --git a/checker/check.mllib b/checker/check.mllib index 246fe64dee..a029b0245c 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store -- cgit v1.2.3 From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- checker/safe_typing.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'checker') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 81a3cc035b..ee33051676 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -13,6 +13,8 @@ open Cic open Names open Environ +let pr_dirpath dp = str (DirPath.to_string dp) + (************************************************************************) (* * Global environment @@ -52,9 +54,9 @@ let check_engagement env (expected_impredicative_set,expected_type_in_type) = let report_clash f caller dir = let msg = - str "compiled library " ++ str(DirPath.to_string caller) ++ + str "compiled library " ++ pr_dirpath caller ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(DirPath.to_string dir) ++ fnl() in + pr_dirpath dir ++ fnl() in f msg -- cgit v1.2.3 From f7433647beb23113faf0bf68326e5dc98e388d79 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 31 Dec 2015 17:04:07 +0100 Subject: Remove unused function Checker.print_loc. There is no location to print anyway, so it will never be useful. --- checker/checker.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index d5d9b9e3b8..a13d529e83 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -217,12 +217,6 @@ open Type_errors let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") -let print_loc loc = - if loc = Loc.ghost then - (str"") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = str "\"" ++ str s ++ str "\"" let where s = -- cgit v1.2.3 From 8a9445fbf65d4ddf2c96348025d487b4d54a5d01 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jan 2016 19:36:02 +0100 Subject: Fix order of files in mllib. CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places. --- checker/check.mllib | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker') diff --git a/checker/check.mllib b/checker/check.mllib index 49ca6bf051..0d36e3a0f1 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -17,6 +17,8 @@ Flags Control Pp_control Loc +CList +CString Serialize Stateid Feedback @@ -25,8 +27,6 @@ Segmenttree Unicodetable Unicode CObj -CList -CString CArray CStack Util -- cgit v1.2.3 From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jan 2016 00:58:42 +0100 Subject: Protect code against changes in Map interface. The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. --- checker/univ.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/univ.mli b/checker/univ.mli index 02c1bbdb91..f3216feac4 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -130,7 +130,7 @@ val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) -module LMap : Map.S with type key = universe_level +module LMap : CSig.MapS with type key = universe_level module LSet : CSig.SetS with type elt = universe_level type 'a universe_map = 'a LMap.t -- cgit v1.2.3 From 6599e31f04b6e8980de72e9d3913b70c04b6698c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 6 Jan 2016 15:08:08 +0100 Subject: Remove deprecated command-line options such as "-as". --- checker/checker.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker') diff --git a/checker/checker.ml b/checker/checker.ml index a13d529e83..da93685f98 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -331,8 +331,6 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- checker/check.ml | 2 +- checker/check_stat.ml | 2 +- checker/check_stat.mli | 2 +- checker/checker.ml | 2 +- checker/cic.mli | 2 +- checker/closure.ml | 2 +- checker/closure.mli | 2 +- checker/indtypes.ml | 2 +- checker/indtypes.mli | 2 +- checker/inductive.ml | 2 +- checker/inductive.mli | 2 +- checker/mod_checking.mli | 2 +- checker/modops.ml | 2 +- checker/modops.mli | 2 +- checker/print.ml | 2 +- checker/reduction.ml | 2 +- checker/reduction.mli | 2 +- checker/safe_typing.ml | 2 +- checker/safe_typing.mli | 2 +- checker/subtyping.ml | 2 +- checker/subtyping.mli | 2 +- checker/term.ml | 2 +- checker/type_errors.ml | 2 +- checker/type_errors.mli | 2 +- checker/typeops.ml | 2 +- checker/typeops.mli | 2 +- checker/univ.ml | 2 +- checker/univ.mli | 2 +- checker/validate.ml | 2 +- checker/values.ml | 2 +- checker/votour.ml | 2 +- 31 files changed, 31 insertions(+), 31 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 21c8f1c5bb..3a5c91217d 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- checker/cic.mli | 3 ++- checker/closure.ml | 8 ++++---- checker/declarations.ml | 13 ++++++++----- checker/environ.ml | 2 +- checker/indtypes.ml | 20 ++++++++++---------- checker/inductive.ml | 48 ++++++++++++++++++++++++------------------------ checker/reduction.ml | 10 +++++----- checker/term.ml | 47 ++++++++++++++++++++++++++--------------------- checker/term.mli | 2 +- checker/typeops.ml | 16 ++++++++-------- checker/values.ml | 6 +++--- 11 files changed, 92 insertions(+), 83 deletions(-) (limited to 'checker') diff --git a/checker/cic.mli b/checker/cic.mli index 041394d466..00ac2f56c3 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint (** {6 Type of assumptions and contexts} *) -type rel_declaration = Name.t * constr option * constr +type rel_declaration = LocalAssum of Name.t * constr (* name, type *) + | LocalDef of Name.t * constr * constr (* name, value, type *) type rel_context = rel_declaration list (** The declarations below in .vo should be outside sections, diff --git a/checker/closure.ml b/checker/closure.ml index 400a535cf2..c2708e97d2 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -217,10 +217,10 @@ let ref_value_cache info ref = let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context - (fun (id,b,t) (i,subs) -> - match b with - | None -> (i+1, subs) - | Some body -> (i+1, (i,body) :: subs)) + (fun decl (i,subs) -> + match decl with + | LocalAssum _ -> (i+1, subs) + | LocalDef (_,body,_) -> (i+1, (i,body) :: subs)) (rel_context env) ~init:(0,[]) (* else (0,[])*) diff --git a/checker/declarations.ml b/checker/declarations.ml index 32d1713a88..2f6eeba1d9 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -517,11 +517,14 @@ let map_decl_arity f g = function | RegularArity a -> RegularArity (f a) | TemplateArity a -> TemplateArity (g a) - -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') +let subst_rel_declaration sub = function + | LocalAssum (id,t) as x -> + let t' = subst_mps sub t in + if t == t' then x else LocalAssum (id,t') + | LocalDef (id,c,t) as x -> + let c' = subst_mps sub c in + let t' = subst_mps sub t in + if c == c' && t == t' then x else LocalDef (id,c',t') let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) diff --git a/checker/environ.ml b/checker/environ.ml index f8f5c29b79..7040fdda46 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -80,7 +80,7 @@ let push_rel d env = let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2865f5bd4a..f11fa5a7ad 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -56,10 +56,10 @@ let is_constructor_head t = let conv_ctxt_prefix env (ctx1:rel_context) ctx2 = let rec chk env rctx1 rctx2 = match rctx1, rctx2 with - (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' -> + (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' -> conv env ty1 ty2; chk (push_rel d1 env) rctx1' rctx2' - | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' -> + | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' -> conv env ty1 ty2; conv env bd1 bd2; chk (push_rel d1 env) rctx1' rctx2' @@ -94,10 +94,10 @@ let rec sorts_of_constr_args env t = match t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in varj :: sorts_of_constr_args env1 c2 | LetIn (name,def,ty,c) -> - let env1 = push_rel (name,Some def,ty) env in + let env1 = push_rel (LocalDef (name,def,ty)) env in sorts_of_constr_args env1 c | _ when is_constructor_head t -> [] | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") @@ -167,7 +167,7 @@ let typecheck_arity env params inds = full_arity is used as argument or subject to cast, an upper universe will be generated *) let id = ind.mind_typename in - let env_ar' = push_rel (Name id, None, arity) env_ar in + let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in env_ar') env inds in @@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | (_,Some _,_)::hyps -> check k (index+1) hyps + | LocalDef (_,_,_) :: hyps -> check k (index+1) hyps | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps @@ -340,7 +340,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs = | ([],_) -> () | (_,[]) -> failwith "number of recursive parameters cannot be greater than the number of parameters." - | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps) + | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps) | (p::lp,_::hyps) -> (match whd_betadeltaiota env p with | Rel w when w = index -> find (index-1) (lp,hyps) @@ -370,14 +370,14 @@ let abstract_mind_lc env ntyps npars lc = [lra] is the list of recursive tree of each variable *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = - (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra) let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in + push_rel (LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar)) env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in diff --git a/checker/inductive.ml b/checker/inductive.ml index 79dba4fac5..9480124211 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -88,10 +88,10 @@ let instantiate_params full t u args sign = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = fold_rel_context - (fun (_,copt,_) (largs,subs,ty) -> - match (copt, largs, ty) with - | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> + (fun decl (largs,subs,ty) -> + match (decl, largs, ty) with + | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) + | (LocalDef (_,b,_),_,LetIn(_,_,_,t)) -> (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) @@ -161,7 +161,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let rec make_subst env = let rec make subst = function - | (_,Some _,_)::sign, exp, args -> + | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) | d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in @@ -174,7 +174,7 @@ let rec make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env a)) in make (cons_subst u s subst) (sign, exp, args) - | (na,None,t)::sign, Some u::exp, [] -> + | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -319,8 +319,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -345,12 +345,12 @@ let is_correct_arity env c (p,pj) ind specif params = let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), LocalAssum (_,a1')::ar' -> (try conv env a1 a1' with NotConvertible -> raise (LocalArity None)); - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (na1,None,a1) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match (whd_betadeltaiota env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in @@ -362,8 +362,8 @@ let is_correct_arity env c (p,pj) ind specif params = | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false - | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + | _, (LocalDef _ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in @@ -530,7 +530,7 @@ let make_renv env recarg tree = genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = - { env = push_rel (x,None,ty) renv.env; + { env = push_rel (LocalAssum (x,ty)) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -628,14 +628,14 @@ let check_inductive_codomain env p = (* The following functions are almost duplicated from indtypes.ml, except that they carry here a poorer environment (containing less information). *) let ienv_push_var (env, lra) (x,a,ra) = -(push_rel (x,None,a) env, (Norec,ra)::lra) +(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra) let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env + push_rel (LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar)) env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -902,7 +902,7 @@ let filter_stack_domain env ci p stack = let t = whd_betadeltaiota env ar in match stack, t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in let ty, args = decompose_app (whd_betadeltaiota env a) in let elt = match ty with | Ind ind -> @@ -956,10 +956,10 @@ let check_one_fix renv recpos trees def = end else begin - match pi2 (lookup_rel p renv.env) with - | None -> + match lookup_rel p renv.env with + | LocalAssum _ -> List.iter (check_rec_call renv []) l - | Some c -> + | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> check_rec_call renv stack (applist(lift p c,l)) @@ -1078,7 +1078,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match (whd_betadeltaiota env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in if n = k+1 then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1127,7 +1127,7 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1168,7 +1168,7 @@ let check_one_cofix env nbfix def deftype = | Lambda (x,a,b) -> assert (args = []); if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in check_rec_call env' alreadygrd (n+1) tree vlra b else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) diff --git a/checker/reduction.ml b/checker/reduction.ml index 3a666a60a4..f1aa5d9194 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -490,7 +490,7 @@ let dest_prod env = let t = whd_betadeltaiota env c in match t with | Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in decrec (push_rel d env) (d::m) c0 | _ -> m,t in @@ -502,10 +502,10 @@ let dest_prod_assum env = let rty = whd_betadeltaiota_nolet env ty in match rty with | Prod (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> @@ -520,10 +520,10 @@ let dest_lam_assum env = let rty = whd_betadeltaiota_nolet env ty in match rty with | Lambda (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty diff --git a/checker/term.ml b/checker/term.ml index 6487d1a152..181d292ad4 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -222,24 +222,29 @@ let rel_context_length = List.length let rel_context_nhyps hyps = let rec nhyps acc = function | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in + | LocalAssum _ :: hyps -> nhyps (1+acc) hyps + | LocalDef _ :: hyps -> nhyps acc hyps in nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init let map_rel_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') + let map_decl = function + | LocalAssum (n, typ) as decl -> + let typ' = f typ in + if typ' == typ then decl else + LocalAssum (n, typ') + | LocalDef (n, body, typ) as decl -> + let body' = f body in + let typ' = f typ in + if body' == body && typ' == typ then decl else + LocalDef (n, body', typ') in List.smartmap map_decl l let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -272,8 +277,8 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match c with - | Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c + | Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in @@ -282,18 +287,18 @@ let decompose_lam_n_assum n = (* Iterate products, with or without lets *) (* Constructs either [(x:t)c] or [[x=b:t]c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> Prod (na, t, c) - | Some b -> LetIn (na, b, t, c) +let mkProd_or_LetIn decl c = + match decl with + | LocalAssum (na,t) -> Prod (na, t, c) + | LocalDef (na,b,t) -> LetIn (na, b, t, c) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let decompose_prod_assum = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in @@ -305,8 +310,8 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if Int.equal n 0 then l,c else match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in @@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign let destArity = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t)::l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") diff --git a/checker/term.mli b/checker/term.mli index ab488b2b7c..d6455e23f4 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -40,7 +40,7 @@ val extended_rel_list : int -> rel_context -> constr list val compose_lam : (name * constr) list -> constr -> constr val decompose_lam : constr -> (name * constr) list * constr val decompose_lam_n_assum : int -> constr -> rel_context * constr -val mkProd_or_LetIn : name * constr option * constr -> constr -> constr +val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr val decompose_prod_assum : constr -> rel_context * constr val decompose_prod_n_assum : int -> constr -> rel_context * constr diff --git a/checker/typeops.ml b/checker/typeops.ml index d49c40a8bd..64afd21b2a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u)) let judge_of_relative env n = try - let (_,_,typ) = lookup_rel n env in + let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in lift n typ with Not_found -> error_unbound_rel env n @@ -296,13 +296,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let j' = execute env1 c2 in Prod(name,c1,j') | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let varj' = execute_type env1 c2 in Sort (sort_of_product env varj varj') @@ -314,7 +314,7 @@ let rec execute env cstr = let env',c2' = (* refresh_arity env *) env, c2 in let _ = execute_type env' c2' in judge_of_cast env' (c1,j1) DEFAULTcast c2' in - let env1 = push_rel (name,Some c1,c2) env in + let env1 = push_rel (LocalDef (name,c1,c2)) env in let j' = execute env1 c3 in subst1 c1 j' @@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr let check_ctxt env rels = fold_rel_context (fun d env -> match d with - (_,None,ty) -> + | LocalAssum (_,ty) -> let _ = infer_type env ty in push_rel d env - | (_,Some bd,ty) -> + | LocalDef (_,bd,ty) -> let j1 = infer env bd in let _ = infer env ty in conv_leq env j1 ty; @@ -399,9 +399,9 @@ let check_polymorphic_arity env params par = let pl = par.template_param_levels in let rec check_p env pl params = match pl, params with - Some u::pl, (na,None,ty)::params -> + Some u::pl, LocalAssum (na,ty)::params -> check_kind env ty u; - check_p (push_rel (na,None,ty) env) pl params + check_p (push_rel (LocalAssum (na,ty)) env) pl params | None::pl,d::params -> check_p (push_rel d env) pl params | [], _ -> () | _ -> failwith "check_poly: not the right number of params" in diff --git a/checker/values.ml b/checker/values.ml index c14e9223da..19cbb50606 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 7c050ff1db22f14ee3a4c44aae533082 checker/cic.mli +MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli *) @@ -154,8 +154,8 @@ and v_prec = Tuple ("prec_declaration", and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) - -let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|] +let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|]; (* LocalAssum *) + [|v_name; v_constr; v_constr|] |] (* LocalDef *) let v_rctxt = List v_rdecl let v_section_ctxt = v_enum "emptylist" 1 -- cgit v1.2.3 From 13e847b7092d53ffec63e4cba54c67d39560e67a Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 23:33:01 +0100 Subject: CLEANUP: Simplifying the changes done in "checker/*" --- checker/declarations.ml | 10 ++-------- checker/indtypes.ml | 7 ++++--- checker/inductive.ml | 5 +++-- checker/term.ml | 26 +++++++++++++------------- checker/term.mli | 1 + 5 files changed, 23 insertions(+), 26 deletions(-) (limited to 'checker') diff --git a/checker/declarations.ml b/checker/declarations.ml index 2f6eeba1d9..3ce3125337 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -517,14 +517,8 @@ let map_decl_arity f g = function | RegularArity a -> RegularArity (f a) | TemplateArity a -> TemplateArity (g a) -let subst_rel_declaration sub = function - | LocalAssum (id,t) as x -> - let t' = subst_mps sub t in - if t == t' then x else LocalAssum (id,t') - | LocalDef (id,c,t) as x -> - let c' = subst_mps sub c in - let t' = subst_mps sub t in - if c == c' && t == t' then x else LocalDef (id,c',t') +let subst_rel_declaration sub = + Term.map_rel_decl (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index f11fa5a7ad..566df673c1 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | LocalDef (_,_,_) :: hyps -> check k (index+1) hyps + | LocalDef _ :: hyps -> check k (index+1) hyps | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps @@ -376,8 +376,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar)) env in + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in diff --git a/checker/inductive.ml b/checker/inductive.ml index 9480124211..5e2e14f7fb 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -634,8 +634,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar)) env + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in diff --git a/checker/term.ml b/checker/term.ml index 181d292ad4..56cc9cdc22 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -227,19 +227,19 @@ let rel_context_nhyps hyps = nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init -let map_rel_context f l = - let map_decl = function - | LocalAssum (n, typ) as decl -> - let typ' = f typ in - if typ' == typ then decl else - LocalAssum (n, typ') - | LocalDef (n, body, typ) as decl -> - let body' = f body in - let typ' = f typ in - if body' == body && typ' == typ then decl else - LocalDef (n, body', typ') - in - List.smartmap map_decl l +let map_rel_decl f = function + | LocalAssum (n, typ) as decl -> + let typ' = f typ in + if typ' == typ then decl else + LocalAssum (n, typ') + | LocalDef (n, body, typ) as decl -> + let body' = f body in + let typ' = f typ in + if body' == body && typ' == typ then decl else + LocalDef (n, body', typ') + +let map_rel_context f = + List.smartmap (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function diff --git a/checker/term.mli b/checker/term.mli index d6455e23f4..0af83e05d7 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -35,6 +35,7 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int val fold_rel_context : (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list val compose_lam : (name * constr) list -> constr -> constr -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- checker/check.mllib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/check.mllib b/checker/check.mllib index 0d36e3a0f1..902ab9ddf6 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -32,7 +32,7 @@ CStack Util Ppstyle Errors -Ephemeron +CEphemeron Future CUnix System -- cgit v1.2.3 From 10e3c8e59664ed5137cd650ba6e0704943c511e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Mar 2016 14:17:48 +0100 Subject: Removing OCaml deprecated function names from the Lazy module. --- checker/inductive.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'checker') diff --git a/checker/inductive.ml b/checker/inductive.ml index 5e2e14f7fb..43a32ea24d 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -527,7 +527,7 @@ type guard_env = let make_renv env recarg tree = { env = env; rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) - genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } + genv = [Lazy.from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = { env = push_rel (LocalAssum (x,ty)) renv.env; @@ -538,7 +538,7 @@ let assign_var_spec renv (i,spec) = { renv with genv = List.assign renv.genv (i-1) spec } let push_var_renv renv (x,ty) = - push_var renv (x,ty,Lazy.lazy_from_val Not_subterm) + push_var renv (x,ty,Lazy.from_val Not_subterm) (* Fetch recursive information about a variable p *) let subterm_var p renv = @@ -549,13 +549,13 @@ let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } let push_fix_renv renv (_,v,_ as recdef) = let n = Array.length v in { env = push_rec_types recdef renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } (* Definition and manipulation of the stack *) @@ -862,7 +862,7 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] + | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t -- cgit v1.2.3 From 2e557589920156fe84335e72c5e765347bcc7c9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 14:45:24 +0200 Subject: A patch renaming equal into eq in the module dealing with hash-consing, so as to avoid having too many kinds of equalities with same name. --- checker/univ.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'checker') diff --git a/checker/univ.ml b/checker/univ.ml index cb2eaced77..96d8270137 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val equal : t -> t -> bool + val eq : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let equal l1 l2 = match l1, l2 with + let eq l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.equal x y then l + if H.eq x y then l else cons y (remove x l) end @@ -229,7 +229,7 @@ module Level = struct type _t = t type t = _t type u = unit - let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -320,7 +320,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -339,7 +339,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let equal x y = x == y || + let eq x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1089,7 +1089,7 @@ struct a end - let equal t1 t2 = + let eq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = -- cgit v1.2.3