diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 14 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 14 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 12 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 2 |
5 files changed, 19 insertions, 24 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 360199fec..119e92c82 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -326,7 +326,7 @@ let inh_coerce_to_ind evdref env loc ty tyi = let binding_vars_of_inductive sigma = function | NotInd _ -> [] - | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) (List.map EConstr.of_constr realargs) + | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs let extract_inductive_data env sigma decl = match decl with @@ -422,7 +422,7 @@ let type_of_tomatch = function | NotInd (_,t) -> t let map_tomatch_type f = function - | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type (fun c -> EConstr.Unsafe.to_constr (f (EConstr.of_constr c))) ind,names) + | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type f ind,names) | NotInd (c,t) -> NotInd (Option.map f c, f t) let liftn_tomatch_type n depth = map_tomatch_type (Vars.liftn n depth) @@ -873,7 +873,7 @@ let specialize_predicate_var (cur,typ,dep) tms ccl = let l = match typ with | IsInd (_, IndType (_, _), []) -> [] - | IsInd (_, IndType (_, realargs), names) -> List.map EConstr.of_constr realargs + | IsInd (_, IndType (_, realargs), names) -> realargs | NotInd _ -> [] in subst_predicate (l,c) ccl tms @@ -922,7 +922,7 @@ let rec extract_predicate ccl = function subst1 cur pred end | Pushed (_,((cur,IsInd (_,IndType(_,realargs),_)),_,na))::tms -> - let realargs = List.rev_map EConstr.of_constr realargs in + let realargs = List.rev realargs in let k, nrealargs = match na with | Anonymous -> 0, realargs | Name _ -> 1, (cur :: realargs) @@ -1064,7 +1064,6 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs) let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = - let realargs = List.map EConstr.of_constr realargs in let pred = abstract_predicate env !evdref indf current realargs dep tms p in (pred, EConstr.of_constr (whd_betaiota !evdref (applist (pred, realargs@[current])))) @@ -1384,7 +1383,6 @@ and match_current pb (initial,tomatch) = if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then compile_all_variables initial tomatch pb else - let realargs = List.map EConstr.of_constr realargs in (* We generalize over terms depending on current term to match *) let pb,deps = generalize_problem (names,dep) pb deps in @@ -1749,7 +1747,6 @@ let build_inversion_problem loc env sigma tms t = match tms with | [] -> [], acc_sign, acc | (t, IsInd (_,IndType(indf,realargs),_)) :: tms -> - let realargs = List.map EConstr.of_constr realargs in let patl,acc = List.fold_map' reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in @@ -1919,7 +1916,6 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = (match tmtype with NotInd _ -> (subst, len - signlen) | IsInd (_, IndType(indf,realargs),_) -> - let realargs = List.map EConstr.of_constr realargs in let subst, len = List.fold_left (fun (subst, len) arg -> @@ -2119,7 +2115,6 @@ let constr_of_pat env evdref arsign pat avoid = let apptype = Retyping.get_type_of env ( !evdref) app in let apptype = EConstr.of_constr apptype in let IndType (indf, realargs) = find_rectype env (!evdref) apptype in - let realargs = List.map EConstr.of_constr realargs in match alias with Anonymous -> pat', sign, app, apptype, realargs, n, avoid @@ -2364,7 +2359,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign = *) match ty with | IsInd (ty, IndType (indf, args), _) when List.length args > 0 -> - let args = List.map EConstr.of_constr args in (* Build the arity signature following the names in matched terms as much as possible *) let argsign = List.tl arsign in (* arguments in inverse application order *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 98b267cfd..cb8b25323 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -58,21 +58,23 @@ let lift_inductive_family n = liftn_inductive_family n 1 let substnl_ind_family l n = map_ind_family (substnl l n) -type inductive_type = IndType of inductive_family * constr list +type inductive_type = IndType of inductive_family * EConstr.constr list let make_ind_type (indf, realargs) = IndType (indf,realargs) let dest_ind_type (IndType (indf,realargs)) = (indf,realargs) let map_inductive_type f (IndType (indf, realargs)) = - IndType (map_ind_family f indf, List.map f realargs) + let f' c = EConstr.Unsafe.to_constr (f (EConstr.of_constr c)) in + IndType (map_ind_family f' indf, List.map f realargs) -let liftn_inductive_type n d = map_inductive_type (liftn n d) +let liftn_inductive_type n d = map_inductive_type (EConstr.Vars.liftn n d) let lift_inductive_type n = liftn_inductive_type n 1 -let substnl_ind_type l n = map_inductive_type (substnl l n) +let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) let mkAppliedInd (IndType ((ind,params), realargs)) = - applist (mkIndU ind,params@realargs) + let open EConstr in + applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs) (* Does not consider imbricated or mutually recursive types *) let mis_is_recursive_subset listind rarg = @@ -471,7 +473,7 @@ let find_rectype env sigma c = if mib.mind_nparams > List.length l then raise Not_found; let l = List.map EConstr.Unsafe.to_constr l in let (par,rargs) = List.chop mib.mind_nparams l in - IndType((indu, par),rargs) + IndType((indu, par),List.map EConstr.of_constr rargs) | _ -> raise Not_found let find_inductive env sigma c = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7af9731f9..1614e1817 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -37,15 +37,15 @@ val substnl_ind_family : constr list -> int -> inductive_family -> inductive_family (** An inductive type with its parameters and real arguments *) -type inductive_type = IndType of inductive_family * constr list -val make_ind_type : inductive_family * constr list -> inductive_type -val dest_ind_type : inductive_type -> inductive_family * constr list -val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type +type inductive_type = IndType of inductive_family * EConstr.constr list +val make_ind_type : inductive_family * EConstr.constr list -> inductive_type +val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list +val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type -val mkAppliedInd : inductive_type -> constr +val mkAppliedInd : inductive_type -> EConstr.constr val mis_is_recursive_subset : int list -> wf_paths -> bool val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7586b54ba..11d50926f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -860,7 +860,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in - let realargs = List.map EConstr.of_constr realargs in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err ~loc (str "Destructing let is only for inductive types" ++ diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 6f03fc462..88899e633 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -123,7 +123,7 @@ let retype ?(polyprop=true) sigma = with Not_found -> retype_error BadRecursiveType in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in - let t = EConstr.of_constr (betazetaevar_applist sigma n p (List.map EConstr.of_constr realargs)) in + let t = EConstr.of_constr (betazetaevar_applist sigma n p realargs) in (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c]))) | _ -> t) |