SATySFiで単相型推論して証明図を出す

code:typed-lambda.ml

@require: list

@require: base/list-ext

@require: base/ref

@require: base/fn

@require: azmath/azmath

@require: derive/derive

@require: class-jlreq/jlreq

% class-jlreq は \ref を提供するクラスなら何でもよい

type expr = Var of string | EInt of int | Add of expr * expr | Abs of string * expr | App of expr * expr

type typ = Int | Fun of typ * typ | Unknown | UVar of int * typ ref

type typ-env = (string * typ) list

type typ-judge = typ-env * expr * typ

type typ-rule = RRef of string | RVar | RInt | RAdd of typ-derive * typ-derive | RApp of typ-derive * typ-derive | RAbs of typ-derive

and typ-derive = typ-judge * typ-rule

module TypedLambda : sig

val derive : typ-env -> expr -> typ -> typ-derive option

end = struct

let-math \sp =

let-math \type typ =

let-rec render t =

match t with

| Int -> ${\mathrm{int}}

| Fun(m, n) -> (

let (m-m, m-n) = (render m, render n) in

let m-m = match m with Fun _ -> ${\p{#m-m}} | _ -> m-m in

let m-n = match n with Fun _ -> ${\p{#m-n}} | _ -> m-n in

)

| Unknown -> ${\?}

| UVar(i, r) ->

let t = !r in

match t with

| Unknown ->

let m-i = math-char MathOrd (arabic i) in

${\tau_{#m-i}}

| _ -> render t

in

render typ

let-math \type-env env =

let xs =

env |> List.map (fun (name, ty) -> ${\mathit-token!(name) : \type!(ty)}) |> List.reverse in

match xs with

| [] -> ${}

let-math \expr e =

let-rec render e =

let p e =

match e with

| Var _ -> render e

| EInt _ -> render e

| _ -> ${\p!(render e)}

in

match e with

| Var(x) -> ${\mathit-token!(x)}

| EInt(i) -> math-char MathOrd (arabic i)

| Add(e1, e2) ->

let (m-e1, m-e2) = (p e1, p e2) in

| Abs(x, e) ->

let m-e = p e in

| App(e1, e2) ->

let (m-e1, m-e2) = (p e1, p e2) in

in

render e

let-math \type-judge (env, expr, ty) = ${\type-env!(env) \vdash \expr!(expr) : \type!(ty)}

let-math \type-derive d =

let double-line = DeriveLine.make (fun ctx pt width thickness -> (

let color = ctx |> get-text-color in

match pt with

| (x, y) -> [

fill color (Gr.rectangle (x, y) (x +' width, y +' thickness));

fill color (Gr.rectangle (x, y +' thickness *' 3.) (x +' width, y +' thickness *' 4.))

]

)) in

let-rec prove (judge, rule) =

open DeriveDSL in

let rules =

match rule with

| RVar -> Fn.id

| RInt -> Fn.id

| RRef(name) -> withLine double-line |> Fn.compose(byOp {(\ref(name);)})

in

derive ${\type-judge!(judge)} |> rules

in

open Derive in

${\proven!(prove d)}

let derive env expr ty =

let fresh =

let-mutable counter <- 0 in

fun () -> (

let t = UVar(!counter, Ref.make(Unknown)) in

let () = counter |> Ref.inc in

t

)

in

let-rec extract j =

let (env, expr, ty) = j in

match expr with

| Var(x) -> (

let bind = env |> List.find (fun (v, _) -> string-same x v) in

bind |> Option.map (fun (_, t) -> (

let d = (j, RVar) in

(d, eq)

))

)

| EInt _ -> (

let d = (j, RInt) in

Some (d, eq)

)

| Add(e1, e2) -> (

let r1 = extract (env, e1, Int) in

let r2 = extract (env, e2, Int) in

match (r1, r2) with

| (Some(d1, eq1), Some(d2, eq2)) -> (

let eq = eq |> List.append eq1 |> List.append eq2 in

let d = (j, RAdd(d1, d2)) in

Some (d, eq)

)

| _ -> None

)

| App(e1, e2) -> (

let t0 = fresh () in

let r1 = extract (env, e1, Fun(t0, ty)) in

let r2 = extract (env, e2, t0) in

match (r1, r2) with

| (Some(d1, eq1), Some(d2, eq2)) -> (

let eq = List.append eq1 eq2 in

let d = (j, RApp(d1, d2)) in

Some (d, eq)

)

| _ -> None

)

| Abs(x, e) -> (

let (t1, t2, eq) =

match ty with

| Fun(t1, t2) -> (t1, t2, [])

| _ -> (

let t1 = fresh () in

let t2 = fresh () in

(t1, t2, eq)

)

in

let r1 = extract ((x, t1)::env, e, t2) in

match r1 with

| Some(d1, eq1) -> (

let eq = eq |> List.append eq1 in

let d = (j, RAbs(d1)) in

Some (d, eq)

)

| _ -> None

)

| _ -> None

in

let-rec unify eq =

let apply i r t =

let-rec exists t =

match t with

| Fun(t1, t2) -> if exists t1 then true else if exists t2 then true else false

| UVar(j, _) -> i == j

| _ -> false

in

if exists t then None

else

let () = r <- t in

Some ()

in

match eq with

| [] -> Some ()

| (UVar(_, r1) as u1, UVar(_, r2) as u2)::eq1 -> (

match (!r1, !r2) with

| (Unknown, Unknown) -> (

match eq1 with

| [] -> None

)

| (t, Unknown) -> unify ((t, u2)::eq1)

| (Unknown, t) -> unify ((t, u1)::eq1)

| (t1, t2) -> unify ((t1, t2)::eq1)

)

| (UVar(i, r), t)::eq1 -> (

match !r with

| Unknown -> apply i r t |> Option.and-then (fun () -> unify eq1)

| t0 -> unify ((t0, t)::eq1)

)

| (t, UVar(i, r))::eq1 -> (

match !r with

| Unknown -> apply i r t |> Option.and-then (fun () -> unify eq1)

| t0 -> unify ((t, t0)::eq1)

)

| (Int, Int)::eq1 -> unify eq1

| (Fun(t11, t12), Fun(t21, t22))::eq1 -> unify ((t11, t21)::(t12, t22)::eq1)

| (_, _)::_ -> None

in

let ty = match ty with Unknown -> fresh () | _ -> ty in

let judge = (env, expr, ty) in

extract judge

|> Option.and-then(fun (d, eq) -> (

eq |> unify |> Option.map(fun () -> d)

))

end