From 9adbbb34bc21806a1db4458d871a621266cb622b Mon Sep 17 00:00:00 2001 From: Galfour Date: Sat, 23 Mar 2019 10:52:25 +0000 Subject: [PATCH] pipeline ok --- src/ligo/ast_simplified.ml | 2 + src/ligo/ast_typed.ml | 110 +++++++++++++++------ src/ligo/ligo-helpers/trace.ml | 22 +++-- src/ligo/ligo.ml | 8 +- src/ligo/mini_c.ml | 117 ++++++++--------------- src/ligo/transpiler.ml | 102 +++++++++++++++++++- src/ligo/typer.ml | 168 +++++++++++++++++++++++++++------ 7 files changed, 380 insertions(+), 149 deletions(-) diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 62da3bfc8..4b8d1d091 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -100,6 +100,8 @@ and matching = let ae expression = {expression ; type_annotation = None} +let annotated_expression expression type_annotation = {expression ; type_annotation} + open Ligo_helpers.Trace module PP = struct diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index 5c303e1e7..4d1acd66d 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -1,3 +1,5 @@ +module S = Ast_simplified + module SMap = Ligo_helpers.X_map.String let list_of_smap (s:'a SMap.t) : (string * 'a) list = @@ -30,13 +32,18 @@ and ae = annotated_expression and tv_map = type_value type_name_map and ae_map = annotated_expression name_map -and type_value = +and type_value' = | Type_tuple of tv list | Type_sum of tv_map | Type_record of tv_map | Type_constant of type_name * tv list | Type_function of tv * tv +and type_value = { + type_value : type_value' ; + simplified : S.type_expression option ; +} + and expression = (* Base *) | Literal of literal @@ -91,23 +98,29 @@ and matching = match_none : b ; match_some : name * b ; } - | Match_tuple of (name * b) list + | Match_tuple of name list * b + +let type_value type_value simplified = { type_value ; simplified } +let annotated_expression expression type_annotation = { expression ; type_annotation } module PP = struct open Format open Ligo_helpers.PP - let rec type_value ppf (tv:type_value) : unit = - match tv with + let rec type_value' ppf (tv':type_value') : unit = + match tv' with | Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst | Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m | Type_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m | Type_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b | Type_constant (c, []) -> fprintf ppf "%s" c | Type_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n + + and type_value ppf (tv:type_value) : unit = + type_value' ppf tv.type_value end -open Ligo_helpers.Trace +open! Ligo_helpers.Trace module Errors = struct let different_kinds a b = @@ -132,22 +145,22 @@ module Errors = struct end open Errors -let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab with - | Type_tuple a as ta, (Type_tuple b as tb) -> ( +let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value, b.type_value) with + | Type_tuple ta, Type_tuple tb -> ( let%bind _ = - trace_strong (different_size_tuples ta tb) - @@ Assert.assert_true List.(length a = length b) in - bind_list_iter type_value_eq (List.combine a b) + trace_strong (different_size_tuples a b) + @@ Assert.assert_true List.(length ta = length tb) in + bind_list_iter assert_type_value_eq (List.combine ta tb) ) - | Type_constant (a, a') as ca, (Type_constant (b, b') as cb) -> ( + | Type_constant (ca, lsta), Type_constant (cb, lstb) -> ( let%bind _ = - trace_strong (different_size_constants ca cb) - @@ Assert.assert_true List.(length a' = length b') in + trace_strong (different_size_constants a b) + @@ Assert.assert_true List.(length lsta = length lstb) in let%bind _ = - trace_strong (different_constants a b) + trace_strong (different_constants ca cb) @@ Assert.assert_true (a = b) in trace (simple_error "constant sub-expression") - @@ bind_list_iter type_value_eq (List.combine a' b') + @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb) ) | Type_sum a, Type_sum b -> ( let a' = list_of_smap a in @@ -156,7 +169,7 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w let%bind _ = Assert.assert_true ~msg:"different keys in sum types" @@ (ka = kb) in - type_value_eq (va, vb) + assert_type_value_eq (va, vb) in trace (simple_error "sum type") @@ bind_list_iter aux (List.combine a' b') @@ -169,13 +182,18 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w let%bind _ = Assert.assert_true ~msg:"different keys in record types" @@ (ka = kb) in - type_value_eq (va, vb) + assert_type_value_eq (va, vb) in trace (simple_error "record type") @@ bind_list_iter aux (List.combine a' b') ) - | a, b -> fail @@ different_kinds a b + | _ -> fail @@ different_kinds a b + +(* No information about what made it fail *) +let type_value_eq ab = match assert_type_value_eq ab with + | Ok _ -> true + | _ -> false let merge_annotation (a:type_value option) (b:type_value option) : type_value result = match a, b with @@ -183,38 +201,68 @@ let merge_annotation (a:type_value option) (b:type_value option) : type_value re | Some a, None -> ok a | None, Some b -> ok b | Some a, Some b -> - let%bind _ = type_value_eq (a, b) in - ok a + let%bind _ = assert_type_value_eq (a, b) in + match a.simplified, b.simplified with + | _, None -> ok a + | None, Some _ -> ok b + | _ -> simple_fail "both have simplified ASTs" -let t_bool : type_value = Type_constant ("bool", []) -let t_string : type_value = Type_constant ("string", []) -let t_bytes : type_value = Type_constant ("bytes", []) -let t_int : type_value = Type_constant ("int", []) -let t_unit : type_value = Type_constant ("unit", []) +let t_bool s : type_value = type_value (Type_constant ("bool", [])) s +let simplify_t_bool s = t_bool (Some s) +let make_t_bool = t_bool None + +let t_string s : type_value = type_value (Type_constant ("string", [])) s +let simplify_t_string s = t_string (Some s) +let make_t_string = t_string None + +let t_bytes s : type_value = type_value (Type_constant ("bytes", [])) s +let simplify_t_bytes s = t_bytes (Some s) +let make_t_bytes = t_bytes None + +let t_int s : type_value = type_value (Type_constant ("int", [])) s +let simplify_t_int s = t_int (Some s) +let make_t_int = t_int None + +let t_unit s : type_value = type_value (Type_constant ("unit", [])) s +let simplify_t_unit s = t_unit (Some s) +let make_t_unit = t_unit None + +let t_tuple lst s : type_value = type_value (Type_tuple lst) s +let simplify_t_tuple lst s = t_tuple lst (Some s) +let make_t_tuple lst = t_tuple lst None + +let t_record m s : type_value = type_value (Type_record m) s +let make_t_record m = t_record m None + +let t_sum m s : type_value = type_value (Type_sum m) s +let make_t_sum m = t_sum m None + +let t_function (param, result) s : type_value = type_value (Type_function (param, result)) s +let make_t_function f = t_function f None let get_annotation (x:annotated_expression) = x.type_annotation -let get_t_bool : type_value -> unit result = function +let get_t_bool (t:type_value) : unit result = match t.type_value with | Type_constant ("bool", []) -> ok () | _ -> simple_fail "not a bool" -let get_t_option : type_value -> type_value result = function +let get_t_option (t:type_value) : type_value result = match t.type_value with | Type_constant ("option", [o]) -> ok o | _ -> simple_fail "not a option" -let get_t_list : type_value -> type_value result = function +let get_t_list (t:type_value) : type_value result = match t.type_value with | Type_constant ("list", [o]) -> ok o | _ -> simple_fail "not a list" -let get_t_tuple : type_value -> type_value list result = function +let get_t_tuple (t:type_value) : type_value list result = match t.type_value with | Type_tuple lst -> ok lst | _ -> simple_fail "not a tuple" -let get_t_sum : type_value -> type_value SMap.t result = function +let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value with | Type_sum m -> ok m | _ -> simple_fail "not a sum" -let get_t_record : type_value -> type_value SMap.t result = function +let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value with | Type_record m -> ok m | _ -> simple_fail "not a record" diff --git a/src/ligo/ligo-helpers/trace.ml b/src/ligo/ligo-helpers/trace.ml index 47485c223..a38cdb871 100644 --- a/src/ligo/ligo-helpers/trace.ml +++ b/src/ligo/ligo-helpers/trace.ml @@ -58,6 +58,14 @@ let rec bind_list = function ok @@ hd :: tl ) +let bind_smap (s:_ X_map.String.t) = + let open X_map.String in + let aux k v prev = + prev >>? fun prev' -> + v >>? fun v' -> + ok @@ add k v' prev' in + fold aux s (ok empty) + let bind_fold_list f init lst = let aux x y = x >>? fun x -> @@ -155,16 +163,18 @@ let pp_to_string pp () x = let errors_to_string = pp_to_string errors_pp module Assert = struct - let assert_true ?msg = function + let assert_true ?(msg="not true") = function | true -> ok () - | false -> simple_fail @@ Option.unopt ~default:"not true" msg + | false -> simple_fail msg - let assert_equal_int ?msg a b = - let msg = Option.unopt ~default:"not equal int" msg in + let assert_equal_int ?(msg="not equal int") a b = assert_true ~msg (a = b) - let assert_list_size ~msg lst n = - assert_true ~msg (List.length lst = n) + let assert_list_size ?(msg="lst doesn't have the right size") lst n = + assert_true ~msg List.(length lst = n) + + let assert_list_same_size ?(msg="lists don't have same size") a b = + assert_true ~msg List.(length a = length b) let assert_list_size_2 ~msg = function | [a;b] -> ok (a, b) diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml index a1c376676..5546de6e0 100644 --- a/src/ligo/ligo.ml +++ b/src/ligo/ligo.ml @@ -75,12 +75,16 @@ let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_pro let type_expression ?(env:Typer.Environment.t = Typer.Environment.empty) (e:AST_Simplified.annotated_expression) : AST_Typed.annotated_expression result = Typer.type_annotated_expression env e -let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression = Typer.untype_annotated_expression e +let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression result = Typer.untype_annotated_expression e let transpile (p:AST_Typed.program) : Mini_c.program result = Transpiler.translate_program p let transpile_expression ?(env:Mini_c.Environment.t = Mini_c.Environment.empty) (e:AST_Typed.annotated_expression) : Mini_c.expression result = Transpiler.translate_annotated_expression env e let transpile_value ?(env:Mini_c.Environment.t = Mini_c.Environment.empty) - (e:AST_Typed.annotated_expression) : Mini_c.expression result = + (e:AST_Typed.annotated_expression) : Mini_c.value result = let%bind e = Transpiler.translate_annotated_expression env e in Mini_c.expression_to_value e + +let untranspile_value (v : Mini_c.value) (e:AST_Typed.type_value) : AST_Typed.annotated_expression result = + Transpiler.untranspile v e + diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 691f70170..03b97c650 100644 --- a/src/ligo/mini_c.ml +++ b/src/ligo/mini_c.ml @@ -360,59 +360,6 @@ module Translate_type = struct end -module Math = struct - - let lt_power_of_two n = - let rec aux prev n = - let cur = prev * 2 in - if cur >= n - then prev - else aux cur n - in - if n > 0 - then ok (aux 1 n) - else fail @@ error "lt_power_of_two" (string_of_int n) - - let ge_power_of_two n = - let rec aux c n = - if c >= n - then c - else aux (c * 2) n - in - if n > 0 - then ok (aux 1 n) - else fail @@ error "ge_power_of_two" (string_of_int n) - - let rec exp x n = - if n = 0 - then 1 - else - let exp' = exp (x * x) (n / 2) in - let m = if n mod 2 = 0 then 1 else x in - m * exp' - - let exp2 = exp 2 - - let log2_c n = - let rec aux acc n = - if n = 1 - then acc - else aux (acc + 1) (n / 2) - in - if n < 1 then raise @@ Failure ("log_2") ; - let n' = aux 0 n in - if exp2 n' = n then n' else n' + 1 - - let int_to_bools n l = - let rec aux acc n = function - | 0 -> acc - | s -> aux ((n mod 2 = 0) :: acc) (n / 2) (s - 1) - in - List.rev @@ aux [] n l - -end - - module Environment = struct open Tezos_utils.Micheline @@ -1020,27 +967,43 @@ module Run = struct end -(* module Combinators = struct - * - * let var x : expression' = Var x - * let apply a b : expression' = Apply(a, b) - * - * let t_int : type_value = `Base Int - * let type_int x : expression = x, `Base Int - * let type_f_int x : expression = x,`Function (`Base Int, `Base Int) - * let type_closure_int t x : expression = x, `Deep_closure (t, `Base Int, `Base Int) - * let int n = type_int @@ Literal(`Int n) - * let neg_int x = type_int @@ Predicate("NEG", [x]) - * let add_int x y = type_int @@ Predicate("ADD_INT", [x ; y]) - * let var_int x = type_int @@ var x - * let apply_int a b = type_int @@ apply a b - * - * let assign_variable v expr = Assignment (Variable (v, expr)) - * let assign_function v anon = Assignment (Variable (v, anon)) - * let function_int body binder result = { - * input = `Base Int ; - * output = `Base Int ; - * body ; binder ; result ; - * } - * - * end *) +module Combinators = struct + + let get_bool (v:value) = match v with + | `Bool b -> ok b + | _ -> simple_fail "not a bool" + + let get_int (v:value) = match v with + | `Int n -> ok n + | _ -> simple_fail "not an int" + + let get_string (v:value) = match v with + | `String s -> ok s + | _ -> simple_fail "not a string" + + let get_bytes (v:value) = match v with + | `Bytes b -> ok b + | _ -> simple_fail "not a bytes" + + let get_unit (v:value) = match v with + | `Unit -> ok () + | _ -> simple_fail "not a bool" + + let get_pair (v:value) = match v with + | `Pair (a, b) -> ok (a, b) + | _ -> simple_fail "not a pair" + + let get_left (v:value) = match v with + | `Left b -> ok b + | _ -> simple_fail "not a left" + + let get_right (v:value) = match v with + | `Right b -> ok b + | _ -> simple_fail "not a right" + + let get_or (v:value) = match v with + | `Left b -> ok (false, b) + | `Right b -> ok (true, b) + | _ -> simple_fail "not a left/right" + +end diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 33f427066..4ea2fe758 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -5,9 +5,12 @@ module AST = Ast_typed let list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun _ v prev -> v :: prev) m [] let kv_list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun k v prev -> (k, v) :: prev) m [] +let map_of_kv_list lst = + let open AST.SMap in + List.fold_left (fun prev (k, v) -> add k v prev) empty lst let rec translate_type (t:AST.type_value) : type_value result = - match t with + match t.type_value with | Type_constant ("bool", []) -> ok (`Base Bool) | Type_constant ("int", []) -> ok (`Base Int) | Type_constant ("string", []) -> ok (`Base String) @@ -81,7 +84,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express if k = m then ( let%bind _ = trace (simple_error "constructor parameter doesn't have expected type (shouldn't happen here)") - @@ AST.type_value_eq (tv, param.type_annotation) in + @@ AST.assert_type_value_eq (tv, param.type_annotation) in ok (Some (param'_expr), param'_tv) ) else ( let%bind tv = translate_type tv in @@ -213,3 +216,98 @@ let translate_program (lst:AST.program) : program result = in let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) lst in ok statements + +open Combinators + +let rec exp x n = + if n = 0 + then 1 + else + let exp' = exp (x * x) (n / 2) in + let m = if n mod 2 = 0 then 1 else x in + m * exp' + +let exp2 = exp 2 + +let extract_constructor (v : value) (tree : _ Append_tree.t') : (string * value * AST.type_value) result = + let open Append_tree in + let rec aux tv : (string * value * AST.type_value) result= + match tv with + | Leaf (k, t), v -> ok (k, v, t) + | Node {a}, `Left v -> aux (a, v) + | Node {b}, `Right v -> aux (b, v) + | _ -> simple_fail "bad constructor path" + in + let%bind (s, v, t) = aux (tree, v) in + ok (s, v, t) + +let extract_tuple (v : value) (tree : AST.type_value Append_tree.t') : ((value * AST.type_value) list) result = + let open Append_tree in + let rec aux tv : ((value * AST.type_value) list) result = + match tv with + | Leaf t, v -> ok @@ [v, t] + | Node {a;b}, `Pair (va, vb) -> + let%bind a' = aux (a, va) in + let%bind b' = aux (b, vb) in + ok (a' @ b') + | _ -> simple_fail "bad tuple path" + in + aux (tree, v) + +let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result = + let open Append_tree in + let rec aux tv : ((string * (value * AST.type_value)) list) result = + match tv with + | Leaf (s, t), v -> ok @@ [s, (v, t)] + | Node {a;b}, `Pair (va, vb) -> + let%bind a' = aux (a, va) in + let%bind b' = aux (b, vb) in + ok (a' @ b') + | _ -> simple_fail "bad record path" + in + aux (tree, v) + + +let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result = + let open! AST in + let return e = ok AST.(annotated_expression e t) in + match t.type_value with + | Type_constant ("bool", []) -> + let%bind b = get_bool v in + return (Literal (Bool b)) + | Type_constant ("int", []) -> + let%bind n = get_int v in + return (Literal (Int n)) + | Type_constant ("string", []) -> + let%bind n = get_string v in + return (Literal (String n)) + | Type_constant _ -> + simple_fail "unknown type_constant" + | Type_sum m -> + let lst = kv_list_of_map m in + let%bind node = match Append_tree.of_list lst with + | Empty -> simple_fail "empty sum type" + | Full t -> ok t + in + let%bind (name, v, tv) = extract_constructor v node in + let%bind sub = untranspile v tv in + return (Constructor (name, sub)) + | Type_tuple lst -> + let%bind node = match Append_tree.of_list lst with + | Empty -> simple_fail "empty tuple" + | Full t -> ok t in + let%bind tpl = extract_tuple v node in + let%bind tpl' = bind_list + @@ List.map (fun (x, y) -> untranspile x y) tpl in + return (Tuple tpl') + | Type_record m -> + let lst = kv_list_of_map m in + let%bind node = match Append_tree.of_list lst with + | Empty -> simple_fail "empty tuple" + | Full t -> ok t in + let%bind lst = extract_record v node in + let%bind lst = bind_list + @@ List.map (fun (x, (y, z)) -> let%bind yz = untranspile y z in ok (x, yz)) lst in + let m' = map_of_kv_list lst in + return (Record m') + | Type_function _ -> simple_fail "no untranspilation for functions yet" diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index a1b1be6d9..dac08e4c7 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -22,10 +22,11 @@ module Environment = struct let get_constructor (e:t) (s:string) : (ele * ele) option = let rec aux = function | [] -> None - | (_, ((O.Type_sum m) as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv) + | (_, (O.{type_value=(O.Type_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv) | _ :: tl -> aux tl in aux e.environment + let add (e:t) (s:string) (tv:ele) : t = {e with environment = (s, tv) :: e.environment} let get_type (e:t) (s:string) : ele option = @@ -101,7 +102,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc | Loop (cond, body) -> let%bind cond = type_annotated_expression e cond in let%bind _ = - O.type_value_eq (cond.type_annotation, (O.Type_constant ("bool", []))) in + O.assert_type_value_eq (cond.type_annotation, O.make_t_bool) in let%bind body = type_block e body in ok (e, O.Loop (cond, body)) | Assignment {name;annotated_expression} -> ( @@ -115,12 +116,12 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc let%bind annotated_expression = type_annotated_expression e annotated_expression in let e' = Environment.add e name annotated_expression.type_annotation in let%bind _ = - O.type_value_eq (annotated_expression.type_annotation, prev) in + O.assert_type_value_eq (annotated_expression.type_annotation, prev) in ok (e', O.Assignment {name;annotated_expression}) | Some _, Some prev -> let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind _assert = trace (simple_error "Annotation doesn't match environment") - @@ O.type_value_eq (annotated_expression.type_annotation, prev) in + @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in let e' = Environment.add e name annotated_expression.type_annotation in ok (e', O.Assignment {name;annotated_expression}) ) @@ -158,23 +159,28 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul let%bind b' = type_block e' b in ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')}) | Match_tuple (lst, b) -> - let%bind lst = + let%bind t_tuple = trace_strong (simple_error "Matching tuple on not-a-tuple") - get_tuple - let aux (x, y) = - let%bind y = type_block e y in - ok (x, y) in - let%bind lst' = bind_list @@ List.map aux lst in - ok (O.Match_tuple lst') + @@ O.get_t_tuple t in + let%bind _ = + trace_strong (simple_error "Matching tuple of different size") + @@ Assert.assert_list_same_size t_tuple lst in + let lst' = List.combine lst t_tuple in + let aux prev (name, tv) = Environment.add prev name tv in + let e' = List.fold_left aux e lst' in + let%bind b' = type_block e' b in + ok (O.Match_tuple (lst, b')) -and evaluate_type (e:environment) : I.type_expression -> O.type_value result = function +and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = + let return tv' = ok O.(type_value tv' (Some t)) in + match t with | Type_function (a, b) -> let%bind a' = evaluate_type e a in let%bind b' = evaluate_type e b in - ok (O.Type_function (a', b')) + return (Type_function (a', b')) | Type_tuple lst -> let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - ok (O.Type_tuple lst') + return (Type_tuple lst') | Type_sum m -> let aux k v prev = let%bind prev' = prev in @@ -182,7 +188,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f ok @@ SMap.add k v' prev' in let%bind m = SMap.fold aux m (ok SMap.empty) in - ok (O.Type_sum m) + return (Type_sum m) | Type_record m -> let aux k v prev = let%bind prev' = prev in @@ -190,7 +196,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f ok @@ SMap.add k v' prev' in let%bind m = SMap.fold aux m (ok SMap.empty) in - ok (O.Type_record m) + return (Type_record m) | Type_variable name -> let%bind tv = trace_option (unbound_type_variable e name) @@ -198,13 +204,13 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f ok tv | Type_constant (cst, lst) -> let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - ok (O.Type_constant(cst, lst')) + return (Type_constant(cst, lst')) and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result = let%bind tv_opt = match ae.type_annotation with | None -> ok None | Some s -> let%bind r = evaluate_type e s in ok (Some r) in - let check tv = O.merge_annotation (Some tv) tv_opt in + let check tv = O.(merge_annotation tv_opt (Some tv)) in match ae.expression with (* Basic *) | Variable name -> @@ -214,25 +220,25 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let%bind type_annotation = check tv' in ok O.{expression = Variable name ; type_annotation} | Literal (Bool b) -> - let%bind type_annotation = check O.t_bool in + let%bind type_annotation = check O.make_t_bool in ok O.{expression = Literal (Bool b) ; type_annotation } | Literal Unit -> - let%bind type_annotation = check O.t_unit in + let%bind type_annotation = check O.make_t_unit in ok O.{expression = Literal (Unit) ; type_annotation } | Literal (String s) -> - let%bind type_annotation = check O.t_string in + let%bind type_annotation = check O.make_t_string in ok O.{expression = Literal (String s) ; type_annotation } | Literal (Bytes s) -> - let%bind type_annotation = check O.t_bytes in + let%bind type_annotation = check O.make_t_bytes in ok O.{expression = Literal (Bytes s) ; type_annotation } | Literal (Number n) -> - let%bind type_annotation = check O.t_int in + let%bind type_annotation = check O.make_t_int in ok O.{expression = Literal (Int n) ; type_annotation } (* Tuple *) | Tuple lst -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in let tv_lst = List.map O.get_annotation lst' in - let%bind type_annotation = check (O.Type_tuple tv_lst) in + let%bind type_annotation = check (O.make_t_tuple tv_lst) in ok O.{expression = Tuple lst' ; type_annotation } | Tuple_accessor (tpl, ind) -> let%bind tpl' = type_annotated_expression e tpl in @@ -248,7 +254,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an trace_option (simple_error "no such constructor") @@ Environment.get_constructor e c in let%bind expr' = type_annotated_expression e expr in - let%bind _assert = O.type_value_eq (expr'.type_annotation, c_tv) in + let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in let%bind type_annotation = check sum_tv in ok O.{expression = O.Constructor(c, expr') ; type_annotation } (* Record *) @@ -259,7 +265,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an ok (SMap.add k expr' prev') in let%bind m' = SMap.fold aux m (ok SMap.empty) in - let%bind type_annotation = check @@ O.Type_record (SMap.map O.get_annotation m') in + let%bind type_annotation = check @@ O.make_t_record (SMap.map O.get_annotation m') in ok O.{expression = O.Record m' ; type_annotation } | Record_accessor (r, ind) -> let%bind r' = type_annotated_expression e r in @@ -281,7 +287,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an let e' = Environment.add e binder input_type in let%bind result = type_annotated_expression e' result in let%bind body = type_block e' body in - let%bind type_annotation = check O.(Type_function (input_type, output_type)) in + let%bind type_annotation = check @@ O.make_t_function (input_type, output_type) in ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation} | Constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in @@ -292,9 +298,9 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | Application (f, arg) -> let%bind f = type_annotated_expression e f in let%bind arg = type_annotated_expression e arg in - let%bind type_annotation = match f.type_annotation with + let%bind type_annotation = match f.type_annotation.type_value with | Type_function (param, result) -> - let%bind _ = O.type_value_eq (param, arg.type_annotation) in + let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in ok result | _ -> simple_fail "applying to not-a-function" in @@ -304,8 +310,108 @@ and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value (* Constant poorman's polymorphism *) let open O in match (name, lst) with - | "ADD", [a ; b] when a = t_int && b = t_int -> ok ("ADD_INT", t_int) - | "ADD", [a ; b] when a = t_string && b = t_string -> ok ("CONCAT", t_string) + | "ADD", [a ; b] when type_value_eq (a, make_t_int) && type_value_eq (b, make_t_int) -> ok ("ADD_INT", make_t_int) + | "ADD", [a ; b] when type_value_eq (a, make_t_string) && type_value_eq (b, make_t_string) -> ok ("CONCAT", make_t_string) | "ADD", [_ ; _] -> simple_fail "bad types to add" | "ADD", _ -> simple_fail "bad number of params to add" | name, _ -> fail @@ unrecognized_constant name + +let untype_type_value (t:O.type_value) : (I.type_expression) result = + match t.simplified with + | Some s -> ok s + | _ -> simple_fail "trying to untype generated type" + +let untype_literal (l:O.literal) : I.literal result = + let open I in + match l with + | Unit -> ok Unit + | Bool b -> ok (Bool b) + | Nat n -> ok (Number n) + | Int n -> ok (Number n) + | String s -> ok (String s) + | Bytes b -> ok (Bytes b) + +let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result = + let open I in + let annotation = e.type_annotation.simplified in + let return e = ok @@ annotated_expression e annotation in + match e.expression with + | Literal l -> + let%bind l = untype_literal l in + return (Literal l) + | Constant (n, lst) -> + let%bind lst' = bind_list + @@ List.map untype_annotated_expression lst in + return (Constant (n, lst')) + | Variable n -> + return (Variable n) + | Application (f, arg) -> + let%bind f' = untype_annotated_expression f in + let%bind arg' = untype_annotated_expression arg in + return (Application (f', arg')) + | Lambda {binder;input_type;output_type;body;result} -> + let%bind input_type = untype_type_value input_type in + let%bind output_type = untype_type_value output_type in + let%bind result = untype_annotated_expression result in + let%bind body = untype_block body in + return (Lambda {binder;input_type;output_type;body;result}) + | Tuple lst -> + let%bind lst' = bind_list + @@ List.map untype_annotated_expression lst in + return (Tuple lst') + | Tuple_accessor (tpl, ind) -> + let%bind tpl' = untype_annotated_expression tpl in + return (Tuple_accessor (tpl', ind)) + | Constructor (n, p) -> + let%bind p' = untype_annotated_expression p in + return (Constructor (n, p')) + | Record r -> + let%bind r' = bind_smap + @@ SMap.map untype_annotated_expression r in + return (Record r') + | Record_accessor (r, s) -> + let%bind r' = untype_annotated_expression r in + return (Record_accessor (r', s)) + +and untype_block (b:O.block) : (I.block) result = + bind_list @@ List.map untype_instruction b + +and untype_instruction (i:O.instruction) : (I.instruction) result = + let open I in + match i with + | Skip -> ok Skip + | Fail e -> + let%bind e' = untype_annotated_expression e in + ok (Fail e') + | Loop (e, b) -> + let%bind e' = untype_annotated_expression e in + let%bind b' = untype_block b in + ok @@ Loop (e', b') + | Assignment a -> + let%bind annotated_expression = untype_annotated_expression a.annotated_expression in + ok @@ Assignment {name = a.name ; annotated_expression} + | Matching (e, m) -> + let%bind e' = untype_annotated_expression e in + let%bind m' = untype_matching m in + ok @@ Matching (e', m') + +and untype_matching (m:O.matching) : (I.matching) result = + let open I in + match m with + | Match_bool {match_true ; match_false} -> + let%bind match_true = untype_block match_true in + let%bind match_false = untype_block match_false in + ok @@ Match_bool {match_true ; match_false} + | Match_tuple (lst, b) -> + let%bind b = untype_block b in + ok @@ Match_tuple (lst, b) + | Match_option {match_none ; match_some = (v, some)} -> + let%bind match_none = untype_block match_none in + let%bind some = untype_block some in + let match_some = v, some in + ok @@ Match_option {match_none ; match_some} + | Match_list {match_nil ; match_cons = (hd, tl, cons)} -> + let%bind match_nil = untype_block match_nil in + let%bind cons = untype_block cons in + let match_cons = hd, tl, cons in + ok @@ Match_list {match_nil ; match_cons}