From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/vnorm.ml | 119 +++++++++++++++++++++++++++-------------------------- 1 file changed, 61 insertions(+), 58 deletions(-) (limited to 'pretyping/vnorm.ml') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 047971d5..19613c4e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,14 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (Name (Id.of_string "x"), dom, codom) + | Name _ -> res exception Find_at of int @@ -34,7 +37,8 @@ let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do let tagj,arity = reloc_tbl.(j) in - if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then + let no_arity = Int.equal arity 0 in + if Int.equal tag tagj && (cst && no_arity || not (cst || no_arity)) then raise (Find_at j) else () done;raise Not_found @@ -44,30 +48,31 @@ let invert_tag cst tag reloc_tbl = let find_rectype_a env c = let (t, l) = let t = whd_betadeltaiota env c in - try destApp t with e when Errors.noncritical e -> (t,[||]) in + try destApp t with DestKO -> (t,[||]) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib typ params = - let s = ind_subst mind mib in +let type_constructor mind mib u typ params = + let s = ind_subst mind mib u in let ctyp = substl s typ in + let ctyp = subst_instance_constr u ctyp in let nparams = Array.length params in - if nparams = 0 then ctyp + if Int.equal nparams 0 then ctyp else let _,ctyp = decompose_prod_n nparams ctyp in - substl (List.rev (Array.to_list params)) ctyp + substl (Array.rev_to_list params) ctyp let construct_of_constr const env tag typ = - let (mind,_ as ind), allargs = find_rectype_a env typ in + let ((mind,_ as ind), u) as indu, allargs = find_rectype_a env typ in (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag), + ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) @@ -80,8 +85,8 @@ let construct_of_constr const env tag typ = let nparams = mib.mind_nparams in let i = invert_tag const tag mip.mind_reloc_tbl in let params = Array.sub allargs 0 nparams in - let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in - (mkApp(mkConstruct(ind,i), params), ctyp) + let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in + (mkApp(mkConstructUi(indu,i), params), ctyp) let construct_of_constr_const env tag typ = fst (construct_of_constr true env tag typ) @@ -91,7 +96,8 @@ let construct_of_constr_block = construct_of_constr false let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, Typeops.type_of_constant env 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 @@ -100,30 +106,33 @@ let constr_type_of_idkey env idkey = let (_,_,ty) = lookup_rel n env in mkRel n, lift n ty -let type_of_ind env ind = - type_of_inductive env (Inductive.lookup_mind_specif env ind) +let type_of_ind env (ind, u) = + type_of_inductive env (Inductive.lookup_mind_specif env ind, u) -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 decl,indapp = decompose_prod_assum typi in - let ind,cargs = find_rectype_a env indapp 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,u),cargs) = find_rectype_a env indapp in let nparams = Array.length params in let carity = snd (rtbl.(i)) in let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in let codom = - let papp = mkApp(lift (List.length decl) p,crealargs) in + let ndecl = List.length decl in + let papp = mkApp(lift ndecl p,crealargs) in if dep then let cstr = ith_constructor_of_inductive ind (i+1) in let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in + let params = Array.map (lift ndecl) params in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in mkApp(papp,[|dep_cstr|]) else papp in - decl, codom + decl, decl_with_letin, codom in Array.mapi build_one_branch mip.mind_nf_lc let build_case_type dep p realargs c = @@ -141,7 +150,7 @@ and nf_whd env whd typ = | Vsort s -> mkSort s | Vprod p -> let dom = nf_vtype env (dom p) in - let name = Name (id_of_string "x") in + let name = Name (Id.of_string "x") in let vc = body_of_vfun (nb_rel env) (codom p) in let codom = nf_vtype (push_rel (name,None,dom) env) vc in mkProd(name,dom,codom) @@ -166,7 +175,7 @@ and nf_whd env whd typ = | Vatom_stk(Aiddef(idkey,v), stk) -> nf_whd env (whd_stack v stk) typ | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind) stk + nf_stk env (mkIndU ind) (type_of_ind env ind) stk and nf_stk env c t stk = match stk with @@ -176,28 +185,25 @@ and nf_stk env c t stk = nf_stk env (mkApp(c,args)) t stk | Zfix (f,vargs) :: stk -> let fa, typ = nf_fix_app env f vargs in - let _,_,codom = - try decompose_prod env typ - with e when Errors.noncritical e -> exit 120 - in + let _,_,codom = decompose_prod env typ in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> - let (mind,_ as ind),allargs = find_rectype_a env t in + 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 - let params,realargs = Util.array_chop nparams allargs in + let params,realargs = Util.Array.chop nparams allargs in let pT = - hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in + hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_betadeltaiota env pT in - let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in + let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) - let btypes = build_branches_type env ind mib mip params dep p in + let btypes = build_branches_type env ind mib mip u params dep p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = - let decl,codom = btypes.(i) in - let b = nf_val (push_rel_context decl env) v codom in - it_mkLambda_or_LetIn b decl + let decl,decl_with_letin,codom = btypes.(i) in + let b = nf_val (Termops.push_rels_assum decl env) v codom in + Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in @@ -209,21 +215,18 @@ and nf_predicate env ind mip params v pT = | Vfun f, Prod _ -> let k = nb_rel env in let vb = body_of_vfun k f in - let name,dom,codom = - try decompose_prod env pT - with e when Errors.noncritical e -> exit 121 - in + let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in dep, mkLambda(name,dom,body) | Vfun f, _ -> let k = nb_rel env in let vb = body_of_vfun k f in - let name = Name (id_of_string "c") in + let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in - let params = if n=0 then params else Array.map (lift n) params in - let dom = mkApp(mkInd ind,Array.append params rargs) in + let params = if Int.equal n 0 then params else Array.map (lift n) params in + let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (name,None,dom) env) vb in true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type @@ -234,10 +237,7 @@ and nf_args env vargs t = let args = Array.init len (fun i -> - let _,dom,codom = - try decompose_prod env !t - with e when Errors.noncritical e -> exit 123 - in + let _,dom,codom = decompose_prod env !t in let c = nf_val env (arg vargs i) dom in t := subst1 c codom; c) in !t,args @@ -248,10 +248,7 @@ and nf_bargs env b t = let args = Array.init len (fun i -> - let _,dom,codom = - try decompose_prod env !t - with e when Errors.noncritical e -> exit 124 - in + let _,dom,codom = decompose_prod env !t in let c = nf_val env (bfield b i) dom in t := subst1 c codom; c) in args @@ -261,8 +258,10 @@ and nf_fun env f typ = let vb = body_of_vfun k f in let name,dom,codom = try decompose_prod env typ - with e when Errors.noncritical e -> - raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ)) + with DestKO -> + (* 27/2/13: Turned this into an anomaly *) + Errors.anomaly + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let body = nf_val (push_rel (name,None,dom) env) vb codom in mkLambda(name,dom,body) @@ -274,9 +273,13 @@ and nf_fix env f = let vb, vt = reduce_fix k f in let ndef = Array.length vt in let ft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in + let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in + (* Third argument of the tuple is ignored by push_rec_types *) let env = push_rec_types (name,ft,ft) env in - let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in + (* We lift here because the types of arguments (in tt) will be evaluated + in an environment where the fixpoints have been pushed *) + let norm_vb v t = nf_fun env v (lift ndef t) in + let fb = Util.Array.map2 norm_vb vb ft in mkFix ((rec_args,init),(name,ft,fb)) and nf_fix_app env f vargs = @@ -292,9 +295,9 @@ and nf_cofix env cf = let vb,vt = reduce_cofix k cf in let ndef = Array.length vt in let cft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in + let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in let env = push_rec_types (name,cft,cft) env in - let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in + let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in mkCoFix (init,(name,cft,cfb)) let cbv_vm env c t = -- cgit v1.2.3