open Names
open Declarations
open Term
open Environ
open Conv_oracle
open Reduction 
open Closure
open Vm
open Csymtable 
open Univ

let val_of_constr env c =
  val_of_constr (pre_env env) c

(* Test la structure des piles *)

let compare_zipper z1 z2 =
  match z1, z2 with
  | Zapp args1, Zapp args2 -> nargs args1 = nargs args2
  | Zfix _, Zfix _ -> true 
  | Zswitch _, Zswitch _ -> true
  | _ , _ -> false

let rec compare_stack stk1 stk2 =
  match stk1, stk2 with
  | [], [] -> true
  | z1::stk1, z2::stk2 ->
      if compare_zipper z1 z2 then compare_stack stk1 stk2
      else false
  | _, _ -> false 

(* Conversion *)
let conv_vect fconv vect1 vect2 cu =
  let n = Array.length vect1 in
  if n = Array.length vect2 then
    let rcu = ref cu in
    for i = 0 to n - 1 do
      rcu := fconv vect1.(i) vect2.(i) !rcu
    done;
    !rcu
  else raise NotConvertible

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 
    
and conv_whd pb k whd1 whd2 cu =  
  match whd1, whd2 with
  | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu 
  | Vprod p1, Vprod p2 ->
      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)
  | Vconstr_const i1, Vconstr_const i2 -> 
      if i1 = i2 then cu else raise NotConvertible 
  | Vconstr_block b1, Vconstr_block b2 ->
      let sz = bsize b1 in
      if btag b1 = btag b2 && sz = bsize b2 then
	let rcu = ref cu in
	for i = 0 to sz - 1 do
	  rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu
	done;
	!rcu
      else raise NotConvertible
  | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> 
      conv_atom pb k a1 stk1 a2 stk2 cu
  | _, Vatom_stk(Aiddef(_,v),stk) -> 
      conv_whd pb k whd1 (force_whd v stk) cu
  | Vatom_stk(Aiddef(_,v),stk), _ -> 
      conv_whd pb k (force_whd v stk) whd2 cu
  | _, _ -> raise NotConvertible

and conv_atom pb k a1 stk1 a2 stk2 cu =
  match a1, a2 with
  | Aind (kn1,i1), Aind(kn2,i2) ->
      if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then
	conv_stack k stk1 stk2 cu
      else raise NotConvertible
  | Aid ik1, Aid ik2 -> 
      if ik1 = ik2 && compare_stack stk1 stk2 then 
	conv_stack k stk1 stk2 cu 
      else raise NotConvertible
  | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
      begin
	try
	  if ik1 = ik2 && compare_stack stk1 stk2 then
	    conv_stack k stk1 stk2 cu 
	  else raise NotConvertible
	with NotConvertible ->
	  if oracle_order ik1 ik2 then             
            conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
          else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
      end
  | Aiddef(ik1,v1), _ ->
      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 =
  match stk1, stk2 with
  | [], [] -> 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
      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
	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
	done;
	conv_stack k stk1 stk2 !rcu
      else raise NotConvertible
  | _, _ -> raise NotConvertible

and conv_fun pb k f1 f2 cu =
  if f1 == f2 then cu
  else
    let arity,b1,b2 = decompose_vfun2 k f1 f2 in
    conv_val pb (k+arity) b1 b2 cu

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 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
    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 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
    else raise NotConvertible

and conv_arguments k args1 args2 cu =
  if args1 == args2 then cu
  else
    let n = nargs args1 in
    if n = nargs args2 then
      let rcu = ref cu in
      for i = 0 to n - 1 do
	rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu
      done;
      !rcu
    else raise NotConvertible

let rec conv_eq pb t1 t2 cu =
  if t1 == t2 then cu 
  else
    match kind_of_term t1, kind_of_term t2 with
    | Rel n1, Rel n2 -> 
	if n1 = n2 then cu else raise NotConvertible
    | Meta m1, Meta m2 ->
	if m1 = m2 then cu else raise NotConvertible
    | Var id1, Var id2 -> 
	if id1 = id2 then cu else raise NotConvertible
    | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu
    | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
    | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
	conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu)
    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu
    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
	conv_eq pb c1 c2 (conv_eq CONV b1 b2 cu)
    | App (c1,l1), App (c2,l2) ->
	conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu)
    | Evar (e1,l1), Evar (e2,l2) ->
	if e1 = e2 then conv_eq_vect l1 l2 cu
	else raise NotConvertible
    | Const c1, Const c2 -> 
	if c1 = c2 then cu else raise NotConvertible
    | Ind c1, Ind c2 -> 
	if c1 = c2 then cu else raise NotConvertible
    | Construct c1, Construct c2 -> 
	if c1 = c2 then cu else raise NotConvertible
    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
	let pcu = conv_eq CONV p1 p2 cu in
	let ccu = conv_eq CONV c1 c2 pcu in
	conv_eq_vect bl1 bl2 ccu
    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
	else raise NotConvertible
    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->	
	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
	else raise NotConvertible
    | _ -> raise NotConvertible

and conv_eq_vect vt1 vt2 cu =
  let len = Array.length vt1 in
  if len = Array.length vt2 then
    let rcu = ref cu in
    for i = 0 to len-1 do
      rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu
    done; !rcu
  else raise NotConvertible
      
let vconv pb env t1 t2 =
  let cu =
    try conv_eq pb t1 t2 Constraint.empty
    with NotConvertible ->
      infos := create_clos_infos betaiotazeta env;
      let v1 = val_of_constr env t1 in
      let v2 = val_of_constr env t2 in
      let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in
      cu
  in cu
    
let _ = Reduction.set_vm_conv vconv

let use_vm = ref false

let set_use_vm b =
  use_vm := b;
  if b then Reduction.set_default_conv vconv
  else Reduction.set_default_conv Reduction.conv_cmp
      
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