1 files changed, 271 insertions, 0 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
new file mode 100644
index 00000000..55f798de
--- /dev/null
+++ b/pretyping/vnorm.ml
@@ -0,0 +1,271 @@
+open Names
+open Declarations
+open Term
+open Environ
+open Inductive
+open Reduction 
+open Vm
+
+(*******************************************)
+(* Calcul de la forme normal d'un terme    *)
+(*******************************************)
+
+let crazy_type = mkSet 
+
+let decompose_prod env t =
+  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+  else res
+
+exception Find_at of int
+
+(* rend le numero du constructeur correspondant au tag [tag],
+   [cst] = true si c'est un constructeur constant *)
+
+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
+	raise (Find_at j)
+      else ()
+    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 = whd_betadeltaiota env c in
+    try destApp t with _ -> (t,[||]) in
+  match kind_of_term t with
+  | Ind ind -> (ind, l)
+  | _ -> raise Not_found
+
+(* Instantiate inductives and parameters in constructor type *)
+let build_type_constructor mind mib params ctyp =
+  let si = ind_subst mind mib in
+  let ctyp1 = substl si ctyp in
+  let nparams = Array.length params in
+  if nparams = 0 then ctyp1
+  else
+    let _,ctyp2 = decompose_prod_n nparams ctyp1 in
+    let sp = List.rev (Array.to_list params) in substl sp ctyp2
+   
+let construct_of_constr_const env tag typ =
+  let ind,params = find_rectype env typ in
+  let (_,mip) = lookup_mind_specif env ind in
+  let i = invert_tag true tag mip.mind_reloc_tbl in
+  applistc (mkConstruct(ind,i)) params
+
+let construct_of_constr_block env tag typ =
+  let (mind,_ as ind), allargs = find_rectype_a env typ in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let nparams = mib.mind_nparams in
+  let i = invert_tag false tag mip.mind_reloc_tbl in
+  let params = Array.sub allargs 0 nparams in
+  let specif = mip.mind_nf_lc in
+  let ctyp = build_type_constructor mind mib params specif.(i-1) in
+  (mkApp(mkConstruct(ind,i), params), ctyp)
+  	
+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 
+      mkVar id, ty
+  | 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 = 
+  type_of_inductive env (Inductive.lookup_mind_specif env ind)
+
+let build_branches_type env (mind,_ as _ind) mib mip 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 = build_type_constructor mind mib params cty in
+    let decl,indapp = Term.decompose_prod typi in
+    let ind,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(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
+	mkApp(papp,[|dep_cstr|])
+      else papp
+    in 
+    decl, codom
+  in Array.mapi build_one_branch mip.mind_nf_lc
+
+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 
+
+and nf_vtype env v =  nf_val env v crazy_type
+
+and nf_whd env whd typ =
+  match whd with
+  | Vsort s -> mkSort s
+  | Vprod p ->
+      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)	  
+  | 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) -> 
+      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) 
+  | 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
+      let args = nf_bargs env b ctyp in
+      mkApp(capp,args)
+  | Vatom_stk(Aid idkey, stk) ->
+      let c,typ = constr_type_of_idkey env idkey in
+      nf_stk env c typ stk
+  | 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 
+	
+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 ->  
+      let fa, typ = nf_fix_app env f vargs 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 (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 = 
+	hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+      let dep, p = nf_predicate env ind 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
+      (* 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 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 
+      let branchs = Array.mapi mkbranch bsw in
+      let tcase = build_case_type dep p realargs c in
+      let ci = case_info sw in
+      nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+
+and nf_predicate env ind mip params v pT =
+  match whd_val v, kind_of_term pT with
+  | Vfun f, Prod _ ->
+      let k = nb_rel env in
+      let vb = body_of_vfun k f 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 n = mip.mind_nrealargs in
+      let rargs = Array.init n (fun i -> mkRel (n-i)) in
+      let dom = mkApp(mkApp(mkInd ind,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
+	
+and nf_args env vargs t =
+  let t = ref t in
+  let len = nargs vargs in
+  let args = 
+    Array.init len 
+      (fun i ->
+	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
+
+and nf_bargs env b t =
+  let t = ref t in
+  let len = bsize b in
+  let args =
+    Array.init len 
+      (fun i -> 
+	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
+
+and nf_fun env f typ =
+  let k = nb_rel env in
+  let vb = body_of_vfun k f in
+  let name,dom,codom = decompose_prod env typ in
+  let body = nf_val (push_rel (name,None,dom) env) vb codom in
+  mkLambda(name,dom,body)
+
+and nf_fix env f =
+  let init = current_fix f in
+  let rec_args = rec_args f in
+  let k = nb_rel env in
+  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 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
+  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 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; 
+  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; 
+  c
+