(* SYNTAX *)

let mode = true (* Verbose mode *)

type subj (* Expression appearing in subject position *)

(* Expressions *)       
type 'a exp = V : string ->  subj exp  (* Variable *)
	    | Id : string -> subj exp (* Channel *)
	    | N : int -> 'a exp (* Integer *)
	    | Pred : 'a exp -> 'a exp  (* -1 *)
	    | Succ : 'a exp -> 'a exp (* +1 *)

(* Process syntax *)				  
type 'a process = Nil
	     | Par of 'a process * 'a process
	     | IfZero of (subj exp) * 'a process * 'a process
	     | In of (subj exp) * ('a exp) list * 'a process
	     | Out of (subj exp) * ('a exp) list
	     | Rin of (subj exp) * ('a exp) list * 'a process (* Replicated Input *)
	     | Nu of (subj exp) *  'a process
			     
(* Pretty printer for expressions *)
let rec print_exp : type a. a exp -> string = function
    V x -> x
  | Id x -> x
  | N x -> string_of_int x
  | Pred x -> (print_exp x)^"-1"
  | Succ x -> (print_exp x)^"+1"			      

(* Pretty printer for processes *)		  
let pretty_print_proc p =
  let rec pretty_print_aux = function
      Nil -> "0"
    | Par(p1,p2) -> "("^(pretty_print_aux p1) ^" | "^(pretty_print_aux p2)^")" 
    | IfZero(e,p1,p2) -> "["^(print_exp e)^"=0] "^(pretty_print_aux p1)^" + ["^(print_exp e)^"!=0] "^(pretty_print_aux p2)
    | In(a,l,p) -> (match l with
		      [] -> (print_exp a)^"."^(pretty_print_aux p)
		    | t::q -> (print_exp a)^"("^(print_exp t)^(List.fold_left (fun x -> (fun y -> x^","^(print_exp y))) "" q)^")."^(pretty_print_aux p))
    | Rin(a,l,p) -> (match l with
		      [] -> "!"^(print_exp a)^"."^(pretty_print_aux p)
		    | t::q -> "!"^(print_exp a)^"("^(print_exp t)^(List.fold_left (fun x -> (fun y -> x^","^(print_exp y))) "" q)^")."^(pretty_print_aux p))
    | Out(a,l) -> (match l with
		      [] -> "^"^(print_exp a)
		    | t::q -> ("^"^(print_exp a)^"<"^(print_exp t)^(List.fold_left (fun x -> (fun y -> x^","^(print_exp y))) "" q))^">")
    | Nu(a,p) -> "(v "^(print_exp a)^") "^(pretty_print_aux p)
  in
  print_endline (pretty_print_aux p)

(* EXAMPLES OF PROCESSSES *)

let example_1 = Par(In(Id("b"),[V("x")],In(V("x"),[],Nil)) ,In(Id("a"),[],Nil))

let add_ex = Rin( Id("add"), [V("x"); V("y"); V("r")], IfZero( V("x"),
						    Out(V("r"), [V("y")]),
						    Nu(Id("c"), Par(Out(Id("add"),[Pred(V("x"));V("y");Id("c")]),
								    In(Id("c"),[V("z")],Out(V("r"),[Succ(V("z"))]))
								   )
						      )
							     )
		) 

		
let mult_ex = Par(add_ex, Rin(Id("mult"), [V("xm"); V("ym"); V("rm")], IfZero( V("x"),
									       Out(V("rm"), [N 0]),
									       Nu (Id "c1", Nu (Id "c2", Par( Out(Id "mult", [Pred (V "xm"); V "ym"; Id "c1"]),
													      Par (In (Id "c1", [V "z1"],
														       Out (Id "add", [V "ym"; V "z1"; Id "c2"])),
														   In (Id "c2", [V "z2"], Out (V "rm", [V "z2"]) ) )))))))
											      


let fact_ex = Par( mult_ex, Rin(Id("fact"), [V("xf"); V("rf")], IfZero( V("xf"),
									       Out(V("rf"), [N 1]),
									       Nu (Id "d1", Nu (Id "d2", Par( Out(Id "fact", [Pred (V "xf"); Id "d1"]),
													      Par (In (Id "d1", [V "u1"],
														       Out (Id "mult", [V "u1"; V "xf"; Id "d2"])),
														   In (Id "d2", [V "u2"], Out (V "rf", [V "u2"]) ) )))))))

let cube_ex = Par (mult_ex, 
				Rin (Id "cube",[V "xc"; V "rc"],
				     Nu (Id "c1",
				      Nu (Id "c2",
				       Par( Out(Id "mult", [V "xc"; V "xc"; Id "c1"]),
					    Par(In (Id "c1", [V "zc1"; ], Out(Id "mult", [V "xc"; V "zc1"; Id "c1"])) ,
						In (Id "c2", [V "zc2"; ], Out(V "rc", [V "zc2"]))
					       )) ))))
		 
		 
let wrong_ex1 = Rin(Id "a", [V "x"; V "y"; V "r"], Out (Id "a", [V "x"]))

let wrong_ex2 = Par(Rin(Id "a", [V "x"; V "y"], Out (Id "a", [V "y"; V "x"])),
		    Par(Out(Id "a", [Id "u"; Id "v"]),
			Par(Out(Id "u", [Id "d"]),
			    Par(Out(Id "v", [N 0]),
				Out(Id "d", [Pred (V "w")])
				   ))))
			
let wrong_ex3 = Par(Out (Id "a", [Id "b"]), Out (Id "b", [Id "a"]))

let wrong_ex4 = In (Id "a", [V "x"], In (Id "a", [V "y"],
					     Par (In (V "x", [], Nil), Rin (V "y", [], Nil))))

let wrong_ex5 = Rin(Id "a",[], Par( Out(Id "a",[]), Rin(Id "b",[], Nil) ))		   
		   
let tricky_ex = Par(Rin(Id "a",[V "n"],Nil),
		    Par(Out(Id "b", [N 3]),
			Par(Out(Id "c", [N 3]),
			    Par(Out(Id "d", [Id "a"]),
			       Out(Id "d", [Id "b"])))))

let tricky_ex2 = Par(Rin(Id "a",[],Nil),
		     Par( Rin (Id "b",[],Nil),
			  Par (Out(Id "c", [Id "a"; Id "d"]),
			       Par (Out(Id "c", [Id "e"; Id "b"]),
				    Par (Out(Id "d", []),
					 Out(Id "e", []))))))

		   
let ok_ex1 = Par( Par (Rin (Id "a",[],Out (Id "b", [])),
		      Rin (Id "b",[],Out (Id "a", []))),
		  Par(Rin (Id "c",[],Out (Id "d", [])),
		      Par(Rin (Id "d",[], Out (Id "e", [])),
			       Rin (Id "e",[], Nil)
			      )
			 ))
  
(* SIMPLE TYPE INFERENCE *)		     

(* Type syntax *)		     

type level = L of int (* actual level *)
	   | V of string (* level variable *)

type comp_type = Nat (* untagged integers *)
	       | Natu (* unsafe integers *)
	       | Nats (* safe integers *)
	       | Ch of comp_type list (* untagged channels *)
	       | Chr of level * comp_type list (* replicated channels *)
	       | Chi of comp_type list (* linear channels *)
	       | Var of string (* type variables for unification *)
			  
type envi = (subj exp * comp_type) list (* environments *)

let print_level = function
    L x -> string_of_int x
  | V s -> s
				     
(* Type variable generator *)

let tvar_count = ref 0
		     
let tvar_gen () = let _ = tvar_count := (!tvar_count + 1) in Var("T"^string_of_int(!tvar_count))

(* Constraint sets as zippers *)								

type constr = C of comp_type * comp_type

type zip_constr = Zip of (constr list) * (constr list)
				   
let add_constr t1 t2 = function Zip (l1,l2) -> (Zip (l1, C(t1,t2)::l2)) 

let rec rewind = function
    Zip ([],l2) -> Zip ([],l2)
  | Zip (h::tl, l2) -> rewind (Zip (tl, h::l2))

let zip_append zip1 zip2 = match zip1,zip2 with
    Zip(l1,l2),Zip(l3,l4) -> Zip(List.append l1 l3, List.append l4 l2)
			      
(* Environment Manipulation *)
						 
exception Not_in of string
		      
let rec env_get a = function
    [] -> raise (Not_in "Variable not in environment.")
  | (x,t)::tl when  x = a  -> t
  | (x,t)::tl -> env_get a tl

let rec env_rem a = function 
    [] -> raise (Not_in "Variable not in environment.")
  | (x,t)::tl when  x = a -> tl
  | (b,t)::tl -> (b,t)::(env_rem a tl)
			  
(* Pretty printer for types *)

let rec print_typ = function
    Nat -> "Nat???"
   | Natu -> "Natu"
   | Nats -> "Nat"	     
  | Ch(ts) -> (match ts with
		 [] -> "#???()"
	       | h::tl -> "#???("^(List.fold_left (fun x -> fun y -> x^","^(print_typ y)) (print_typ h) tl)^")")
  | Chi(ts) -> (match ts with
		 [] -> "#()"
	       | h::tl -> "#("^(List.fold_left (fun x -> fun y -> x^","^(print_typ y)) (print_typ h) tl)^")")
  | Chr(l, ts) -> (match ts with
		 [] -> "#"^(print_level l)^"()"
	       | h::tl -> "#"^(print_level l)^"("^(List.fold_left (fun x -> fun y -> x^","^(print_typ y)) (print_typ h) tl)^")")
  | Var(s) -> s

(* Expression Simplification *)
		  
exception Int_found

let rec simp_exp : type a. a exp -> subj exp  =
    function
      Pred x -> (simp_exp x)
    | Succ x -> (simp_exp x)
    | N x -> raise Int_found
    | V x  as v -> v
    | Id x as v -> v
		     
(* Pretty printers for environment and constraint sets *)

let pretty_print_env env =
  let rec pretty_print_aux = function
      [] -> ""
    | (id,typ)::tl -> (print_exp id)^" : "^(print_typ typ)^"\n"^(pretty_print_aux tl)
  in
  print_endline ("{\n"^(pretty_print_aux env)^"}")

let pretty_print_constr zip =
  let rec pretty_print_aux = function
      Zip(l1,[]) -> ""
    | Zip(l1,C(t1,t2)::tl) -> (print_typ t1)^" = "^(print_typ t2)^"\n"^(pretty_print_aux (Zip (C(t1,t2)::l1,tl)))
  in
  print_endline ("{\n"^(pretty_print_aux (rewind zip))^"}")
		
let type_ex1 = Chr(L 2,[Nat; Nat; Ch([Nat])])		  
let env_ex1 = [Id("a"), type_ex1; (V "x"), Nat; V("y"), Nat; V("r"), Ch([Nat]); Id("c"), Ch([Nat])]
let constr_ex1 = Zip([],[C(type_ex1, Chr(L 2,[tvar_gen ()])); C(Ch([tvar_gen ()]), tvar_gen ())])

(* Generating constraints from +1 and -1 *)
		    
let rec const_from_op env = function
    [] -> Zip ([],[])
  | h::tl -> match h with
	     | Pred x -> (try (zip_append (Zip ([],[C (env_get (simp_exp x) env, Nat)])) (const_from_op env tl))
			 with
			   Int_found -> (const_from_op env tl))
	     | Succ x -> (try (zip_append (Zip ([],[C (env_get (simp_exp x) env, Nat)])) (const_from_op env tl))		   
			  with
			    Int_found -> (const_from_op env tl))
	     | _ -> (const_from_op env tl)

(* Merging environments *)
		      
let rec env_merge env = function
    [] -> (env, Zip([],[]))
  | (id,typ1)::tl -> let res,zip = env_merge env tl in
		     try let typ2 = (env_get id res) in
			 match zip with Zip(l1,l2) -> 								       (id, typ2)::(env_rem id res), Zip(l1, C(typ1,typ2)::l2)
		     with (Not_in s) -> ((id,typ1)::res, zip)
					  
(* Genrating environment skeleton and constraints from a process *)
					  
let rec generate_env_constr : type a. a process -> (envi * zip_constr) =
    function
      Nil -> ([], Zip([],[]))
    | Out(a,l) ->  (let env = (a, (tvar_gen ()))::(List.fold_left (fun x -> fun y -> (try ((simp_exp y), (tvar_gen ()))::x  with Int_found -> x)) [] l) in (* Environment for prefix *)
		    let zip0 = (const_from_op env l) in (* Constraints for +1/-1 *)
		    let zip = (zip_append zip0 (Zip ([], [C( (env_get a env), Ch (List.map (fun x -> try (env_get (simp_exp x) env) with Int_found -> Nat) l))]))) in (* Constraints for prefix *)
		    (env, zip))
    | In(a,l,p) -> (let resenv, reszip = (generate_env_constr p) in
		    let env = (a, (tvar_gen ()))::(List.fold_left (fun x -> fun y -> ((simp_exp y), (tvar_gen ()))::x ) [] l) in
		    let zip0 = (const_from_op env l) in 
		    let zip = (zip_append zip0 (Zip ([], [C( (env_get a env), Ch (List.map (fun x -> try (env_get (simp_exp x) env) with Int_found -> Nat) l))]))) in
		    let menv,mzip = env_merge resenv env in (* Merge env with continuation *)
		    menv , (zip_append zip (zip_append mzip reszip)))    (* Merge constr with continuation*)
    | Rin(a,l,p) -> (let resenv, reszip = (generate_env_constr p) in
		     let env = (a, (tvar_gen ()))::(List.fold_left (fun x -> fun y -> ((simp_exp y), (tvar_gen ()))::x ) [] l) in
		    let zip0 = (const_from_op env l) in 
		    let zip = (zip_append zip0 (Zip ([], [C( (env_get a env), Ch (List.map (fun x -> (env_get (simp_exp x) env)) l))]))) in
		     let menv,mzip = env_merge resenv env in
		     menv , (zip_append zip (zip_append mzip reszip)))    
    | Par(p1,p2) -> (let resenv1, reszip1 = (generate_env_constr p1) in
		     let resenv2, reszip2 = (generate_env_constr p2) in
		     let menv,mzip = env_merge resenv1 resenv2 in
		     menv, (zip_append reszip1 (zip_append reszip2 mzip)))
    | Nu(a,p) -> (generate_env_constr p)
    | IfZero(a,p1,p2) -> (let resenv1, reszip1 = (generate_env_constr p1) in
			  let resenv2, reszip2 = (generate_env_constr p2) in
			  let menv,mzip = env_merge resenv1 resenv2 in
			  let newt = tvar_gen () in
			  let fmenv,fmzip = try
			      let sa = a in
			      env_merge menv [sa,newt]
			    with Int_found -> menv, Zip([],[]) 
			  in
			  menv, (zip_append reszip1 (zip_append reszip2 (zip_append mzip (zip_append (Zip([],[C(newt,Nat)])) fmzip)))))


(* Type substitution *)		    
let rec replace_tvar_typ vari typ = function
    t1 when t1 = vari -> typ
  | Ch l1 -> Ch(List.map (replace_tvar_typ vari typ) l1)
  | _ as t -> t

(* Substitution in environment *)		
let rec replace_tvar_env env vari typ =
  match env with
    [] -> []
  | h::tl -> (match h with
	       (id,t) -> (id,(replace_tvar_typ vari typ t))::(replace_tvar_env tl vari typ))

(* Substitution in constraint set *)	       
let replace_tvar_zip zip vari typ =
  let rec replace_tvar_zip_aux zip =
    match zip with
      Zip (l,[]) -> Zip(l,[])
    | Zip (l, C(t1,t2)::tl) -> replace_tvar_zip_aux (Zip(C((replace_tvar_typ vari typ t1),
							   (replace_tvar_typ vari typ t2))::l,tl))
  in replace_tvar_zip_aux (rewind zip)

exception Failed_Unify of string

type unify_res = Success of envi  | Failure of string

(* Occurcheck for recursive types *)
let rec occur_check var = function
  | Nat -> false
  | Var(n1) when (Var(n1) = var) -> true
  | Var(n1) -> false
  | Ch (l1) -> List.fold_left (fun x -> fun y -> x || (occur_check var y)) false l1
  | Chr (l,l1) -> List.fold_left (fun x -> fun y -> x || (occur_check var y)) false l1
  | Chi (l1) -> List.fold_left (fun x -> fun y -> x || (occur_check var y)) false l1 
  | _ -> failwith "Unexpected type in occur check."
     
let rec list_constraint l1 l2 = match (l1,l2) with
    [],[] -> Zip([],[])
  | h1::tl1, h2::tl2 -> let zip = list_constraint tl1 tl2 in
			(zip_append (Zip ([],[C(h1,h2)])) zip)
  | _,_ -> failwith "Unifying lists of different lengths."
			      
(* Unification algorithm for simple types *)
let unify zc env =
  let comm s =
    if mode then
      print_endline s
    else ()
  in
  let rec unify_aux zc env flag = (* Flag notifies expected rewind *) 
    match zc with
      Zip ([],[]) -> env (* Termination *)
    | Zip (t,[]) as z -> if flag then env else unify_aux (rewind z) env true (* Termination or Rewind *)
    | Zip (t,h::tl) -> (match h with 
			  C(Nat, Nat) -> let _ = (comm "Unifying Nat and Nat") (* Trivial *)
					 in (unify_aux (Zip (t,tl)) env flag)
			| C(Var(s1),t2) -> let _ = (comm ("Unifying "^(print_typ (Var s1))^" and "^(print_typ t2))) (* Substitution done if no recursive type *)
					   in
					   if (Var s1 <> t2) && (occur_check (Var s1) t2) then
					     raise (Failed_Unify "Recursive channel type detected.")
					   else
					     let nenv = (replace_tvar_env env (Var s1) t2) in
					     let nzip = (replace_tvar_zip (Zip (t,tl)) (Var s1) t2) in
					     (unify_aux nzip nenv false)
			| C(t1, Var s2) -> let _ = (comm ("Unifying "^(print_typ (Var s2))^" and "^(print_typ t1)))
					   in
					   if (Var s2 <> t1) && (occur_check (Var s2) t1) then
					     raise (Failed_Unify "Recursive channel type detected.")
					   else
					     let nenv = (replace_tvar_env env (Var s2) t1) in
					     let nzip = (replace_tvar_zip (Zip (t,tl)) (Var s2) t1) in
					     (unify_aux nzip nenv false)						  
			| C(Nat, t2) -> (* Nat cannot be unified with non Nat non variable types *)
			   let _ = (comm ("Unifying Nat and "^(print_typ t2)))
			   in
			   raise (Failed_Unify "Nat unified with channel.")						 
			| C(t1, Nat) -> let _ = (comm ("Unifying Nat and "^(print_typ t1)))
					in
					raise (Failed_Unify "Nat unified with channel.")
			| C(Ch(l1),Ch(l2)) -> let _ = (comm ("Unifying "^(print_typ (Ch l1))^" and "^(print_typ (Ch l2))))
					      in
					      if (List.length l1) <> (List.length l2) then
						raise (Failed_Unify "Number of arguments mismatch.")
					      else
						let nzip = (zip_append (Zip (t,tl)) (list_constraint l1 l2) ) in
						(unify_aux nzip env false)
		       	| C(t1,t2) -> raise (Failed_Unify ("Unknown constraint "^(print_typ t1)^" = "^(print_typ t2))))
  in
  try Success (unify_aux zc env true) with
    Failed_Unify s -> Failure s
exception LinRep of string

(* NAME KIND INFERENCE *)

		      
type name_kind = Lin (* Linear *)
	       | Rep (* Replicated *)
	       | Unk (* Can be instantiated *)
	       | Fail (* Both linear and replicated *)

(* Martching kinds for composition *)		   
let match_kind k1 k2 =
  match (k1, k2) with
    (a, b) when a = b -> a
  | (Unk, a) | (a, Unk) -> a
  | (Fail, a) -> Fail
  | (a, Fail) -> Fail
  | (Lin, Rep) -> Fail
  | (Rep, Lin) -> Fail
  | _ -> failwith "Error in linear/replicated type matching."

(* Deciding the kind of a name *)		  
let rec name_kind p a = 						    
  match p with
    Nil -> Unk
  | Par (p1,p2) -> (match_kind (name_kind p1 a) (name_kind p2 a))
  | Out(_,_) -> Unk
  | In(b,_,pc) when a = b -> match_kind Lin (name_kind pc a)
  | In(_,_,pc) -> (name_kind pc a)
  | Rin(b,_,pc) when a = b -> match_kind Rep (name_kind pc a)
  | Rin(_,_,pc) -> (name_kind pc a)
  | Nu (_,pc) -> (name_kind pc a)
  | IfZero (_,p1,p2) -> (match_kind (name_kind p1 a) (name_kind p2 a))

(* Object lists record which name is used by which name *)			  
let rec object_list_merge l1 = function 
    [] -> l1
  | (a,l)::tl -> (a, (List.fold_left (fun x ->
				      function
					(b,lb) when b = a -> List.append x lb
				      | (b,lb) -> x) l l1))
		 :: (object_list_merge l1 tl)

let indexify l = 
  let rec indexify_aux n = function
      [] -> []
    | h::tl -> try (simp_exp h, n)::(indexify_aux (n + 1) tl) with Int_found -> (indexify_aux (n + 1) tl) 
  in
  indexify_aux 1 l

(* Build the object list *)	       
let rec object_list = function
    Nil -> []
  | Out (a,l) -> [(a,(indexify l))]
  | In (a,l,p) -> object_list_merge [(a,(indexify l))] (object_list p)
  | Rin (a,l,p) -> object_list_merge [(a,(indexify l))] (object_list p)
  | Nu (a,p) -> object_list p
  | Par (p1, p2) -> object_list_merge (object_list p1) (object_list p2)
  | IfZero (a, p1, p2) -> object_list_merge (object_list p1) (object_list p2) 	      

type binder = Nu | Inp of (subj exp) | Rinp of (subj exp)

(* Return the constructor binding b *)					    
let rec bound_by b = function
    Nil -> None
  | Out (a,l) -> None
  | In (a,l,p) -> if (List.mem b l) then Some (Inp a) else (bound_by b p)
  | Rin (a,l,p) -> if (List.mem b l) then Some (Rinp a) else (bound_by b p)
  | Nu (a,p) -> if a = b then Some Nu else (bound_by b p)
  | Par (p1, p2) -> (match (bound_by b p1), (bound_by b p2) with
		       None, None -> None
		     | None, Some x -> Some x
		     | Some x, None -> Some x
		     | _,_ -> failwith "Name bound twice.")
  | IfZero (a, p1, p2) ->  (match (bound_by b p1), (bound_by b p2) with
			     None, None -> None
			   | None, Some x -> Some x
			   | Some x, None -> Some x
			   | _,_ -> failwith "Name bound twice.")

					    
(* Give all the names appearing as objects of a in prefix, with their position *)
let rec get_obj a = function
    [] -> []
  | (b,l)::tl when b = a -> l
  | (b,l)::tl -> get_obj a tl

let rec obj_list_mem a = function
    [] -> []
  | (b,n)::tl when a = b -> n::(obj_list_mem a tl)
  | (b,n)::tl -> (obj_list_mem a tl)
			 
(* Give all the names where a appears as object in a prefix, with its position *)
let rec get_subj a = function
    [] -> []
  | (b,l)::tl -> List.fold_left (fun x -> fun n -> List.append x [(b,n)]) (get_subj a tl) (obj_list_mem a l) 

(* Generation of level variables *)				
let lvar_count = ref 0
		     
let lvar_gen () = let _ = lvar_count := (!lvar_count + 1) in V ("L"^string_of_int(!lvar_count))

let rec nth n = function
    [] -> failwith "Length mismatch."
  | h::tl -> if n = 1 then h else (nth (n-1) tl)

exception No_change			     
	    
(* Update type ot to type nt according to LinRep promotion *)
let rec update_type ot nt =
  (* Auxiliary function updating list of types *)
  let rec update_type_list l1 l2 = match (l1,l2) with
      [],[] -> []
    | h1::tl1, h2::tl2 -> let nt = try (update_type h1 h2)
				   with No_change -> h1
			  in
			  nt::(update_type_list tl1 tl2)
    | _ -> failwith "Different list lengths while updating."
  in
  match (ot, nt) with
    (_,_) when ot = nt -> raise No_change
  | Ch(l1), Ch(l2) ->  Ch (update_type_list l1 l2)
  | Chi(l1), Chi(l2) ->  Chi (update_type_list l1 l2)
  | Chr(lv1,l1), Chr(lv2,l2) ->  Chr (lv1, update_type_list l1 l2)
  | Ch(l1), Chr(lv, l2) ->  Chr (lv, update_type_list l1 l2)
  | Ch(l1), Chi(l2) ->  Chi (update_type_list l1 l2)
  | Chi(l1), Chr(lv, l2) -> raise (LinRep "Try to update linear type as replicated type.")
  | Chr(lv, l1), Chi(l2) -> raise (LinRep "Try to update replicated type as linear type.")
  | t1,t2 ->  failwith ("Unexpected type update case: "^(print_typ t1)^" and "^(print_typ t2))

(* Update a type in an environment *)
(* Parametrised with a update type function *)
let rec flat_update_env f a ntyp = function
    [] -> failwith "Try to update unknown type."
  | (id, typ)::tl when id = a -> (id, (f typ ntyp))::tl
  | (id, typ)::tl -> (id, typ)::(flat_update_env f a ntyp tl)

let rec replace_nth l e n = match l with
    [] -> failwith "Index out of bounds in replacement."
  | h::tl -> if n = 1  then e::tl else h::(replace_nth tl e (n-1))

(* Replacing nth component of a type by typ*)       
let rep_subj_typ n typ = function
    Ch(l) -> Ch(replace_nth l typ n)
  | Chr(lv, l) -> Chr(lv, replace_nth l typ n)
  | Chi(l) -> Chi(replace_nth l typ n)
  | _ -> failwith "Subject is a non-channel type."
	 
let rec get_nth_typ n = function
    Ch(l) -> (nth n l)
  | Chr(lv, l) -> (nth n l)
  | Chi(l) -> (nth n l)
  | _ -> failwith "Subject is a non-channel type in object type update."

exception Stop_propagate
		  
(* Updating an environment *)
let update_env f a typ env obl =
  let rec update_env_aux a typ env =
    let _ = if mode then (print_endline ("Updating "^(print_exp a)^" with type "^(print_typ typ)))
    else () in
    try(
      let nenv = try (flat_update_env f a typ env)
		 with No_change -> raise Stop_propagate in (* Type already changed, no need to propagate *)
      let subj = get_subj a obl in
      let obj = get_obj a obl in
      let nenv2 = (List.fold_left (fun x -> fun (y,n) ->
					    (update_env_aux y
							    (rep_subj_typ n typ (env_get y x))
							    x)
				  ) nenv subj) in (* Propagating upward *)
      (List.fold_left (fun x -> fun (y,n) -> (update_env_aux y
							     (get_nth_typ n typ)
							     x)
		      ) nenv2 obj)) (*Propagating downward *)
    with Stop_propagate -> env
  in
  (update_env_aux a typ env)

let prom_rep_typ = function
    Ch(l) -> Chr((lvar_gen ()), l)
  | Chi(l) -> raise (LinRep "Promoting to replicated a linear name.")
  | Chr(lv, l) -> Chr(lv, l)
  | _ -> failwith "Unexpected type promotion."

let prom_lin_typ = function
    Ch(l) -> Chi(l)
  | Chr(_,l) -> raise (LinRep "Promoting to linear a replicated name.")
  | Chi(l) -> Chi(l)
  | _ -> failwith "Unexpected type promotion."
		  
(* Promoting token types according to name kind *)
let promote_env env p =
  let obl = object_list p in
  let names = List.map (fun (x,y) -> x) env in
  let purge_nk_env ns aenv =
    List.fold_left (fun x -> fun y -> match env_get y x with Ch(l) -> (update_env (update_type) y (Chi l) x obl) | _ -> x) aenv ns
  in
  let res = (List.fold_left (fun x -> fun y ->
				      match (name_kind p y) with
					Unk -> x
				      | Fail -> raise (LinRep "Name used in both linear and replicated inputs.")
				      | Rep -> (update_env (update_type) y (prom_rep_typ (env_get y x)) x obl)
				      | Lin -> (update_env (update_type) y (prom_lin_typ (env_get y x)) x obl)
			    ) env names) in
  (purge_nk_env names res)

(* Detecting nested replications *)
let nest_rep p = 
  let rec nest_rep_aux under = function
      Nil -> false
    | Par(p1,p2) -> (nest_rep_aux under p1) || (nest_rep_aux under p2)
    | Out(a,l) -> false
    | In(a,l,pc) -> (nest_rep_aux under pc)
    | Rin(a,l,pc) -> if under then true else (nest_rep_aux true pc)
    | Nu(a,pc) -> (nest_rep_aux under pc)
    | IfZero(a,p1,p2) -> (nest_rep_aux under p1) || (nest_rep_aux under p2)		   
  in
  nest_rep_aux false p

(* LEVEL INFERENCE *)
	       
type lconst = Und of (level * level) (* Level constraints *)

type 'a option = None | Some of 'a		       
				  
(* Generate level constraints in non-nested processes based on output
 * occurence inside replications *)
let generate_const p env =
  let rec generate_const_aux env under = function
      Nil -> []
    | Nu(a, pc) -> (generate_const_aux env under pc)
    | Par(p1, p2) -> List.append (generate_const_aux env under p1) (generate_const_aux env under p2)
    | IfZero(a, p1, p2) -> List.append (generate_const_aux env under p1) (generate_const_aux env under p2)
    | Out(a,l) -> (match under with None -> []
				  | Some b -> (match (env_get a env),(env_get b env) with
						 Chr(lv1,l1), Chr(lv2, l2) -> [Und (lv1,lv2)]
					       | _ -> []))
    | In(a,l,pc) -> (generate_const_aux env under pc)
    | Rin(a,l,pc) -> (generate_const_aux env (Some a) pc) 						      
  in
  generate_const_aux env None p

(* Print level constraints for verbose mode *)
let pretty_print_lconst con =		     
  let rec pretty_print_lconst_aux = function
      [] -> ""
    | (Und (l1,l2))::tl -> let a,b = match l1,l2 with
			       V s1, V s2 -> s1,s2
			     | V s1, L n2 -> s1,(string_of_int n2)
			     | L n1, V s2 -> (string_of_int n1),s2
			     | L n1, L n2 -> (string_of_int n1),(string_of_int n2)
			   in
			   (a^" < "^b^"\n"^(pretty_print_lconst_aux tl))
  in "{\n"^(pretty_print_lconst_aux con)^"}"      

(* Collect all levels directly higher than a *)
let rec higher a = function
    [] -> []
  | Und(x,y)::tl when x = a -> y::(higher a tl)
  | Und(_,_)::tl -> higher a tl

(* Collect all levels directyl lower than a *)
let rec lower a = function
    [] -> []
  | Und(x,y)::tl when y = a -> x::(lower a tl)
  | Und(_,_)::tl -> lower a tl
			    
(* Collect all levels higher than a, transitively *)
let all_higher a const =
  let l = ref [] in
  let rec all_aux b = 
    if List.mem b !l then ()
    else let _ = (l := b::(!l)) in
	 List.fold_left (fun x -> fun y -> (all_aux y)) () (higher b const)
  in
  let _ = all_aux a
  in !l		  

(* Collect all levels lower than a, transitively *)
let all_lower a const =
  let l = ref [] in
  let rec all_aux b = 
    if List.mem b !l then ()
    else let _ = (l := b::(!l)) in
	 List.fold_left (fun x -> fun y -> (all_aux y)) () (lower b const)
  in
  let _ = all_aux a
  in !l		  

let rec inter_list l1 = function
    [] -> []
  | h::tl -> if (List.mem h) l1 then h::(inter_list l1 tl) else (inter_list l1 tl)
      
type con_comp = CC of string (* Connected components *)
      
type ccconst = UndC of (con_comp * con_comp) (* CC constraints *)

let pretty_print_cc_const con =		     
  let rec pretty_print_cc_const_aux = function
      [] -> ""
    | (UndC (CC s1,CC s2))::tl -> (s1^" < "^s2^"\n"^(pretty_print_cc_const_aux tl))
  in "{\n"^(pretty_print_cc_const_aux con)^"}"      

(* Connected component name generator *)			 
let cc_count = ref 0

let cc_gen () = let _ = cc_count := (!cc_count + 1) in CC ("C"^string_of_int(!cc_count))

(* Fetch the cc associated to a level *)
let rec lvl_get a = function
    [] -> failwith "Level not found."
  | (lv, cc)::tl when lv = a -> cc
  | (lv, cc)::tl -> (lvl_get a tl)

(* Decide if a level is in a list *)
let rec mem_left e = function
    [] -> false
  | (a,_)::_ when a = e -> true
  | (a,_)::tl -> (mem_left e tl)		     
		      
(* Extract all levels from a set of constraints, and associate them with None *)
let rec extract_lv = function
    [] -> []
  | Und(lv1,lv2)::tl -> let res = (extract_lv tl)  
			in
			(match ((mem_left lv1 res),(mem_left lv2 res)) with
			   false, false -> if lv1 = lv2 then (lv1, None)::res else
					     (lv1, None)::((lv2, None)::res)
			 | false, true ->(lv1, None)::res
			 | true, false -> (lv2, None)::res
			 | true, true ->  res)

(* Associate levels of l with connected component cc *)
let rec replace_cc l cc = function
    [] -> []
  | (lv,occ)::tl -> if List.mem lv l then (lv,Some cc)::(replace_cc l cc tl)
		    else (lv, occ)::(replace_cc l cc tl)

(* Decide the connected components of all levels from a set of
 * constraints *)
let solve_lconst const =
  let levels = (extract_lv const) in
  (List.fold_left (fun x-> fun (y,_) -> match (lvl_get y x) with
					  Some a -> x
					| None -> let ncc = cc_gen () in
						  let to_be_changed = y::(inter_list (all_higher y const) (all_lower y const)) in
						  replace_cc to_be_changed ncc x)
		  levels
		  levels)
    
(* Generate a set of connected component constraint from a set of
 * level constraints *)
let rec gen_cc_const levels = function
    [] -> []
  | Und(lv1,lv2)::tl -> (match (lvl_get lv1 levels),(lvl_get lv2 levels) with
			   (Some a, Some b) -> UndC(a,b)::(gen_cc_const levels tl)  
			 | _,_ -> failwith "Level not assigned.")

let rec print_cc = function
    [] -> ""
  | (CC s,None)::tl -> "("^s^", None)"^(print_cc tl)
  | (CC s,Some n)::tl -> "("^s^", "^(string_of_int n)^") "^(print_cc tl)

exception Not_Found

(* Fetch a number associated to a connected component *)	    
let rec cc_get cc = function
    [] -> raise Not_Found
  | (a,b)::tl when a = cc -> b 
  | (_,_)::tl -> (cc_get cc tl)

(* Assign a number to a connected component *)		   
let rec cc_set cc value = function
    [] -> [(cc, value)]
  | (a,b)::tl when a = cc -> (a,value)::tl
  | (a,b)::tl -> (a,b)::(cc_set cc value tl)

(* Get all the connected components from constraints *)
let rec extract_cc = function
    [] -> []
  | UndC(cc1,cc2)::tl -> let res = (extract_cc tl) in  
			 (match ((mem_left cc1 res),(mem_left cc2 res)) with
			    false, false -> if cc1 = cc2 then (cc1, None)::res else
					      (cc1, None)::((cc2, None)::res)
			  | false, true ->(cc1, None)::res
			  | true, false -> (cc2, None)::res
			  | true, true ->  res)
			   
exception All_Assigned

(* Get a non assigned connected component *)
let rec get_non_ass = function
    [] -> raise All_Assigned
  | (a,b)::tl when b = None -> a
  | (_,_)::tl -> (get_non_ass tl)

(* Get the whole weakly connected component of a connected component *)
let rec all_cc const larg =
  let rec aux l flag = function
      [] -> (flag, l)
    | UndC(b,c)::tl -> (match (List.mem b l), (List.mem c l) with
			  true, true -> (aux l flag tl)
			| false, false -> (aux l flag tl)
			| true, false -> (aux (c::l) false tl)
			| false, true -> (aux (b::l) false tl))
  in (match (aux larg true const) with
	true, li -> li
      | false, li -> all_cc const li)

(* Get the higher weakly connected component of a connected component *)
let rec higher_cc const larg =
  let rec aux l flag = function
      [] -> (flag, l)
    | UndC(b,c)::tl -> (match (List.mem b l), (List.mem c l) with
			  true, true -> (aux l flag tl)
			| false, false -> (aux l flag tl)
			| true, false -> (aux (c::l) false tl)
			| false, true -> (aux l true tl))
  in (match (aux larg true const) with
	true, li -> li
      | false, li -> higher_cc const li)

       
type comparison = Less | More | Unc
				  
(* Compare two connected components according to constraints *)
let compare a b const =
  match a,b with CC sa, CC sb ->
    if (List.mem b (higher_cc const [a])) then Less
    else (if (List.mem a (higher_cc const [b])) then More
	  else Unc)

(* Get a minimal connected component of a list *)
let min_cc const = function
    [] -> failwith "Minimum of empty cc list."
  | h::tl -> List.fold_left (fun (x,l) -> fun y -> match (compare x y const) with
						     More -> (y,x::l)
						   | _ -> (x,y::l)
			    ) (h,[]) tl

(* Select sort a list of connected components *)
let sort_cc const l =
  let rec aux = function
      [] -> []
    | li -> let (min,rest) = (min_cc const li) in
	    min::(aux rest)
  in
  aux l
      
(* Assign numbers to a whole weakly connected component *)
let assign_one_cc const ccs n =
  let first = (get_non_ass ccs) in
  let all = (all_cc const [first]) in 
  let sorted = (sort_cc const all) in
  List.fold_left (fun (x,m) -> fun y -> 
			       (cc_set y (Some m) x, m+1))
		 (ccs,n) sorted

		 
(* Assign numbers to a all weakly connected components *)
let assign_all_cc const ccs =
  let rec aux res n =
    try  let resu,m = (assign_one_cc const res n) in
	 aux resu 1 (* 1 can be changed to m for unicity of level. *)  
    with All_Assigned -> res 
  in aux ccs 1	 

(* Assign proper level to type *)
let rec assign_level levels ccs = function
    Chi(l) -> Chi(List.map (assign_level levels ccs) l)
  | Chr(lv,l) -> (match (lvl_get lv levels) with
		    None -> failwith "Level not assigned."
		  | Some bla ->
		     (match (cc_get bla ccs) with
			None -> Chr(L 0, List.map (assign_level levels ccs) l)
		      | Some n-> Chr(L n, List.map (assign_level levels ccs) l)))
  | t -> t

let rec purge_level_typ = function
    Chr(lv, l) -> (match lv with V s -> Chr(L 0, (List.map (purge_level_typ) l))
			       | L i -> Chr(lv,  (List.map (purge_level_typ) l)))
  | Chi(l) -> Chi((List.map purge_level_typ l))
  | t -> t
	   
(* Assign proper levels to environment  *)
let level_assignment env = function
    [] -> List.map (fun (x,y) -> (x, purge_level_typ y)) env
  | _ as lconst ->
     let levels = (solve_lconst lconst) in
     let ccconsts = (gen_cc_const levels lconst) in
     let ccs = (extract_cc ccconsts) in
     let sved_ccs = (assign_all_cc ccconsts ccs) in
     List.map (fun (x,y) -> (x, purge_level_typ y))
	      (List.fold_left (fun x -> fun (a,typ) ->
			       (a,(assign_level
				    levels
				    sved_ccs
				    typ))::x
		    ) [] env)


(* NAT INFERENCE *)

(* Get the level of a name in an environment *)		       
let rec level_of a = function
    [] -> failwith "Trying to fetch level of an unknown identifier."
  | (b,Chr(lv,l)):: tl when a = b -> lv
  | (b,_):: tl when a = b -> failwith "Trying to fetch level of a non-(replicated channel) identifier."
  | _::tl -> level_of a tl				       
		    
(* Collect the nat types *)
let rec collect_nat = function
    [] -> []
  | (a,typ)::tl when typ = Nat -> (a, false)::(collect_nat tl)
  | (a, typ)::tl -> (collect_nat tl)

(* Store an upcoming type promotion. *)
let rec up_nat a = function
    [] -> []
  | (b,v)::tl when a = b -> (b, true)::tl
  | (b,v)::tl -> (b, v)::(up_nat a tl)

let rec merge_nat l1 l2 = match (l1,l2) with
    [], [] -> []
  | (a1, v1)::tl1, (a2, v2)::tl2 when a1 = a2 -> (a1, (v1 || v2))::(merge_nat tl1 tl2)
  | _ -> failwith "Mismatch while merging Nat types list"
						
(* Decide which type must be unsafe. *)
let decide env p =
  let rec aux under nats = function 
      Nil -> nats
    | Par (p1,p2) -> (merge_nat (aux under nats p1) (aux under nats p2))
    | Out (a,l) -> (match under with
		      None -> nats
		    | Some b -> if (env_get a env) = (env_get b env)
				then
				  List.fold_left
				    (fun x -> fun y -> match y with
							 Pred z ->
							 (try let zz = (simp_exp z) in
							      (up_nat zz x)
							  with Int_found -> x)
						       | _ -> x )
				    nats
				    l
				else nats)
    | Rin(a,l,pc) -> (aux (Some a) nats pc) 
    | In(a,l,pc) -> (aux under nats pc) 
    | Nu(a,pc) -> (aux under nats pc) 
    | IfZero(a,p1,p2) -> (merge_nat (aux under nats p1) (aux under nats p2))
  in
  aux None (collect_nat env) p

(* All types which are not unsafe are safe. *)
let rec purge_nat_typ = function
    Nat -> Nats
  | Chr(lv,l) -> Chr(lv, (List.map purge_nat_typ l))
  | Chi(l) -> Chi(List.map purge_nat_typ l)		    
  | t -> t

(* Decide when type does not need to be updated. *)	   
let rec more_precise (typ1 : comp_type) (typ2 : comp_type) under =
  let rec gen_pair x1 x2 =
    (match x1, x2 with
     | [],[] -> []
     | h1::tl1, h2::tl2 -> (h1, h2)::(gen_pair tl1 tl2)
     | _ -> failwith "Zipping lists of different size.")
  in  
  match typ1, typ2 with
    t1, t2 when t1 = t2 -> true
  | Natu, Nat -> true
  | Nats, Nat -> true
  | Nats, Natu -> true (* Once a name have been update with Nats it is safe *)
  | Nat, Natu -> if under then true else false (* No update of nat type inside linear channel *)
  | Chr(lv1, l1), Chr(lv2, l2) -> List.fold_left
				    (fun x -> fun (y1,y2) -> (x && (more_precise y1 y2 false)))
				    true
				    (gen_pair l1 l2)
  | Chi(l1), Chi(l2) -> List.fold_left
			  (fun x -> fun (y1,y2) -> (x && (more_precise y1 y2 true)))
			  true
			  (gen_pair l1 l2)
  | _ -> false
		   
exception Nat_fail of string
	   
let rec update_nat_type ot nt =
  let rec aux ot nt under =
    let rec update_type_list l1 l2 under = match (l1,l2) with
	[],[] -> []
      | h1::tl1, h2::tl2 -> let nt = try (aux h1 h2 under)
				     with No_change -> h1
			    in
			    nt::(update_type_list tl1 tl2 under)
      | _ -> failwith "Different list lengths while updating."
    in
    match (ot, nt) with
      (_,_) when (more_precise ot nt under) -> raise No_change
    | Chi(l1), Chi(l2) ->  Chi (update_type_list l1 l2 true)
    | Chr(lv1,l1), Chr(lv2,l2) ->  Chr (lv1, update_type_list l1 l2 false)
    | Nat, Natu -> if under then Nats else Natu
    | Nat, Nats -> Nats
    | Natu, Nats -> if under then Nats else raise (Nat_fail "Integer unsafe and safe.")		      
    | t1,t2 ->  failwith ("Unexpected type update case: "^(print_typ t1)^" and "^(print_typ t2))
  in aux ot nt false

(* When a integer is bound by a channel, its type is safe *)
let rec purge_linear_argument p = function
    [] -> []
  | (a, Natu)::tl -> 
     (match (bound_by a p) with
 	None -> (a, Natu)::(purge_linear_argument p tl)
      | Some (Inp b) -> (a, Nats)::(purge_linear_argument p tl)
      | _ -> (a, Natu)::(purge_linear_argument p tl))
  | h::tl -> h::(purge_linear_argument p tl)
  	 
let up_nat_env env p =
  let obl = object_list p in
  let nats = (decide env p) in
  purge_linear_argument p
  (List.fold_left
    (fun x -> fun (a,t) -> (a, (purge_nat_typ t))::x )
    []
    (List.fold_left
       (fun x -> fun (y,v) -> if v
			      then (update_env (update_nat_type) y Natu x obl)
			      else x
       )
       env
       nats))

(* WORK IN PROGRESS (\* DECREASING CHECK  *\) *)

(* exception RepTyp of string *)

(* let get_level exp env = *)
(*   match env_get exp env with *)
(*     Chr(L lev, l) -> lev *)
(*   | Chr(V va, l) -> failwith "Level "^va^" not instantiated." *)
(*   | _ -> failwith "Trying to get level of a non-levelled expression." *)

(* let separate_args pars =  function *)
(*     Chr(lv, ts) -> if List.length ts != List.length pars *)
(* 		   then failwith "Number of parameters not coherent with type." *)
(* 		   else *)
(* 		     let rec aux accu accs l1 = function *)
(* 			 [] -> (accu,accs) *)
(* 		       | Natu::t2 -> (match l1 with h1::t1 -> (aux h1::accu accs t1 t2) *)
(* 						  | _ -> failwith "List lengths mismatch.") *)
(* 		       | Nats::t2 -> (match l1 with h1::t1 -> (aux accu h1::accs t1 t2) *)
(* 						  | _ -> failwith "List lengths mismatch.") *)
(* 		       | T::t2 -> (match l1 with h1::t1 -> (aux accu accs t1 t2) *)
(* 					       | _ -> failwith "List lengths mismatch.") *)
(* 		     in aux [] [] pars ts *)

(* let compare_expr exp1 exp2 = match  *)
(*     let rec aux = function *)
	
				    
(* let output_check p env = *)
(*   let rec output_aux acc = function *)
(*       Nil -> () *)
(*     | Out(s,l) -> (match acc with *)
(* 		   | None -> () *)
(* 		   | Some (lc, pars, paru) ->  (match env_get s env with *)
(* 						  Chi(ts) -> () *)
(* 						| Chr(L l, ts) -> if (l < lc) then () else *)
 								    
									
(* 								     | _ -> failwith "Ill-formed output." *)
(* 		  ))) *)

		    
(* TYPECHECKING PROCEDURE *)
		    
let process_typecheck p =
  let _ = print_endline "" in
  let _ = print_endline "****** TYPECHECKING NEW PROCESS *********" in
  let _ = print_endline "" in
  let _ = print_endline "" in
  let _ = print_endline "*** Printing process." in
  let _ = (pretty_print_proc p) in
  let _ = print_endline "" in
  let _ = print_endline "=== TYPE INFERENCE ===" in
  let _ = print_endline "*** Generating constraints and environment." in
  let env,zip = (generate_env_constr p) in
  let _ = if mode then (print_endline "") else () in
  let _ = if mode then (print_endline "Environment:") else () in
  let _ = if mode then (pretty_print_env env) else () in
  let _ = if mode then (print_endline "") else () in
  let _ = if mode then (print_endline "Constraints:") else () in
  let _ = if mode then (pretty_print_constr zip) else () in  
  let _ = if mode then (print_endline "") else () in
  let _ = print_endline "*** Solving constraints." in
  match unify zip env with
  | Success e ->   (let _ = if mode then (print_endline "") else () in
		    let _ = (if mode then
			       let _ = print_endline "*** SUCCESS\nSimple Types: " in
			       pretty_print_env e
			     else print_endline "*** SUCCESS")
		    in
		    let _ = print_endline "" in
 		    let _ = print_endline "=== KIND INFERENCE ===" in
 		    let _ = print_endline "*** Deciding name kinds." in
		    try (let nk = promote_env e p in
			 let _ = (if mode then
				    (let _ = print_endline "" in
				     let _ = print_endline "*** SUCCESS. Name kinds:" in
				     let _ = pretty_print_env nk in
				     print_endline "")
				  else
				    (let _ = print_endline "*** SUCCESS." in
				     print_endline ""))
			 in
			 let _ = print_endline "*** Checking for nested replications." in
			 if (nest_rep p) then (print_endline "*** FAILURE. Nested replications detected.")
			 else
			   let _ = print_endline "*** SUCCESS." in
			   let _ = print_endline "" in
 			   let _ = print_endline "=== LEVEL INFERENCE ===" in
			   let _ = print_endline "*** Generating level constraints." in
			   let lconst = (generate_const p nk) in
			   let _ = if mode then (print_endline "") else () in
			   let _ = if mode then (print_endline "Level constraints:") else () in
			   let _ = if mode then print_endline (pretty_print_lconst lconst) else () in
			   let _ = print_endline "*** Assigning levels." in
			   let _ = print_endline "*** SUCCESS." in
			   let _ = print_endline "" in
			   let nj = level_assignment nk lconst in
			   let _ = if mode then pretty_print_env nj else () in
			   let _ = print_endline "*** Deciding Natural Types." in
			   let nl = (up_nat_env nj p) in
			   let _ = print_endline "*** SUCCESS." in
			   let _ = if mode then print_endline "Final types:" else () in
			   if true then (pretty_print_env nl) else ()
			)
		    with LinRep s -> print_endline ("*** FAILURE. "^s)
		   )
  | Failure s -> print_endline ("*** FAILURE. "^s)

(* main-like part *)
			       
let _ = process_typecheck wrong_ex1
			  
let _ = process_typecheck wrong_ex2

let _ = process_typecheck wrong_ex3

let _ = process_typecheck wrong_ex4

let _ = process_typecheck wrong_ex5

let _ = process_typecheck tricky_ex

let _ = process_typecheck tricky_ex2

let _ = process_typecheck ok_ex1
			  
let _ = process_typecheck add_ex

let _ = process_typecheck mult_ex

let _ = process_typecheck cube_ex

let _ = process_typecheck fact_ex