System Fのインタプリタ（未完成）

gistfile1.fs

type ty =
 | TyVar of int * int
 | TyArr of ty * ty
 | TyAll of string * ty
 | TySome of string * ty

type binding =
 | NameBind
 | VarBind of ty
 | TyVarBind

let tymap onvar c tyT =
  let rec walk c tyT =
    match tyT with
    | TyArr(tyT1, tyT2) -> TyArr(walk c tyT1, walk c tyT2)
    | TyVar(x, n) -> onvar c x n
    | TyAll(tyX, tyT2) -> TyAll(tyX, walk (c+1) tyT2)
    | TySome(tyX, tyT2) -> TySome(tyX, walk (c+1) tyT2)
  walk c tyT

let typeShiftAbove d c tyT =
  tymap (fun c x n ->
    if x >= c then
      if x+d<0 then failwith "Scoping error!"
      else TyVar(x+d, n+d)
    else TyVar(x,n+d)
  ) c tyT

let typeShift d tyT = typeShiftAbove d 0 tyT

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)

type info = unit

type term =
 | TmVar of info * int * int
 | TmAbs of info * string * ty * term
 | TmApp of info * term * term
 | TmTAbs of info * string * term
 | TmTApp of info * term * ty
 | TmPack of info * ty * term * ty
 | TmUnpack of info * string * string * term * term

let tmmap onvar ontype c t =
  let rec walk c t =
    match t with
    | 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)
    | TmTAbs(fi, tyX, t2) -> TmTAbs(fi, tyX, 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)
  walk c t

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 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 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 termSubstTop s t =
  termShift (-1) (termSubst 0 (termShift 1 s) t)

let tytermSubstTop tyS t =
  termShift (-1) (tytermSubst (typeShift 1 tyS) 0 t)

type context = (string * binding) list

let isval (ctx : context) t =
  match t with
  | TmVar(_,_,_)
  | TmAbs(_,_,_,_)
  | TmTAbs(_,_,_) -> true
  | _ -> false

let addbinding (ctx : context) (x : string) (bind : binding) = (x, bind)::ctx
let getbinding fi ctx i = List.nth ctx (i-1) |> snd

let getTypeFromContext fi ctx i =
  match getbinding fi ctx i with
  | VarBind(tyT) -> tyT

let rec typeof (ctx : context) t =
  match t with
  | TmVar(fi, i, _) -> getTypeFromContext fi ctx i
  | TmAbs(fi, x, tyT1, t2) ->
    let ctx' = addbinding ctx x (VarBind(tyT1))
    let tyT2 = typeof ctx' t2
    TyArr(tyT1, typeShift (-1) tyT2)
  | TmApp(fi, t1, t2) ->
    let tyT1 = typeof ctx t1
    let tyT2 = typeof ctx t2
    (match tyT1 with
     | TyArr(tyT11,tyT12) -> if tyT2 = tyT11 then tyT12 else failwith ""
     | _ -> failwith "")
  | TmTAbs(f1, tyX, t2) ->
    let ctx = addbinding ctx tyX TyVarBind
    let tyT2 = typeof ctx t2
    TyAll(tyX, tyT2)
  | TmTApp(fi, t1, tyT2) ->
    let tyT1 = typeof ctx t1
    (match tyT1 with
     | TyAll(_, tyT12) -> typeSubstTop tyT2 tyT12)
  | TmPack(fi, tyT1, t2, tyT) ->
    (match tyT with
     | TySome(tyY,tyT2) ->
       let tyU = typeof ctx t2
       let tyU' = typeSubstTop tyT1 tyT2
       if tyU = tyU' then tyT else failwith "")
  | TmUnpack(fi,tyX,x,t1,t2) ->
    let tyT1 = typeof ctx t1
    (match tyT1 with
     | TySome(tyY, tyT11) ->
       let ctx' = addbinding ctx tyX TyVarBind
       let ctx'' = addbinding ctx' x (VarBind tyT11)
       let tyT2 = typeof ctx'' t2
       typeShift (-2) tyT2)

exception Done

let rec eval1 (ctx : context) (t :term) =
  match t with
  | TmApp(fi, TmAbs(_,x,ty,t12),v2) when isval ctx v2 ->
    if typeof ctx t = ty then
      termSubstTop v2 t12
    else failwith "type error!"
  | TmApp(fi, v1, v2) when isval ctx v1 ->
    let v1' = eval1 ctx v1
    TmApp(fi, v1', v2)
  (* ... *)
  | TmTApp(fi, TmTAbs(_,x,t11),tyT2) -> tytermSubstTop tyT2 t11
  | TmTApp(fi, t1, tyT2) -> let t1' = eval1 ctx t1 in TmTApp(fi, t1', tyT2)
  | TmUnpack(fi,_,_,TmPack(_,tyT11,v12,_),t2) when isval ctx v12 ->
    tytermSubstTop tyT11 (termSubstTop (termShift 1 v12) t2)
  | TmUnpack(fi, tyX, x, t1, t2) -> let t1' = eval1 ctx t1 in TmUnpack(fi, tyX, x, t1', t2)
  | TmPack(fi, tyT1, t2, tyT3) -> let t2' = eval1 ctx t2 in TmPack(fi, tyT1, t2', tyT3)
  | _ -> raise Done

let rec eval ctx t =
  try
    let t' = eval1 ctx t
    eval ctx t'
  with Done -> t

//eval [] (TmApp((), TmAbs((), "x", TyVar(1, 1), TmVar((), 1, 1)),  TmAbs((), "x", TyVar(1, 1), TmVar((), 1, 1))))

TODO:
FParsecでパーサ書く
Big-stepに変える
VMとコンパイラ作りたい…