- Ajout d'un cast vm dans la syntaxe : x <: t

    Part contre ces cas sont detruis dans les "Definition" 
    (pas dans les "Lemma") je comprends pas ou ils sont enlev'e...
    Si une id'ee ...

- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.

- Meilleur compilation des coinductifs, on utilise maintenant vraimment
  du lazy. 

- Enfin un peu plus de doc dans le code de la vm.

  Benjamin



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 336 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 653f8978c..7115097e4 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -17,7 +17,7 @@ let val_of_constr env c =
 let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> nargs args1 = nargs args2
-  | Zfix _, Zfix _ -> true 
+  | Zfix(f1,args1), Zfix(f2,args2) ->  nargs args1 = nargs args2
   | Zswitch _, Zswitch _ -> true
   | _ , _ -> false
 
@@ -42,8 +42,9 @@ let conv_vect fconv vect1 vect2 cu =
 
 let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
-let rec conv_val pb k v1 v2 cu =
-  if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu 
+let rec conv_val pb k v1 v2 cu = 
+  if v1 == v2 then cu 
+  else conv_whd pb k (whd_val v1) (whd_val v2) cu
     
 and conv_whd pb k whd1 whd2 cu =  
   match whd1, whd2 with
@@ -52,21 +53,14 @@ and conv_whd pb k whd1 whd2 cu =
       let cu = conv_val CONV k (dom p1) (dom p2) cu in
       conv_fun pb k (codom p1) (codom p2) cu
   | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu
-  | Vfix f1, Vfix f2 -> conv_fix k f1 f2 cu
-  | Vfix_app fa1, Vfix_app fa2 ->
-      let f1 = fix fa1 in
-      let args1 = args_of_fix fa1 in
-      let f2 = fix fa2 in
-      let args2 = args_of_fix fa2 in
-      conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
-  | Vcofix cf1, Vcofix cf2 -> 
-      conv_cofix k cf1 cf2 cu
-  | Vcofix_app cfa1, Vcofix_app cfa2 ->	
-      let cf1 = cofix cfa1 in
-      let args1 = args_of_cofix cfa1 in
-      let cf2 = cofix cfa2 in
-      let args2 = args_of_cofix cfa2 in
-      conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
+  | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu
+  | Vfix (f1,Some args1), Vfix(f2,Some args2) ->
+      if nargs args1 <> nargs args2 then raise NotConvertible
+      else conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
+  | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu
+  | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->	
+      if nargs args1 <> nargs args2 then raise NotConvertible
+      else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 -> 
       if i1 = i2 then cu else raise NotConvertible 
   | Vconstr_block b1, Vconstr_block b2 ->
@@ -111,8 +105,6 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
       conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
       conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
-  | Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ -> 
-      Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work"
   | _, _ -> raise NotConvertible 
 	
 and conv_stack k stk1 stk2 cu =
@@ -120,22 +112,17 @@ and conv_stack k stk1 stk2 cu =
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
       conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) 
