about summary refs log tree commit diff
diff options
context:
space:
mode:
authorWilliam Carroll <wpcarro@gmail.com>2022-10-24T21·51-0400
committerwpcarro <wpcarro@gmail.com>2022-10-25T03·59+0000
commit1e9c3955bf2c17206c6dd536ebaf96a7e6f4f22d (patch)
tree3ad05bbd2f8c6fc7ccfe8e6e507fe386d9957a75
parenta8876a4cdaaf0a1f051fefad436e08d983b402e2 (diff)
refactor(wpcarro/compiler): Modularize debug fns r/5195
Define `debug.ml` and `prettify.ml` to clean-up some code.

Change-Id: Iee2e1ed666f2ccb5e56cc50054ca85b8ba513f3b
Reviewed-on: https://cl.tvl.fyi/c/depot/+/7078
Tested-by: BuildkiteCI
Reviewed-by: wpcarro <wpcarro@gmail.com>
-rw-r--r--users/wpcarro/scratch/compiler/debug.ml66
-rw-r--r--users/wpcarro/scratch/compiler/expr_parser.ml27
-rw-r--r--users/wpcarro/scratch/compiler/inference.ml13
-rw-r--r--users/wpcarro/scratch/compiler/prettify.ml9
-rw-r--r--users/wpcarro/scratch/compiler/register_vm.ml2
-rw-r--r--users/wpcarro/scratch/compiler/type_parser.ml10
-rw-r--r--users/wpcarro/scratch/compiler/types.ml49
7 files changed, 91 insertions, 85 deletions
diff --git a/users/wpcarro/scratch/compiler/debug.ml b/users/wpcarro/scratch/compiler/debug.ml
new file mode 100644
index 0000000000..e39ff13742
--- /dev/null
+++ b/users/wpcarro/scratch/compiler/debug.ml
@@ -0,0 +1,66 @@
+open Types
+
+(* Print x prefixed with tag and return x unchanged. *)
+let print (f : 'a -> string) (tag : string) (x : 'a) : 'a =
+  Printf.printf "%s: %s\n" tag (f x);
+  x
+
+let rec ast (tree : Types.value) : string =
+  match tree with
+  | ValueLiteral (LiteralBool x) ->
+     Printf.sprintf "ValueLiteral (LiteralBool %s)" (string_of_bool x)
+  | ValueLiteral (LiteralInt x) ->
+     Printf.sprintf "ValueLiteral (LiteralInt %s)" (string_of_int x)
+  | ValueVariable x ->
+     Printf.sprintf "ValueVariable %s" x
+  | ValueFunction (x, body) ->
+     Printf.sprintf "ValueFunction (%s, %s)" x (ast body)
+  | ValueApplication (f, x) ->
+     Printf.sprintf "ValueApplication (%s, %s)" (ast f) (ast x)
+  | ValueVarApplication (f, x) ->
+     Printf.sprintf "ValueVarApplication (%s, %s)" f (ast x)
+  | ValueBinder (k, v, x) ->
+      Printf.sprintf "ValueBinder (%s, %s, %s)" k (ast v) (ast x)
+
+let rec 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 (value x)
+  | ValueApplication (f, x) ->
+     Printf.sprintf "App %s %s" (value f) (value x)
+  | ValueVarApplication (name, x) ->
+     Printf.sprintf "App %s %s" name (value x)
+  | ValueBinder (name, x, body) ->
+     Printf.sprintf "Bind %s %s %s" name (value x) (value body)
+
+let rec type' (t : _type) : string =
+  match t with
+  | TypeInt -> "Integer"
+  | TypeBool -> "Boolean"
+  | TypeVariable k -> Printf.sprintf "%s" k
+  | TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (type' a) (type' b)
+
+let quantified_type (q : quantified_type) : string =
+  let QuantifiedType (vars, t) = q in
+  if List.length vars == 0 then
+    Printf.sprintf "%s" (type' t)
+  else
+    Printf.sprintf "forall %s. %s" (String.concat "," vars) (type' t)
+
+let substitution (s : substitution) : string =
+  FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (type' v)) s ""
+  |> Printf.sprintf "{ %s }"
+
+let env (s : env) : string =
+  FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (quantified_type v)) s ""
+  |> Printf.sprintf "{ %s }"
+
+let inference (Inference (s, t)) =
+  Printf.sprintf "type: %s; sub: %s" (type' t) (substitution s)
+
diff --git a/users/wpcarro/scratch/compiler/expr_parser.ml b/users/wpcarro/scratch/compiler/expr_parser.ml
index 7d24efc80d..04ec1dbe92 100644
--- a/users/wpcarro/scratch/compiler/expr_parser.ml
+++ b/users/wpcarro/scratch/compiler/expr_parser.ml
@@ -28,6 +28,8 @@
 
 open Parser
 open Inference
+open Debug
+open Prettify
 
 let to_array (q : 'a Queue.t) : 'a array =
   let result = Array.make (Queue.length q) "" in
@@ -149,27 +151,6 @@ let parse_language (x : string) : Types.value option =
   print_tokens tokens;
   parse_expression (new parser tokens)
 
-let rec debug (ast : Types.value) : string =
-  match ast with
-  | ValueLiteral (LiteralBool x) ->
-     Printf.sprintf "ValueLiteral (LiteralBool %s)" (string_of_bool x)
-  | ValueLiteral (LiteralInt x) ->
-     Printf.sprintf "ValueLiteral (LiteralInt %s)" (string_of_int x)
-  | ValueVariable x ->
-     Printf.sprintf "ValueVariable %s" x
-  | ValueFunction (x, body) ->
-     Printf.sprintf "ValueFunction (%s, %s)" x (debug body)
-  | ValueApplication (f, x) ->
-     Printf.sprintf "ValueApplication (%s, %s)" (debug f) (debug x)
-  | ValueVarApplication (f, x) ->
-     Printf.sprintf "ValueVarApplication (%s, %s)" f (debug x)
-  | ValueBinder (k, v, x) ->
-      Printf.sprintf "ValueBinder (%s, %s, %s)" k (debug v) (debug x)
-
-let debug_ast (ast : Types.value) : Types.value =
-  ast |> debug |> Printf.sprintf "ast: %s" |> print_string |> print_newline;
-  ast
-
 let main =
   while true do
     begin
@@ -177,14 +158,14 @@ let main =
       let x = read_line () in
       match parse_language x with
       | Some ast ->
-         (match ast |> debug_ast |> do_infer with
+         (match ast |> Debug.print Debug.ast "ast" |> do_infer with
           | None ->
              "Type-check failed"
              |> print_string
              |> print_newline
           | Some x ->
              x
-             |> Types.pretty
+             |> Prettify.type'
              |> print_string
              |> print_newline)
       | None ->
diff --git a/users/wpcarro/scratch/compiler/inference.ml b/users/wpcarro/scratch/compiler/inference.ml
index 52838f85e6..c9d4ba9c78 100644
--- a/users/wpcarro/scratch/compiler/inference.ml
+++ b/users/wpcarro/scratch/compiler/inference.ml
@@ -7,6 +7,7 @@
  ******************************************************************************)
 
 open Types
+open Debug
 
 (*******************************************************************************
  * Library
@@ -107,25 +108,25 @@ let rec unify (a : _type) (b : _type) : substitution option =
       let* s1 = unify a c in
       let* s2 = unify (substitute_type s1 b) (substitute_type s1 d) in
       let s3 = compose_substitutions [s1; s2] in
-      s1 |> Types.debug_substitution |> Printf.sprintf "s1: %s\n" |> print_string;
-      s2 |> Types.debug_substitution |> Printf.sprintf "s2: %s\n" |> print_string;
-      s3 |> Types.debug_substitution |> Printf.sprintf "s3: %s\n" |> print_string;
+      s1 |> Debug.substitution |> Printf.sprintf "s1: %s\n" |> print_string;
+      s2 |> Debug.substitution |> Printf.sprintf "s2: %s\n" |> print_string;
+      s3 |> Debug.substitution |> Printf.sprintf "s3: %s\n" |> print_string;
       Some s3
   | _ -> None
 
 let print_env (env : env) =
-  Printf.sprintf "env: %s\n" (Types.debug_env env)
+  Printf.sprintf "env: %s\n" (Debug.env env)
   |> print_string
 
 let print_val (x : value) =
-  Printf.sprintf "val: %s\n" (Types.debug_value x)
+  Printf.sprintf "val: %s\n" (Debug.value x)
   |> print_string
 
 let print_inference (x : inference option) =
   match x with
   | None -> "no inference\n" |> print_string
   | Some x ->
-     Printf.sprintf "inf: %s\n" (Types.debug_inference x)
+     Printf.sprintf "inf: %s\n" (Debug.inference x)
      |> print_string
 
 let rec infer (env : env) (x : value) : inference option =
diff --git a/users/wpcarro/scratch/compiler/prettify.ml b/users/wpcarro/scratch/compiler/prettify.ml
new file mode 100644
index 0000000000..7903ad3694
--- /dev/null
+++ b/users/wpcarro/scratch/compiler/prettify.ml
@@ -0,0 +1,9 @@
+open Types
+
+(* Pretty-print the type, t. *)
+let rec type' (t : _type) : string =
+  match t with
+  | TypeInt -> "Integer"
+  | TypeBool -> "Boolean"
+  | TypeVariable k -> Printf.sprintf "%s" k
+  | TypeArrow (a, b) -> Printf.sprintf "%s -> %s" (type' a) (type' b)
diff --git a/users/wpcarro/scratch/compiler/register_vm.ml b/users/wpcarro/scratch/compiler/register_vm.ml
index aa5062cb24..17d3f55894 100644
--- a/users/wpcarro/scratch/compiler/register_vm.ml
+++ b/users/wpcarro/scratch/compiler/register_vm.ml
@@ -6,7 +6,7 @@
   because one of the goals was to see how similar this OCaml implementation
   could be to the Python implementation.
 
-  Conclusion: It's pretty easily to switch between the two languages.
+  Conclusion: It's pretty easy to switch between the two languages.
 
   Usage: Recommended compilation settings I hastily found online:
   $ ocamlopt -w +A-42-48 -warn-error +A-3-44 ./register_vm.ml && ./a.out
diff --git a/users/wpcarro/scratch/compiler/type_parser.ml b/users/wpcarro/scratch/compiler/type_parser.ml
index 9b6c0a3093..a11dcdba2b 100644
--- a/users/wpcarro/scratch/compiler/type_parser.ml
+++ b/users/wpcarro/scratch/compiler/type_parser.ml
@@ -12,6 +12,7 @@
  ******************************************************************************)
 
 open Types
+open Prettify
 open Parser
 open Inference
 
@@ -20,10 +21,7 @@ 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
+  s |> Debug.substitution |> print_string |> print_newline
 
 let to_array (q : 'a Queue.t) : 'a array =
   let result = Array.make (Queue.length q) "" in
@@ -80,7 +78,7 @@ let print_tokens (xs : string array) =
   |> print_string |> print_newline
 
 let print_type (t : _type) =
-  t |> pretty |> Printf.sprintf "type: %s" |> print_string |> print_newline
+  t |> Debug.type' |> Printf.sprintf "type: %s" |> print_string |> print_newline
 
 let parse_input (x : string) : _type option =
   let tokens = tokenize x in
@@ -109,7 +107,7 @@ let main =
       let rhs = read_type RHS in
       match unify lhs rhs with
       | None ->
-         Printf.printf "Cannot unify \"%s\" with \"%s\"\n" (pretty lhs) (pretty rhs)
+         Printf.printf "Cannot unify \"%s\" with \"%s\"\n" (Debug.type' lhs) (Debug.type' rhs)
       | Some x -> printsub x
     end
   done
diff --git a/users/wpcarro/scratch/compiler/types.ml b/users/wpcarro/scratch/compiler/types.ml
index 99f35cd5a5..79c51c6812 100644
--- a/users/wpcarro/scratch/compiler/types.ml
+++ b/users/wpcarro/scratch/compiler/types.ml
@@ -9,23 +9,6 @@ type 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 =
@@ -34,43 +17,11 @@ type _type =
   | 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)