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 \ (TVar v) = \(v)" | "type_of \ (Type t) = t" types constraint = "tvar * tvar" constraints = "constraint list" fun constraint_holds :: "tyenv => constraint => bool" (infix "\" 50) where "\ \ (v, v') <-> type_of \ v = type_of \ 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: "\ \ c <-> (\C \ set (ccollect c). \ \ C)" quickcheck[iterations=200,size=8,report] oops subsection {* Constraint solving *} fun setVarInList::" tvar=>tvar=> (name*tvar)list => (name*tvar) list" where "setVarInList _ _ []=[]" | "setVarInList (TVar b_vgl) (Type b_neu) ((a,b_alt)#M )= (if (b_alt=(TVar b_vgl)) (*Frage: Warum ist der Konstruktor TVar hier nötig?*) then (a,Type b_neu)#(setVarInList (TVar b_vgl) (Type b_neu) M) (*Frage: Warum ist hier Type b_neu nötig?*) else (a,b_alt)#(setVarInList (TVar b_vgl) (Type b_neu) M))" | "setVarInList (TVar b_vgl) (TVar b_neu) ((a,b_alt)#M )= (if (b_alt= (TVar b_vgl)) then (a,TVar b_neu)#(setVarInList (TVar b_vgl) (TVar b_neu) M) else (a,b_alt)#(setVarInList (TVar b_vgl) (TVar b_neu) M))" 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=(case (map_of M n) of None => None (*Startliste unvollständig*) |Some (Type tn) =>(if tn=t then solve clst M else None) |Some (TVar v ) =>solve clst (setVarInList (TVar v) (Type t) 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=(case (map_of M n) of None => None (*Startliste unvollständig*) |Some (Type tn) =>(if tn=t then solve clst M else None) |Some (TVar v ) =>solve clst (setVarInList (TVar v) (Type t) 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=( case (map_of M n1) of None => None (*->Startliste unvollständig*) |Some(Type t) => (case (map_of M n2) of None => None (*Startliste unvollständig*) |Some (Type t2) =>(if t2=t then solve clst M else None) |Some (TVar v ) =>solve clst (setVarInList (TVar v) (Type t) M) ) |Some(TVar tn1)=> (case (map_of M n2) of None => None (*Startliste unvollständig*) |Some (Type t) => solve clst (setVarInList (TVar tn1) (Type t) M) |Some (TVar tv) => solve clst (setVarInList (TVar tn1) (TVar tv) 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 *) value "solve [ (TVar 0, TVar 2), (TVar 2, Type Rty), (TVar 1, TVar 0)] ( (map (\x. (x, TVar x)) [0,1,2]))" subsection {* Type inference *} fun type_infer :: "com => (name * tvar) list option" where "type_infer c = (let constraints = ccollect c; vars = cvars c []; init = map (\x. (x, TVar x)) vars in solve constraints init)" subsection {* Specification of type inference *} definition instantiate :: "(name => ty) => (name \ tvar) list => tyenv" where "instantiate I M = (\x. case map_of M x of None => I x | Some (Type T) => T | Some (TVar y) => I y)" fun is_instance :: "tyenv => (name \ tvar) list => bool" (infix "<:" 50) where "\ <: [] <-> True" | "\ <: ((x,Type t)#M) <-> (\(x) = t \ \ <: M)" | "\ <: ((x,TVar y)#M) <-> (\(x) = \(y) \ \ <: 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 \ c))" quickcheck[iterations=200,size=8,report] oops lemma type_infer_complete: "\ \ c --> (case type_infer c of None => False | Some M => \ <: M)" quickcheck[iterations=200,size=8,report] oops end