-  | Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
-      let f1 = fix fa1 in
-      let args1 = args_of_fix fa1 in
-      let f2 = fix fa2 in
-      let args2 = args_of_fix fa2 in
+  | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
       conv_stack k stk1 stk2 
 	(conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
-      if eq_tbl sw1 sw2 then
+      if check_switch sw1 sw2 then
 	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
 	let rcu = ref (conv_val CONV k vt1 vt2 cu) in
 	let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
 	for i = 0 to Array.length b1 - 1 do
 	  rcu := 
-	    conv_val CONV (k + fst b1.(i)) 
-	      (snd b1.(i)) (snd b2.(i)) !rcu
+	    conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
 	done;
 	conv_stack k stk1 stk2 !rcu
       else raise NotConvertible
@@ -151,24 +138,20 @@ and conv_fix k f1 f2 cu =
   if f1 == f2 then cu 
   else
     if check_fix f1 f2 then
-      let tf1 = types_of_fix f1 in
-      let tf2 = types_of_fix f2 in
+      let bf1, tf1 = reduce_fix k f1 in
+      let bf2, tf2 = reduce_fix k f2 in
       let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in
-      let bf1 = bodies_of_fix k f1 in
-      let bf2 = bodies_of_fix k f2 in
-      conv_vect (conv_fun CONV (k + (fix_ndef f1))) bf1 bf2 cu
+      conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu
     else raise NotConvertible
 
 and conv_cofix k cf1 cf2 cu =
   if cf1 == cf2 then cu
   else
     if check_cofix cf1 cf2 then
-      let tcf1 = types_of_cofix cf1 in
-      let tcf2 = types_of_cofix cf2 in
+      let bcf1, tcf1 = reduce_cofix k cf1 in
+      let bcf2, tcf2 = reduce_cofix k cf2 in
       let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in
-      let bcf1 = bodies_of_cofix k cf1 in
-      let bcf2 = bodies_of_cofix k cf2 in
-      conv_vect (conv_val CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
+      conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu
     else raise NotConvertible
 
 and conv_arguments k args1 args2 cu =
@@ -255,302 +238,4 @@ let set_use_vm b =
       
 let use_vm _ = !use_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*)
-
-(* Build the substitution that replaces Rels by the appropriate 
-  inductives *)
-let ind_subst mind mib =
-  let ntypes = mib.mind_ntypes in
-  let make_Ik k = mkInd (mind,ntypes-k-1) in 
-  Util.list_tabulate make_Ik ntypes
-
-(* Instantiate inductives and parameters in constructor type
-   in normal form *)
-let constructor_instantiate 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 destApplication t =
-  try destApp t 
-  with _ -> t,[||]
-
-let construct_of_constr_const env tag typ =
-  let cind,params = destApplication (whd_betadeltaiota env typ) in
-  let ind = destInd cind in
-  let (_,mip) = Inductive.lookup_mind_specif env ind in
-  let rtbl = mip.mind_reloc_tbl in
-  let i = invert_tag true tag rtbl in
-  mkApp(mkConstruct(ind,i), params)
-
-let find_rectype typ =
-  let cind,args = destApplication typ in
-  let ind = destInd cind in
-  ind, args
-
-let construct_of_constr_block env tag typ =
-  let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let nparams = mib.mind_nparams in
-  let rtbl = mip.mind_reloc_tbl in
-  let i = invert_tag false tag rtbl in
-  let params = Array.sub allargs 0 nparams in
-  let specif = mip.mind_nf_lc in
-  let ctyp = constructor_instantiate 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 ->
-      let ty = (lookup_constant cst env).const_type in
-      mkConst cst, ty
-  | 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 = 
-  let specif = Inductive.lookup_mind_specif env ind in
-  Inductive.type_of_inductive specif
-
-let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl =
-  (* [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 = constructor_instantiate mind mib params cty in
-    let decl,indapp = Term.decompose_prod typi in
-    let ind,cargs = find_rectype 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
-
-(* La fonction de normalisation *)
-
-let rec nf_val env v t = nf_whd env (whd_val v) t 
-
-and nf_whd env whd typ =
-  match whd with
-  | Vsort s -> mkSort s
-  | Vprod p ->
-      let dom = nf_val env (dom p) crazy_type in
-      let name = Name (id_of_string "x") in
-      let vc = body_of_vfun (nb_rel env) (codom p) in
-      let codom = nf_val (push_rel (name,None,dom) env) vc crazy_type in      
-      mkProd(name,dom,codom)	  
-  | Vfun f -> nf_fun env f typ
-  | Vfix f -> nf_fix env f
-  | Vfix_app fa ->
-      let f = fix fa in
-      let vargs = args_of_fix fa in
-      let fd = nf_fix env f in
-      let (_,i),(_,ta,_) = destFix fd in
-      let t = ta.(i) in
-      let _, args = nf_args  env vargs t in
-      mkApp(fd,args)
-  | Vcofix cf -> nf_cofix env cf 
-  | Vcofix_app cfa -> 
-      let cf = cofix cfa in
-      let vargs = args_of_cofix cfa in
-      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 
-  | Vatom_stk(_,stk) -> assert false
-
-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 fa :: stk ->   
-      let f = fix fa in
-      let vargs = args_of_fix fa in
-      let fd = nf_fix env f in
-      let (_,i),(_,ta,_) = destFix fd in
-      let tf = ta.(i) in
-      let typ, args = nf_args env vargs tf in
-      let _,_,codom = decompose_prod env typ in
-      nf_stk env (mkApp(mkApp(fd,args),[|c|])) (subst1 c codom) stk
-  | Zswitch sw :: stk -> 
-      let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota 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
-      (* calcul du predicat du case, 
-        [dep] indique si c'est un case dependant *)
-      let dep,p = 
-	let dep = ref false in
-	let rec nf_predicate env 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 body = 
-		nf_predicate (push_rel (name,None,dom) env) vb codom in
-              mkLambda(name,dom,body)
-	  | Vfun f, _ ->
-	      dep := true;
-	      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_val (push_rel (name,None,dom) env) vb crazy_type in
-	      mkLambda(name,dom,body)
-          | _, _ -> nf_val env v crazy_type
-	in 
-	let aux = 
-	  nf_predicate env (type_of_switch sw) 
-	    (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params))
-	in
-	!dep,aux in
-      (* Calcul du type des branches *)
-      let btypes = 
-	build_branches_type ind mib mip params dep p mip.mind_reloc_tbl 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 = 
-	if dep then mkApp(mkApp(p, params), [|c|])
-	else mkApp(p, params)
-      in
-      let ci = case_info sw in
-      nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
-       
-and nf_args env vargs t =
-  let t = ref t in
-  let len = nargs vargs in
-  let targs = 
-    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,targs
-
-and nf_bargs env b t =
-  let t = ref t in
-  let len = bsize b in
-  let args = Array.create len crazy_type in
-  for i = 0 to len - 1 do
-    let _,dom,codom = decompose_prod env !t in
-    let c = nf_val env (bfield b i) dom in
-    args.(i) <- c;
-    t := subst1 c codom
-  done;
-  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) *) 
-
-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 = fix_init f in
-  let rec_args = rec_args f in
-  let ndef = fix_ndef f in
-  let vt = types_of_fix f 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 k = nb_rel env in
-  let vb = bodies_of_fix k f 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_cofix env cf =
-  let init = cofix_init cf in
-  let ndef = cofix_ndef cf in
-  let vt = types_of_cofix cf 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 k = nb_rel env in
-  let vb = bodies_of_cofix k cf 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 = val_of_constr env c in
-  let c = nf_val env v t in
-  if not transp then set_transp_values false; 
-  c
-