mdebray/tvl-depot
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(wpcarro/compiler): Modularize debug fns

Browse source 
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>
This commit is contained in:
William Carroll 2022-10-24 17:51:48 -04:00 • committed by wpcarro
parent a8876a4cda
commit 1e9c3955bf
7 changed files with 91 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
users/wpcarro/scratch/compiler/debug.ml Normal file
View file

@ -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)

27
users/wpcarro/scratch/compiler/expr_parser.ml
View file

@ -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 ->

13
users/wpcarro/scratch/compiler/inference.ml
View file

@ -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 =

9
users/wpcarro/scratch/compiler/prettify.ml Normal file
View file

@ -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)

2
users/wpcarro/scratch/compiler/register_vm.ml
View file

@ -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

10
users/wpcarro/scratch/compiler/type_parser.ml
View file

@ -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

49
users/wpcarro/scratch/compiler/types.ml
View file

@ -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)