about summary refs log tree commit diff
path: root/users/wpcarro/scratch/compiler/type_parser.ml
diff options
context:
space:
mode:
Diffstat (limited to 'users/wpcarro/scratch/compiler/type_parser.ml')
-rw-r--r--users/wpcarro/scratch/compiler/type_parser.ml115
1 files changed, 115 insertions, 0 deletions
diff --git a/users/wpcarro/scratch/compiler/type_parser.ml b/users/wpcarro/scratch/compiler/type_parser.ml
new file mode 100644
index 000000000000..9b6c0a309309
--- /dev/null
+++ b/users/wpcarro/scratch/compiler/type_parser.ml
@@ -0,0 +1,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