theory Type_Inference_Template
imports Types
begin

text {* Make the typing relation executable: *}

code_pred ctyping .

text {* Auxiliary function to collect variables in expressions and commands.  The function @{const List.insert} adds an element to a list if it is not already in the list. *}

fun avars :: "aexp => name list => name list"
where
  "avars (V x) vs = List.insert x vs"
| "avars (Plus e1 e2) vs = avars e2 (avars e1 vs)"
| "avars _ vs = vs"

fun bvars :: "bexp => name list => name list"
where
  "bvars (B _) vs = vs"
| "bvars (Not e) vs = bvars e vs"
| "bvars (And e1 e2) vs = bvars e2 (bvars e1 vs)"
| "bvars (Less e1 e2) vs = avars e2 (avars e1 vs)"

fun cvars :: "com => name list => name list"
where
  "cvars SKIP vs = vs"
| "cvars (x ::= a) vs = List.insert x (avars a vs)"
| "cvars (c1 ; c2) vs = cvars c2 (cvars c1 vs)"
| "cvars (IF b THEN c1 ELSE c2) vs =
    cvars c2 (cvars c1 (bvars b vs))"
| "cvars (WHILE b DO c) vs =
    cvars c (bvars b vs)"


text {* Type variables and constraints *}

datatype tvar = TVar name | Type ty

fun type_of :: "tyenv => tvar => ty"
where
  "type_of \<Gamma> (TVar v) = \<Gamma>(v)"
| "type_of \<Gamma> (Type t) = t"

types
  constraint = "tvar * tvar"
  constraints = "constraint list"

fun constraint_holds :: "tyenv => constraint => bool" (infix "\<Turnstile>" 50)
where "\<Gamma> \<Turnstile> (v, v') <-> type_of \<Gamma> v = type_of \<Gamma> v'"

subsection {* Constraint generation *}

fun alist2constr :: "tvar=>name list=>constraints"
where
  "alist2constr t (h#nl) =  ( t , (TVar h))# (alist2constr t nl)"|
  "alist2constr t []=[]"


fun aconstcoll:: "tvar=>aexp=>constraints"
where
  "aconstcoll tv (Ic i)=(tv, Type Ity)#[]"|
  "aconstcoll tv (Rc i)=(tv, Type Rty)#[]"|
  "aconstcoll tv (V n)=[]"|
  "aconstcoll tv (Plus a1 a2)=(aconstcoll tv a1)@(aconstcoll tv a2)"
(*aexp fertig*)

fun atvarcoll::"aexp=>tvar list => tvar list"
where
  "atvarcoll (V x)  vs = List.insert (TVar x)   vs"
| "atvarcoll (Ic i) vs = (Type Ity) # vs"
| "atvarcoll (Rc r) vs = (Type Rty) # vs"   
| "atvarcoll (Plus e1 e2) vs = atvarcoll e2 (atvarcoll e1 vs)"
| "atvarcoll _ vs = vs"



fun blist2constr:: "tvar list => constraints"
where
  "blist2constr []=[]"|(*eine leere Liste erzeugt kein constraint*)
  "blist2constr (h#[])=[]"|(*einzelne Variablen erzeugen kein Constraint*)
  "blist2constr (h1#h2#nl)=(h1,h2)#(blist2constr (h2#nl))"(*Die ersten 2 Elemente bilden ein constraint, da alle Variablen im Konstrukt den gleichen Typ haben müssen.*)

fun btvarcoll::"bexp=>tvar list => constraints"
where
  "btvarcoll (B _) vs=[]"
| "btvarcoll (Not e) vs = btvarcoll e vs"
| "btvarcoll (And e1 e2) vs = (btvarcoll e2 vs)@(btvarcoll e1 vs)"
| "btvarcoll (Less e1 e2) vs = blist2constr (atvarcoll e2 (atvarcoll e1 vs))"


fun ccollect :: "com => constraints"
where 
  "ccollect (c1;c2)= (ccollect c1)@(ccollect c2)"|
  "ccollect  SKIP  = []"|
  "ccollect (n::=ae) = (alist2constr (TVar n) (avars ae []))@(aconstcoll (TVar n) ae)"|  (*todo: Konstanten<-> var  hinzufügen*)
  "ccollect (IF be THEN c1 ELSE c2)=(btvarcoll be [] )@((ccollect c1)@(ccollect c2))"|
  "ccollect (WHILE be DO c)=(btvarcoll  be [])@(ccollect c)"
