1 files changed, 76 insertions, 0 deletions
diff --git a/users/wpcarro/scratch/compiler/types.ml b/users/wpcarro/scratch/compiler/types.ml
new file mode 100644
index 0000000000..99f35cd5a5
--- /dev/null
+++ b/users/wpcarro/scratch/compiler/types.ml
@@ -0,0 +1,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)