From 5131ac00243b28df4f3926692262f153c852d62c Mon Sep 17 00:00:00 2001 From: Galfour Date: Wed, 17 Apr 2019 08:24:21 +0000 Subject: [PATCH] centralize declarations ; prompt questions --- src/lib_utils/trace.ml | 15 +++++++ src/ligo/operators.ml | 67 +++++++++++++++++------------- src/ligo/simplify.ml | 20 +-------- src/ligo/simplify_multifix.ml | 12 +----- src/ligo/typer.ml | 77 +++++++++++------------------------ 5 files changed, 79 insertions(+), 112 deletions(-) diff --git a/src/lib_utils/trace.ml b/src/lib_utils/trace.ml index 3c9d6b724..d76c61c32 100644 --- a/src/lib_utils/trace.ml +++ b/src/lib_utils/trace.ml @@ -60,6 +60,9 @@ let simple_error str () = mk_error ~title:str () let simple_fail str = fail @@ simple_error str +(* To be used when wrapped by a "trace_strong" for instance *) +let dummy_fail = simple_fail "dummy" + let map f = function | Ok x -> f x | Errors _ as e -> e @@ -154,6 +157,18 @@ let bind_fold_list f init lst = in List.fold_left aux (ok init) lst +let bind_find_map_list error f lst = + let rec aux lst = + match lst with + | [] -> fail error + | hd :: tl -> ( + match f hd with + | Ok x -> ok x + | Errors _ -> aux tl + ) + in + aux lst + let bind_list_iter f lst = let aux () y = f y in bind_fold_list aux () lst diff --git a/src/ligo/operators.ml b/src/ligo/operators.ml index fa59a47ae..257b48a01 100644 --- a/src/ligo/operators.ml +++ b/src/ligo/operators.ml @@ -1,23 +1,27 @@ open Trace -let type_constants = [ - ("unit" , 0) ; - ("string" , 0) ; - ("nat" , 0) ; - ("int" , 0) ; - ("bool" , 0) ; - ("operation" , 0) ; - ("list" , 1) ; - ("option" , 1) ; - ("set" , 1) ; - ("map" , 2) ; -] +module Simplify = struct -let constants = [ - ("get_force" , 2) ; - ("size" , 1) ; - ("int" , 1) ; -] + let type_constants = [ + ("unit" , 0) ; + ("string" , 0) ; + ("nat" , 0) ; + ("int" , 0) ; + ("bool" , 0) ; + ("operation" , 0) ; + ("list" , 1) ; + ("option" , 1) ; + ("set" , 1) ; + ("map" , 2) ; + ] + + let constants = [ + ("get_force" , 2) ; + ("size" , 1) ; + ("int" , 1) ; + ] + +end module Typer = struct module Errors = struct @@ -32,7 +36,7 @@ module Typer = struct type typer_predicate = type_value list -> bool type type_result = string * type_value type typer' = type_value list -> type_value option -> type_result result - type typer = string * (typer_predicate * typer') list + type typer = string * int * (typer_predicate * typer') list let predicate_0 : typer_predicate = fun lst -> match lst with @@ -87,34 +91,34 @@ module Typer = struct typer'_2 aux let make_2 : string -> _ list -> typer = fun name pfs -> - (name , List.map (Tuple.map_h_2 predicate_2 typer'_2) pfs) + (name , 2 , List.map (Tuple.map_h_2 predicate_2 typer'_2) pfs) let same_2 : string -> (string * type_value) list -> typer = fun s lst -> let aux (s, tv) = eq_2 tv, constant_2 s tv in - (s , List.map aux lst) + (s , 2 , List.map aux lst) let very_same_2 : string -> type_value -> typer = fun s tv -> same_2 s [s , tv] open Combinators - let comparator : string -> typer = fun s -> s , [ + let comparator : string -> typer = fun s -> s , 2 , [ (eq_2 (t_int ()), constant_2 s (t_bool ())) ; (eq_2 (t_nat ()), constant_2 s (t_bool ())) ; ] let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ()) - let none = "NONE" , [ + let none = "NONE" , 0 , [ predicate_0 , typer'_0 (fun tv_opt -> match tv_opt with | None -> simple_fail "untyped NONE" | Some t -> ok ("NONE", t)) ] - let some = "SOME" , [ + let some = "SOME" , 1 , [ true_1 , typer'_1 (fun s -> ok ("SOME", t_option s ())) ; ] - let map_remove : typer = "MAP_REMOVE" , [ + let map_remove : typer = "MAP_REMOVE" , 2 , [ (true_2 , typer'_2 (fun k m -> let%bind (src, _) = get_t_map m in let%bind () = assert_type_value_eq (src, k) in @@ -122,7 +126,7 @@ module Typer = struct )) ] - let map_update : typer = "MAP_UPDATE" , [ + let map_update : typer = "MAP_UPDATE" , 3 , [ (true_3 , typer'_3 (fun k v m -> let%bind (src, dst) = get_t_map m in let%bind () = assert_type_value_eq (src, k) in @@ -130,26 +134,29 @@ module Typer = struct ok ("MAP_UPDATE", m))) ] - let size : typer = "size" , [ + let size : typer = "size" , 1 , [ (true_1, typer'_1 (fun t -> let%bind () = bind_or (assert_t_map t, assert_t_list t) in ok ("SIZE", t_nat ()))) ] - let get_force : typer = "get_force" , [ + let get_force : typer = "get_force" , 2 , [ (true_2, typer'_2 (fun i_ty m_ty -> let%bind (src, dst) = get_t_map m_ty in let%bind _ = assert_type_value_eq (src, i_ty) in ok ("GET_FORCE", dst))) ] - let int : typer = "int" , [ + let int : typer = "int" , 1 , [ (true_1, typer'_1 (fun t -> let%bind () = assert_t_nat t in ok ("INT", t_int ()))) ] - let constant_typers = Map.String.of_list [ + let constant_typers = + let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in + Map.String.of_list + @@ List.map typer_to_kv [ same_2 "ADD" [ ("ADD_INT" , t_int ()) ; ("ADD_NAT" , t_nat ()) ; @@ -171,6 +178,8 @@ module Typer = struct map_remove ; map_update ; int ; + size ; + get_force ; ] end diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index f4410fdc6..4c92e46ce 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -10,18 +10,8 @@ let pseq_to_list = function | Some lst -> npseq_to_list lst let get_value : 'a Raw.reg -> 'a = fun x -> x.value -let type_constants = [ - ("unit", 0) ; - ("string", 0) ; - ("nat", 0) ; - ("int", 0) ; - ("bool", 0) ; - ("operation", 0) ; - ("list", 1) ; - ("option", 1) ; - ("set", 1) ; - ("map", 2) ; -] +let type_constants = Operators.Simplify.type_constants +let constants = Operators.Simplify.constants let rec simpl_type_expression (t:Raw.type_expr) : type_expression result = match t with @@ -76,12 +66,6 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result let%bind lst = bind_list @@ List.map simpl_type_expression lst in ok @@ T_tuple lst -let constants = [ - ("get_force", 2) ; - ("size", 1) ; - ("int", 1) ; -] - let rec simpl_expression (t:Raw.expr) : ae result = let return x = ok @@ ae x in let simpl_projection = fun (p:Raw.projection) -> diff --git a/src/ligo/simplify_multifix.ml b/src/ligo/simplify_multifix.ml index f4ab0dc77..fc240a8f8 100644 --- a/src/ligo/simplify_multifix.ml +++ b/src/ligo/simplify_multifix.ml @@ -5,17 +5,7 @@ module O = Ast_simplified let unwrap : type a . a Location.wrap -> a = Location.unwrap -let type_constants = [ - ("unit", 0) ; - ("string", 0) ; - ("nat", 0) ; - ("int", 0) ; - ("bool", 0) ; - ("list", 1) ; - ("option", 1) ; - ("set", 1) ; - ("map", 2) ; -] +let type_constants = Operators.Simplify.type_constants let type_variable : string -> O.type_expression result = fun str -> match List.assoc_opt str type_constants with diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 0d12eac09..272515218 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -80,6 +80,14 @@ module Errors = struct let full () = n in error title full () + let wrong_arity (n:string) (expected:int) (actual:int) () = + let title () = "wrong arity" in + let full () = + Format.asprintf "Wrong number of args passed to [%s]. Expected was %d, received was %d." + n expected actual + in + error title full () + let program_error (p:I.program) () = let title = (thunk "typing program") in let full () = Format.asprintf "%a" I.PP.program p in @@ -449,60 +457,21 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result = (* Constant poorman's polymorphism *) - let open O in - match (name, lst) with - | "ADD", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("ADD_INT", t_int ()) - | "ADD", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("ADD_NAT", t_nat ()) - | "ADD", [a ; b] when type_value_eq (a, t_string ()) && type_value_eq (b, t_string ()) -> ok ("CONCAT", t_string ()) - | "ADD", [_ ; _] -> simple_fail "bad types to add" - | "ADD", _ -> simple_fail "bad number of params to add" - | "TIMES", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("TIMES_INT", t_int ()) - | "TIMES", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("TIMES_NAT", t_nat ()) - | "TIMES", [_ ; _] -> simple_fail "bad types to TIMES" - | "TIMES", _ -> simple_fail "bad number of params to TIMES" - | "EQ", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("EQ", t_bool ()) - | "EQ", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("EQ", t_bool ()) - | "EQ", _ -> simple_fail "EQ only defined over int and nat" - | "LT", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("LT", t_bool ()) - | "LT", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("LT", t_bool ()) - | "LT", _ -> simple_fail "LT only defined over int and nat" - | "OR", [a ; b] when type_value_eq (a, t_bool ()) && type_value_eq (b, t_bool ()) -> ok ("OR", t_bool ()) - | "OR", _ -> simple_fail "OR only defined over bool" - | "AND", [a ; b] when type_value_eq (a, t_bool ()) && type_value_eq (b, t_bool ()) -> ok ("AND", t_bool ()) - | "AND", _ -> simple_fail "AND only defined over bool" - | "NONE", [] -> ( - match tv_opt with - | Some t -> ok ("NONE", t) - | None -> simple_fail "untyped NONE" - ) - | "NONE", _ -> simple_fail "bad number of params to NONE" - | "SOME", [s] -> ok ("SOME", t_option s ()) - | "SOME", _ -> simple_fail "bad number of params to SOME" - | "MAP_REMOVE", [k ; m] -> - let%bind (src, _) = get_t_map m in - let%bind () = O.assert_type_value_eq (src, k) in - ok ("MAP_REMOVE", m) - | "MAP_REMOVE", _ -> simple_fail "bad number of params to MAP_REMOVE" - | "MAP_UPDATE", [k ; v ; m] -> - let%bind (src, dst) = get_t_map m in - let%bind () = O.assert_type_value_eq (src, k) in - let%bind () = O.assert_type_value_eq (dst, v) in - ok ("MAP_UPDATE", m) - | "MAP_UPDATE", _ -> simple_fail "bad number of params to MAP_UPDATE" - | "get_force", [i_ty;m_ty] -> - let%bind (src, dst) = get_t_map m_ty in - let%bind _ = O.assert_type_value_eq (src, i_ty) in - ok ("GET_FORCE", dst) - | "get_force", _ -> simple_fail "bad number of params to get_force" - | "size", [t] -> - let%bind () = bind_or (assert_t_map t, assert_t_list t) in - ok ("SIZE", t_nat ()) - | "size", _ -> simple_fail "bad number of params to size" - | "int", [t] -> - let%bind () = assert_t_nat t in - ok ("INT", t_int ()) - | "int", _ -> simple_fail "bad number of params to int" - | name, _ -> fail @@ unrecognized_constant name + let ct = Operators.Typer.constant_typers in + let%bind v = + trace_option (unrecognized_constant name) @@ + Map.String.find_opt name ct in + let (arity, typer) = v in + let%bind () = + let l = List.length lst in + trace_strong (wrong_arity name arity l) @@ + Assert.assert_true (arity = l) in + let aux = fun (predicate, typer') -> + match predicate lst with + | true -> typer' lst tv_opt + | false -> dummy_fail + in + bind_find_map_list (simple_error "typing: unrecognized constant") aux typer let untype_type_value (t:O.type_value) : (I.type_expression) result = match t.simplified with