open Format open Support.Error open Support.Pervasive (* ---------------------------------------------------------------------- *) (* Datatypes *) type ty = TyTop | TyVar of int * int | TyString | TyAll of string * ty * ty | TySome of string * ty * ty | TyArr of ty * ty | TyRecord of (string * ty) list | TyBool | TyNat | TyUnit | TyId of string | TyFloat type term = TmAscribe of info * term * ty | TmString of info * string | TmTAbs of info * string * ty * term | TmTApp of info * term * ty | TmPack of info * ty * term * ty | TmUnpack of info * string * string * term * term | TmVar of info * int * int | TmAbs of info * string * ty * term | TmApp of info * term * term | TmRecord of info * (string * term) list | TmProj of info * term * string | TmTrue of info | TmFalse of info | TmIf of info * term * term * term | TmZero of info | TmSucc of info * term | TmPred of info * term | TmIsZero of info * term | TmUnit of info | TmFloat of info * float | TmTimesfloat of info * term * term | TmLet of info * string * term * term | TmInert of info * ty | TmFix of info * term type binding = NameBind | TyVarBind of ty | VarBind of ty | TyAbbBind of ty | TmAbbBind of term * (ty option) type context = (string * binding) list type command = Import of string | Eval of info * term | Bind of info * string * binding | SomeBind of info * string * string * term (* ---------------------------------------------------------------------- *) (* Context management *) let emptycontext = [] let ctxlength ctx = List.length ctx let addbinding ctx x bind = (x,bind)::ctx let addname ctx x = addbinding ctx x NameBind let rec isnamebound ctx x = match ctx with [] -> false | (y,_)::rest -> if y=x then true else isnamebound rest x let rec pickfreshname ctx x = if isnamebound ctx x then pickfreshname ctx (x^"'") else ((x,NameBind)::ctx), x let index2name fi ctx x = try let (xn,_) = List.nth ctx x in xn with Failure _ -> let msg = Printf.sprintf "Variable lookup failure: offset: %d, ctx size: %d" in error fi (msg x (List.length ctx)) let rec name2index fi ctx x = match ctx with [] -> error fi ("Identifier " ^ x ^ " is unbound") | (y,_)::rest -> if y=x then 0 else 1 + (name2index fi rest x) (* ---------------------------------------------------------------------- *) (* Shifting *) let tymap onvar c tyT = let rec walk c tyT = match tyT with TyString -> TyString | TyTop -> TyTop | TyVar(x,n) -> onvar c x n | TyAll(tyX,tyT1,tyT2) -> TyAll(tyX,walk c tyT1,walk (c+1) tyT2) | TySome(tyX,tyT1,tyT2) -> TySome(tyX,walk c tyT1,walk (c+1) tyT2) | TyArr(tyT1,tyT2) -> TyArr(walk c tyT1,walk c tyT2) | TyRecord(fieldtys) -> TyRecord(List.map (fun (li,tyTi) -> (li, walk c tyTi)) fieldtys) | TyBool -> TyBool | TyNat -> TyNat | TyId(b) as tyT -> tyT | TyUnit -> TyUnit | TyFloat -> TyFloat in walk c tyT let tmmap onvar ontype c t = let rec walk c t = match t with TmAscribe(fi,t1,tyT1) -> TmAscribe(fi,walk c t1,ontype c tyT1) | TmString _ as t -> t | TmTAbs(fi,tyX,tyT1,t2) -> TmTAbs(fi,tyX,ontype c tyT1,walk (c+1) t2) | TmTApp(fi,t1,tyT2) -> TmTApp(fi,walk c t1,ontype c tyT2) | TmPack(fi,tyT1,t2,tyT3) -> TmPack(fi,ontype c tyT1,walk c t2,ontype c tyT3) | TmUnpack(fi,tyX,x,t1,t2) -> TmUnpack(fi,tyX,x,walk c t1,walk (c+2) t2) | TmVar(fi,x,n) -> onvar fi c x n | TmAbs(fi,x,tyT1,t2) -> TmAbs(fi,x,ontype c tyT1,walk (c+1) t2) | TmApp(fi,t1,t2) -> TmApp(fi,walk c t1,walk c t2) | TmProj(fi,t1,l) -> TmProj(fi,walk c t1,l) | TmRecord(fi,fields) -> TmRecord(fi,List.map (fun (li,ti) -> (li,walk c ti)) fields) | TmTrue(fi) as t -> t | TmFalse(fi) as t -> t | TmIf(fi,t1,t2,t3) -> TmIf(fi,walk c t1,walk c t2,walk c t3) | TmZero(fi) -> TmZero(fi) | TmSucc(fi,t1) -> TmSucc(fi, walk c t1) | TmPred(fi,t1) -> TmPred(fi, walk c t1) | TmIsZero(fi,t1) -> TmIsZero(fi, walk c t1) | TmLet(fi,x,t1,t2) -> TmLet(fi,x,walk c t1,walk (c+1) t2) | TmUnit(fi) as t -> t | TmInert(fi,tyT) -> TmInert(fi,ontype c tyT) | TmFloat _ as t -> t | TmTimesfloat(fi,t1,t2) -> TmTimesfloat(fi, walk c t1, walk c t2) | TmFix(fi,t1) -> TmFix(fi,walk c t1) in walk c t let typeShiftAbove d c tyT = tymap (fun c x n -> if x>=c then TyVar(x+d,n+d) else TyVar(x,n+d)) c tyT let termShiftAbove d c t = tmmap (fun fi c x n -> if x>=c then TmVar(fi,x+d,n+d) else TmVar(fi,x,n+d)) (typeShiftAbove d) c t let termShift d t = termShiftAbove d 0 t let typeShift d tyT = typeShiftAbove d 0 tyT let bindingshift d bind = match bind with NameBind -> NameBind | TyVarBind(tyS) -> TyVarBind(typeShift d tyS) | VarBind(tyT) -> VarBind(typeShift d tyT) | TyAbbBind(tyT) -> TyAbbBind(typeShift d tyT) | TmAbbBind(t,tyT_opt) -> let tyT_opt' = match tyT_opt with None->None | Some(tyT) -> Some(typeShift d tyT) in TmAbbBind(termShift d t, tyT_opt') (* ---------------------------------------------------------------------- *) (* Substitution *) let termSubst j s t = tmmap (fun fi j x n -> if x=j then termShift j s else TmVar(fi,x,n)) (fun j tyT -> tyT) j t let termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t) let typeSubst tyS j tyT = tymap (fun j x n -> if x=j then (typeShift j tyS) else (TyVar(x,n))) j tyT let typeSubstTop tyS tyT = typeShift (-1) (typeSubst (typeShift 1 tyS) 0 tyT) let rec tytermSubst tyS j t = tmmap (fun fi c x n -> TmVar(fi,x,n)) (fun j tyT -> typeSubst tyS j tyT) j t let tytermSubstTop tyS t = termShift (-1) (tytermSubst (typeShift 1 tyS) 0 t) (* ---------------------------------------------------------------------- *) (* Context management (continued) *) let rec getbinding fi ctx i = try let (_,bind) = List.nth ctx i in bindingshift (i+1) bind with Failure _ -> let msg = Printf.sprintf "Variable lookup failure: offset: %d, ctx size: %d" in error fi (msg i (List.length ctx)) let getTypeFromContext fi ctx i = match getbinding fi ctx i with VarBind(tyT) -> tyT | TmAbbBind(_,Some(tyT)) -> tyT | TmAbbBind(_,None) -> error fi ("No type recorded for variable " ^ (index2name fi ctx i)) | _ -> error fi ("getTypeFromContext: Wrong kind of binding for variable " ^ (index2name fi ctx i)) (* ---------------------------------------------------------------------- *) (* Extracting file info *) let tmInfo t = match t with TmAscribe(fi,_,_) -> fi | TmString(fi,_) -> fi | TmTAbs(fi,_,_,_) -> fi | TmTApp(fi,_, _) -> fi | TmPack(fi,_,_,_) -> fi | TmUnpack(fi,_,_,_,_) -> fi | TmVar(fi,_,_) -> fi | TmAbs(fi,_,_,_) -> fi | TmApp(fi, _, _) -> fi | TmProj(fi,_,_) -> fi | TmRecord(fi,_) -> fi | TmTrue(fi) -> fi | TmFalse(fi) -> fi | TmIf(fi,_,_,_) -> fi | TmZero(fi) -> fi | TmSucc(fi,_) -> fi | TmPred(fi,_) -> fi | TmIsZero(fi,_) -> fi | TmUnit(fi) -> fi | TmFloat(fi,_) -> fi | TmTimesfloat(fi,_,_) -> fi | TmLet(fi,_,_,_) -> fi | TmInert(fi,_) -> fi | TmFix(fi,_) -> fi (* ---------------------------------------------------------------------- *) (* Printing *) (* The printing functions call these utility functions to insert grouping information and line-breaking hints for the pretty-printing library: obox Open a "box" whose contents will be indented by two spaces if the whole box cannot fit on the current line obox0 Same but indent continuation lines to the same column as the beginning of the box rather than 2 more columns to the right cbox Close the current box break Insert a breakpoint indicating where the line maybe broken if necessary. See the documentation for the Format module in the OCaml library for more details. *) let obox0() = open_hvbox 0 let obox() = open_hvbox 2 let cbox() = close_box() let break() = print_break 0 0 let small t = match t with TmVar(_,_,_) -> true | _ -> false let rec printty_Type outer ctx tyT = match tyT with TyAll(tyX,tyT1,tyT2) -> let (ctx1,tyX) = (pickfreshname ctx tyX) in obox(); pr "All "; pr tyX; proty ctx tyT1; pr "."; print_space (); printty_Type outer ctx1 tyT2; cbox() | tyT -> printty_ArrowType outer ctx tyT and proty ctx tyS = if tyS <> TyTop then (pr "<:"; printty_Type false ctx tyS) and printty_ArrowType outer ctx tyT = match tyT with TyArr(tyT1,tyT2) -> obox0(); printty_AType false ctx tyT1; if outer then pr " "; pr "->"; if outer then print_space() else break(); printty_ArrowType outer ctx tyT2; cbox() | tyT -> printty_AType outer ctx tyT and printty_AType outer ctx tyT = match tyT with TyString -> pr "String" | TyTop -> pr "Top" | TyVar(x,n) -> if ctxlength ctx = n then pr (index2name dummyinfo ctx x) else pr ("[bad index: " ^ (string_of_int x) ^ "/" ^ (string_of_int n) ^ " in {" ^ (List.fold_left (fun s (x,_) -> s ^ " " ^ x) "" ctx) ^ " }]") | TySome(tyX,tyT1,tyT2) -> let (ctx1,tyX) = pickfreshname ctx tyX in obox(); pr "{Some "; pr tyX; proty ctx tyT1; pr ","; if outer then print_space() else break(); printty_Type false ctx1 tyT2; pr "}"; cbox() | TyRecord(fields) -> let pf i (li,tyTi) = if (li <> ((string_of_int i))) then (pr li; pr ":"); printty_Type false ctx tyTi in let rec p i l = match l with [] -> () | [f] -> pf i f | f::rest -> pf i f; pr","; if outer then print_space() else break(); p (i+1) rest in pr "{"; open_hovbox 0; p 1 fields; pr "}"; cbox() | TyBool -> pr "Bool" | TyNat -> pr "Nat" | TyUnit -> pr "Unit" | TyId(b) -> pr b | TyFloat -> pr "Float" | tyT -> pr "("; printty_Type outer ctx tyT; pr ")" let printty ctx tyT = printty_Type true ctx tyT let rec printtm_Term outer ctx t = match t with TmTAbs(fi,x,tyS,t) -> (let (ctx1,x) = (pickfreshname ctx x) in obox(); pr "lambda "; pr x; proty ctx tyS; pr "."; if (small t) && not outer then break() else print_space(); printtm_Term outer ctx1 t; cbox()) | TmUnpack(fi,tyX,x,t1,t2) -> (let (ctx',tyX) = (pickfreshname ctx tyX) in let (ctx',x) = (pickfreshname ctx' x) in obox(); pr "let {"; pr tyX; pr ","; pr x; pr "} ="; print_space(); printtm_Term false ctx t1; pr " in "; printtm_Term outer ctx' t2; cbox()) | TmAbs(fi,x,tyT1,t2) -> (let (ctx',x') = (pickfreshname ctx x) in obox(); pr "lambda "; pr x'; pr ":"; printty_Type false ctx tyT1; pr "."; if (small t2) && not outer then break() else print_space(); printtm_Term outer ctx' t2; cbox()) | TmIf(fi, t1, t2, t3) -> obox0(); pr "if "; printtm_Term false ctx t1; print_space(); pr "then "; printtm_Term false ctx t2; print_space(); pr "else "; printtm_Term false ctx t3; cbox() | TmLet(fi, x, t1, t2) -> obox0(); pr "let "; pr x; pr " = "; printtm_Term false ctx t1; print_space(); pr "in"; print_space(); printtm_Term false (addname ctx x) t2; cbox() | TmFix(fi, t1) -> obox(); pr "fix "; printtm_Term false ctx t1; cbox() | t -> printtm_AppTerm outer ctx t and printtm_AppTerm outer ctx t = match t with TmTApp(fi,t,tyS) -> obox0(); printtm_AppTerm false ctx t; print_space(); pr "["; printty_Type false ctx tyS; pr "]"; cbox() | TmApp(fi, t1, t2) -> obox0(); printtm_AppTerm false ctx t1; print_space(); printtm_ATerm false ctx t2; cbox() | TmPred(_,t1) -> pr "pred "; printtm_ATerm false ctx t1 | TmIsZero(_,t1) -> pr "iszero "; printtm_ATerm false ctx t1 | TmTimesfloat(_,t1,t2) -> pr "timesfloat "; printtm_ATerm false ctx t2; pr " "; printtm_ATerm false ctx t2 | t -> printtm_PathTerm outer ctx t and printtm_AscribeTerm outer ctx t = match t with TmAscribe(_,t1,tyT1) -> obox0(); printtm_AppTerm false ctx t1; print_space(); pr "as "; printty_Type false ctx tyT1; cbox() | t -> printtm_ATerm outer ctx t and printtm_PathTerm outer ctx t = match t with TmProj(_, t1, l) -> printtm_ATerm false ctx t1; pr "."; pr l | t -> printtm_AscribeTerm outer ctx t and printtm_ATerm outer ctx t = match t with TmString(_,s) -> pr ("\"" ^ s ^ "\"") | TmPack(fi,tyT1,t2,tyT3) -> obox(); pr "{*"; printty_Type false ctx tyT1; pr ","; if outer then print_space() else break(); printtm_Term false ctx t2; pr "}"; print_space(); pr "as "; printty_Type outer ctx tyT3; cbox() | TmVar(fi,x,n) -> if ctxlength ctx = n then pr (index2name fi ctx x) else pr ("[bad index: " ^ (string_of_int x) ^ "/" ^ (string_of_int n) ^ " in {" ^ (List.fold_left (fun s (x,_) -> s ^ " " ^ x) "" ctx) ^ " }]") | TmRecord(fi, fields) -> let pf i (li,ti) = if (li <> ((string_of_int i))) then (pr li; pr "="); printtm_Term false ctx ti in let rec p i l = match l with [] -> () | [f] -> pf i f | f::rest -> pf i f; pr","; if outer then print_space() else break(); p (i+1) rest in pr "{"; open_hovbox 0; p 1 fields; pr "}"; cbox() | TmTrue(_) -> pr "true" | TmFalse(_) -> pr "false" | TmZero(fi) -> pr "0" | TmSucc(_,t1) -> let rec f n t = match t with TmZero(_) -> pr (string_of_int n) | TmSucc(_,s) -> f (n+1) s | _ -> (pr "(succ "; printtm_ATerm false ctx t1; pr ")") in f 1 t1 | TmUnit(_) -> pr "unit" | TmFloat(_,s) -> pr (string_of_float s) | TmInert(_,tyT) -> pr "inert["; printty_Type false ctx tyT; pr "]" | t -> pr "("; printtm_Term outer ctx t; pr ")" let printtm ctx t = printtm_Term true ctx t let prbinding ctx b = match b with NameBind -> () | TyVarBind(tyS) -> pr "<: ";printty_Type false ctx tyS | VarBind(tyT) -> pr ": "; printty ctx tyT | TyAbbBind(tyT) -> pr "= "; printty ctx tyT | TmAbbBind(t,tyT) -> pr "= "; printtm ctx t