-
Notifications
You must be signed in to change notification settings - Fork 0
/
abt.ml
143 lines (116 loc) · 3.56 KB
/
abt.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
(* -*- mode: ocaml; -*- *)
(* A copy of https://gist.github.com/neel-krishnaswami/834b892327271e348f79 *)
module type FUNCTOR = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}
type var = string
module V = Set.Make(struct type t = var let compare = compare end)
module type ABT = sig
type 'a signature
type 'a f = Var of var | Abs of var * 'a | Tm of 'a signature
val map : ('a -> 'b) -> 'a f -> 'b f
type t
val into : t f -> t
val out : t -> t f
val freevars : t -> V.t
val var : V.elt -> t
val abs : V.elt * t -> t
val tm : t signature -> t
val subst : t -> var -> t -> t
end
module type SIGNATURE = sig
include FUNCTOR
val join : 'a monoid -> 'a t -> 'a
end
module Abt(F : SIGNATURE) : ABT with type 'a signature := 'a F.t =
struct
type 'a f =
| Var of var
| Abs of var * 'a
| Tm of 'a F.t
let map f = function
| Var x -> Var x
| Abs(x, e) -> Abs(x, f e)
| Tm t -> Tm (F.map f t)
type t = In of V.t * t f
let freevars (In(vs, _)) = vs
let out (In(_, t)) = t
let m = {unit = V.empty; join = V.union}
let var x = In(V.singleton x, Var x)
let abs(z, e) = In(V.remove z (freevars e), Abs(z, e))
let tm t = In(F.join m (F.map freevars t), Tm t)
let into = function
| Var x -> var x
| Abs(x, e) -> abs(x, e)
| Tm t -> tm t
let rec fresh vs v =
if V.mem v vs then fresh vs (v ^ "'") else v
let rec rename x y (In(fvs, t)) =
match t with
| Var z -> if x = z then var y else var z
| Abs(z, e) -> if x = z then abs(z, e) else abs(z, rename x y e)
| Tm v -> tm (F.map (rename x y) v)
let rec subst t x body =
match out body with
| Var z when x = z -> t
| Var z -> var z
| Abs(x, e) ->
let x' = fresh (V.union (freevars t) (freevars body)) x in
let e' = subst t x (rename x x' e) in
abs(x', e')
| Tm body -> tm (F.map (subst t x) body)
end
module Lambda =
struct
type tp = Base | Arrow of tp * tp
type 'a t = Lam of 'a | App of 'a * 'a | Let of 'a * 'a | Annot of tp * 'a
let map f = function
| Lam x -> Lam (f x)
| App (x, y) -> App(f x, f y)
| Let (x, y) -> Let(f x, f y)
| Annot(t, x) -> Annot(t, f x)
let join m = function
| Lam x -> x
| App(x, y) -> m.join x y
| Let(x, y) -> m.join x y
| Annot(_, x) -> x
end
module Syntax = Abt(Lambda)
module Bidir = struct
open Lambda
open Syntax
type ctx = (var * tp) list
let is_synth = function
| Tm (Lam _) | Tm (Let (_, _)) -> false
| _ -> true
let is_check e = not(is_synth e)
let unabs e =
match out e with
| Abs(x, e) -> (x, e)
| _ -> assert false
let rec check ctx e tp =
match out e, tp with
| Tm (Lam t), Arrow(tp1, tp') ->
let (x, e') = unabs t in
check ((x, tp1) :: ctx) e' tp'
| Tm (Lam _), _ -> failwith "expected arrow type"
| Tm (Let(e', t)), _ ->
let (x, e'') = unabs t in
let tp1 = synth ctx e' in
check ((x, tp1) :: ctx) e'' tp
| body, _ when is_synth body ->
if tp = synth ctx e then () else failwith "Type mismatch"
| _ -> assert false
and synth ctx e =
match out e with
| Var x -> (try List.assoc x ctx with Not_found -> failwith "unbound variable")
| Tm(Annot(tp, e)) -> let () = check ctx e tp in tp
| Tm(App(f, e)) ->
(match synth ctx f with
| Arrow(tp, tp') -> let () = check ctx e tp in tp'
| _ -> failwith "Applying a non-function!")
| body when is_check body -> failwith "Cannot synthesize type for checking term"
| _ -> assert false
end