diff options
| -rw-r--r-- | kernel/environ.ml | 25 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/term.ml | 26 | ||||
| -rw-r--r-- | kernel/term.mli | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/typing.ml | 3 | ||||
| -rw-r--r-- | kernel/typing.mli | 2 |
9 files changed, 28 insertions, 47 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3608e969f..67198e9f1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -26,6 +26,16 @@ type 'a unsafe_env = { env_metamap : (int * constr) list; env_universes : universes } +let empty_env = { + env_context = ENVIRON (([],[]),[]); + env_globals = { + env_constants = Spmap.empty; + env_inductives = Spmap.empty; + env_abstractions = Spmap.empty }; + env_sigma = mt_evd; + env_metamap = []; + env_universes = initial_universes } + let universes env = env.env_universes let metamap env = env.env_metamap let evar_map env = env.env_sigma @@ -79,9 +89,6 @@ let lookup_mind_specif i env = mis_mip = mind_nth_type_packet mib tyi } | _ -> invalid_arg "lookup_mind_specif" -let mind_nparams env i = - let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams - let lookup_meta n env = List.assoc n env.env_metamap @@ -94,7 +101,8 @@ let lowercase_first_char id = String.lowercase (first_char id) (* id_of_global gives the name of the given sort oper *) let id_of_global env = function - | Const sp -> basename sp + | Const sp -> + basename sp | MutInd (sp,tyi) -> (* Does not work with extracted inductive types when the first inductive is logic : if tyi=0 then basename sp else *) @@ -104,11 +112,10 @@ let id_of_global env = function | MutConstruct ((sp,tyi),i) -> let mib = lookup_mind sp env in let mip = mind_nth_type_packet mib tyi in - if i <= Array.length mip.mind_consnames & i > 0 then - mip.mind_consnames.(i-1) - else - failwith "id_of_global" - | _ -> assert false + assert (i <= Array.length mip.mind_consnames && i > 0); + mip.mind_consnames.(i-1) + | _ -> + assert false let hdchar env c = let rec hdrec = function diff --git a/kernel/environ.mli b/kernel/environ.mli index 15b2ca821..a1b7307e1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -18,6 +18,8 @@ open Sign type 'a unsafe_env +val empty_env : 'a unsafe_env + val evar_map : 'a unsafe_env -> 'a evar_map val universes : 'a unsafe_env -> universes val metamap : 'a unsafe_env -> (int * constr) list @@ -55,8 +57,6 @@ val evaluable_const : 'a unsafe_env -> constr -> bool val is_existential : constr -> bool -val mind_nparams : 'a unsafe_env -> constr -> int - (*s Unsafe judgments. We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its type. *) diff --git a/kernel/names.mli b/kernel/names.mli index e5c5ad0f4..be26f0f32 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -40,7 +40,6 @@ type path_kind = CCI | FW | OBJ val string_of_kind : path_kind -> string val kind_of_string : string -> path_kind - type section_path val make_path : string list -> identifier -> path_kind -> section_path diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 77331bf5a..1e72c4033 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -519,6 +519,9 @@ let contract_cofix = function sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies) | _ -> assert false +let mind_nparams env i = + let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let reduce_mind_case env mia = match mia.mconstr with | DOPN(MutConstruct((indsp,tyindx),i),_) -> @@ -827,9 +830,6 @@ and eqappr cv_pb infos appr1 appr2 = bool_and_convert (n=m) (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) - | (FOP0 Implicit, FOP0 Implicit) -> - convert_of_bool (Array.length v1 = 0 & Array.length v2 = 0) - (* 2 constants or 2 abstractions *) | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) -> convert_or diff --git a/kernel/term.ml b/kernel/term.ml index 46bcebcd8..a16625023 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -15,7 +15,6 @@ type 'a oper = (* DOP0 *) | Meta of int | Sort of 'a - | Implicit (* DOP2 *) | Cast | Prod | Lambda (* DOPN *) @@ -472,7 +471,6 @@ type kindOfTerm = | IsVar of identifier | IsXtra of string | IsSort of sorts - | IsImplicit | IsCast of constr*constr | IsProd of name*constr*constr | IsLambda of name*constr*constr @@ -501,7 +499,6 @@ let kind_of_term c = | DOP0 (Meta n) -> IsMeta n | DOP0 (Sort s) -> IsSort s | DOP0 (XTRA s) -> IsXtra s - | DOP0 Implicit -> IsImplicit | DOP2 (Cast, t1, t2) -> IsCast (t1,t2) | DOP2 (Prod, t1, (DLAM (x,t2))) -> IsProd (x,t1,t2) | DOP2 (Lambda, t1, (DLAM (x,t2))) -> IsLambda (x,t1,t2) @@ -1075,35 +1072,12 @@ let prefix_application_eta k (c:constr) (t:constr) = None | (_,_) -> None -(* Used in trad and progmach *) -let rec rename_rels curidx sofar = function - | [] -> sofar - | ((id,Rel n)::tl as l) -> - if curidx = n then - rename_rels (curidx+1) (subst1 (VAR id) sofar) tl - else - rename_rels (curidx+1) (subst1 (DOP0 Implicit) sofar) l - | _ -> assert false - let sort_increasing_snd = Sort.list (fun x y -> match x,y with (_,Rel m),(_,Rel n) -> m < n | _ -> assert false) -let clean_rhs rhs worklist = - let workvars = List.filter (compose isVAR snd) worklist in - let rhs' = - replace_vars - (List.map (fun (id',v) -> let id = destVar v in - (id,{sinfo=Closed; sit=VAR id'})) - workvars) - rhs - in - let workrels = List.filter (compose isRel snd) worklist in - let workrels' = sort_increasing_snd workrels in - rename_rels 1 rhs' workrels' - (* Recognizing occurrences of a given subterm in a term for Pattern : (subst_term c t) substitutes (Rel 1) for all occurrences of term c in a (closed) term t *) diff --git a/kernel/term.mli b/kernel/term.mli index 0fc2a5e8f..6ef98691f 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -13,7 +13,6 @@ type 'a oper = (* DOP0 *) | Meta of int | Sort of 'a - | Implicit (* DOP2 *) | Cast | Prod | Lambda (* DOPN *) @@ -77,7 +76,6 @@ type kindOfTerm = | IsVar of identifier | IsXtra of string | IsSort of sorts - | IsImplicit | IsCast of constr * constr | IsProd of name * constr * constr | IsLambda of name * constr * constr @@ -495,8 +493,6 @@ val rename_bound_var : identifier list -> constr -> constr val eta_reduce_head : constr -> constr val eq_constr : constr -> constr -> bool val eta_eq_constr : constr -> constr -> bool -val rename_rels : int -> constr -> (identifier * constr) list -> constr -val clean_rhs : constr -> (identifier * constr) list -> constr val subst_term : constr -> constr -> constr val subst_term_eta_eq : constr -> constr -> constr val replace_consts : diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 40f41d603..7e8161865 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -349,7 +349,6 @@ let type_of_sort c g = match c with | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' | DOP0 (Sort (Prop _)) -> mkType prop_univ, g - | DOP0 (Implicit) -> mkImplicit, g | _ -> invalid_arg "type_of_sort" (* Type of a lambda-abstraction. *) @@ -743,6 +742,9 @@ let check_fix env = function (* Co-fixpoints. *) +let mind_nparams env i = + let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let check_guard_rec_meta env nbfix def deftype = let rec codomain_is_coind c = match whd_betadeltaiota env (strip_outer_cast c) with diff --git a/kernel/typing.ml b/kernel/typing.ml index 1b5a14a3a..e69c84665 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -33,7 +33,6 @@ let tjudge_of_judge env j = typ = match whd_betadeltaiota env j.uj_type with (* Nécessaire pour ZFC *) | DOP0 (Sort s) -> s - | DOP0 Implicit -> anomaly "Tiens, un implicit" | _ -> anomaly "Not a type (tjudge_ofjudge)" } let vect_lift = Array.mapi lift @@ -256,6 +255,8 @@ let safe_machine_v env cv = type 'a environment = 'a unsafe_env +let empty_environment = empty_env + let evar_map = evar_map let universes = universes let metamap = metamap diff --git a/kernel/typing.mli b/kernel/typing.mli index 314554e85..ec3ca5d7d 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -18,6 +18,8 @@ open Typeops type 'a environment +val empty_environment : 'a environment + val evar_map : 'a environment -> 'a evar_map val universes : 'a environment -> universes val metamap : 'a environment -> (int * constr) list |