(* INTERPRETE ASTRATTO SUI TIPI *)

module type types =
sig


open Expr

type tipo = Vvar of string
        | Intero
        | Booleano
        | Mkprod of tipo * tipo
        | Mkarrow of tipo * tipo
val infertypes : exp -> tipo



end



module Typeinfer: types =
struct
open Expr

type gterm = 
  |Gvar of string
  |Node of string * gterm list

type subst = (gterm * gterm) list
 
let emptysubst = []

let newassociation (x,t) = [(x,t)]

let rec map f l =
  match l with
  [] -> []
  |(a::ll) -> ((f a)::(map f ll))

let rec assoc (st,s) =
   match s with 
   [] -> st
   |((x,t)::y) -> if x = st then t else assoc(st,y)

let rec applysubst s t =
  match t with
  (Gvar(x)) -> assoc(Gvar(x),s)
  |(Node(x,y)) -> Node(x,map (applysubst s) y)

    
let rec occurs (x,s) =
  match s with
  [] -> false
  |((y,t)::z) -> if x=y then true else occurs(x,z)
  
let rec simpl (sigma1,sigma2) = 
  match sigma2 with
  [] -> []
  |((x,t)::y) -> if occurs (x,sigma1) 
                 then simpl(sigma1,y)
                 else ((x,t)::(simpl(sigma1,y))) 

let rec compose (sigma1,sigma2) =
   match sigma1 with
   [] -> simpl(sigma1,sigma2)
   |((x,t)::s) -> let n = applysubst sigma2 t in
                  if n = x 
                  then compose(s,sigma2)
                  else ((x, n)::(compose(s,sigma2)))

let rec bigor l =
   match l with
   [] -> false
   |(a::b) -> if a then true else bigor(b)

let rec occur_in_term x t =
   match t with
   Gvar(y) -> if x=t then true else false
   |Node(_,l) -> bigor(map (occur_in_term x) l)