(*  "ccollect _ = []"*) (* add definition here *) (*todo: löschen?*)


lemma ccollect_sound_and_complete:
"\<Gamma> \<turnstile> c <-> (\<forall>C \<in> set (ccollect c). \<Gamma> \<Turnstile> C)"
quickcheck[iterations=200,size=8,report] 
oops


subsection {* Constraint solving *}


fun constrVarCheck:: "tvar => tvar => (name * tvar) list => (name * tvar) list option "
where
  "constrVarCheck (TVar n) t M=( if ((map_of M n)=None) then  (Some ((n,t)#[]))  else (None))"(*todo: Else Teil mit if*)

fun solve :: "constraints => (name * tvar) list => (name * tvar) list option"
where
  "solve ((Type Ity,Type Rty)#clst) M=None"(*erstmal Konstanten filtern (funktionierend/nicht funktionierend)*)
| "solve ((Type Rty,Type Ity)#clst) M=None"
| "solve ((Type Ity,Type Ity)#clst) M=solve clst M"(*ohne Widerspruch zum nächsten Constraint*)
| "solve ((Type Rty,Type Rty)#clst) M=solve clst M"

| "solve ((TVar n  ,Type t)#clst)   M=(if ((map_of M n)=None) then (solve clst (( n,Type t)#M)) else (if ((map_of M n)=(Some (Type t))) then (solve clst M) else None ) )"(*entweder: neu, vorhanden oder Widerspruch*)(*Problem, wenn TVar und Type verglichen werden*)
| "solve ((Type t  ,TVar n)#clst)   M=(if ((map_of M n)=None) then (solve clst (( n,Type t)#M)) else (if ((map_of M n)=(Some (Type t))) then (solve clst M) else None ) )"(*entweder: neu, vorhanden oder Widerspruch*)

| "solve ((TVar n1 ,TVar n2)#clst)  M=(if ((map_of M n1)=None) 
                                      then (if ((map_of M n2)=None) 
                                            then ( solve clst ((n1,TVar n2)#M)(* auch n2, n1?*)) (*neu komplett*)
                                            else ( solve clst ((n1,TVar n2)#M)) )                (*neu links*)
                                      else (if ((map_of M n2)=None)
                                       then ( solve clst ((n2, TVar n1)#M)) (*neu rechts*)
                                       else  (
                                            (if ((map_of M n2)=(map_of M n1)) (*          <----------------- mögliches Problem, wenn TVar und Type hier verglichen werden*)
                                            then ( solve clst M) (*vorhanden*)
                                            else ( None))))        (*Wenn ungleich-> Widerspruch*)
                                      )"(*todo neu rechts*)(*neu komplett, neu links, vorhanden oder Widerspruch*)

| "solve [] M = Some M" (*Constraints ohne Widerspruch abgearbeitet *)




subsection {* Type inference *}

fun type_infer :: "com => (name * tvar) list option"
where
  "type_infer c = 
    (let constraints = ccollect c;
         vars = cvars c [];
         init = map (\<lambda>x. (x, TVar x)) vars
     in solve constraints init)"

subsection {* Specification of type inference *}

definition instantiate :: "(name => ty) => (name \<times> tvar) list => tyenv"
where
  "instantiate I M =
    (\<lambda>x. case map_of M x of
      None => I x
    | Some (Type T) => T
    | Some (TVar y) => I y)"

fun is_instance :: "tyenv => (name \<times> tvar) list => bool" (infix "<:" 50)
where
  "\<Gamma> <: [] <-> True"
| "\<Gamma> <: ((x,Type t)#M) <-> (\<Gamma>(x) = t \<and> \<Gamma> <: M)"
| "\<Gamma> <: ((x,TVar y)#M) <-> (\<Gamma>(x) = \<Gamma>(y) \<and> \<Gamma> <: M)"

text {* The following lemmas are formulated in a way that is suitable
for counterexample generation with quickcheck. *}

lemma type_infer_sound:
"(case type_infer c of
    None => True
  | Some M => (instantiate I M \<turnstile> c))"
quickcheck[iterations=200,size=8,report]
oops

lemma type_infer_complete:
"\<Gamma> \<turnstile> c -->
  (case type_infer c of 
     None => False
   | Some M => \<Gamma> <: M)"
quickcheck[iterations=200,size=8,report]
oops


end