balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

centralize declarations ; prompt questions

Browse Source
This commit is contained in:
Galfour 2019-04-17 08:24:21 +00:00
parent d72d60a08d
commit 5131ac0024
5 changed files with 79 additions and 112 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/lib_utils/trace.ml
View File

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

41
src/ligo/operators.ml
View File

@ -1,6 +1,8 @@
open Trace
let type_constants = [
module Simplify = struct
let type_constants = [
("unit" , 0) ;
("string" , 0) ;
("nat" , 0) ;
@ -11,13 +13,15 @@ let type_constants = [
("option" , 1) ;
("set" , 1) ;
("map" , 2) ;
]
]
let constants = [
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

20
src/ligo/simplify.ml
View File

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

12
src/ligo/simplify_multifix.ml
View File

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

77
src/ligo/typer.ml
View File

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