(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew, David Walker,                       *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* talcon.ml
 * TAL kind & type constructor verifier and manipulation utilities
 *
 * Kinds: subkind & equal kinds.
 * Type constructors: well formed of kind, nomalise, alpha equality
 * Utilities: unroll, size, stack size, seperate function type
 *)
 
open Utilities;;
open Identifier;;
open Tal;;
open Talctxt;;

(*** Statistics/Profiling Infrastructure ***)

let stats : (int ref * string) list ref = ref []
let click r = (fun () -> r := (!r) + 1);;
let new_stat s = 
  let r = ref 0 in begin stats := (r,s)::(!stats); click r end;;
let print_stats () = 
  List.iter 
    (fun (r,s) -> print_string s; print_string ": "; print_int (!r); 
      print_string "\n") (!stats)

let rename_count = new_stat "rename count";;
let fast_rename_count = new_stat "fast rename count";;
let sizeof_count = new_stat "sizeof"
let kindleq_count = new_stat "kindleq";;
let kindeq_count = new_stat "kindeq";;
let subst_one_count = new_stat "substitutions of one constructor";;
let subst_one_cutoff = new_stat "cutoff of substitutions of one constructor";;
let subst_count = new_stat "substitutions";;
let subst_cutoff = new_stat "substitution cutoffs";;
let check_count = new_stat "kind check";;
let whnorm_count = new_stat "weak-head normalization";; 
let fast_whead_count = new_stat "fast weak-head normalizations";; 
let normalize_count = new_stat "full normalizations";;
let norm_count = new_stat "norm calls";;
let check_whnorm_count = new_stat "kind check & weak-head normalize";;
let alphaeqcon_count = new_stat "alphaeqcon";;
let fast_alphaeq_count = new_stat "fast alphaeq";;
let alphaeqcon_nodes = new_stat "alphaeqcon nodes";;
let eqcon_count = new_stat "eqcon";;
let fast_eqcon_count = new_stat "fast eqcon";;
let unroll_count = new_stat "unroll count";;

let size_of_scale scale =
  match scale with
    Byte1 -> 1
  | Byte2 -> 2
  | Byte4 -> 4
  | Byte8 -> 8
;;

(*************************************************************************)
(* k1 <= k2, k1 = k2, and kind meet                                      *)
(*************************************************************************)

(* kindleq k1 k2:
 *   if     k1 <= k2 then ()
 *   if not k1 <= k2 then generate error Kindleq (k1,k2)
 *)

let rec kindleq ctxt k1 k2 =
  kindleq_count(); 
  if k1 == k2 then () else
  match k1,k2 with
    (Kbyte s1,Kbyte s2) when s1=s2 -> ()
  | (Kbyte _,Ktype) -> ()
  | (Ktype,Ktype) -> ()
  | (Kmemi i1,Kmemi i2) when i1=i2 -> ()
  | (Kmemi _,Kmem) -> ()
  | (Kmem,Kmem) -> ()
  | (Kstack,Kstack) -> ()
  | (Kint,Kint) -> ()
  | (Karrow(k1a,k1b),Karrow(k2a,k2b)) -> 
      (kindleq ctxt k2a k1a; kindleq ctxt k1b k2b)
  | (Kprod k1s,Kprod k2s) -> kindsleq ctxt (Kindleq (k1,k2)) k1s k2s
  | (_,_) -> generate_error ctxt (Kindleq (k1,k2))
and kindsleq ctxt ve k1s k2s =
  match k1s,k2s with
    ([],[]) -> ()
  | (k1::k1s,k2::k2s) -> (kindleq ctxt k1 k2; kindsleq ctxt ve k1s k2s)
  | (_,_) -> generate_error ctxt ve
;;

(* kindeq k1 k2:
 *   if k1  = k2 then ()
 *   if k1 != k2 then generate error Kindeq (k1,k2)
 *)

let rec kindeq ctxt k1 k2 =
  kindeq_count(); 
  if k1 == k2 then () else
  match k1,k2 with
    (Kbyte s1,Kbyte s2) when s1=s2 -> ()
  | (Ktype,Ktype) -> ()
  | (Kmemi i1,Kmemi i2) when i1=i2 -> ()
  | (Kmem,Kmem) -> ()
  | (Kstack,Kstack) -> ()
  | (Kint,Kint) -> ()
  | (Karrow(k1a,k1b),Karrow(k2a,k2b)) ->
      (kindeq ctxt k1a k2a; kindeq ctxt k2a k2b)
  | (Kprod k1s,Kprod k2s) -> kindseq ctxt (Kindeq (k1,k2)) k1s k2s
  | (_,_) -> generate_error ctxt (Kindeq (k1,k2))
and kindseq ctxt ve k1s k2s =
  match k1s,k2s with
    ([],[]) -> ()
  | (k1::k1s,k2::k2s) -> (kindeq ctxt k1 k2; kindseq ctxt ve k1s k2s)
  | (_,_) -> generate_error ctxt ve
;;

(* kindmeet k1 k2:
 *   if the meet of k1 & k2 exists return it
 *   otherwise generate error Kindmeet (k1,k2)
 * kindjoin k1 k2:
 *   if the join of k1 & k2 exists return it
 *   otherwise generate error Kindjoin (k1,k2)
 *)

let rec kindmeet ctxt k1 k2 =
  if k1==k2 then k1
  else match k1,k2 with
    Kbyte s1,Kbyte s2 when s1=s2 -> k1
  | Kbyte _,Ktype -> k1
  | Ktype,Kbyte _ -> k2
  | Ktype,Ktype -> Ktype
  | Kmemi i1,Kmemi i2 when i1=i2 -> k1
  | Kmemi _,Kmem -> k1
  | Kmem,Kmemi _ -> k2
  | Kmem,Kmem -> Kmem
  | Kstack,Kstack -> Kstack
  | Kint,Kint -> Kint
  | Karrow (k11,k12),Karrow (k21,k22) ->
      Karrow (kindjoin ctxt k11 k21,kindmeet ctxt k12 k22)
  | Kprod k1s,Kprod k2s -> Kprod (kindsmeet ctxt (Kindmeet (k1,k2)) k1s k2s)
  | _,_ -> generate_error ctxt (Kindmeet (k1,k2)); raise Talfail
and kindsmeet ctxt ve k1s k2s =
  match k1s,k2s with
    [],[] -> []
  | k1::k1s,k2::k2s -> (kindmeet ctxt k1 k2)::(kindsmeet ctxt ve k1s k2s)
  | _,_ -> generate_error ctxt ve; raise Talfail
and kindjoin ctxt k1 k2 =
  if k1==k2 then k1
  else match k1,k2 with
    Kbyte s1,Kbyte s2 -> if s1=s2 then k1 else Ktype
  | Ktype,(Kbyte _|Ktype) | (Kbyte _|Ktype),Ktype -> Ktype
  | Kmemi i1,Kmemi i2 when i1=i2 -> k1
  | (Kmemi _|Kmem),(Kmemi _|Kmem) -> Kmem
  | Kstack,Kstack -> Kstack
  | Kint,Kint -> Kint
  | Karrow (k11,k12),Karrow (k21,k22) ->
      Karrow (kindmeet ctxt k11 k21,kindjoin ctxt k12 k22)
  | Kprod k1s,Kprod k2s -> Kprod (kindsjoin ctxt (Kindjoin (k1,k2)) k1s k2s)
  | _,_ -> generate_error ctxt (Kindjoin (k1,k2)); raise Talfail
