Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 49 insertions, 49 deletions

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
-  
+