blob: 99f35cd5a57d787071058044b5bf6206710acdec (
plain) (
blame)
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
|
type literal = LiteralInt of int | LiteralBool of bool
(* Lambda Calculus definition *)
type value =
| ValueLiteral of literal
| ValueVariable of string
| ValueFunction of string * value
| ValueApplication of value * value
| ValueVarApplication of string * value
| ValueBinder of string * value * value
let rec debug_value (x : value) : string =
match x with
| ValueLiteral (LiteralInt x) ->
Printf.sprintf "Int %d" x
| ValueLiteral (LiteralBool x) ->
Printf.sprintf "Bool %b" x
| ValueVariable x ->
Printf.sprintf "Var %s" x
| ValueFunction (name, x) ->
Printf.sprintf "Fn %s %s" name (debug_value x)
| ValueApplication (f, x) ->
Printf.sprintf "App %s %s" (debug_value f) (debug_value x)
| ValueVarApplication (name, x) ->
Printf.sprintf "App %s %s" name (debug_value x)
| ValueBinder (name, x, body) ->
Printf.sprintf "Bind %s %s %s" name (debug_value x) (debug_value body)
module FromString = Map.Make (String)
type _type =
| TypeInt
| TypeBool
| TypeVariable of string
| TypeArrow of _type * _type
let rec debug_type (t : _type) : string =
match t with
| TypeInt -> "Integer"
| TypeBool -> "Boolean"
| TypeVariable k -> Printf.sprintf "%s" k
| TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (debug_type a) (debug_type b)
type quantified_type = QuantifiedType of string list * _type
let debug_quantified_type (q : quantified_type) : string =
let QuantifiedType (vars, t) = q in
if List.length vars == 0 then
Printf.sprintf "%s" (debug_type t)
else
Printf.sprintf "forall %s. %s" (String.concat "," vars) (debug_type t)
type set = bool FromString.t
type substitution = _type FromString.t
let debug_substitution (s : substitution) : string =
FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (debug_type v)) s ""
|> Printf.sprintf "{ %s }"
type env = quantified_type FromString.t
let debug_env (s : env) : string =
FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (debug_quantified_type v)) s ""
|> Printf.sprintf "{ %s }"
type inference = Inference of substitution * _type
let debug_inference (Inference (s, t)) =
Printf.sprintf "type: %s; sub: %s" (debug_type t) (debug_substitution s)
let rec pretty (t : _type) : string =
match t with
| TypeInt -> "Integer"
| TypeBool -> "Boolean"
| TypeVariable k -> Printf.sprintf "%s" k
| TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (pretty a) (pretty b)
|