let rec gunify (pat,ter) =
  match (pat, ter) with
  |(Gvar(x),Gvar(y)) -> if x = y then emptysubst else
                        newassociation(pat,ter)
  |(Gvar(x),t) -> if occur_in_term pat ter 
                 then failwith ("no unification - left occur") 
                 else newassociation(pat,ter)
  |(t,Gvar(x)) -> if occur_in_term ter pat 
                 then failwith ("no unification - right occur") 
                 else newassociation(ter,pat)
  |(Node(x,lp),Node(y,lt)) -> if x = y 
                              then lgunify(lp,lt)
                              else failwith ("no unification - different 
                              constructors")
  and lgunify (lp,lt) =
  match (lp,lt) with
  ([],[]) -> emptysubst
  |((p1::pp),(t1::tt)) -> let sigma = gunify(p1,t1) in
                          compose(sigma,
                          (lgunify 
                             (map (applysubst sigma) pp,
                              map (applysubst sigma) tt)))
  | (_,_) -> failwith ("no unification - different arity")

let rec appplys (s,l) =
   match l with
     |[] -> []
     |(a,b)::l1 -> [(((applysubst s) a),((applysubst s) 
     b))] @ appplys(s,l1) 

  
let rec unifylist (l) =
   match l with
     |[] -> emptysubst
     |(a,b)::l1 -> let sigma = gunify(a,b) in
                     compose(sigma, 
                     unifylist(appplys(sigma,l1)))          

let (newvar,initvar) =
   let count = ref(-1) in
   (fun () -> count := !count +1;
              Gvar("var" ^ (string_of_int !count))),
   (fun () -> count := -1)

type tipo = Vvar of string
        | Intero
        | Booleano
        | Mkprod of tipo * tipo
        | Mkarrow of tipo * tipo
        
let rec up t = 
  match t with
  (Gvar(x)) -> Vvar(x)
  |(Node("Intero",[])) -> Intero
  |(Node("Booleano",[])) -> Booleano
  |(Node("Mkprod",[x;y])) -> Mkprod(up(x),up(y))  
  |(Node("Mkarrow",[x;y])) -> Mkarrow(up(x),up(y))
  |(_) -> failwith("term with wrong signature")

let rec down t =
  match t with 
  (Vvar(x)) -> Gvar(x)
  |(Intero) -> Node("Intero",[])
  |(Booleano) -> Node("Booleano",[])
  |(Mkprod(x,y)) -> Node("Mkprod",[down(x);down(y)])   
  |(Mkarrow(x,y)) -> Node("Mkarrow",[down(x);down(y)])


  type env = int

  type proc = exp * env	   
	 
  and ceval =
    	  Funval of proc	  
    	| Mkpair of ceval * ceval
      	| Int of int 
      	| Bool of bool 
      	| Unbound
      	| Indef  

type eval = 
       | T of (gterm * ((gterm* gterm) list))
       | T1 of ceval
       | Tunbound
       
  let alfa (x) = match x with
       | Int(n) -> T(down(Intero),[])
       | Bool(n) -> T(down(Booleano),[])
       | Indef -> T(newvar(),[])
       | Unbound -> Tunbound
       | Funval(a,b) -> T1(Funval(a,b))
       | _ -> failwith "manca il caso del Mkpair" 

  let gamma (x) = match x with
       | T1(y) -> y
       | _ -> Unbound
       
  let abstrproc (b) = 
      let b1 = gamma(b) in
      (match b1 with 
         | Funval(x,y) -> true
         | _ -> false)
         
  let abstreq (x,y) =
      match (x,y) with
      | (T(v1,c1),T(v2,c2)) -> (v1 = v2)
      | (_,_) -> (x = y)

    let minus x = 
      match x with
        | T(v,c) -> T(down(Intero),
                               unifylist((v,down(Intero)) :: c))
        | _ -> failwith ("type error")
      
    	
    let iszero x =
      match x with
        | T(v,c) -> T(down(Booleano),
                               unifylist((v,down(Intero)) :: c))
        | _ -> failwith ("type error")
     	
    let equ (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let plus (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let diff (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let mult (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
    
    let pair (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    let sigma = unifylist(c1 @ c2) in
                    T(applysubst sigma (down(Mkprod(up(v1),up(v2)))),sigma)
        | _ -> failwith ("type error") 
    
      
    let first x =
       match x with
   	     |T(y,z) -> let f1 =newvar() in
   	               let sigma = unifylist((down(Mkprod(up(f1),up(newvar()))),y):: z) in
   	                    T(applysubst sigma f1,sigma)
   	     |_ -> failwith ("type error")
   	     
    let snd x =
       match x with
   	     |T(y,z) -> let f1 =newvar() in
   	               let sigma = unifylist((down(Mkprod(up(newvar()),up(f1))),y):: z) in
   	                    T(applysubst sigma f1,sigma)
   	     |_ -> failwith ("type error")
   	      
    let et (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Booleano)) :: (v2,down(Booleano)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let vel (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Booleano)) :: (v2,down(Booleano)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let non x =
      match x with
        | T(v,c) -> T(down(Booleano),
                               unifylist((v,down(Booleano)) :: c))
        | _ -> failwith ("type error")
      
  let merge (g,x,y) =
    match (g,x,y) with
        | (T(v0,c0),T(v1,c1),T(v2,c2)) ->
             let sigma = unifylist((v0,down(Booleano)) :: (v1,v2) :: (c0 @ c1 @ c2)) in 
                  T(applysubst sigma v1,sigma)                    
        | _ -> failwith ("type error")
                     
  let valid (x) = false
  
  let unsatisfiable (x) = false

type 'x stack = ('x array) * int ref

let emptystack(nm,x) = (Array.create nm x, ref(-1))

let push(x,(s,n)) = if !n = (Array.length(s) - 1) then
                   failwith("full stack") else 
                   (Array.set s (!n +1) x;
                   n := !n +1)
                                     
let top(s,n) = if !n = -1 then
                           failwith("top is undefined")
                           else Array.get s !n 

let pop(s,n) = if !n = -1 then
                           failwith("pop is undefined")
                           else n:= !n -1
                           
let empty(s,n) = if !n = -1 then
                           true
                           else false 
                           
let lungh(s,n) = !n 

let access ((s,n), k) =
          if not(k > !n) & not(k < 0) then
          Array.get s k
          else failwith("error in access")
          
let svuota (s,n) = n := -1

(* Etichette: aggiunto il caso per il condizionale *)           
          
type label = Tovisit| Ready| Revisited




(* Funzioni di comodo e pile globali *)

let nop = function () -> let x =ref(1) in x:= 0

let stacksize = 100

let cframesize(e) = 20

let tframesize(e) = 20

let namestack = emptystack(stacksize,Id("dummy"))

let dvalstack = emptystack(stacksize,alfa(Unbound))

let slinkstack = emptystack(stacksize, -1)

type tag = Standard | Retained

let tagstack = emptystack(stacksize, Standard)

let retained (n:env) = if access(tagstack,n) = Retained 
                       then true else false  

let currentenv = ref(0)

let cstack = emptystack(stacksize,emptystack(1,(Tovisit,Eint(0))))

let tempvalstack = emptystack(stacksize,emptystack(1,alfa(Unbound)))

let newframes(e) =
   let cframe = emptystack(cframesize(e),(Tovisit,e)) in
   let tframe = emptystack(tframesize(e),alfa(Unbound)) in
   push((Tovisit,e),cframe);
   push(cframe,cstack);
   push(tframe,tempvalstack)
   
let retain () = 
       match tagstack with (a,m) ->
       Array.set a !currentenv Retained;
       let cont = ref(lungh(dvalstack)) in
       while !cont > -1  & retained(!cont) do cont := !cont - 1 done;
       currentenv := !cont

(* Operazioni sull'ambiente: astrazione di Unbound *)

let emptyenv = -1

let applyenv ((x: env), (y: ide)) = 
       let n = ref(x) in
       let den = ref(alfa(Unbound)) in
       while !n > -1 do
          if access(namestack,!n)=y then
          (den := access(dvalstack,!n);
          n := -1)
          else n := access(slinkstack,!n)
       done;
       !den
       
let bind ((r:env),i,d) = 
        push(i,namestack); 
        push(d,dvalstack);
        push(Standard,tagstack);
        push(r,slinkstack);   
        currentenv:= lungh(dvalstack); 
        !currentenv 

(* Tabelle per il memoing *)

let size = 100

let emptyclos = (Eint 1  ,-1)

let tproc = Array.create size emptyclos

let targ = Array.create size (alfa Unbound)

let tres = Array.create size (alfa Indef)

let inittables () = let i = ref(0) in
                    while !i < size do
                      Array.set tproc !i emptyclos;
                      i := !i + 1 
                    done  


let initstate () =
     currentenv := lungh(dvalstack)

let makefun ((a:exp),(x:env)) =
      (match a with
      |	Fun(ii,aa) -> alfa(Funval(a,x))
      |	_ -> failwith ("Non-functional object"))

let rec	applyfun ((a1:eval),(b:eval)) =
      (match (gamma a1) with
      | Funval(Fun(ii,aa),x) ->
        let i = ref(0) in
        let v = ref(alfa(Indef)) in
        while !i < size do
          if Array.get tproc !i = (Fun(ii,aa),x) & 
              abstreq(Array.get targ !i, b) then
          (v := Array.get tres !i;
          i := size)
          else (if Array.get tproc !i = emptyclos then
          (Array.set tproc !i (Fun(ii,aa),x);
          Array.set targ !i b;
          Array.set tres !i !v;
          bind(x,ii,b);
          v := sem1(aa);  
          Array.set tres !i !v;
          i := size)
          else i := !i +1)
        done;
        !v
        
      | Unbound -> 
         (match (a1,b) with
         | (T(v,c),T(vb,cb)) -> let v1 = newvar() in 
                     let v2 = newvar() in
                     let sigma = unifylist( 
                (v, (down(Mkarrow(up(v1),up(v2))))) :: (vb,v1) :: (c @ cb)) in
                T(applysubst sigma v2,sigma)
         | (T(v,c), T1(b1)) -> 
             (match inffuncttype(b) with 
              | T(vb,cb) -> let v1 = newvar() in 
                     let v2 = newvar() in
                     let sigma = unifylist( 
                (v, (down(Mkarrow(up(v1),up(v2))))) :: (vb,v1) :: (c @ cb)) in
                T(applysubst sigma v2,sigma)
              | _ -> failwith "errore in applyfun")    
         | _ -> failwith "errore in applyfun"))


and inffuncttype (e) = 
    match e with 
    | T1 (x) -> 
         let v1 = newvar() in
         initstate();
         let f1 = applyfun(e,T(v1,[])) in
         let f2 = inffuncttype(f1) in
         (match f2 with
         | T(v2,c2) -> let sigma = unifylist(c2) in
           T(applysubst sigma (down(Mkarrow(up(v1),up(v2)))),sigma)
         | _ -> failwith "caso impossibile")
    | x -> x

      
and	sem1 ((e:exp)) =
  let l = lungh(cstack) in
  newframes(e);
  while not(lungh(cstack) = l) do 
    while not(empty(top(cstack))) do  
     let continuation = top(cstack) in
     let tempstack = top(tempvalstack) in     
     let rho = !currentenv in             
     match top(continuation) with
      |(Tovisit,x) -> 
         (pop(continuation);
         push((Ready,x),continuation); 
         match x with
          | Pair(a,b) -> push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Iszero(a) -> push((Tovisit,a),continuation)
          | Eq(a,b) -> push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | First(a) -> push((Tovisit,a),continuation)
          | Snd(a) -> push((Tovisit,a),continuation)
          | Prod(a,b) ->  push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Sum(a,b) -> push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Diff(a,b)  ->  push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Minus(a) ->  push((Tovisit,a),continuation)
          | And(a,b) ->  push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Or(a,b) ->  push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)
          | Not(a) -> push((Tovisit,a),continuation)
          | Ifthenelse(a,b,c) -> push((Tovisit,a),continuation)          
          | Appl(a,b) -> push((Tovisit,a),continuation); 
                push((Tovisit,b),continuation)                
          | Let(i,a,b) -> push((Tovisit,a),continuation)              
          | (_) -> nop())             
      |(Ready,x) -> 
         (pop(continuation);
         match x with        
          | Eint(n) ->  push(alfa(Int(n)),tempstack)
          | Ebool(b) -> push(alfa(Bool(b)),tempstack)          
          | Var(i) ->   let d = applyenv(rho,i) in
                          if d = alfa(Unbound) then
                          failwith "Unbound atom" else   
                          push(d,tempstack)
          | Pair(a,b) -> let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(pair(firstarg,sndarg),tempstack)
          | Iszero(a) -> 
             let arg=top(tempstack) in
             pop(tempstack);
             push(iszero(arg),tempstack)
          | Eq(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(equ(firstarg,sndarg),tempstack)
          | First(a) -> let arg=top(tempstack) in
             pop(tempstack);
             push(first(arg),tempstack)
          | Snd(a) -> let arg=top(tempstack) in
             pop(tempstack);
             push(snd(arg),tempstack)
          | Prod(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(mult(firstarg,sndarg),tempstack)  
          | Sum(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(plus(firstarg,sndarg),tempstack)
          | Diff(a,b)  -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(diff(firstarg,sndarg),tempstack) 
          | Minus(a) -> 
             let arg=top(tempstack) in
             pop(tempstack);
             push(minus(arg),tempstack)  
          | And(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(et(firstarg,sndarg),tempstack)  
          | Or(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack);
             push(vel(firstarg,sndarg),tempstack)  
          | Not(a) -> 
             let arg=top(tempstack) in
             pop(tempstack);
             push(non(arg),tempstack)
          | Ifthenelse(a,b,c) ->
             let arg=top(tempstack) in
             pop(tempstack);
             if valid(arg) 
              then push((Tovisit,b),continuation)
              else 
              (if unsatisfiable(arg) then 
                  push((Tovisit,c),continuation)
               else
               (push(arg,tempstack); 
               push((Revisited,Ifthenelse(a,b,c)),continuation);
               push((Tovisit,b),continuation);
               push((Tovisit,c),continuation)))
          | Fun(i,a) ->  push(makefun(Fun(i,a),rho),tempstack)
          | Appl(a,b) -> 
             let firstarg=top(tempstack) in
             pop(tempstack);
             let sndarg=top(tempstack) in
             pop(tempstack); 
             push(applyfun(firstarg,sndarg),tempstack)
          | Let(i,a,b) -> 
             let arg=top(tempstack) in
             pop(tempstack);
             bind(rho,i,arg); 
             newframes(b)              
          | Letrec(i,a,b) ->
             bind(rho,i,makefun(a,lungh(dvalstack) + 1));
      	     newframes(b))
      	 |(Revisited,x) -> 
         (pop(continuation);
         match x with
         | Ifthenelse(a,b,c) ->
             let arg3 = top(tempstack) in
             (pop(tempstack);
             let arg2 = top(tempstack) in
             (pop(tempstack);
             let arg1 = top(tempstack) in
             (pop(tempstack);
                push(merge(arg1,arg2,arg3),tempstack))))
         | _ -> failwith "caso impossibile")
      done;
      let valore= top(top(tempvalstack)) in
      pop(cstack);
      pop(tempvalstack);
      push(valore,top(tempvalstack));
      if !currentenv < lungh(dvalstack) then retain()
        else if abstrproc(valore) then retain()
         else
           (pop(tagstack);
            pop(namestack);
            pop(dvalstack);
            pop(slinkstack);
            while not(empty(dvalstack)) & retained(lungh(dvalstack)) do
               pop(tagstack);
               pop(namestack);
               pop(dvalstack);
               pop(slinkstack) done;
            currentenv := lungh(dvalstack))
    done;
    let r = top(top(tempvalstack)) in
    pop(top(tempvalstack));
    r





     

let	infertypes ((e:exp)) =
  svuota(cstack);svuota(tempvalstack);svuota(dvalstack);
  svuota(namestack);svuota(slinkstack);svuota(tagstack);
  inittables();
  push(emptystack(2,alfa(Unbound)),tempvalstack);
  bind(emptyenv,Id "dummy", alfa(Unbound)); 
  let r = inffuncttype(sem1(e)) in
  (match r with 
  | T(v,c) -> up(v)
  | _ -> failwith "errore nel'inferenza dei tipi")



end