diff options
Diffstat (limited to 'users/wpcarro/scratch/compiler/types.ml')
-rw-r--r-- | users/wpcarro/scratch/compiler/types.ml | 76 |
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 000000000000..99f35cd5a57d --- /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) |