open Format open Syntax open Support.Error open Support.Pervasive (* ------------------------ EVALUATION ------------------------ *) let rec isval ctx t = match t with TmTrue(_) -> true | TmFalse(_) -> true | TmAbs(_,_,_,_) -> true | _ -> false exception NoRuleApplies let rec eval1 ctx t = match t with TmIf(_,TmTrue(_),t2,t3) -> t2 | TmIf(_,TmFalse(_),t2,t3) -> t3 | TmVar(fi,n,_) -> (match getbinding fi ctx n with TmAbbBind(t,_) -> t | _ -> raise NoRuleApplies) | TmApp(_,TmError(fi),t2) -> TmError(fi) | TmApp(_,v1,TmError(fi)) when isval ctx v1 -> TmError(fi) | TmApp(fi,TmAbs(_,x,tyT11,t12),v2) when isval ctx v2 -> termSubstTop v2 t12 | TmApp(fi,v1,t2) when isval ctx v1 -> let t2' = eval1 ctx t2 in TmApp(fi, v1, t2') | TmApp(fi,t1,t2) -> let t1' = eval1 ctx t1 in TmApp(fi, t1', t2) | TmIf(_,TmError(fi),t2,t3) -> TmError(fi) | TmIf(fi,t1,t2,t3) -> let t1' = eval1 ctx t1 in TmIf(fi, t1', t2, t3) | _ -> raise NoRuleApplies let rec eval ctx t = try let t' = eval1 ctx t in eval ctx t' with NoRuleApplies -> t (* ------------------------ SUBTYPING ------------------------ *) let evalbinding ctx b = match b with TmAbbBind(t,tyT) -> let t' = eval ctx t in TmAbbBind(t',tyT) | bind -> bind let istyabb ctx i = match getbinding dummyinfo ctx i with TyAbbBind(tyT) -> true | _ -> false let gettyabb ctx i = match getbinding dummyinfo ctx i with TyAbbBind(tyT) -> tyT | _ -> raise NoRuleApplies let rec computety ctx tyT = match tyT with TyVar(i,_) when istyabb ctx i -> gettyabb ctx i | _ -> raise NoRuleApplies let rec simplifyty ctx tyT = try let tyT' = computety ctx tyT in simplifyty ctx tyT' with NoRuleApplies -> tyT let rec tyeqv ctx tyS tyT = let tyS = simplifyty ctx tyS in let tyT = simplifyty ctx tyT in match (tyS,tyT) with (TyBool,TyBool) -> true | (TyBot,TyBot) -> true | (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) -> (tyeqv ctx tyS1 tyT1) && (tyeqv ctx tyS2 tyT2) | (TyTop,TyTop) -> true | (TyVar(i,_), _) when istyabb ctx i -> tyeqv ctx (gettyabb ctx i) tyT | (_, TyVar(i,_)) when istyabb ctx i -> tyeqv ctx tyS (gettyabb ctx i) | (TyVar(i,_),TyVar(j,_)) -> i=j | _ -> false let rec subtype ctx tyS tyT = tyeqv ctx tyS tyT || let tyS = simplifyty ctx tyS in let tyT = simplifyty ctx tyT in match (tyS,tyT) with (TyBot,_) -> true | (_,TyTop) -> true | (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) -> (subtype ctx tyT1 tyS1) && (subtype ctx tyS2 tyT2) | (_,_) -> false let rec join ctx tyS tyT = if subtype ctx tyS tyT then tyT else if subtype ctx tyT tyS then tyS else let tyS = simplifyty ctx tyS in let tyT = simplifyty ctx tyT in match (tyS,tyT) with (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) -> TyArr(meet ctx tyS1 tyT1, join ctx tyS2 tyT2) | _ -> TyTop and meet ctx tyS tyT = if subtype ctx tyS tyT then tyS else if subtype ctx tyT tyS then tyT else let tyS = simplifyty ctx tyS in let tyT = simplifyty ctx tyT in match (tyS,tyT) with (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) -> TyArr(join ctx tyS1 tyT1, meet ctx tyS2 tyT2) | _ -> TyBot (* ------------------------ TYPING ------------------------ *) let rec typeof ctx t = match t with TmVar(fi,i,_) -> getTypeFromContext fi ctx i | TmAbs(fi,x,tyT1,t2) -> let ctx' = addbinding ctx x (VarBind(tyT1)) in let tyT2 = typeof ctx' t2 in TyArr(tyT1, typeShift (-1) tyT2) | TmApp(fi,t1,t2) -> let tyT1 = typeof ctx t1 in let tyT2 = typeof ctx t2 in (match simplifyty ctx tyT1 with TyArr(tyT11,tyT12) -> if subtype ctx tyT2 tyT11 then tyT12 else error fi "parameter type mismatch" | TyBot -> TyBot | _ -> error fi "arrow type expected") | TmTrue(fi) -> TyBool | TmFalse(fi) -> TyBool | TmIf(fi,t1,t2,t3) -> if subtype ctx (typeof ctx t1) TyBool then join ctx (typeof ctx t2) (typeof ctx t3) else error fi "guard of conditional not a boolean" | TmError(fi) -> TyBot | TmTry(fi,t1,t2) -> join ctx (typeof ctx t1) (typeof ctx t2)