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


(* Hacked by Dan to profile and try to improve running time.
   Changes:
     1. Removed statistics since they're work and the profiler does it better
     2. Re-wrote kindleq so common case could be inlined.
 *)

(* 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 Numtypes;;
open Identifier;;
open Tal;;
open Talctxt;;

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

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

let rec kindleq ctxt k1 k2 =
  if k1 == k2 then () else kindleq' ctxt k1 k2
and kindleq' ctxt k1 k2 =
  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
(* Cyclone *)
  | (Ktstack,Ktstack) -> ()
(* End Cyclone *)
  | (_,_) -> 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 =
  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)
(* Cyclone *)
  | Ktstack,Ktstack -> Ktstack
(* End Cyclone *)
  | _,_ -> 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)
(* Cyclone *)
  | Ktstack,Ktstack -> Ktstack
(* End Cyclone *)
  | _,_ -> 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
;;

(*************************************************************************)
(* ctxt |- c : k                                                         *)
(*************************************************************************)

(* These functions return the least kind of a constructor in a given context.
 * They assume that the constructor is well formed and has been checked and
 * put into a canonical form.
 *)

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

let km2t4 = Karrow (Kmem,k4byte)

let primcon_kind ctxt pc = 
  match pc with
    PCbytes sc -> Kbyte sc
  | PCjunk i -> Kmemi i
  | PCexn -> k4byte
  | PCexnname -> km2t4
  | PCint i -> Kint
;;

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 (scale_to_int32 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 i32_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
(* Cyclone *)
  | Ctempty -> Ktstack
  | Ctcons(_,_) -> Ktstack
  | Ctmpl _ | Ctrgn _ | Ctptr _ -> k4byte
(* End Cyclone *)
  (* Everything else is T4 *)
  | Cforall (_,_,_) | Cexist (_,_,_) | Ccode _ | Chptr (_,_) | Csing _
  | Csptr _ -> k4byte
;;

(*************************************************************************)
(* Free variables of a constructor                                       *)
(*************************************************************************)

(* Calculates the free variables of a constructor and updates the freevars
 * field.  No assumptions about well formedness or canonical form.
 *)

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 -> 
      let s1 = 
	(match rs_get_tla rs with None -> empty_set | Some c -> freevars c)
      in rs_fold_reg (fun r c s -> Set.union s (freevars c)) rs s1
  | 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)
(* Cyclone *)
  | Ctmpl(c1,c2_opt,labels,holes) ->
      let c2_fv =
        match c2_opt with None -> empty_set | Some c2 -> freevars c2 in
      List.fold_right
        (fun (i,c) fvs -> Set.union (freevars c) fvs)
        (labels@holes)
        (Set.union (freevars c1) c2_fv)
  | Ctptr _ -> empty_set
  | Ctrgn(c1,None,_) -> freevars c1
  | Ctrgn(c1,Some c2,t) ->
      let regions = List.map (fun (i,_,_) -> i) t in
      let cons =
        List.concat
          (List.map
             (fun (_,labels,holes) ->
               (List.map (fun (_,c) -> c) labels)
               @(List.map (fun (_,c) -> c) holes))
             t) in
      List.fold_left
        Set.insert
        (List.fold_right
           (fun c fvs -> Set.union (freevars c) fvs)
           cons
           (Set.union (freevars c1) (freevars c2)))
        regions
  | Ctcons(c1,c2) -> Set.union (freevars c1) (freevars c2)
  | Ctempty -> empty_set
(* End Cyclone *)
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
;;

(*************************************************************************)
(* Capture avoiding substitution for constructors                        *)
(*************************************************************************)

(* These functions do capture avoiding substitution on constructors.
 * There are two main forms:
 *   subst c1 x c2 = c2{x:=c1}
 *   substs d c = c{d}
 * But many auxilary functions to make this all go fast.  First, there are
 * functions optimised for single variable case rcsubsta & substa.  substa
 * checks for cutoff and rcsubsta does the actual substitution.  Second, there
 * are functions for multiple substitutions rcsubstsa & substsa.  Again,
 * substsa does a cutoff check and rcsubsta does the substitution.  The
 * functions only rename if necessary.  Since renaming requires multiple
 * substitutions, rcsubsta fails over to rcsubstsa via subst12d if renaming is
 * required.  Renaming is actually done by the function rename.
 *
 * Requires free variable calculation.  No assumptions about well formedness or
 * canonical form.
 *)

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

