blob: 9b6c0a309309592c1a858a27e03a3bfab396fae7 (
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
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
|
(******************************************************************************
* Type Expression Language:
*
* Helpers:
* symbol -> [a-z]
*
* Core:
* type -> function
* function -> ( variable | literal ) '->' type
* literal -> 'Integer' | 'Boolean'
* variable -> symbol
******************************************************************************)
open Types
open Parser
open Inference
type side = LHS | RHS
let ( let* ) = Option.bind
let printsub (s : substitution) =
FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (pretty v)) s ""
|> Printf.sprintf "Sub { %s }"
|> print_string
|> print_newline
let to_array (q : 'a Queue.t) : 'a array =
let result = Array.make (Queue.length q) "" in
let i = ref 0 in
Queue.iter
(fun x ->
result.(!i) <- x;
i := !i + 1)
q;
result
let tokenize (x : string) : token array =
let q = Queue.create () in
let i = ref 0 in
while !i < String.length x do
match x.[!i] with
| ' ' -> i := !i + 1
| _ ->
let beg = !i in
while (!i < String.length x) && (x.[!i] != ' ') do
i := !i + 1
done;
Queue.push (String.sub x beg (!i - beg)) q
done;
to_array q
let rec parse_type (p : parser) : _type option =
parse_function p
and parse_function (p : parser) : _type option =
match p#next with
| Some "->" ->
let* a = parse_literal p in
p#advance;
let* b = parse_type p in
Some (TypeArrow (a, b))
| _ -> parse_literal p
and parse_literal (p : parser) : _type option =
match p#curr with
| Some "Integer" | Some "Int" -> p#advance; Some TypeInt
| Some "Boolean" | Some "Bool" -> p#advance; Some TypeBool
| Some _ -> parse_variable p
| None -> None
and parse_variable (p : parser) : _type option =
match p#curr with
| Some x when String.length x = 1 -> p#advance; Some (TypeVariable x)
| _ -> None
let print_tokens (xs : string array) =
xs
|> Array.to_list
|> List.map (Printf.sprintf "\"%s\"")
|> String.concat ", "
|> Printf.sprintf "tokens: [ %s ]"
|> print_string |> print_newline
let print_type (t : _type) =
t |> pretty |> Printf.sprintf "type: %s" |> print_string |> print_newline
let parse_input (x : string) : _type option =
let tokens = tokenize x in
print_tokens tokens;
parse_type (new parser tokens)
(* Continually prompt until user provides a parseable type expression *)
let rec read_type (arg : side) : _type =
let prompt = match arg with
| LHS -> "lhs> "
| RHS -> "rhs> " in
print_string prompt;
let x = read_line () in
match parse_input x with
| None ->
print_string "Failed to parse input.\n";
read_type arg
| Some ast ->
print_type ast;
ast
let main =
while true do
begin
let lhs = read_type LHS in
let rhs = read_type RHS in
match unify lhs rhs with
| None ->
Printf.printf "Cannot unify \"%s\" with \"%s\"\n" (pretty lhs) (pretty rhs)
| Some x -> printsub x
end
done
|