From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- pretyping/vnorm.ml | 98 +++++++++++++++++++++++++++--------------------------- 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'pretyping/vnorm.ml') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 5d09570e..c894d2b5 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -6,21 +6,21 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*) +(*i $Id$ i*) open Names open Declarations open Term open Environ open Inductive -open Reduction +open Reduction open Vm (*******************************************) (* Calcul de la forme normal d'un terme *) (*******************************************) -let crazy_type = mkSet +let crazy_type = mkSet let decompose_prod env t = let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in @@ -33,18 +33,18 @@ exception Find_at of int [cst] = true si c'est un constructeur constant *) let invert_tag cst tag reloc_tbl = - try + 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 raise (Find_at j) else () - done;raise Not_found - with Find_at j -> (j+1) + done;raise Not_found + with Find_at j -> (j+1) (* Argggg, ces constructeurs de ... qui commencent a 1*) let find_rectype_a env c = - let (t, l) = + let (t, l) = let t = whd_betadeltaiota env c in try destApp t with _ -> (t,[||]) in match kind_of_term t with @@ -53,13 +53,13 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib typ params = +let type_constructor mind mib typ params = let s = ind_subst mind mib in let ctyp = substl s typ in let nparams = Array.length params in if nparams = 0 then ctyp else - let _,ctyp = decompose_prod_n nparams ctyp in + let _,ctyp = decompose_prod_n nparams ctyp in substl (List.rev (Array.to_list params)) ctyp @@ -85,7 +85,7 @@ let construct_of_constr const env tag typ = let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in (mkApp(mkConstruct(ind,i), params), ctyp) -let construct_of_constr_const env tag typ = +let construct_of_constr_const env tag typ = fst (construct_of_constr true env tag typ) let construct_of_constr_block = construct_of_constr false @@ -94,15 +94,15 @@ let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> mkConst cst, Typeops.type_of_constant env cst - | VarKey id -> - let (_,_,ty) = lookup_named id env in + | VarKey id -> + let (_,_,ty) = lookup_named id env in mkVar id, ty - | RelKey i -> + | 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 = +let type_of_ind env ind = type_of_inductive env (Inductive.lookup_mind_specif env ind) let build_branches_type env (mind,_ as _ind) mib mip params dep p = @@ -116,7 +116,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = 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 codom = let papp = mkApp(p,crealargs) in if dep then let cstr = ith_constructor_of_inductive ind (i+1) in @@ -124,17 +124,17 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in mkApp(papp,[|dep_cstr|]) else papp - in + in decl, codom in Array.mapi build_one_branch mip.mind_nf_lc -let build_case_type dep p realargs c = +let build_case_type dep p realargs c = if dep then mkApp(mkApp(p, realargs), [|c|]) else mkApp(p, realargs) (* La fonction de normalisation *) -let rec nf_val env v t = nf_whd env (whd_val v) t +let rec nf_val env v t = nf_whd env (whd_val v) t and nf_vtype env v = nf_val env v crazy_type @@ -145,18 +145,18 @@ and nf_whd env whd typ = let dom = nf_vtype env (dom p) 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) + let codom = nf_vtype (push_rel (name,None,dom) env) vc in + mkProd(name,dom,codom) | Vfun f -> nf_fun env f typ | Vfix(f,None) -> nf_fix env f | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs) - | Vcofix(cf,_,None) -> nf_cofix env cf - | Vcofix(cf,_,Some vargs) -> + | Vcofix(cf,_,None) -> nf_cofix env cf + | Vcofix(cf,_,Some vargs) -> let cfd = nf_cofix env cf in let i,(_,ta,_) = destCoFix cfd in let t = ta.(i) in let _, args = nf_args env vargs t in - mkApp(cfd,args) + mkApp(cfd,args) | Vconstr_const n -> construct_of_constr_const env n typ | Vconstr_block b -> let capp,ctyp = construct_of_constr_block env (btag b) typ in @@ -168,24 +168,24 @@ 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 (mkInd ind) (type_of_ind env ind) stk + and nf_stk 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 - | Zfix (f,vargs) :: 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 _ -> exit 120 in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk - | Zswitch sw :: stk -> + | Zswitch sw :: stk -> let (mind,_ as ind),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 pT = + let pT = hnf_prod_applist env (type_of_ind env ind) (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 @@ -195,12 +195,12 @@ and nf_stk env c t stk = let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = let decl,codom = btypes.(i) in - let env = - List.fold_right + let env = + List.fold_right (fun (name,t) env -> push_rel (name,None,t) env) decl env in let b = nf_val env v codom in - compose_lam decl b - in + compose_lam decl b + in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in let ci = case_info sw in @@ -212,10 +212,10 @@ and nf_predicate env ind mip params v pT = let k = nb_rel env in let vb = body_of_vfun k f in let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in - let dep,body = + let dep,body = nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | Vfun f, _ -> let k = nb_rel env in let vb = body_of_vfun k f in let name = Name (id_of_string "c") in @@ -226,12 +226,12 @@ and nf_predicate env ind mip params v pT = let body = nf_vtype (push_rel (name,None,dom) env) vb in true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type - + and nf_args env vargs t = let t = ref t in let len = nargs vargs in - let args = - Array.init len + let args = + Array.init len (fun i -> let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in let c = nf_val env (arg vargs i) dom in @@ -242,8 +242,8 @@ and nf_bargs env b t = let t = ref t in let len = bsize b in let args = - Array.init len - (fun i -> + Array.init len + (fun i -> let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in let c = nf_val env (bfield b i) dom in t := subst1 c codom; c) in @@ -252,7 +252,7 @@ and nf_bargs env b t = and nf_fun env f typ = let k = nb_rel env in let vb = body_of_vfun k f in - let name,dom,codom = + let name,dom,codom = try decompose_prod env typ with _ -> raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ)) @@ -268,17 +268,17 @@ and nf_fix env f = 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 env = push_rec_types (name,ft,ft) env in + 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 mkFix ((rec_args,init),(name,ft,fb)) - + and nf_fix_app env f vargs = let fd = nf_fix env f in let (_,i),(_,ta,_) = destFix fd in let t = ta.(i) in let t, args = nf_args env vargs t in mkApp(fd,args),t - + and nf_cofix env cf = let init = current_cofix cf in let k = nb_rel env in @@ -286,15 +286,15 @@ and nf_cofix env cf = 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 env = push_rec_types (name,cft,cft) env 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 mkCoFix (init,(name,cft,cfb)) - + let cbv_vm env c t = let transp = transp_values () in - if not transp then set_transp_values true; + if not transp then set_transp_values true; let v = Vconv.val_of_constr env c in let c = nf_val env v t in - if not transp then set_transp_values false; + if not transp then set_transp_values false; c - + -- cgit v1.2.3