(* Do renaming if necessary.
 * Current substitutions are d where s=fv(ran(d)).
 * x of kind k binding in c is to be renamed if necessary.
 * If x in dom(d) then remove that substitution.
 * If x in s then renaming necessary.
 * Otherwise no conflicts to keep same name.
 * Ouput: new d,s pair, new (x,k,c) triple.
 *)
let rename ((x,k,c) as t) ((d,s) as z) =
  if Dict.member d x then
    ((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 (z,t)
;;

(* Rename then apply f to c in t
 *  - discards new d,s pair and returns new (x,k,c) triple
 *)
let rename_then f p t =
  let (p',(x,k,c)) = rename t p in
  (x,k,f p' c)
;;

(* Actually do multiple substitutions *)
(* con{d} where fvs=fv(ran(d)) *)
let rec rcsubstsa (d,fvs as p) con = 
  match con.rcon with
    Cvar a ->
      (try Dict.lookup d a with Dict.Absent -> con)
  | Clam(x,k,c) -> 
     let (x',k',c') = rename_then substsa p (x,k,c) in defcon(Clam(x',k',c'))
  | Capp(c1,c2) -> defcon(Capp(substsa p c1, substsa p c2))
  | Ctuple cs -> defcon(Ctuple(List.map (substsa p) cs))
  | Cproj(i,c) -> defcon(Cproj(i,substsa p c))
  | Clab _ -> con
  | Cprim _ -> con
  | Crec fs ->
      let g f (p,fs) = let (p',f') = rename f p in (p',f'::fs) in
      let (p',fs') = List.fold_right g fs (p,[]) in
      defcon (Crec (List.map (fun (x',k,c) -> (x',k,substsa p' c)) fs'))
  | Cforall (x,k,c) -> 
      let (x',k',c') = rename_then substsa p (x,k,c) in
      defcon(Cforall(x',k',c'))
  | Cexist (x,k,c) -> 
      let (x',k',c') = rename_then substsa p (x,k,c) in
      defcon(Cexist(x',k',c'))
  | Ccode rs -> defcon(Ccode(rs_map (substsa p) rs))
  | Chptr (is,co) ->
      (match co with
 	None -> con
      | Some c -> defcon (Chptr (is,Some (substsa p c))))
  | Cfield (c,v) -> defcon (Cfield (substsa p c,v))
  | Cprod cs -> defcon (Cprod (List.map (substsa p) cs))
  | Csum cs -> defcon (Csum (List.map (substsa p) cs))
  | Carray (c1,c2) -> defcon (Carray (substsa p c1,substsa p c2))
  | Csing c -> defcon (Csing (substsa p c))
  | Csptr c -> defcon (Csptr (substsa p c))
  | Cempty -> con
  | Ccons (c1,c2) -> defcon(Ccons(substsa p c1,substsa p c2))
  | Cappend (c1,c2) -> defcon(Cappend(substsa p c1, substsa p c2))
(* Cyclone *)
  | Ctempty -> con
  | Ctcons (c1,c2) -> defcon(Ctcons(substsa p c1,substsa p c2))
  | Ctmpl(c1,c2_opt,labels,holes) ->
      let c2_subst =
        match c2_opt with None -> None | Some c2 -> Some(substsa p c2) in
      defcon(Ctmpl(substsa p c1,
                   c2_subst,
                   List.map (fun (i,c) -> (i,substsa p c)) labels,
                   List.map (fun (i,c) -> (i,substsa p c)) holes))
  | Ctptr _ -> con
  | Ctrgn(c1,None,t) ->
      defcon(Ctrgn(substsa p c1, None,
                   List.map
                     (fun (v,labels,holes) ->
                       (v,
                        List.map
                          (fun (i,c) -> (i,substsa p c))
                          labels,
                        List.map
                          (fun (i,c) -> (i,substsa p c))
                          holes))
                     t))
  | Ctrgn(c1,Some c2,t) ->
      defcon(Ctrgn(substsa p c1, Some(substsa p c2), 
                   List.map
                     (fun (v,labels,holes) ->
                       (v,
                        List.map
                          (fun (i,c) -> (i,substsa p c))
                          labels,
                        List.map
                          (fun (i,c) -> (i,substsa p c))
                          holes))
                     t))
(* End Cyclone *)
(* Multiple substitutions - check for cutoff otherwise rcsubstsa *)
(* c{d} where s=fv(ran(d)) *)
and substsa (d,_ as p) c = 
  match c.freevars with
    None -> rcsubstsa p c
  | Some cfvs ->
      let aux x c (d,fvs as z) = 
	if Set.member cfvs x then
	  (Dict.insert d x c,Set.union fvs (freevars c))
	else z in
      let d,_ as p = Dict.fold_dict aux d (Dict.empty id_compare,empty_set) in
      if Dict.is_empty d then
	c
      else 
      	rcsubstsa p c
;;

(* Fail over function when rcsubsta needs to do renaming *)
(* c2{x:=c1} where fvs=fv(c1) *)
let subst12d c1 x fvs c2 = substsa (Dict.singleton id_compare x c1,fvs) c2;;

(* Actually do single substitution *)
(* con{a:=ca} where fvs=fv(ca) *)
let rec rcsubsta ca a fvs con = 
  match con.rcon with
    Cvar x ->
      if (id_compare x a)=0 then ca else con
  | Clam(x,k,c) -> 
      if (id_compare x a)=0 then con
      else if Set.member fvs x then subst12d ca a fvs con 
      else defcon(Clam(x,k,substa ca a fvs c))
  | Capp(c1,c2) -> defcon(Capp(substa ca a fvs c1, substa ca a fvs c2))
  | Ctuple cs -> defcon(Ctuple(List.map (substa ca a fvs) cs))
  | Cproj(i,c) -> defcon(Cproj(i,substa ca a fvs c))
  | Clab _ -> con
  | Cprim _ -> con
  | Crec fs ->
      if List.exists (fun (x,_,_) -> (id_compare x a)=0) fs then
	con
      else if List.exists (fun (x,_,_) -> Set.member fvs x) fs then
	subst12d ca a fvs con
      else 
	defcon(Crec(List.map (fun (x,k,c) -> (x,k,substa ca a fvs c)) fs))
  | Cforall (x,k,c) -> 
      if (id_compare x a)=0 then con
      else if Set.member fvs x then subst12d ca a fvs con
      else defcon(Cforall(x,k,substa ca a fvs c))
  | Cexist (x,k,c) -> 
      if (id_compare x a)=0 then con
      else if Set.member fvs x then subst12d ca a fvs con
      else defcon(Cexist(x,k,substa ca a fvs c))
  | Ccode rs -> defcon(Ccode(rs_map (substa ca a fvs) rs))
  | Chptr (is,co) ->
      (match co with
 	None -> con
      | Some c -> defcon (Chptr (is,Some (substa ca a fvs c))))
  | Cfield (c,v) -> defcon (Cfield (substa ca a fvs c,v))
  | Cprod cs -> defcon (Cprod (List.map (substa ca a fvs) cs))
  | Csum cs -> defcon (Csum (List.map (substa ca a fvs) cs))
  | Carray (c1,c2) -> defcon (Carray (substa ca a fvs c1,substa ca a fvs c2))
  | Csing c -> defcon (Csing (substa ca a fvs c))
  | Csptr c -> defcon (Csptr (substa ca a fvs c))
  | Cempty -> con
  | Ccons (c1,c2) -> defcon(Ccons(substa ca a fvs c1,substa ca a fvs c2))
  | Cappend (c1,c2) -> defcon(Cappend(substa ca a fvs c1, substa ca a fvs c2))
(* Cyclone *)
  | Ctptr _ -> con
  | Ctempty -> con
  | Ctcons (c1,c2) -> defcon(Ctcons(substa ca a fvs c1,substa ca a fvs c2))
  | Ctmpl (c1,c2_opt,labels,holes) ->
      let c2_substa =
        match c2_opt with None -> None | Some c2 -> Some(substa ca a fvs c2) in
      defcon(Ctmpl(substa ca a fvs c1,
                   c2_substa,
                   List.map (fun (i,c) -> (i,substa ca a fvs c)) labels,
                   List.map (fun (i,c) -> (i,substa ca a fvs c)) holes))
  | Ctrgn (c1,None,t) ->
      defcon(Ctrgn(substa ca a fvs c1,
                   None,
                   List.map
                     (fun (v,labels,holes) ->
                       (v,
                        List.map
                          (fun (i,c) -> (i,substa ca a fvs c))
                          labels,
                        List.map
                          (fun (i,c) -> (i,substa ca a fvs c))
                          holes))
                     t))
  | Ctrgn (c1,Some c2,t) ->
      defcon(Ctrgn(substa ca a fvs c1,
                   Some(substa ca a fvs c2),
                   List.map
                     (fun (v,labels,holes) ->
                       (v,
                        List.map
                          (fun (i,c) -> (i,substa ca a fvs c))
                          labels,
                        List.map
                          (fun (i,c) -> (i,substa ca a fvs c))
                          holes))
                     t))
(* End Cyclone *)
(* Single substitution - check for cutoff otherwise rcsubsta *)
(* c{a:=ca} where fvs=fv(ca) *)
and substa ca a fvs c =
  match c.freevars with
    None -> rcsubsta ca a fvs c
  | Some cfvs ->
      if Set.member cfvs a then
	rcsubsta ca a fvs c
      else 
 	c
;;

(*** Substitution entry points ***)

(* c{a:=ca} *)
let subst ca a c = substa ca a (freevars ca) c;;

(* c{d} *)
let substs d c =
  let aux x c s = Set.union s (freevars c) in
  let s = Dict.fold_dict aux d empty_set in
  substsa (d,s) c
;;

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

(* Check the well formedness of a constructor, put it into canonical form,
 * and return its kind.  Also computes the normal form flag and free variable
 * set.
 *
 * Requires substitution, free variable calculation, constructor kinding, and
 * kind functions.
 *)

(* Canonical form:
 *   + Abbrevs expanded
 *   + Tags are non-pointer integers
 *   + Tags sorted and unique
 *   + Sum branches have an index
 *   + Sum branches sorted
 *)

(* 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) ;;

let expand_abbrevs ctxt c = substs (get_abbrevs ctxt) c;;

(* checks the kind of a constructor, expands abbrevs entered in the context,
 * and returns the kind and new constructor.
 *)
let check ctxt c =
  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 ->
	(* JGM: we could be a bit stronger here and verify that in fact
	 * the TLA is a pointer to a tuple, but then what the hell --
	 * you can't use it if it's not.
	 *)
	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 ck_dict rs in
(* Cyclone *)
        let rs =
          begin
            try
              match Tal.get_cyclone_field rs with
                None -> rs
              | Some(c,v) ->
                  let (k,c) = ck ctxt c in
                  kindleq ctxt k Ktstack;
                  Tal.set_cyclone_field rs c v
            with Failure "get_cyclone_field" ->
              error ctxt cbyte4 "Ccode: bad type for tla";
              rs
          end in
(* End Cyclone *)
 	(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 (scale_to_int32 s)
	  | Ktype -> Kmem
(* Cyclone *)
	  | Ktstack -> Kmem
(* End Cyclone *)
	  | _ -> 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 i32_0) true cs []
    | Csum [] -> con.isnorm <- true; freevars con; (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 _,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)))
(* Cyclone *)
    | Ctptr _ -> (k4byte,defcon true c)
    | Ctempty -> (Ktstack,defcon true c)
    | Ctcons(c1,c2) ->
	let (k1,c1) = ck ctxt c1 in
	let (k2,c2) = ck ctxt c2 in
	kindleq ctxt k1 k4byte;
 	kindleq ctxt k2 Ktstack;
	(Ktstack,defcon (c1.isnorm & c2.isnorm) (Ctcons(c1,c2)))
    | Ctmpl(c1,c2_opt,labels,holes) ->
	let (k1,c1) = ck ctxt c1 in
	kindleq ctxt k1 k4byte;
	let isnorm = ref c1.isnorm in
	let c2_opt =
          match c2_opt with
            None -> None
          | Some c2 ->
              let (k2,c2) = ck ctxt c2 in
	      kindleq ctxt k2 k4byte;
	      if not c2.isnorm then isnorm := false;
              Some c2
        in
        let ck_id_con (i,c) =
          begin
            let (k,c) = ck ctxt c in
	    if not c.isnorm then isnorm := false;
	    kindleq ctxt k k4byte;
            (i,c)
          end in
        (* SHOULD CHECK THAT LABELS & HOLES ARE UNIQUE *)
        let labels = List.map ck_id_con labels in
        let holes = List.map ck_id_con holes in
 	(k4byte,defcon (!isnorm) (Ctmpl(c1,c2_opt,labels,holes)))
    | Ctrgn(c1,None,t) ->
	let (k1,c1) = ck ctxt c1 in
	let isnorm = ref c1.isnorm in
        let t =
          List.map
            (fun (a,labels,holes) ->
              let ck_id_con (i,c) =
                begin
                  let (k,c) = ck ctxt c in
                  if not c.isnorm then isnorm := false;
                  kindleq ctxt k k4byte;
                  (i,c)
                end in
              (* SHOULD CHECK THAT LABELS & HOLES ARE UNIQUE *)
              let labels = List.map ck_id_con labels in
              let holes = List.map ck_id_con holes in
              (a,labels,holes))
            t in
 	(k4byte,defcon (!isnorm) (Ctrgn(c1,None,t)))
    | Ctrgn(c1,Some c2,t) ->
	let (k1,c1) = ck ctxt c1 in
	let (k2,c2) = ck ctxt c2 in
	let isnorm = ref (c1.isnorm & c2.isnorm) in
        let t =
          List.map
            (fun (a,labels,holes) ->
              let ck_id_con (i,c) =
                begin
                  let (k,c) = ck ctxt c in
                  if not c.isnorm then isnorm := false;
                  kindleq ctxt k k4byte;
                  (i,c)
                end in
              (* SHOULD CHECK THAT LABELS & HOLES ARE UNIQUE *)
              let labels = List.map ck_id_con labels in
              let holes = List.map ck_id_con holes in
              (a,labels,holes))
            t in
 	(k4byte,defcon (!isnorm) (Ctrgn(c1,Some c2,t)))
(* End Cyclone *)
  in
  ck ctxt (expand_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
(* Cyclone *)
  let gamma =
    begin
      try
        match Tal.get_cyclone_field gamma with
          None -> gamma
        | Some(c,v) ->
            let (k,c) = check ctxt c in
            kindleq ctxt k Ktstack;
            Tal.set_cyclone_field gamma c v
      with Failure "get_cyclone_field" ->
        error ctxt cbyte4 "verify_gamma: bad type for tla";
        gamma
    end in 
(* End Cyclone *)
  rs_map_reg f gamma
;;

(*************************************************************************)
(*** From here on, all functions assume the constructors are checked!  ***)
(*************************************************************************)

(*************************************************************************)
(* Normalization of constructors                                         *)
(*************************************************************************)

(* Requires substitution *)

(* weak-head normalization *)
let whnorm ctxt c =
  let rec wh (c : con) : con =
    if c.isnorm then 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
;;

(* Full normalisation *)
let normalize ctxt c =
  let rec norm c =
    if not c.isnorm then begin
      let rec aux c =
      	match c with
      	  Cvar _ -> ()
      	| Clam (_,_,c) -> norm c
      	| Capp (c1,c2) -> norm c1; norm c2
      	| Ctuple cs -> List.iter norm cs
      	| Cproj (_,c) -> norm c
      	| Clab _ -> ()
      	| Cprim _ -> ()
      	| Crec fs -> List.iter (fun (x,k,c) -> norm c) fs
      	| Cforall (_,_,c) -> norm c
      	| Cexist (_,_,c) -> norm c
      	| Ccode rs -> (rs_app (fun 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
(* Cyclone *)
        | Ctempty -> ()
        | Ctcons(c1,c2) -> norm c1; norm c2
        | Ctptr _ -> ()
        | Ctmpl(c1,c2_opt,labels,holes) ->
            begin
              norm c1;
              (match c2_opt with None -> () | Some c2 -> norm c2);
              List.iter (fun (i,c) -> norm c) labels;
              List.iter (fun (i,c) -> norm c) holes
            end
        | Ctrgn(c1,None,t) ->
            begin
              norm c1;
              List.iter
                (fun (_,labels,holes) ->
                  List.iter
                    (fun (i,c) -> norm c) labels;
                  List.iter
                    (fun (i,c) -> norm c) holes)
                t
            end
        | Ctrgn(c1,Some c2,t) ->
            begin
              norm c1;
              norm c2;
              List.iter
                (fun (_,labels,holes) ->
                  List.iter
                    (fun (i,c) -> norm c) labels;
                  List.iter
                    (fun (i,c) -> norm c) holes)
                t
            end
(* End Cyclone *)
      in
      aux (whnorm ctxt c).rcon; c.isnorm <- true
    end in    
  norm c; c
;;

(* Check and then return kind & weak head normal form - con *)
let check_whnorm ctxt c =
  let (k,c) = check ctxt c in
  (k,whnorm ctxt c)

(* Check and then return kind & weak head normal form - reg state *)
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
;;

(*************************************************************************)
(* Equality of type constructors, alpha equality of type constructors    *)
(*************************************************************************)

(* Computes c1 =a c2 & c1 =c2
 * Assumes checked and canonicalised constructors.
 * Requires normalisation function.
 *)

(* Alpha equality and also subtyping is done in an "alpha context" which
 * maps type variables from c1 to types variables in c2 that are supposed to
 * be equal.
 *
 * An alpha context consists of a list of pairs (x,y).  If an x appears in the
 * list then it is bound in c1 by an outer constructor and maps to the y of c2.
 * If a y appears in the list then it is bound in c2 by an outer constructor
 * and maps to the x of c1.  If an x is absent from the list then it is free in
 * c1. If a y is absent from the list then it is free in c2.
 * Note that type variables cannot be blindly compared as they may map to
 * different variables or may be bound in c1 but free in c2 or vice versa.
 *)

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

let empty_ctxt = ([],Dict.empty id_compare);;
let extend (vm,km) x1 x2 k : alphactxt =
  ((x1,x2)::vm,Dict.insert km x2 k)
;;
let rec compare error c x1 x2 =
  match c with
    [] -> if (id_compare x1 x2)<>0 then error ()
  | (y1,y2)::c ->
      if (id_compare x1 y1)=0 then
 	(if (id_compare x2 y2)<>0 then error ())
      else if (id_compare x2 y2)=0 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 () else
  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 (id_compare l1 l2)<>0 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;
	(match rs_get_tla rs1, rs_get_tla rs2 with
	  Some c1,Some c2 -> aeq error ctxt ctx c1 c2
	| None,None -> ()
	| _,_ -> error())
      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
(* Cyclone *)
  | Ctempty,Ctempty -> ()
  | Ctcons (c11,c12),Ctcons (c21,c22) ->
      aeq error ctxt ctx c11 c21;
      aeq error ctxt ctx c12 c22
  | Ctmpl(c11,c12_opt,labels1,holes1),Ctmpl(c21,c22_opt,labels2,holes2) ->
      begin
        aeq error ctxt ctx c11 c21;
        (match c12_opt,c22_opt with
          None,None -> ()
        | Some c12,Some c22 ->
            aeq error ctxt ctx c12 c22
        | _ -> error());
        let id_con_list_eq l1 l2 =
          try
            List.iter2
              (fun (i1,c1) (i2,c2) ->
                if i1<>i2 then aeq error ctxt ctx c1 c2
                else error())
              l1
              l2
          with Invalid_argument _ -> error()
        in
        id_con_list_eq labels1 labels2;
        id_con_list_eq holes1 holes2
      end
  | Ctrgn(c11,c12,t1),Ctrgn(c21,c22,t2) -> ()
(* t : (id * (id * con) list) list *)
(* alphas : id list *)
(* holes : ((id * con) list) list *)
(*
      begin
        aeq error ctxt ctx c11 c21;
        aeq error ctxt ctx c12 c22;
        let (alphas_1,holes_1) = List.split t1 in
        let (alphas_2,holes_2) = List.split t2 in
        let (hs1,cs1) = List.split holes_1 in
        let (hs2,cs2) = List.split holes_2 in
        if
          try List.forall2 (=) alphas_1 alphas_2
              & List.forall2 (=) hs1 hs2
          with Invalid_argument -> error()
        then aeqs error ctxt ctx cs1 cs2
        else error()
      end      
*)
(* End Cyclone *)
  | (_,_) -> 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 =
  aeq error ctxt empty_ctxt c1 c2
    (* could set c1 == c2 and force more sharing *)
;;

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

let eqcon ctxt c1 c2 =
  if c1 <> c2 then
    try
      let ctxt' = error_handler ctxt eqerror' in
      aeqcon eqerror ctxt' c1 c2
    with NotEq -> 
      let c1 = normalize ctxt c1
      and 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                                            *)
(*************************************************************************)

(* See notes on equality & alpha equality *)

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

let rec mem i l =
  match l with
    [] -> false
  | i'::_ when i=$i' -> true
  | _::l -> mem i l
;;

let extend_d ctx dir v1 v2 k =
  if dir then extend ctx v1 v2 k else extend ctx v2 v1 k
;;

(* ctxt |- c1 <= c2
 * in alpha context ctx
 * exactsize = no width subtyping?
 * dir = ctx maps c1->c2 (true) or c2->c1 (false)
 *)

let rec leqc error ctxt (ctx : alphactxt) dir exactsize c1 c2 =
  if (fst ctx)<>[] or c1!=c2 then
  match c1.rcon,c2.rcon with
    Cvar x1,Cvar x2 ->
      if dir then compare error (fst ctx) x1 x2
      else compare error (fst ctx) x2 x1
  | Clam (v1,k1,c1),Clam (v2,k2,c2) ->
      kindeq ctxt k1 k2;
      leqc error ctxt (extend_d ctx dir v1 v2 k1) dir exactsize c1 c2
  | Capp (c11,c12),Capp (c21,c22) ->
      leqc error ctxt ctx dir exactsize c11 c21;
      if dir then aeq error ctxt ctx c12 c22 else aeq error ctxt ctx c22 c12
  | Ctuple cs1,Ctuple cs2 ->
      (try List.iter2 (leqc error ctxt ctx dir exactsize) cs1 cs2
      with Invalid_argument _ -> error ())
  | Cproj (i1,c1),Cproj (i2,c2) ->
      if i1=i2 then leqc error ctxt ctx dir exactsize c1 c2 else error ()
  | Clab l1,Clab l2 -> if (id_compare l1 l2)<>0 then error ()
  | _,Cprim (PCjunk i) ->
      (match con_kind ctxt c1 with
	Kmemi j when i=j -> ()
      |	_ -> error ())
  | Cprim pc1,Cprim pc2 -> if pc1<>pc2 then error ()
  | Crec fs1,Crec fs2 ->
      if dir then
        aeq (fun () -> failwith "Talcon.leqc - nonequal Crec unimplemented")
          ctxt ctx c1 c2
      else
      	aeq (fun () -> failwith "Talcon.leqc - nonequal Crec unimplemented")
          ctxt ctx c2 c1
  | Cforall (v1,k1,c1),Cforall (v2,k2,c2) ->
      kindleq ctxt k2 k1;
      leqc error ctxt (extend_d ctx dir v1 v2 k2) dir exactsize c1 c2
  | Cexist (v1,k1,c1),Cexist (v2,k2,c2) ->
      kindleq ctxt k1 k2;
      leqc error ctxt (extend_d ctx dir v1 v2 k1) dir exactsize c1 c2
  | Ccode rs1,Ccode rs2 -> leqrs error ctxt ctx (not dir) 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 dir false c1 c2
      else
	error ()
  | Cfield (c1,v1),Cfield (c2,v2) ->
      leqcv error ctxt ctx dir exactsize c1 v1 c2 v2
  | 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 dir (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 dir 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
	if dir then aeq error ctxt ctx c11 c21 else aeq error ctxt ctx c21 c11
      else
      	leqc error ctxt ctx dir false c11 c21;
      leqc error ctxt ctx dir exactsize c12 c22
  | Csing c1,Csing c2 -> leqc error ctxt ctx dir exactsize c1 c2
  | Csing _,Cprim (PCbytes Byte4) -> ()
  | Csing {rcon=Cprim (PCint i)},Chptr (is,_) ->
      if not (mem i is) then error ()
  | Csptr c1,Csptr c2 -> leqc error ctxt ctx dir false c1 c2
  | Cempty,Cempty -> ()
  | Ccons (c11,c12),Ccons (c21,c22) ->
      (match c21.rcon with
	Cprim (PCjunk i) ->
	  (match con_kind ctxt c11 with
	    Kmemi j when i=j -> ()
	  | Kbyte s when i=(scale_to_int32 s) -> ()
	  | _ -> error ())
      |	_ -> leqc error ctxt ctx dir true c11 c21);
      leqc error ctxt ctx dir exactsize c12 c22
  | Cappend (c11,c12),Cappend (c21,c22) -> 
      leqc error ctxt ctx dir true c11 c21;
      leqc error ctxt ctx dir exactsize c12 c22
(* Cyclone *)
  | Ctptr x1,Ctptr x2 -> compare error (fst ctx) x1 x2
  | Ctempty,Ctempty -> ()
  | Ctcons (c11,c12),Ctcons (c21,c22) ->
      leqc error ctxt ctx dir false c11 c21;
      leqc error ctxt ctx dir false c12 c22
  | Ctmpl(c11,c12_opt,l1,h1),Ctmpl(c21,c22_opt,l2,h2) ->
      begin
        leqc error ctxt ctx dir false c21 c11;
        match c12_opt,c22_opt with
          None,_ -> ()
        | Some c12,Some c22 ->
            leqc error ctxt ctx dir false c12 c22
        | _ -> error ()
      end
  | Ctrgn(c11,None,t1),Ctrgn(c21,_,t2) ->
      leqc error ctxt ctx dir false c21 c11
  | Ctrgn(c11,Some c12,t1),Ctrgn(c21,Some c22,t2) ->
      leqc error ctxt ctx dir false c21 c11;
      leqc error ctxt ctx dir false c12 c22
(* End Cyclone *)
  | _,_ -> error ()
and leqrs error ctxt ctx dir rs1 rs2 =
   let aux r c2 =
    try leqc error ctxt ctx dir false (rs_get_reg rs1 r) c2
    with Dict.Absent -> error () in
   rs_app_reg aux rs2;
   match rs_get_tla rs1,rs_get_tla rs2 with
     _,None -> ()
   | Some c1,Some c2 -> leqc error ctxt ctx dir false c1 c2
   | _ -> error()
and leqcv error ctxt ctx dir exactsize c1 v1 c2 v2 =
  match v2 with
    Read ->
      if v1=Read or v1=ReadWrite then leqc error ctxt ctx dir exactsize c1 c2
      else error ()
  | Write ->
      if v1=Write or v1=ReadWrite then
 	leqc error ctxt ctx (not dir) exactsize c2 c1
      else
 	error ()
  | ReadWrite ->
      if v1=ReadWrite then
 	if dir then aeq error ctxt ctx c1 c2 else aeq error ctxt ctx c2 c1
      else error ()
  | Uninit -> 
      if v1=Uninit or v1=ReadWrite then
 	if dir then aeq error ctxt ctx c1 c2 else aeq error ctxt ctx c2 c1
      else error ()
;;

let leqc_norm error ctxt c1 c2 =
  if c1 <> c2 then
    try
      let ctxt' = error_handler ctxt eqerror' in
      leqc eqerror ctxt' empty_ctxt true false c1 c2
    with NotEq ->
      let c1 = normalize ctxt c1
      and c2 = normalize ctxt c2 in
      leqc error ctxt empty_ctxt true 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 =
  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)

  | Chptr (is,Some c) ->
      let c = whnorm ctxt c in
      whnorm ctxt (defcon (Chptr (is,Some (unroll_rec exact ctxt c))))
  | _ -> generate_error ctxt (BadUnroll c); raise Talfail
;;

(* calculates the size (in bytes) of values who have type c *)	
let rec sizeof ctxt c =
  match con_kind ctxt c with
    Kbyte s -> scale_to_int32 s
  | Kmemi i -> i
  | _ ->
      let c = normalize ctxt c in
      match con_kind ctxt c with
    	Kbyte s -> scale_to_int32 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 -> i32_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); i32_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 =$ i32_0 then
	if depth=None then
	  let (f,con) = get_max_depth ctxt c1 in
	  ((fun c -> ccons (f c) c2),con,i32_0)
	else
	  ((fun c -> ccons c c2),c1,i32_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 =$ i32_0 then
	if depth=None then
	  let (f,con) = get_max_depth ctxt c in
	  ((fun c -> (f c)::cs),con,i32_0)
	else
	  ((fun c -> c::cs),c,i32_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 <>$ i32_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 >$ i32_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
    i,_ when i =$ i32_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 *)