and kindsjoin ctxt ve k1s k2s =
  match k1s,k2s with
    [],[] -> []
  | k1::k1s,k2::k2s -> (kindjoin ctxt k1 k2)::(kindsjoin ctxt ve k1s k2s)
  | _,_ -> generate_error ctxt ve; raise Talfail
;;

(*************************************************************************)
(* D |- c : k  where D is a kind assignment                              *)
(*************************************************************************)

let error ctxt c s = generate_error ctxt (Conwf (c,s));;

(* primcon_kind returns the least kind of a primitive constructor *)
let k2 = Karrow(k4byte,k4byte)
let ks = Karrow(Kstack,k4byte)
let primcon_kind ctxt pc = 
  match pc with
    PCbytes sc -> Kbyte sc
  | PCjunk i -> Kmemi i
  | PCexn -> k4byte
  | PCexnname -> k2
  | PCint i -> Kint
;;

(* assumes the constructor has been checked already *)
let rec con_kind ctxt con =
  match con.rcon with
    Cvar a -> get_variable_kind ctxt a 
  | Clam(a,k1,c) -> 
      Karrow(k1,con_kind (add_var ctxt a k1) c)
  | Capp(c1,c2) ->
      (match con_kind ctxt c1 with
	Karrow(_,k2) -> k2
      |	_ -> error ctxt con "Capp: not a Karrow"; raise Talfail)
  | Ctuple cs -> Kprod(List.map (con_kind ctxt) cs)
  | Cproj(i,c') ->
      (match con_kind ctxt c' with
	Kprod ks ->
	  (try List.nth ks i with Failure _ -> 
	    error ctxt con "Cproj: index out of range"; raise Talfail)
      |	_ -> error ctxt con "Cproj: not a Kprod"; raise Talfail)
  | Clab l -> get_label_kind ctxt l
  | Cprim pc -> primcon_kind ctxt pc
  | Crec fs -> Kprod (List.map (fun (_,k,_) -> k) fs)
  | Cfield (c,_) ->
      (match con_kind ctxt c with
	Kbyte s -> Kmemi (size_of_scale s)
      |	Ktype -> Kmem
      |	_ -> error ctxt con "Cfield: not a T/Ti"; Kmem)
  | Cprod cs ->
      let rec aux n cs =
	match cs with
	  [] -> Kmemi n
	| c::cs ->
	    match con_kind ctxt c with
	      Kmemi i -> aux (n+i) cs
	    | _ -> Kmem in
      aux 0 cs
  | Csum cs ->
      (match cs with
	[] -> Kmem
      |	c::cs ->
	  match con_kind ctxt c with
	    Kmemi i ->
	      let rec aux cs =
		match cs with
		  [] -> Kmemi i
		| c::cs ->
		    match con_kind ctxt c with
		      Kmemi j when i=j -> aux cs
		    | _ -> Kmem in
	      aux cs
	  | _ -> Kmem)
  | Carray (c1,c2) ->
      (match con_kind ctxt c2 with
	Kmemi i ->
	  (match c1.rcon with
	    Cprim (PCint j) -> Kmemi (i*j)
	  | _ -> Kmem)
      |	_ -> Kmem)
  | Cempty -> Kstack
  | Ccons(_,_) -> Kstack
  | Cappend(_,_) -> Kstack
  (* Everything else is T4 *)
  | Cforall (_,_,_) | Cexist (_,_,_) | Ccode _ | Chptr (_,_) | Csing _
  | Csptr _ -> k4byte
;;

let singleton = Set.singleton id_compare
let empty_set = Set.empty id_compare

let rec rc_freevars (c : rcon) : identifier Set.set =
  match c with
    Cvar a -> singleton a
  | Clam(v,_,c) -> Set.delete (freevars c) v
  | Capp(c1,c2) -> Set.union (freevars c1) (freevars c2)
  | Ctuple cs -> unions (List.map freevars cs)
  | Cproj(_,c) -> freevars c
  | Clab _ -> empty_set
  | Cprim _ -> empty_set
  | Crec fs -> 
      let s =
 	List.fold_left (fun s (_,_,c) -> Set.union s (freevars c))
	  empty_set fs in
      List.fold_left (fun s (x,_,_) -> Set.delete s x) s fs
  | Cforall(v,k,c) -> Set.delete (freevars c) v
  | Cexist(v,k,c) -> Set.delete (freevars c) v
  | Ccode rs -> 
      rs_fold_reg (fun r c s -> Set.union s (freevars c)) rs empty_set
  | Chptr (_,co) -> (match co with None -> empty_set | Some c -> freevars c)
  | Cfield (c,_) -> freevars c
  | Cprod cs -> unions (List.map freevars cs)
  | Csum cs -> unions (List.map freevars cs)
  | Carray (c1,c2) -> Set.union (freevars c1) (freevars c2)
  | Csing c -> freevars c
  | Csptr c -> freevars c
  | Cempty -> empty_set
  | Ccons(c1,c2) -> Set.union (freevars c1) (freevars c2)
  | Cappend(c1,c2) -> Set.union (freevars c1) (freevars c2)
and unions (l : (identifier Set.set) list) : identifier Set.set = 
  List.fold_left Set.union empty_set l
and freevars (c : con) : identifier Set.set = 
  match c.freevars with
    None -> let s = rc_freevars c.rcon in c.freevars <- (Some s); s
  | Some s -> s
;;

(*************************************************************************)
(* [c'/a]c : capture-avoiding substitution for constructors              *)
(*************************************************************************)

let defvarcon x =
  { rcon=Cvar x;
    isnorm=true;
    freevars=Some(Set.singleton id_compare x)
  }
;;

let rename ((x,k,c) as t) ((d,s) as z) =
  rename_count();
  if Dict.member d x then
    (fast_rename_count(); (Dict.delete d x,s),t)
  else if Set.member s x then
    let x' = id_unique x in
    ((Dict.insert d x (defvarcon x'),s),(x',k,c))
  else (fast_rename_count(); (z,t))
;;

let rename_then f d t =
  let (d',(x,k,c)) = rename t d in
  (x,k,f d' c)
;;

(* applies the substitution d to c, alpha-converting c as necessary
 * in order to avoid capture. *)
let rec rcsubsts d con = 
  let c = con.rcon in
  subst_count(); 
  match c with
    Cvar a ->
      (* variable a may be free, return it if so *)
      (try Dict.lookup (fst d) a with Dict.Absent -> con)
  | Clam(x,k,c) -> 
     let (x',k',c') = rename_then substs d (x,k,c) in defcon(Clam(x',k',c'))
  | Capp(c1,c2) -> defcon(Capp(substs d c1, substs d c2))
  | Ctuple cs -> defcon(Ctuple(List.map (substs d) cs))
  | Cproj(i,c) -> defcon(Cproj(i,substs d c))
  | Clab _ -> con
  | Cprim _ -> con
  | Crec fs ->
      let g f (d,fs) = let (d',f') = rename f d in (d',f'::fs) in
      let (d',fs') = List.fold_right g fs (d,[]) in
      defcon(Crec (List.map (fun (x',k,c) -> (x',k,substs d' c)) fs'))
  | Cforall (x,k,c) -> 
      let (x',k',c') = rename_then substs d (x,k,c) in
      defcon(Cforall(x',k',c'))
  | Cexist (x,k,c) -> 
      let (x',k',c') = rename_then substs d (x,k,c) in
      defcon(Cexist(x',k',c'))
  | Ccode rs -> defcon(Ccode(rs_map_reg (substs d) rs))
  | Chptr (is,co) ->
      (match co with
 	None -> con
      | Some c -> defcon (Chptr (is,Some (substs d c))))
  | Cfield (c,v) -> defcon (Cfield (substs d c,v))
  | Cprod cs -> defcon (Cprod (List.map (substs d) cs))
  | Csum cs -> defcon (Csum (List.map (substs d) cs))
  | Carray (c1,c2) -> defcon (Carray (substs d c1,substs d c2))
  | Csing c -> defcon (Csing (substs d c))
  | Csptr c -> defcon (Csptr (substs d c))
  | Cempty -> con
  | Ccons (c1,c2) -> defcon(Ccons(substs d c1,substs d c2))
  | Cappend (c1,c2) -> defcon(Cappend(substs d c1, substs d c2))
and substs ((d,s) as p) c = 
  match c.freevars with
    None -> rcsubsts p c
  | Some cfreevars ->
      let (d,s) = 
	Dict.fold_dict 
	  (fun x c ((d,s) as z) -> 
	    if Set.member cfreevars x then 
	      (Dict.insert d x c,Set.union s (freevars c))
	    else z)
	  d (Dict.empty id_compare,Set.empty id_compare)
      in if Dict.is_empty d then (subst_cutoff(); c) else 
      let c = rcsubsts (d,s) c in (* freevars c;*) c
      (* JGM: calculating the freevars here seems to actually slow things
       * down...*)
;;

(* substitute c1 for free occurrences of x in c2 *)
let subst c1 x c2 = substs (Dict.singleton id_compare x c1,freevars c1) c2;;

let subst_one c1 x fv c2 = substs (Dict.singleton id_compare x c1,fv) c2;;

let substs_list l c =
  let aux (d,s) (x,c) = (Dict.insert d x c,Set.union s (freevars c)) in
  substs (List.fold_left aux (Dict.empty id_compare,Set.empty id_compare) l) c

let rec rcsubst ca a (fvs : identifier Set.set) con = 
  let c = con.rcon in
  subst_one_count(); 
  match c with
    Cvar x ->
      (* variable a may be free, return it if so *)
      if x = a then ca else con
  | Clam(x,k,c) -> 
      if x = a then (subst_one_cutoff(); con) else
      if Set.member fvs x then subst_one ca a fvs con 
      else defcon(Clam(x,k,subst ca a fvs c))
  | Capp(c1,c2) -> defcon(Capp(subst ca a fvs c1, subst ca a fvs c2))
  | Ctuple cs -> defcon(Ctuple(List.map (subst ca a fvs) cs))
  | Cproj(i,c) -> defcon(Cproj(i,subst ca a fvs c))
  | Clab _ -> con
  | Cprim _ -> con
  | Crec fs ->
      if List.exists (fun (x,_,_) -> x = a) fs then (subst_one_cutoff(); con)
      else if List.exists (fun (x,_,_) -> Set.member fvs x) fs then
	subst_one ca a fvs con
      else 
	defcon(Crec(List.map (fun (x,k,c) -> (x,k,subst ca a fvs c)) fs))
  | Cforall (x,k,c) -> 
      if x = a then (subst_one_cutoff(); con)
      else if Set.member fvs x then subst_one ca a fvs con
      else defcon(Cforall(x,k,subst ca a fvs c))
  | Cexist (x,k,c) -> 
      if x = a then (subst_one_cutoff(); con)
      else if Set.member fvs x then subst_one ca a fvs con
      else defcon(Cexist(x,k,subst ca a fvs c))
  | Ccode rs -> defcon(Ccode(rs_map_reg (subst ca a fvs) rs))
  | Chptr (is,co) ->
      (match co with
 	None -> con
      | Some c -> defcon (Chptr (is,Some (subst ca a fvs c))))
  | Cfield (c,v) -> defcon (Cfield (subst ca a fvs c,v))
  | Cprod cs -> defcon (Cprod (List.map (subst ca a fvs) cs))
  | Csum cs -> defcon (Csum (List.map (subst ca a fvs) cs))
  | Carray (c1,c2) -> defcon (Carray (subst ca a fvs c1,subst ca a fvs c2))
  | Csing c -> defcon (Csing (subst ca a fvs c))
  | Csptr c -> defcon (Csptr (subst ca a fvs c))
  | Cempty -> con
  | Ccons (c1,c2) -> defcon(Ccons(subst ca a fvs c1,subst ca a fvs c2))
  | Cappend (c1,c2) -> defcon(Cappend(subst ca a fvs c1, subst ca a fvs c2))
and subst ca a fvs c =
  match c.freevars with
    None -> rcsubst ca a fvs c
  | Some cfreevars ->
      if Set.member cfreevars a then
	rcsubst ca a fvs c
      else (subst_one_cutoff(); c)
;;
let subst ca a c = subst ca a (freevars ca) c

let substs d c =
  let s =
    Dict.fold_dict (fun x c s -> Set.union s (freevars c)) d
      (Set.empty id_compare) in
  substs (d,s) c
;;

(*************************************************************************)
(* Check constructor well formedness and canonicalise                    *)
(*************************************************************************)

(* l is sorted, removes duplicates *)
let remove_duplicates l =
  let rec aux l =
    match l with
      [] | [_] -> l
    | x1::(x2::rest as tl) ->
 	if x1=x2 then aux (x1::rest) else x1::(aux tl) in
  aux l
;;

(* A sum branch must start with a known tag.
 * The forms S(i)^_ and *[S(i)^_,...] are acceptable
 *)
let sum_index error c =
  match c.rcon with
    Cfield ({rcon=Csing {rcon=Cprim (PCint i)}},_) -> i
  | Cprod ({rcon=Cfield ({rcon=Csing {rcon=Cprim (PCint i)}},_)}::_) -> i
  | _ -> error (); raise Talfail
;;

let not_fun c = 
  (match c.rcon with
    Clam(_,_,_) -> false
  | _ -> true) ;;
let not_tuple c =
  (match c.rcon with
    Ctuple _ -> false
  | _ -> true) ;;
let not_prod c =
  (match c.rcon with
    Cprod _ -> false
  | _ -> true) ;;
let not_sum c =
  (match c.rcon with
    Csum _ -> false
  | _ -> true) ;;

(* checks the kind of a constructor, performs the substitutions entered in
 * the context, and returns the kind and new constructor.
 *)
let check ctxt c =
  check_count(); 
  let defcon b rc = {rcon=rc; isnorm=b; freevars=Some(rc_freevars rc)} in
  let rec ck (ctxt : ctxt) (con : con) =
    let c = con.rcon in
    match c with
      Cvar a -> 
 	(get_variable_kind ctxt a,defcon true c)
    | Clam(a,k1,c) -> 
	let (k2,c') = ck (add_var ctxt a k1) c in
	let c = defcon true (Clam(a,k1,c')) in
	(Karrow(k1,k2), c)
    | Capp(c1,c2) ->
	let (k1,c1) = ck ctxt c1 in
	let (k2,c2) = ck ctxt c2 in
	let isnorm = c1.isnorm & c2.isnorm & (not_fun c1) in
	begin
	  match k1 with
	    Karrow(ka,kb) -> 
	      kindleq ctxt k2 ka; (kb,defcon isnorm (Capp(c1,c2)))
	  | _ -> error ctxt con "Capp: not a Karrow"; raise Talfail
	end
    | Ctuple cs -> 
	let (ks,cs,isnorm) = 
	  List.fold_left 
	    (fun (ks,cs,isnorm) c ->
	      let (k,c) = ck ctxt c in (k::ks,c::cs,c.isnorm & isnorm))
	    ([],[],true) cs in
	(Kprod ks,defcon isnorm (Ctuple cs))
    | Cproj(i,c') ->
	let (k,c') = ck ctxt c' in
	let isnorm = c'.isnorm & (not_tuple c') in
	begin
	  match k with
	    Kprod ks ->
	      (try (List.nth ks i,defcon isnorm (Cproj(i,c'))) with
		Failure _ -> error ctxt con "Cproj: index out of range"; 
		  raise Talfail)
	  | _ -> error ctxt con "Cproj: not a Kprod"; raise Talfail
	end
    | Clab l ->
	let k = get_label_kind ctxt l in
	(k,defcon true c)
    | Cprim pc -> (primcon_kind ctxt pc,defcon true c)
    | Crec fs ->
	let g ctxt (a,k,_) = add_var ctxt a k in
	let ctxt' = List.fold_left g ctxt fs in
	let isnorm = ref true in
	let check_f (a,k,c) = 
	  let (k',c') = ck ctxt' c in
	  kindleq ctxt' k' k;
	  isnorm := (!isnorm) & c'.isnorm;
	  (a,k,c') in
	let fs = List.map check_f fs in
	let k = Kprod (List.map (fun (_,k,_) -> k) fs) in
	(k,defcon (!isnorm) (Crec fs))
    | Cforall(a,k,c) ->
	let (k',c') = ck (add_var ctxt a k) c in
	kindleq ctxt k' k4byte;
	(k4byte,defcon c'.isnorm (Cforall(a,k,c')))
    | Cexist(a,k,c) ->
	let (k',c') = ck (add_var ctxt a k) c in
	kindleq ctxt k' k4byte;
	(k4byte,defcon c'.isnorm (Cexist(a,k,c')))
    | Ccode rs ->
	let isnorm = ref true in
	let ck_dict c = 
	  let (k,c) = ck ctxt c in
	  begin
	    if not c.isnorm then isnorm := false;
	    kindleq ctxt k k4byte; c
	  end in
	let rs = rs_map_reg ck_dict rs in
 	(k4byte,defcon (!isnorm) (Ccode rs))
    | Chptr (is,co) ->
	let is = remove_duplicates (Sort.list (fun i j -> i<=j) is) in
	if not (List.for_all is_non_pointer_integer is) then
	  error ctxt con "Chptr: possible pointer tag";
	let (isnorm,co) =
	  match co with
	    None -> (true,None)
	  | Some c -> 
	      let (k',c') = ck ctxt c in
	      kindleq ctxt k' Kmem;
	      (c'.isnorm,Some c') in
	(k4byte,defcon isnorm (Chptr (is,co)))
    | Cfield (c,v) ->
	let (k',c') = ck ctxt c in
	let k =
	  match k' with
	    Kbyte s -> Kmemi (size_of_scale s)
	  | Ktype -> Kmem
	  | _ -> error ctxt con "Cfield: not a type"; Kmem in
	(k,defcon c'.isnorm (Cfield (c',v)))
    | Cprod cs ->
	let rec aux sz isnorm cs new_cs =
	  match cs with
	    [] ->
	      ((match sz with None -> Kmem | Some i -> Kmemi i),
	       defcon isnorm (Cprod (List.rev new_cs)))
	  | c::cs ->
	      let (k,c) = ck ctxt c in
	      let isnorm = isnorm & c.isnorm in
	      match k with
		Kmem -> aux None isnorm cs (c::new_cs)
	      |	Kmemi i ->
		  let sz = match sz with None -> None | Some j -> Some (i+j) in
		  aux sz isnorm cs (c::new_cs)
	      |	_ ->
		  error ctxt con "Cprod: not a Tm";
		  aux None isnorm cs (c::new_cs) in
	aux (Some 0) true cs []
    | Csum [] -> con.isnorm <- true; (Kmem,con)
    | Csum (c1::_ as cs) ->
	let sz =
	  match fst (ck ctxt c1) with
	    Kmem -> None
	  | Kmemi i -> Some i
	  | _ -> error ctxt con "Csum: not a Tm"; None in
	let rec aux sz isnorm cs new_cs =
	  match cs with
	    [] ->
	      (isnorm,(match sz with None -> Kmem | Some i -> Kmemi i),new_cs)
	  | c::cs ->
	      let (k,c) = ck ctxt c in
	      let isnorm = isnorm & c.isnorm in
	      let k =
	      	match k with
		  Kmem -> None
	      	| Kmemi i -> (match sz with Some j when i=j -> sz | _ -> None)
	      	| _ -> error ctxt con "Csum: not a Tm"; None in
	      let err () = error ctxt con "Csum: no tag" in
	      let i = sum_index err c in
	      aux sz isnorm cs ((i,c)::new_cs) in
	let (isnorm,k,ics) = aux sz true cs [] in
	let (is,cs) = List.split (Sort.list (fun (i,_) (j,_) -> i<=j) ics) in
	(k,defcon isnorm (Csum cs))
    | Carray (c1,c2) ->
	let (k1,c1) = ck ctxt c1
	and (k2,c2) = ck ctxt c2 in
	kindleq ctxt k1 Kint; kindleq ctxt k2 Kmem;
	let con = defcon (c1.isnorm & c2.isnorm) (Carray (c1,c2)) in
	(con_kind ctxt con,con)
    | Csing c ->
	let (k',c') = ck ctxt c in
	kindleq ctxt k' Kint;
	(k4byte,defcon c'.isnorm (Csing c'))
    | Csptr c ->
	let (k',c') = ck ctxt c in
	kindleq ctxt k' Kstack;
	(k4byte,defcon c'.isnorm (Csptr c'))
    | Cempty -> (Kstack,defcon true c)
    | Ccons(c1,c2) ->
	let (k1,c1) = ck ctxt c1 in
	let (k2,c2) = ck ctxt c2 in
	(match k1 with
	  Ktype | Kbyte _ | Kmem | Kmemi _ -> ()
	| _ -> error ctxt con "Ccons: head must be T or Tm");
 	kindleq ctxt k2 Kstack; 
	(Kstack,defcon (c1.isnorm & c2.isnorm) (Ccons(c1,c2)))
    | Cappend(c1,c2) ->
	let (k1,c1) = ck ctxt c1 in
	let (k2,c2) = ck ctxt c2 in	
	kindleq ctxt k1 Kstack; kindleq ctxt k2 Kstack;
	(Kstack,defcon false (Cappend(c1,c2))) in
  ck ctxt (substs (get_abbrevs ctxt) c)
;;

(* check a register state *)
let verify_gamma ctxt gamma =
  let ctxt = set_verify_ctxt ctxt "checking register state" in
  let f c = let (k,c') = check ctxt c in kindleq ctxt k k4byte; c' in
  rs_map_reg f gamma
;;

(*************************************************************************)
(* c ->* c' : normalization of constructors                              *)
(*************************************************************************)

(* weak-head normalization *)
let whnorm ctxt c =
  let rec wh (c : con) : con =
    whnorm_count(); 
    if c.isnorm then (fast_whead_count(); c) else 
    match c.rcon with
      Capp(c1,c2) ->
	begin
	  wh c1;
	  match c1.rcon with
	    Clam(x,k,c3) -> 
	      let c' = wh(subst c2 x c3) in
	      c.rcon <- c'.rcon; 
	      (*c.iswhead <- true;*)
	      c.freevars <- c'.freevars;
	      c'
	  | _ -> (*c.iswhead <- true;*) c
	end
    | Cproj(i,c1) ->
	begin
	  try 
	    wh c1;
	    match c1.rcon with
	      Ctuple cs -> 
		let c' = wh (List.nth cs i) in
		c.rcon <- c'.rcon; 
		(*c.iswhead <- true;*)
		c.freevars <- c'.freevars;
		c'
	    | _ -> (*c.iswhead <- true;*) c
	  with Failure _ -> failwith "Talcon.whnorm Cproj"
	end
    | Cappend(c1,c2) ->
	begin
	  wh c1;
	  match c1.rcon with
	    Cempty -> 
	      let c' = wh c2 in
	      c.rcon <- c'.rcon; 
	      (*c.iswhead <- true;*)
	      c.freevars <- c'.freevars;
	      c'
	  | Ccons(f,c1) -> 
	      c.rcon <- Ccons(f,defcon(Cappend(c1,c2)));
	      (*c.iswhead <- true;*)
	      c
	  | Cappend(ca,cb) -> 
	      c.rcon <- Cappend(ca,defcon(Cappend(cb,c2)));
	      wh c
	  | c1 -> (*c.iswhead <- true;*) c
	end
    | _ -> (*c.iswhead <- true;*) c
  in
  wh c
;;

(* normalization: assumes c is well-formed *)
let normalize ctxt c =
  normalize_count(); 
  let rec norm (c : con) : unit =
    if not c.isnorm then begin
      norm_count();
      let rec aux (c:rcon) : unit =
      	match c with
      	  Cvar _ -> ()
      	| Clam(x,k,c) -> norm c
      	| Capp(c1,c2) -> norm c1; norm c2
      	| Ctuple cs -> List.iter norm cs
      	| Cproj(i,c) -> norm c
      	| Clab _ -> ()
      	| Cprim _ -> ()
      	| Crec fs -> List.iter (fun (x,k,c) -> norm c) fs
      	| Cforall(x,k,c) -> norm c
      	| Cexist(x,k,c) -> norm c
      	| Ccode rs -> (rs_app_reg (fun r c -> norm c) rs)
      	| Chptr (_,co) -> (match co with None -> () | Some c -> norm c)
      	| Cfield (c,_) -> norm c
      	| Cprod cs -> List.iter norm cs
      	| Csum cs -> List.iter norm cs
      	| Carray (c1,c2) -> norm c1; norm c2
      	| Csing c -> norm c
      	| Csptr c -> norm c
      	| Cempty -> ()
      	| Ccons (c1,c2) -> norm c1; norm c2
      	| Cappend(c1,c2) -> norm c1; norm c2 in
      aux (whnorm ctxt c).rcon; c.isnorm <- true
    end in    
  norm c; c
;;

let check_whnorm ctxt c =
  check_whnorm_count(); 
  let (k,c) = check ctxt c in
  (k,whnorm ctxt c)

let verify_gamma_whnorm ctxt gamma =
  let ctxt = set_verify_ctxt ctxt "checking register state" in
  let f c = let (k,c') = check_whnorm ctxt c in kindleq ctxt k k4byte; c' in
  rs_map_reg f gamma
;;

(*************************************************************************)
(* c ==alpha c'                                                          *)
(*************************************************************************)

type alphactxt = (identifier*identifier) list * (identifier,kind) Dict.dict;;

let empty_ctxt = ([],Dict.empty id_compare);;
let extend c x1 x2 k : alphactxt =
  ((x1,x2)::(fst c),Dict.insert (snd c) x2 k)
;;
let rec compare error c x1 x2 =
  match c with
    [] -> if x1<>x2 then error ()
  | (y1,y2)::c ->
      if x1=y1 then
 	(if x2<>y2 then error ())
      else if x2=y2 then
 	error ()
      else compare error c x1 x2
;;

(* compare two constructors up to alpha-equivalence *)
let rec aeq error ctxt ((varmap,kenv) as ctx) c1 c2 = 
  if varmap=[] & c1 == c2 then fast_alphaeq_count();
  alphaeqcon_nodes(); 
  match c1.rcon,c2.rcon with
    (Cvar x,Cvar y) -> compare error varmap x y
  | (Clam(x1,k1,c1),Clam(x2,k2,c2)) ->
      kindeq ctxt k1 k2;
      aeq error ctxt (extend ctx x1 x2 k1) c1 c2
  | (Capp(c1a,c1b),Capp(c2a,c2b)) ->
      aeq error ctxt ctx c1a c2a;
      aeq error ctxt ctx c1b c2b
  | (Ctuple cs1, Ctuple cs2) -> aeqs error ctxt ctx cs1 cs2
  | (Cproj(i1,c1),Cproj(i2,c2)) ->
      if i1 = i2 then aeq error ctxt ctx c1 c2 else error ()
  | (Clab l1,Clab l2) -> if l1<>l2 then error ()
  | (Cprim pc1,Cprim pc2) -> if pc1 <> pc2 then error ()
  | (Crec fs1,Crec fs2) -> 
      let ctx2 = 
	List.fold_right2 
	  (fun (x1,k1,_) (x2,k2,_) ctx ->
	    (kindeq ctxt k1 k2; extend ctx x1 x2 k1))
	  fs1 fs2 ctx in
      List.iter2 (fun (_,_,c1) (_,_,c2) -> aeq error ctxt ctx2 c1 c2) fs1 fs2
  | (Cforall(x1,k1,c1),Cforall(x2,k2,c2)) ->
      kindeq ctxt k1 k2;
      aeq error ctxt (extend ctx x1 x2 k1) c1 c2
  | (Cexist(x1,k1,c1),Cexist(x2,k2,c2)) ->
      kindeq ctxt k1 k2;
      aeq error ctxt (extend ctx x1 x2 k1) c1 c2
  | (Ccode rs1,Ccode rs2) -> 
      (try
	rs_app_reg (fun r c1 -> aeq error ctxt ctx c1 (rs_get_reg rs2 r)) rs1;
	rs_app_reg (fun r _ -> rs_get_reg rs1 r) rs2
      with Dict.Absent -> error())
  | (Chptr (is1,co1),Chptr (is2,co2)) ->
      if is1=is2 then
	match co1,co2 with
	  None,None -> ()
	| Some c1,Some c2 -> aeq error ctxt ctx c1 c2
	| _,_ -> error ()
      else
	error ()
  | (Cfield (c1,v1),Cfield (c2,v2)) ->
      if v1=v2 then aeq error ctxt ctx c1 c2 else error ()
  | (Cprod cs1,Cprod cs2) -> aeqs error ctxt ctx cs1 cs2
  | (Csum cs1,Csum cs2) -> aeqs error ctxt ctx cs1 cs2
  | (Carray (c1a,c1b),Carray (c2a,c2b)) ->
      aeq error ctxt ctx c1a c2a;
      aeq error ctxt ctx c1b c2b
  | (Csing c1,Csing c2) -> aeq error ctxt ctx c1 c2
  | (Csptr c1,Csptr c2) -> aeq error ctxt ctx c1 c2
  | (Cempty,Cempty) -> ()
  | (Ccons(hd1,c1),Ccons(hd2,c2)) ->
      aeq error ctxt ctx hd1 hd2;
      aeq error ctxt ctx c1 c2
  | (Cappend(c1a,c1b),Cappend(c2a,c2b)) ->
      aeq error ctxt ctx c1a c2a;
      aeq error ctxt ctx c1b c2b
  | (_,_) -> error ()
and aeqs error ctxt ctx cs1 cs2 =
  try List.iter2 (aeq error ctxt ctx) cs1 cs2
  with Invalid_argument _ -> error ()
;;

let aeqcon error ctxt c1 c2 =
  alphaeqcon_count(); 
  aeq error ctxt empty_ctxt c1 c2
    (* could set c1 == c2 and force more sharing *)
;;

exception NotEq
let eqerror () = raise NotEq
let dieerror ctxt c1 c2 () = generate_error ctxt (Neqcon (c1,c2))

let eqcon ctxt c1 c2 =
  eqcon_count(); 
  if (c1 == c2) then fast_eqcon_count() else
  try aeqcon eqerror ctxt c1 c2 with NotEq -> 
    let c1 = normalize ctxt c1 in
    let c2 = normalize ctxt c2 in
    aeqcon (dieerror ctxt c1 c2) ctxt c1 c2;;

let alphaeqcon ctxt c1 c2 = aeqcon (dieerror ctxt c1 c2) ctxt c1 c2

(*************************************************************************)
(* Type constructor subtyping                                            *)
(*************************************************************************)

let rec subset l1 l2 =
  match l1,l2 with
    [],_ -> true
  | _::_,[] -> false
  | i1::l1',i2::l2' ->
      if i1=i2 then
 	subset l1' l2'
      else if i1>i2 then
 	subset l1 l2'
      else
      	false
;;

(* ctxt |- c1 <= c2 *)

let rec leqc error ctxt (ctx : alphactxt) exactsize c1 c2 =
  match c1.rcon,c2.rcon with
    Cvar x1,Cvar x2 -> compare error (fst ctx) x1 x2
  | Clam (v1,k1,c1),Clam (v2,k2,c2) ->
      kindeq ctxt k1 k2;
      leqc error ctxt (extend ctx v1 v2 k1) true c1 c2
  | Capp (c11,c12),Capp (c21,c22) ->
      leqc error ctxt ctx exactsize c11 c21;
      aeq error ctxt ctx c12 c22
  | Ctuple cs1,Ctuple cs2 ->
      let rec aux cs1 cs2 =
	match cs1,cs2 with
	  [],[] -> ()
	| c1::cs1,c2::cs2 -> leqc error ctxt ctx exactsize c1 c2; aux cs1 cs2
	| [],_::_ | _::_,[] -> error () in
      aux cs1 cs2
  | Cproj (i1,c1),Cproj (i2,c2) ->
      if i1=i2 then leqc error ctxt ctx exactsize c1 c2 else error ()
  | Clab l1,Clab l2 -> if l1<>l2 then error ()
  | Cprim pc1,Cprim pc2 -> if pc1<>pc2 then error ()
  | Crec fs1,Crec fs2 -> failwith "Talcon.leqc - Crec unimplemented"
  | Cforall (v1,k1,c1),Cforall (v2,k2,c2) ->
      kindleq ctxt k2 k1; leqc error ctxt (extend ctx v1 v2 k2) exactsize c1 c2
  | Cexist (v1,k1,c1),Cexist (v2,k2,c2) ->
      kindleq ctxt k1 k2; leqc error ctxt (extend ctx v1 v2 k1) exactsize c1 c2
  | Ccode rs1,Ccode rs2 -> leqrs error ctxt ctx rs2 rs1
  | Chptr (is1,co1),Chptr (is2,co2) ->
      if subset is1 is2 then
	match co1,co2 with
	  None,_ -> ()
	| Some _,None -> error ()
	| Some c1,Some c2 -> leqc error ctxt ctx false c1 c2
      else
	error ()
  | Cfield (c1,v1),Cfield (c2,v2) ->
      (match v2 with
	Read ->
	  if v1=Read or v1=ReadWrite then leqc error ctxt ctx exactsize c1 c2
	  else error ()
      |	Write ->
	  if v1=Write or v1=ReadWrite then leqc error ctxt ctx exactsize c2 c1
	  else error ()
      |	ReadWrite ->
	  if v1=ReadWrite then aeq error ctxt ctx c1 c2 else error ()
      |	Uninit -> 
	  if v1=Uninit or v1=ReadWrite then aeq error ctxt ctx c1 c2
	  else error ())
  | Cprod cs1,Cprod cs2 ->
      let rec aux cs1 cs2 =
      	match cs1,cs2 with
	  _,[] -> if exactsize & cs1<>[] then error ()
      	| [],_ -> error ()
      	| c1::cs1,c2::cs2 ->
	    leqc error ctxt ctx (exactsize or cs2<>[]) c1 c2; aux cs1 cs2 in
      aux cs1 cs2
  | Csum _,Csum [] ->
      if exactsize then kindleq ctxt (con_kind ctxt c1) (con_kind ctxt c2)
  | Csum cs1,Csum (c2::_ as cs2) ->
      let sz = match con_kind ctxt c2 with Kmemi i -> Some i | _ -> None in
      let rec aux1 sz cs1 cs2 =
	match cs2 with
	  [] ->
	    (if exactsize then
	      match sz with
		None -> ()
	      |	Some i ->
		  let chk c =
		    match con_kind ctxt c with Kmemi j when i=j -> ()
		    | _ -> error () in
		  List.iter chk cs1)
	| c2::cs2 ->
	    let i2 = sum_index error c2 in
	    aux2 sz cs1 i2 c2 cs2
      and aux2 sz cs1 i2 c2 cs2 =
	match cs1 with
	  [] -> error ()
	| c1::cs1 ->
	    let i1 = sum_index error c1 in
	    if i1=i2 then begin
	      leqc error ctxt ctx exactsize c1 c2;
	      let sz =
	    	match sz with
		  None -> sz
	    	| Some i ->
		    match con_kind ctxt c2 with Kmemi j when i=j -> sz
		    | _ -> None in
	      aux1 sz cs1 cs2
	    end else if i1<i2 then begin
	      if exactsize then
		(match sz with None -> ()
		| Some i ->
		    match con_kind ctxt c1 with Kmemi j when i=j -> ()
		    | _ -> error ());
	      aux2 sz cs1 i2 c2 cs2
	    end else
	      error () in
      aux1 sz cs1 cs2
  | Carray (c11,c12),Carray (c21,c22) ->
      if exactsize then
	aeq error ctxt ctx c11 c21
      else
      	leqc error ctxt ctx false c11 c21;
      leqc error ctxt ctx exactsize c12 c22
  | Csing c1,Csing c2 -> leqc error ctxt ctx exactsize c1 c2
  | Csing _,Cprim (PCbytes Byte4) -> ()
  | Csptr c1,Csptr c2 -> leqc error ctxt ctx false c1 c2
  | Cempty,Cempty -> ()
  | Ccons (c11,c12),Ccons (c21,c22) ->
      leqc error ctxt ctx true c11 c21;
      leqc error ctxt ctx exactsize c12 c22
  | Cappend (c11,c12),Cappend (c21,c22) -> 
      leqc error ctxt ctx true c11 c21;
      leqc error ctxt ctx exactsize c12 c22
  | _,_ -> error ()
and leqrs error ctxt ctx rs1 rs2 =
   let aux r c2 =
    try leqc error ctxt ctx false (rs_get_reg rs1 r) c2
    with Dict.Absent -> error () in
  rs_app_reg aux rs2
;;

let leqc_norm error ctxt c1 c2 =
  if (c1==c2) then
    ()
  else
    try leqc eqerror ctxt empty_ctxt false c1 c2
    with NotEq ->
      let c1 = normalize ctxt c1
      and c2 = normalize ctxt c2 in
      leqc error ctxt empty_ctxt false c1 c2
;;

let leqcon ctxt c1 c2 =
  let error () = generate_error ctxt (Nleqcon (c1,c2)) in
  leqc_norm error ctxt c1 c2
;;

let reg_state_leq ctxt gamma1 gamma2 =
  let error r () = generate_error ctxt (Rsnleq (r,gamma1,gamma2)) in
  let check1 r c2 =
    let ctxt =
      set_verify_ctxt ctxt ("register state leq @ "^(Talpp.string_of_reg r)) in
    try leqc_norm (error r) ctxt (rs_get_reg gamma1 r) c2
    with Dict.Absent -> error r ()
    | Talfail -> () in
  rs_app_reg check1 gamma2
;;

(* NG - For now conmeet & conjoin check only for types in a subtype relation
 *      and reg_state_meet & reg_state_join are complete except they call
 *      conmeet & conjoin
 *)
let rec conmeet ctxt c1 c2 =
  let ctxt' = error_handler ctxt (fun _ _ -> raise NotEq) in
  try leqcon ctxt' c1 c2; c1
  with NotEq -> try leqcon ctxt' c2 c1; c2
  with NotEq -> generate_error ctxt (Conmeet (c1,c2)); raise Talfail
and conjoin ctxt c1 c2 =
  let ctxt' = error_handler ctxt (fun _ _ -> raise NotEq) in
  try leqcon ctxt' c1 c2; c2
  with NotEq -> try leqcon ctxt' c2 c1; c1
  with NotEq -> generate_error ctxt (Conjoin (c1,c2)); raise Talfail
and reg_state_meet ctxt rs1 rs2 =
  let aux r c1 rs =
    try
      rs_set_reg rs r (conmeet ctxt c1 (rs_get_reg rs2 r))
    with Dict.Absent -> rs in
  rs_fold_reg aux rs1 rs_empty
and reg_state_join ctxt rs1 rs2 =
  let aux r c1 rs =
    rs_set_reg rs r
      (try conjoin ctxt c1 (rs_get_reg rs r)
      with Dict.Absent -> c1) in
  rs_fold_reg aux rs1 rs2
;;

(*************************************************************************)
(* Utilities                                                             *)
(*************************************************************************)

(* replace all singleton unions with single element *)
let from_union ctxt c =
  let rec aux c =
    match c.rcon with
      Cprod cs -> defcon (Cprod (List.map aux cs))
    | Csum [c] -> aux c
    | Csum cs -> defcon (Csum (List.map aux cs))
    | _ -> c in
  match  c.rcon with
    Chptr (is,Some c) -> defcon (Chptr (is,Some (aux c)))
  | _ -> c
;;
    
(* unroll a recursive type *)
let rec unroll_rec exact ctxt c =
  unroll_count(); 
  match c.rcon with
    Cproj (i,c1) ->
      (let c1 = whnorm ctxt c1 in
      match c1.rcon with
	Crec [(v,k,c2)] -> subst c v c2
      |	Crec fs ->
	  let aux (d,n) (v,_,_) =
	    let uc = if n=i then c else defcon (Cproj (n,c1)) in
	    (Dict.insert d v uc,n+1) in
	  let (d,_) = List.fold_left aux (Dict.empty id_compare,0) fs in
	  let (_,_,c2) =
	    try List.nth fs i
	    with Failure _ ->
	      generate_error ctxt (BadUnroll c); raise Talfail in
	  substs d c2
      |	_ ->
	  whnorm ctxt (defcon (Cproj (i,unroll_rec exact ctxt c))))
  | Capp (c1,c2) ->
      (let c1 = whnorm ctxt c1 in
      whnorm ctxt (defcon (Capp (unroll_rec exact ctxt c1,c2))))
  | Clab l ->
      (match get_label_def ctxt l with
	AbsCon -> generate_error ctxt (BadUnroll c); raise Talfail
      |	BoundCon c -> if exact then generate_error ctxt (BadUnroll c); c
      |	ConcCon c -> c)
  | _ -> generate_error ctxt (BadUnroll c); raise Talfail
;;

(* calculates the size (in bytes) of values who have type c *)	
let rec sizeof ctxt c =
  sizeof_count();
  match con_kind ctxt c with
    Kbyte s -> size_of_scale s
  | Kmemi i -> i
  | _ ->
      let c = normalize ctxt c in
      match con_kind ctxt c with
    	Kbyte s -> size_of_scale s
      | Kmemi i -> i
      | _ -> generate_error ctxt (Unknown_size c); raise Talfail
;;

(* Calclulate the size of a stack type *)
let rec sizeof_stack ctxt c =
  match (whnorm ctxt c).rcon with
    Cempty -> 0
  | Ccons (c1,c2) -> (sizeof ctxt c1) + (sizeof_stack ctxt c2)
  | Cappend (c1, c2) -> (sizeof_stack ctxt c1) + (sizeof_stack ctxt c2)
  | _ -> generate_error ctxt (Unknown_size c); 0
;;

(* From a tal function type c, separate abstracted type variables and value
   variables *)
let rec separate_fun_type ctxt c =
  match c.rcon with
    Cforall (v,k,c) -> 
      let (vks, regstate) = separate_fun_type ctxt c in
      ((v,k) :: vks, regstate)
  | Ccode regstate -> ([], regstate)
  | _ -> generate_error ctxt (Conwf (c,"not a function type")); raise Talfail
;;

(*************************************************************************)
(* Field/Stack Slot Utilities                                            *)
(*************************************************************************)

let rec get_mem_offset_p ctxt c offset depth =
  let c = whnorm ctxt c in
  match c.rcon with
    Cprod cs ->
      let (f,c,i) = get_mem_offset_l ctxt cs offset depth in
      ((fun c -> cprod (f c)),c,i)
  | Ccons (c1,c2) ->
      if offset=0 then
	if depth=None then
	  let (f,con) = get_max_depth ctxt c1 in
	  ((fun c -> ccons (f c) c2),con,0)
	else
	  ((fun c -> ccons c c2),c1,0)
      else
      	let c1s = sizeof ctxt c1 in
      	if c1s<=offset then
	  let (f,c,i) = get_mem_offset_p ctxt c2 (offset-c1s) depth in
	  ((fun c -> ccons c1 (f c)),c,i)
      	else
	  (match depth with
	    None ->
	      let (f,c,i) = get_mem_offset_p ctxt c1 offset depth in
	      ((fun c -> ccons (f c) c2),c,i)
	  | Some 0 ->
	      (id,c1,offset)
	  | Some n ->
	      let (f,c,i) = get_mem_offset_p ctxt c1 offset (Some (n-1)) in
	      ((fun c -> ccons (f c) c2),c,i))
  | _ ->
      match depth with
	None | Some 0 -> (id,c,offset)
      | Some d -> generate_error ctxt (Bad_depth d); raise Talfail
and get_mem_offset_l ctxt cs offset depth =
  match cs with
    [] -> generate_error ctxt (Bad_offset offset); raise Talfail
  | c::cs ->
      if offset=0 then
	if depth=None then
	  let (f,con) = get_max_depth ctxt c in
	  ((fun c -> (f c)::cs),con,0)
	else
	  ((fun c -> c::cs),c,0)
      else
      	let csize = sizeof ctxt c in
      	if csize<=offset then
	  let (f,con,i) = get_mem_offset_l ctxt cs (offset-csize) depth in
	  ((fun c' -> c::(f c')),con,i)
      	else
	  match depth with
	    None ->
	      let (f,con,i) = get_mem_offset_p ctxt c offset depth in
	      ((fun c -> (f c)::cs),con,i)
	  | Some 0 ->
	      ((fun c -> c::cs),c,offset)
	  | Some n ->
	      let (f,con,i) = get_mem_offset_p ctxt c offset (Some (n-1)) in
	      ((fun c -> (f c)::cs),con,i)
and get_max_depth ctxt c =
  match (whnorm ctxt c).rcon with
  | Cprod (c::cs) ->
      let (f,con) = get_max_depth ctxt c in ((fun c -> cprod (c::cs)),con)
  | _ -> (id,c)
;;

let get_mem_offset ctxt cs offset depth =
  let (f,c,i) = get_mem_offset_p ctxt cs offset depth in
  if i<>0 then
    (generate_error ctxt (Bad_offset i); raise Talfail)
  else
    (f,c)
;;

(* verify that the stack constructor c1 is a tail of stack constructor c2.
 * assumes c1,c2 normalized and returns a function, which when given a 
 * mutated version of c1, generates the corresponding mutated version of c2.
 * (see assign_simple_path below).  That is, we verify that there exists
 * a c3 such that Cappend(c1,c3) = c2 and return a function which maps
 * c1' to Cappend(c1',c3).
 *
 * JGM: this is a stupid algorithm for doing this, but will probably
 * work well in practice.
 *)
exception Tryrest
let verify_stack_tail ctxt c1 c2 =
  let ctxt' = error_handler ctxt (fun _ _ -> raise Tryrest) in
  let rec aux c2 =
    try
      eqcon ctxt' c1 c2;
      id
    with
      Tryrest -> 
      	(match (whnorm ctxt c2).rcon with
	  Ccons(ca,cb) -> 
	    let f = aux cb in (fun c -> ccons ca (f c))
	| Cappend(ca,cb) ->
	    let f = aux cb in (fun c -> defcon(Cappend(ca,f c)))
	| _ -> generate_error ctxt (Not_tail (c1,c2)); id)
  in
  aux c2
;;

let write_stack_rest ctxt c1 size c2 =
  let c1s = sizeof ctxt c1 in
  let rec aux size c2 =
    if size=c1s then
      c2
    else if size>c1s then
      ccons (pcjunk (size-c1s)) c2
    else
      match (whnorm ctxt c2).rcon with
	Ccons (c1,c2) -> aux (size+(sizeof ctxt c1)) c2
      |	_ -> generate_error ctxt Stack_write_alignment; raise Talfail in
  ccons c1 (aux size c2)
;;

let rec write_stack_offset ctxt cs i c =
  match (whnorm ctxt cs).rcon with
    Ccons (c1,c2) ->
      let c1s = sizeof ctxt c1 in
      if i<c1s then
	let c2 = write_stack_rest ctxt c (c1s-i) c2 in
	if i>0 then ccons (pcjunk i) c2 else c2
      else
	ccons c1 (write_stack_offset ctxt c2 (i-c1s) c)
  | _ -> generate_error ctxt (Bad_offset i); raise Talfail
;;

let rec get_stack_tail ctxt i con =
  match i,(whnorm ctxt con).rcon with
    0,_ -> con
  | i,Ccons (c,con) ->
      let sc = sizeof ctxt c in
      if sc>i then
	ccons (pcjunk (sc-i)) con
      else if sc=i then
	con
      else
	get_stack_tail ctxt (i-sc) con
  | _,_ -> generate_error ctxt (Bad_offset i); raise Talfail
;;

(* EOF: talcon.ml *)
