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

refactor ast_typed

Browse Source
This commit is contained in:
Galfour 2019-04-20 19:14:18 +00:00
parent 50926c205e
commit 369e73a110
9 changed files with 736 additions and 723 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/lib_utils/trace.ml
View File

@ -116,6 +116,10 @@ let trace_f_ez f name =
let trace_f_2_ez f name =
trace_f_2 f (error (thunk "in function") name)
let to_bool = function
| Ok _ -> true
| Errors _ -> false
let to_option = function
| Ok (o, annotations) -> ignore annotations; Some o
| Errors _ -> None

104
src/ligo/ast_typed/PP.ml Normal file
View File

@ -0,0 +1,104 @@
open Types
open Format
open PP_helpers
let list_sep_d x = list_sep x (const " , ")
let smap_sep_d x = smap_sep x (const " , ")
let rec type_value' ppf (tv':type_value') : unit =
match tv' with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d type_value) lst
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_value) m
| T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_value) m
| T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
| T_constant (c, []) -> fprintf ppf "%s" c
| T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value'
let rec annotated_expression ppf (ae:annotated_expression) : unit =
match ae.type_annotation.simplified with
| Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
| _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
and lambda ppf l =
let {binder;input_type;output_type;result;body} = l in
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
and expression ppf (e:expression) : unit =
match e with
| E_literal l -> literal ppf l
| E_constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep_d annotated_expression) lst
| E_constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
| E_variable a -> fprintf ppf "%s" a
| E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
| E_lambda l -> fprintf ppf "%a" lambda l
| E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| E_record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| E_tuple lst -> fprintf ppf "tuple[@; @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
| E_map m -> fprintf ppf "map[@; @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
| E_list m -> fprintf ppf "list[@; @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) m
| E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and value ppf v = annotated_expression ppf v
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and literal ppf (l:literal) : unit =
match l with
| Literal_unit -> fprintf ppf "unit"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "%d" n
| Literal_string s -> fprintf ppf "%s" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((s, ae) : string * ae) =
fprintf ppf "%s <- %a" s annotated_expression ae
and matching : type a . (formatter -> a -> unit) -> _ -> a matching -> unit = fun f ppf m -> match m with
| Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep_d (fun ppf -> fprintf ppf "%s")) lst f b
| Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
and pre_access ppf (a:access) = match a with
| Access_record n -> fprintf ppf ".%s" n
| Access_tuple i -> fprintf ppf ".%d" i
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| I_loop (cond, b) -> fprintf ppf "while (%a) {@; @[<v>%a@]@;}" annotated_expression cond block b
| I_declaration {name;annotated_expression = ae} ->
fprintf ppf "let %s = %a" name annotated_expression ae
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
| I_patch (s, p, e) ->
fprintf ppf "%s%a := %a"
s.type_name (fun ppf -> List.iter (pre_access ppf)) p
annotated_expression e
let declaration ppf (d:declaration) =
match d with
| Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) =
fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) (List.map Location.unwrap p)

667
src/ligo/ast_typed/ast_typed.ml
View File

@ -1,659 +1,8 @@
module S = Ast_simplified
module SMap = Map.String
type name = string
type type_name = string
type 'a name_map = 'a SMap.t
type 'a type_name_map = 'a SMap.t
type program = declaration Location.wrap list
and declaration =
| Declaration_constant of named_expression
(* | Macro_declaration of macro_declaration *)
and annotated_expression = {
expression: expression ;
type_annotation: tv ;
}
and named_expression = {
name: name ;
annotated_expression: ae ;
}
and tv = type_value
and ae = annotated_expression
and tv_map = type_value type_name_map
and ae_map = annotated_expression name_map
and type_value' =
| T_tuple of tv list
| T_sum of tv_map
| T_record of tv_map
| T_constant of type_name * tv list
| T_function of tv * tv
and type_value = {
type_value' : type_value' ;
simplified : S.type_expression option ;
}
and named_type_value = {
type_name: name ;
type_value : type_value ;
}
and lambda = {
binder: name ;
input_type: tv ;
output_type: tv ;
result: ae ;
body: block ;
}
and expression =
(* Base *)
| E_literal of literal
| E_constant of (name * ae list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_variable of name
| E_application of (ae * ae)
| E_lambda of lambda
(* Tuple *)
| E_tuple of ae list
| E_tuple_accessor of (ae * int) (* Access n'th tuple's element *)
(* Sum *)
| E_constructor of (name * ae) (* For user defined constructors *)
(* Record *)
| E_record of ae_map
| E_record_accessor of (ae * string)
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_look_up of (ae * ae)
(* Advanced *)
| E_matching of (ae * matching_expr)
and value = annotated_expression (* todo (for refactoring) *)
and literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of int
| Literal_nat of int
| Literal_string of string
| Literal_bytes of bytes
and block = instruction list
and b = block
and instruction =
| I_declaration of named_expression
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_skip
| I_fail of ae
| I_patch of named_type_value * access_path * ae
and access = Ast_simplified.access
and access_path = Ast_simplified.access_path
and 'a matching =
| Match_bool of {
match_true : 'a ;
match_false : 'a ;
}
| Match_list of {
match_nil : 'a ;
match_cons : name * name * 'a ;
}
| Match_option of {
match_none : 'a ;
match_some : (name * type_value) * 'a ;
}
| Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = ae matching
open! Trace
let type_value type_value' simplified = { type_value' ; simplified }
let annotated_expression expression type_annotation = { expression ; type_annotation }
let get_type_annotation x = x.type_annotation
let get_entry (p:program) (entry : string) : annotated_expression result =
let aux (d:declaration) =
match d with
| Declaration_constant {name ; annotated_expression} when entry = name -> Some annotated_expression
| Declaration_constant _ -> None
in
let%bind result =
trace_option (simple_error "no entry point with given name") @@
Tezos_utils.List.find_map aux (List.map Location.unwrap p) in
ok result
let get_functional_entry (p:program) (entry : string) : (lambda * type_value) result =
let%bind entry = get_entry p entry in
match entry.expression with
| E_lambda l -> ok (l, entry.type_annotation)
| _ -> simple_fail "given entry point is not functional"
module PP = struct
open Format
open PP_helpers
let list_sep_d x = list_sep x (const " , ")
let smap_sep_d x = smap_sep x (const " , ")
let rec type_value' ppf (tv':type_value') : unit =
match tv' with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d type_value) lst
| T_sum m -> fprintf ppf "sum[%a]" (smap_sep_d type_value) m
| T_record m -> fprintf ppf "record[%a]" (smap_sep_d type_value) m
| T_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
| T_constant (c, []) -> fprintf ppf "%s" c
| T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value'
let rec annotated_expression ppf (ae:annotated_expression) : unit =
match ae.type_annotation.simplified with
| Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
| _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
and lambda ppf l =
let {binder;input_type;output_type;result;body} = l in
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
binder type_value input_type type_value output_type
block body annotated_expression result
and expression ppf (e:expression) : unit =
match e with
| E_literal l -> literal ppf l
| E_constant (c, lst) -> fprintf ppf "%s(%a)" c (list_sep_d annotated_expression) lst
| E_constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
| E_variable a -> fprintf ppf "%s" a
| E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
| E_lambda l -> fprintf ppf "%a" lambda l
| E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| E_record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| E_tuple lst -> fprintf ppf "tuple[@; @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
| E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
| E_map m -> fprintf ppf "map[@; @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
| E_list m -> fprintf ppf "list[@; @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) m
| E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
| E_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and value ppf v = annotated_expression ppf v
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and literal ppf (l:literal) : unit =
match l with
| Literal_unit -> fprintf ppf "unit"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int n -> fprintf ppf "%d" n
| Literal_nat n -> fprintf ppf "%d" n
| Literal_string s -> fprintf ppf "%s" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((s, ae) : string * ae) =
fprintf ppf "%s <- %a" s annotated_expression ae
and matching : type a . (formatter -> a -> unit) -> _ -> a matching -> unit = fun f ppf m -> match m with
| Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep_d (fun ppf -> fprintf ppf "%s")) lst f b
| Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
and pre_access ppf (a:access) = match a with
| Access_record n -> fprintf ppf ".%s" n
| Access_tuple i -> fprintf ppf ".%d" i
and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
| I_loop (cond, b) -> fprintf ppf "while (%a) {@; @[<v>%a@]@;}" annotated_expression cond block b
| I_declaration {name;annotated_expression = ae} ->
fprintf ppf "let %s = %a" name annotated_expression ae
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
| I_patch (s, p, e) ->
fprintf ppf "%s%a := %a"
s.type_name (fun ppf -> List.iter (pre_access ppf)) p
annotated_expression e
let declaration ppf (d:declaration) =
match d with
| Declaration_constant {name ; annotated_expression = ae} ->
fprintf ppf "const %s = %a" name annotated_expression ae
let program ppf (p:program) =
fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) (List.map Location.unwrap p)
end
module Free_variables = struct
type bindings = string list
let mem : string -> bindings -> bool = List.mem
let singleton : string -> bindings = fun s -> [ s ]
let union : bindings -> bindings -> bindings = (@)
let unions : bindings list -> bindings = List.concat
let empty : bindings = []
let of_list : string list -> bindings = fun x -> x
let rec expression : bindings -> expression -> bindings = fun b e ->
let self = annotated_expression b in
match e with
| E_lambda l ->
let b' = union (singleton l.binder) b in
let (b'', frees) = block' b' l.body in
union (annotated_expression b'' l.result) frees
| E_literal _ -> empty
| E_constant (_ , lst) -> unions @@ List.map self lst
| E_variable name -> (
match mem name b with
| true -> empty
| false -> singleton name
)
| E_application (a, b) -> unions @@ List.map self [ a ; b ]
| E_tuple lst -> unions @@ List.map self lst
| E_constructor (_ , a) -> self a
| E_record m -> unions @@ List.map self @@ Map.String.to_list m
| E_record_accessor (a, _) -> self a
| E_tuple_accessor (a, _) -> self a
| E_list lst -> unions @@ List.map self lst
| E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
| E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
expression b ae.expression
and instruction' : bindings -> instruction -> bindings * bindings = fun b i ->
match i with
| I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression)
| I_assignment n -> b , (annotated_expression b n.annotated_expression)
| I_skip -> b , empty
| I_fail e -> b , annotated_expression b e
| I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl)
| I_patch (_ , _ , a) -> b , annotated_expression b a
| I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs)
and block' : bindings -> block -> (bindings * bindings) = fun b bl ->
let aux = fun (binds, frees) cur ->
let (binds', frees') = instruction' binds cur in
(binds', union frees frees') in
List.fold_left aux (b , []) bl
and block : bindings -> block -> bindings = fun b bl ->
let (_ , frees) = block' b bl in
frees
and matching : type a . (bindings -> a -> bindings) -> bindings -> a matching -> bindings = fun f b m ->
match m with
| Match_bool { match_true = t ; match_false = fa } -> union (f b t) (f b fa)
| Match_list { match_nil = n ; match_cons = (hd, tl, c) } -> union (f b n) (f (union (of_list [hd ; tl]) b) c)
| Match_option { match_none = n ; match_some = ((opt, _), s) } -> union (f b n) (f (union (singleton opt) b) s)
| Match_tuple (lst, a) -> f (union (of_list lst) b) a
and matching_expression = fun x -> matching annotated_expression x
and matching_block = fun x -> matching block x
end
module Errors = struct
let different_kinds a b () =
let title = (thunk "different kinds") in
let full () = Format.asprintf "(%a) VS (%a)" PP.type_value a PP.type_value b in
error title full ()
let different_constants a b () =
let title = (thunk "different constants") in
let full () = Format.asprintf "%s VS %s" a b in
error title full ()
let different_size_type name a b () =
let title () = name ^ " have different sizes" in
let full () = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
error title full ()
let different_size_constants = different_size_type "constants"
let different_size_tuples = different_size_type "tuples"
let different_size_sums = different_size_type "sums"
let different_size_records = different_size_type "records"
end
open Errors
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
| T_tuple ta, T_tuple tb -> (
let%bind _ =
trace_strong (fun () -> (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)
)
| T_tuple _, _ -> fail @@ different_kinds a b
| T_constant (ca, lsta), T_constant (cb, lstb) -> (
let%bind _ =
trace_strong (different_size_constants a b)
@@ Assert.assert_true List.(length lsta = length lstb) in
let%bind _ =
trace_strong (different_constants ca cb)
@@ Assert.assert_true (ca = cb) in
trace (simple_error "constant sub-expression")
@@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
)
| T_constant _, _ -> fail @@ different_kinds a b
| T_sum sa, T_sum sb -> (
let sa' = SMap.to_kv_list sa in
let sb' = SMap.to_kv_list sb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in sum types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
trace_strong (different_size_sums a b)
@@ Assert.assert_list_same_size sa' sb' in
trace (simple_error "sum type") @@
bind_list_iter aux (List.combine sa' sb')
)
| T_sum _, _ -> fail @@ different_kinds a b
| T_record ra, T_record rb -> (
let ra' = SMap.to_kv_list ra in
let rb' = SMap.to_kv_list rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
trace_strong (different_size_records a b)
@@ Assert.assert_list_same_size ra' rb' in
trace (simple_error "record type")
@@ bind_list_iter aux (List.combine ra' rb')
)
| T_record _, _ -> fail @@ different_kinds a b
| T_function (param, result), T_function (param', result') ->
let%bind _ = assert_type_value_eq (param, param') in
let%bind _ = assert_type_value_eq (result, result') in
ok ()
| T_function _, _ -> 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 assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with
| Literal_bool a, Literal_bool b when a = b -> ok ()
| Literal_bool _, Literal_bool _ -> simple_fail "different bools"
| Literal_bool _, _ -> simple_fail "bool vs non-bool"
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> simple_fail "different ints"
| Literal_int _, _ -> simple_fail "int vs non-int"
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> simple_fail "different nats"
| Literal_nat _, _ -> simple_fail "nat vs non-nat"
| Literal_string a, Literal_string b when a = b -> ok ()
| Literal_string _, Literal_string _ -> simple_fail "different strings"
| Literal_string _, _ -> simple_fail "string vs non-string"
| Literal_bytes a, Literal_bytes b when a = b -> ok ()
| Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
let rec assert_value_eq (a, b: (value*value)) : unit result =
let error_content () =
Format.asprintf "%a vs %a" PP.value a PP.value b
in
trace (fun () -> error (thunk "not equal") error_content ()) @@
match (a.expression, b.expression) with
| E_literal a, E_literal b ->
assert_literal_eq (a, b)
| E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> (
let%bind lst =
generic_try (simple_error "constants with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_constant _, E_constant _ ->
simple_fail "different constants"
| E_constant _, _ ->
let error_content () =
Format.asprintf "%a vs %a"
PP.annotated_expression a
PP.annotated_expression b
in
fail @@ (fun () -> error (thunk "comparing constant with other stuff") error_content ())
| E_constructor (ca, a), E_constructor (cb, b) when ca = cb -> (
let%bind _eq = assert_value_eq (a, b) in
ok ()
)
| E_constructor _, E_constructor _ ->
simple_fail "different constructors"
| E_constructor _, _ ->
simple_fail "comparing constructor with other stuff"
| E_tuple lsta, E_tuple lstb -> (
let%bind lst =
generic_try (simple_error "tuples with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_tuple _, _ ->
simple_fail "comparing tuple with other stuff"
| E_record sma, E_record smb -> (
let aux _ a b =
match a, b with
| Some a, Some b -> Some (assert_value_eq (a, b))
| _ -> Some (simple_fail "different record keys")
in
let%bind _all = bind_smap @@ SMap.merge aux sma smb in
ok ()
)
| E_record _, _ ->
simple_fail "comparing record with other stuff"
| E_map lsta, E_map lstb -> (
let%bind lst = generic_try (simple_error "maps of different lengths")
(fun () ->
let lsta' = List.sort compare lsta in
let lstb' = List.sort compare lstb in
List.combine lsta' lstb') in
let aux = fun ((ka, va), (kb, vb)) ->
let%bind _ = assert_value_eq (ka, kb) in
let%bind _ = assert_value_eq (va, vb) in
ok () in
let%bind _all = bind_map_list aux lst in
ok ()
)
| E_map _, _ ->
simple_fail "comparing map with other stuff"
| E_list lsta, E_list lstb -> (
let%bind lst =
generic_try (simple_error "list of different lengths")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_list _, _ ->
simple_fail "comparing list with other stuff"
| _, _ -> simple_fail "comparing not a value"
let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
match a, b with
| None, None -> simple_fail "no annotation"
| Some a, None -> ok a
| None, Some b -> ok b
| Some a, Some b ->
let%bind _ = assert_type_value_eq (a, b) in
match a.simplified, b.simplified with
| _, None -> ok a
| _, Some _ -> ok b
module Combinators = struct
let t_bool ?s () : type_value = type_value (T_constant ("bool", [])) s
let t_string ?s () : type_value = type_value (T_constant ("string", [])) s
let t_bytes ?s () : type_value = type_value (T_constant ("bytes", [])) s
let t_int ?s () : type_value = type_value (T_constant ("int", [])) s
let t_nat ?s () : type_value = type_value (T_constant ("nat", [])) s
let t_unit ?s () : type_value = type_value (T_constant ("unit", [])) s
let t_option o ?s () : type_value = type_value (T_constant ("option", [o])) s
let t_tuple lst ?s () : type_value = type_value (T_tuple lst) s
let t_list t ?s () : type_value = type_value (T_constant ("list", [t])) s
let t_pair a b ?s () = t_tuple [a ; b] ?s ()
let t_record m ?s () : type_value = type_value (T_record m) s
let make_t_ez_record (lst:(string * type_value) list) : type_value =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
type_value (T_record map) None
let ez_t_record lst ?s () : type_value =
let m = SMap.of_list lst in
t_record m ?s ()
let t_map key value ?s () = type_value (T_constant ("map", [key ; value])) s
let t_sum m ?s () : type_value = type_value (T_sum m) s
let make_t_ez_sum (lst:(string * type_value) list) : type_value =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
type_value (T_sum map) None
let t_function param result ?s () : type_value = type_value (T_function (param, result)) s
let t_shallow_closure param result ?s () : type_value = type_value (T_function (param, result)) s
let get_annotation (x:annotated_expression) = x.type_annotation
let get_t_bool (t:type_value) : unit result = match t.type_value' with
| T_constant ("bool", []) -> ok ()
| _ -> simple_fail "not a bool"
let get_t_option (t:type_value) : type_value result = match t.type_value' with
| T_constant ("option", [o]) -> ok o
| _ -> simple_fail "not a option"
let get_t_list (t:type_value) : type_value result = match t.type_value' with
| T_constant ("list", [o]) -> ok o
| _ -> simple_fail "not a list"
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst
| _ -> simple_fail "not a tuple"
let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_sum m -> ok m
| _ -> simple_fail "not a sum"
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_record m -> ok m
| _ -> simple_fail "not a record"
let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let assert_t_map (t:type_value) : unit result =
match t.type_value' with
| T_constant ("map", [_ ; _]) -> ok ()
| _ -> simple_fail "not a map"
let assert_t_list (t:type_value) : unit result =
match t.type_value' with
| T_constant ("list", [_]) -> ok ()
| _ -> simple_fail "assert: not a list"
let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("int", []) -> ok ()
| _ -> simple_fail "not an int"
let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("nat", []) -> ok ()
| _ -> simple_fail "not an nat"
let e_record map : expression = E_record map
let ez_e_record (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
e_record map
let e_some s : expression = E_constant ("SOME", [s])
let e_none : expression = E_constant ("NONE", [])
let e_map lst : expression = E_map lst
let e_unit : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_pair a b : expression = E_tuple [a; b]
let e_list lst : expression = E_list lst
let e_a_unit = annotated_expression e_unit (t_unit ())
let e_a_int n = annotated_expression (e_int n) (t_int ())
let e_a_nat n = annotated_expression (e_nat n) (t_nat ())
let e_a_bool b = annotated_expression (e_bool b) (t_bool ())
let e_a_string s = annotated_expression (e_string s) (t_string ())
let e_a_pair a b = annotated_expression (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
let e_a_some s = annotated_expression (e_some s) (t_option s.type_annotation ())
let e_a_none t = annotated_expression e_none (t_option t ())
let e_a_tuple lst = annotated_expression (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ())
let e_a_record r = annotated_expression (e_record r) (t_record (SMap.map get_type_annotation r) ())
let ez_e_a_record r = annotated_expression (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_annotation) r) ())
let e_a_map lst k v = annotated_expression (e_map lst) (t_map k v ())
let e_a_list lst t = annotated_expression (e_list lst) (t_list t ())
let get_a_int (t:annotated_expression) =
match t.expression with
| E_literal (Literal_int n) -> ok n
| _ -> simple_fail "not an int"
let get_a_unit (t:annotated_expression) =
match t.expression with
| E_literal (Literal_unit) -> ok ()
| _ -> simple_fail "not a unit"
let get_a_bool (t:annotated_expression) =
match t.expression with
| E_literal (Literal_bool b) -> ok b
| _ -> simple_fail "not a bool"
end
include Types
include Misc
module Types = Types
module Environment = Environment
module PP = PP
module Combinators = Combinators
module Misc = Misc

131
src/ligo/ast_typed/combinators.ml Normal file
View File

@ -0,0 +1,131 @@
open Trace
open Types
let make_t type_value' simplified = { type_value' ; simplified }
let make_a_e expression type_annotation = { expression ; type_annotation }
let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
let t_pair a b ?s () = t_tuple [a ; b] ?s ()
let t_record m ?s () : type_value = make_t (T_record m) s
let make_t_ez_record (lst:(string * type_value) list) : type_value =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
make_t (T_record map) None
let ez_t_record lst ?s () : type_value =
let m = SMap.of_list lst in
t_record m ?s ()
let t_map key value ?s () = make_t (T_constant ("map", [key ; value])) s
let t_sum m ?s () : type_value = make_t (T_sum m) s
let make_t_ez_sum (lst:(string * type_value) list) : type_value =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
make_t (T_sum map) None
let t_function param result ?s () : type_value = make_t (T_function (param, result)) s
let t_shallow_closure param result ?s () : type_value = make_t (T_function (param, result)) s
let get_type_annotation (x:annotated_expression) = x.type_annotation
let get_t_bool (t:type_value) : unit result = match t.type_value' with
| T_constant ("bool", []) -> ok ()
| _ -> simple_fail "not a bool"
let get_t_option (t:type_value) : type_value result = match t.type_value' with
| T_constant ("option", [o]) -> ok o
| _ -> simple_fail "not a option"
let get_t_list (t:type_value) : type_value result = match t.type_value' with
| T_constant ("list", [o]) -> ok o
| _ -> simple_fail "not a list"
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst
| _ -> simple_fail "not a tuple"
let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_sum m -> ok m
| _ -> simple_fail "not a sum"
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_record m -> ok m
| _ -> simple_fail "not a record"
let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let assert_t_map (t:type_value) : unit result =
match t.type_value' with
| T_constant ("map", [_ ; _]) -> ok ()
| _ -> simple_fail "not a map"
let assert_t_list (t:type_value) : unit result =
match t.type_value' with
| T_constant ("list", [_]) -> ok ()
| _ -> simple_fail "assert: not a list"
let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("int", []) -> ok ()
| _ -> simple_fail "not an int"
let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with
| T_constant ("nat", []) -> ok ()
| _ -> simple_fail "not an nat"
let e_record map : expression = E_record map
let ez_e_record (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
e_record map
let e_some s : expression = E_constant ("SOME", [s])
let e_none : expression = E_constant ("NONE", [])
let e_map lst : expression = E_map lst
let e_unit : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_pair a b : expression = E_tuple [a; b]
let e_list lst : expression = E_list lst
let e_a_unit = make_a_e e_unit (t_unit ())
let e_a_int n = make_a_e (e_int n) (t_int ())
let e_a_nat n = make_a_e (e_nat n) (t_nat ())
let e_a_bool b = make_a_e (e_bool b) (t_bool ())
let e_a_string s = make_a_e (e_string s) (t_string ())
let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
let e_a_none t = make_a_e e_none (t_option t ())
let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ())
let e_a_record r = make_a_e (e_record r) (t_record (SMap.map get_type_annotation r) ())
let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_annotation) r) ())
let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ())
let e_a_list lst t = make_a_e (e_list lst) (t_list t ())
let get_a_int (t:annotated_expression) =
match t.expression with
| E_literal (Literal_int n) -> ok n
| _ -> simple_fail "not an int"
let get_a_unit (t:annotated_expression) =
match t.expression with
| E_literal (Literal_unit) -> ok ()
| _ -> simple_fail "not a unit"
let get_a_bool (t:annotated_expression) =
match t.expression with
| E_literal (Literal_bool b) -> ok b
| _ -> simple_fail "not a bool"

56
src/ligo/ast_typed/environment.ml Normal file
View File

@ -0,0 +1,56 @@
open Types
type ele = type_value
type t = {
environment: (string * ele) list ;
type_environment: (string * ele) list ;
}
let empty : t = {
(* TODO: use maps *)
environment = [] ;
type_environment = [] ;
}
let get (e:t) (s:string) : ele option =
List.assoc_opt s e.environment
let get_constructor (e:t) (s:string) : (ele * ele) option =
let rec aux = function
| [] -> None
| (_, ({type_value'=(T_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 =
List.assoc_opt s e.type_environment
let add_type (e:t) (s:string) (tv:ele) : t =
{e with type_environment = (s, tv) :: e.type_environment}
module PP = struct
open Format
open PP_helpers
let list_sep_d x = list_sep x (const " , ")
let value ppf (e:t) =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in
fprintf ppf "ValueEnv[%a]" (list_sep_d pp) e.environment
let type_ ppf e =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s PP.type_value e in
fprintf ppf "TypeEnv[%a]" (list_sep_d pp) e.type_environment
let full ppf e =
fprintf ppf "%a\n%a" value e type_ e
end
module Combinators = struct
let env_sum_type ?(env = empty)
?(name = "a_sum_type")
(lst : (string * ele) list) =
add env name (Combinators.make_t_ez_sum lst)
end

280
src/ligo/ast_typed/misc.ml Normal file
View File

@ -0,0 +1,280 @@
open Trace
open Types
module Errors = struct
let different_kinds a b () =
let title = (thunk "different kinds") in
let full () = Format.asprintf "(%a) VS (%a)" PP.type_value a PP.type_value b in
error title full ()
let different_constants a b () =
let title = (thunk "different constants") in
let full () = Format.asprintf "%s VS %s" a b in
error title full ()
let different_size_type name a b () =
let title () = name ^ " have different sizes" in
let full () = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
error title full ()
let different_size_constants = different_size_type "constants"
let different_size_tuples = different_size_type "tuples"
let different_size_sums = different_size_type "sums"
let different_size_records = different_size_type "records"
end
module Free_variables = struct
type bindings = string list
let mem : string -> bindings -> bool = List.mem
let singleton : string -> bindings = fun s -> [ s ]
let union : bindings -> bindings -> bindings = (@)
let unions : bindings list -> bindings = List.concat
let empty : bindings = []
let of_list : string list -> bindings = fun x -> x
let rec expression : bindings -> expression -> bindings = fun b e ->
let self = annotated_expression b in
match e with
| E_lambda l ->
let b' = union (singleton l.binder) b in
let (b'', frees) = block' b' l.body in
union (annotated_expression b'' l.result) frees
| E_literal _ -> empty
| E_constant (_ , lst) -> unions @@ List.map self lst
| E_variable name -> (
match mem name b with
| true -> empty
| false -> singleton name
)
| E_application (a, b) -> unions @@ List.map self [ a ; b ]
| E_tuple lst -> unions @@ List.map self lst
| E_constructor (_ , a) -> self a
| E_record m -> unions @@ List.map self @@ Map.String.to_list m
| E_record_accessor (a, _) -> self a
| E_tuple_accessor (a, _) -> self a
| E_list lst -> unions @@ List.map self lst
| E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
| E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
| E_matching (a , cs) -> union (self a) (matching_expression b cs)
and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae ->
expression b ae.expression
and instruction' : bindings -> instruction -> bindings * bindings = fun b i ->
match i with
| I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression)
| I_assignment n -> b , (annotated_expression b n.annotated_expression)
| I_skip -> b , empty
| I_fail e -> b , annotated_expression b e
| I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl)
| I_patch (_ , _ , a) -> b , annotated_expression b a
| I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs)
and block' : bindings -> block -> (bindings * bindings) = fun b bl ->
let aux = fun (binds, frees) cur ->
let (binds', frees') = instruction' binds cur in
(binds', union frees frees') in
List.fold_left aux (b , []) bl
and block : bindings -> block -> bindings = fun b bl ->
let (_ , frees) = block' b bl in
frees
and matching : type a . (bindings -> a -> bindings) -> bindings -> a matching -> bindings = fun f b m ->
match m with
| Match_bool { match_true = t ; match_false = fa } -> union (f b t) (f b fa)
| Match_list { match_nil = n ; match_cons = (hd, tl, c) } -> union (f b n) (f (union (of_list [hd ; tl]) b) c)
| Match_option { match_none = n ; match_some = ((opt, _), s) } -> union (f b n) (f (union (singleton opt) b) s)
| Match_tuple (lst, a) -> f (union (of_list lst) b) a
and matching_expression = fun x -> matching annotated_expression x
and matching_block = fun x -> matching block x
end
open Errors
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
| T_tuple ta, T_tuple tb -> (
let%bind _ =
trace_strong (fun () -> (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)
)
| T_tuple _, _ -> fail @@ different_kinds a b
| T_constant (ca, lsta), T_constant (cb, lstb) -> (
let%bind _ =
trace_strong (different_size_constants a b)
@@ Assert.assert_true List.(length lsta = length lstb) in
let%bind _ =
trace_strong (different_constants ca cb)
@@ Assert.assert_true (ca = cb) in
trace (simple_error "constant sub-expression")
@@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
)
| T_constant _, _ -> fail @@ different_kinds a b
| T_sum sa, T_sum sb -> (
let sa' = SMap.to_kv_list sa in
let sb' = SMap.to_kv_list sb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in sum types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
trace_strong (different_size_sums a b)
@@ Assert.assert_list_same_size sa' sb' in
trace (simple_error "sum type") @@
bind_list_iter aux (List.combine sa' sb')
)
| T_sum _, _ -> fail @@ different_kinds a b
| T_record ra, T_record rb -> (
let ra' = SMap.to_kv_list ra in
let rb' = SMap.to_kv_list rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@@ (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
trace_strong (different_size_records a b)
@@ Assert.assert_list_same_size ra' rb' in
trace (simple_error "record type")
@@ bind_list_iter aux (List.combine ra' rb')
)
| T_record _, _ -> fail @@ different_kinds a b
| T_function (param, result), T_function (param', result') ->
let%bind _ = assert_type_value_eq (param, param') in
let%bind _ = assert_type_value_eq (result, result') in
ok ()
| T_function _, _ -> fail @@ different_kinds a b
(* No information about what made it fail *)
let type_value_eq ab = Trace.to_bool @@ assert_type_value_eq ab
let assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with
| Literal_bool a, Literal_bool b when a = b -> ok ()
| Literal_bool _, Literal_bool _ -> simple_fail "different bools"
| Literal_bool _, _ -> simple_fail "bool vs non-bool"
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> simple_fail "different ints"
| Literal_int _, _ -> simple_fail "int vs non-int"
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> simple_fail "different nats"
| Literal_nat _, _ -> simple_fail "nat vs non-nat"
| Literal_string a, Literal_string b when a = b -> ok ()
| Literal_string _, Literal_string _ -> simple_fail "different strings"
| Literal_string _, _ -> simple_fail "string vs non-string"
| Literal_bytes a, Literal_bytes b when a = b -> ok ()
| Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
let rec assert_value_eq (a, b: (value*value)) : unit result =
let error_content () =
Format.asprintf "%a vs %a" PP.value a PP.value b
in
trace (fun () -> error (thunk "not equal") error_content ()) @@
match (a.expression, b.expression) with
| E_literal a, E_literal b ->
assert_literal_eq (a, b)
| E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> (
let%bind lst =
generic_try (simple_error "constants with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_constant _, E_constant _ ->
simple_fail "different constants"
| E_constant _, _ ->
let error_content () =
Format.asprintf "%a vs %a"
PP.annotated_expression a
PP.annotated_expression b
in
fail @@ (fun () -> error (thunk "comparing constant with other stuff") error_content ())
| E_constructor (ca, a), E_constructor (cb, b) when ca = cb -> (
let%bind _eq = assert_value_eq (a, b) in
ok ()
)
| E_constructor _, E_constructor _ ->
simple_fail "different constructors"
| E_constructor _, _ ->
simple_fail "comparing constructor with other stuff"
| E_tuple lsta, E_tuple lstb -> (
let%bind lst =
generic_try (simple_error "tuples with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_tuple _, _ ->
simple_fail "comparing tuple with other stuff"
| E_record sma, E_record smb -> (
let aux _ a b =
match a, b with
| Some a, Some b -> Some (assert_value_eq (a, b))
| _ -> Some (simple_fail "different record keys")
in
let%bind _all = bind_smap @@ SMap.merge aux sma smb in
ok ()
)
| E_record _, _ ->
simple_fail "comparing record with other stuff"
| E_map lsta, E_map lstb -> (
let%bind lst = generic_try (simple_error "maps of different lengths")
(fun () ->
let lsta' = List.sort compare lsta in
let lstb' = List.sort compare lstb in
List.combine lsta' lstb') in
let aux = fun ((ka, va), (kb, vb)) ->
let%bind _ = assert_value_eq (ka, kb) in
let%bind _ = assert_value_eq (va, vb) in
ok () in
let%bind _all = bind_map_list aux lst in
ok ()
)
| E_map _, _ ->
simple_fail "comparing map with other stuff"
| E_list lsta, E_list lstb -> (
let%bind lst =
generic_try (simple_error "list of different lengths")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_list _, _ ->
simple_fail "comparing list with other stuff"
| _, _ -> simple_fail "comparing not a value"
let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
match a, b with
| None, None -> simple_fail "no annotation"
| Some a, None -> ok a
| None, Some b -> ok b
| Some a, Some b ->
let%bind _ = assert_type_value_eq (a, b) in
match a.simplified, b.simplified with
| _, None -> ok a
| _, Some _ -> ok b

142
src/ligo/ast_typed/types.ml Normal file
View File

@ -0,0 +1,142 @@
module S = Ast_simplified
module SMap = Map.String
type name = string
type type_name = string
type 'a name_map = 'a SMap.t
type 'a type_name_map = 'a SMap.t
type program = declaration Location.wrap list
and declaration =
| Declaration_constant of named_expression
(* | Macro_declaration of macro_declaration *)
and annotated_expression = {
expression: expression ;
type_annotation: tv ;
}
and named_expression = {
name: name ;
annotated_expression: ae ;
}
and tv = type_value
and ae = annotated_expression
and tv_map = type_value type_name_map
and ae_map = annotated_expression name_map
and type_value' =
| T_tuple of tv list
| T_sum of tv_map
| T_record of tv_map
| T_constant of type_name * tv list
| T_function of tv * tv
and type_value = {
type_value' : type_value' ;
simplified : S.type_expression option ;
}
and named_type_value = {
type_name: name ;
type_value : type_value ;
}
and lambda = {
binder: name ;
input_type: tv ;
output_type: tv ;
result: ae ;
body: block ;
}
and expression =
(* Base *)
| E_literal of literal
| E_constant of (name * ae list) (* For language constants, like (Cons hd tl) or (plus i j) *)
| E_variable of name
| E_application of (ae * ae)
| E_lambda of lambda
(* Tuple *)
| E_tuple of ae list
| E_tuple_accessor of (ae * int) (* Access n'th tuple's element *)
(* Sum *)
| E_constructor of (name * ae) (* For user defined constructors *)
(* Record *)
| E_record of ae_map
| E_record_accessor of (ae * string)
(* Data Structures *)
| E_map of (ae * ae) list
| E_list of ae list
| E_look_up of (ae * ae)
(* Advanced *)
| E_matching of (ae * matching_expr)
and value = annotated_expression (* todo (for refactoring) *)
and literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of int
| Literal_nat of int
| Literal_string of string
| Literal_bytes of bytes
and block = instruction list
and b = block
and instruction =
| I_declaration of named_expression
| I_assignment of named_expression
| I_matching of ae * matching_instr
| I_loop of ae * b
| I_skip
| I_fail of ae
| I_patch of named_type_value * access_path * ae
and access = Ast_simplified.access
and access_path = Ast_simplified.access_path
and 'a matching =
| Match_bool of {
match_true : 'a ;
match_false : 'a ;
}
| Match_list of {
match_nil : 'a ;
match_cons : name * name * 'a ;
}
| Match_option of {
match_none : 'a ;
match_some : (name * type_value) * 'a ;
}
| Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = ae matching
open Trace
let get_entry (p:program) (entry : string) : annotated_expression result =
let aux (d:declaration) =
match d with
| Declaration_constant {name ; annotated_expression} when entry = name -> Some annotated_expression
| Declaration_constant _ -> None
in
let%bind result =
trace_option (simple_error "no entry point with given name") @@
Tezos_utils.List.find_map aux (List.map Location.unwrap p) in
ok result
let get_functional_entry (p:program) (entry : string) : (lambda * type_value) result =
let%bind entry = get_entry p entry in
match entry.expression with
| E_lambda l -> ok (l, entry.type_annotation)
| _ -> simple_fail "given entry point is not functional"

2
src/ligo/transpiler.ml
View File

@ -489,7 +489,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
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
let return e = ok (make_a_e e t) in
match t.type_value' with
| T_constant ("unit", []) ->
let%bind () = get_unit v in

73
src/ligo/typer.ml
View File

@ -6,64 +6,11 @@ open O.Combinators
module SMap = O.SMap
module Environment = struct
type ele = O.type_value
type t = {
environment: (string * ele) list ;
type_environment: (string * ele) list ;
}
let empty : t = {
(* TODO: use maps *)
environment = [] ;
type_environment = [] ;
}
let get (e:t) (s:string) : ele option =
List.assoc_opt s e.environment
let get_constructor (e:t) (s:string) : (ele * ele) option =
let rec aux = function
| [] -> None
| (_, (O.{type_value'=(O.T_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 =
List.assoc_opt s e.type_environment
let add_type (e:t) (s:string) (tv:ele) : t =
{e with type_environment = (s, tv) :: e.type_environment}
module PP = struct
open Format
open PP_helpers
let list_sep_d x = list_sep x (const " , ")
let value ppf (e:t) =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in
fprintf ppf "ValueEnv[%a]" (list_sep_d pp) e.environment
let type_ ppf e =
let pp ppf (s, e) = fprintf ppf "%s -> %a" s O.PP.type_value e in
fprintf ppf "TypeEnv[%a]" (list_sep_d pp) e.type_environment
let full ppf e =
fprintf ppf "%a\n%a" value e type_ e
end
module Combinators = struct
let env_sum_type ?(env = empty)
?(name = "a_sum_type")
(lst : (string * ele) list) =
add env name (make_t_ez_sum lst)
end
end
module Environment = O.Environment
type environment = Environment.t
module Errors = struct
let unbound_type_variable (e:environment) (n:string) () =
let title = (thunk "unbound type variable") in
@ -245,7 +192,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
ok (O.Match_tuple (lst, b'))
and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let return tv' = ok O.(type_value tv' (Some t)) in
let return tv' = ok (make_t tv' (Some t)) in
match t with
| T_function (a, b) ->
let%bind a' = evaluate_type e a in
@ -313,7 +260,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
(* Tuple *)
| E_tuple lst ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let tv_lst = List.map get_annotation lst' in
let tv_lst = List.map get_type_annotation lst' in
let%bind type_annotation = check (t_tuple tv_lst ()) in
ok O.{expression = E_tuple lst' ; type_annotation }
| E_accessor (ae, path) ->
@ -357,7 +304,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
ok (SMap.add k expr' prev)
in
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
let%bind type_annotation = check @@ t_record (SMap.map get_annotation m') () in
let%bind type_annotation = check @@ t_record (SMap.map get_type_annotation m') () in
ok O.{expression = O.E_record m' ; type_annotation }
(* Data-structure *)
| E_list lst ->
@ -372,11 +319,11 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind init = match tv_opt with
| None -> ok None
| Some ty ->
let%bind ty' = Ast_typed.Combinators.get_t_list ty in
let%bind ty' = get_t_list ty in
ok (Some ty') in
let%bind ty =
let%bind opt = bind_fold_list aux init
@@ List.map Ast_typed.get_type_annotation lst' in
@@ List.map get_type_annotation lst' in
trace_option (simple_error "empty list expression without annotation") opt in
check (t_list ty ())
in
@ -393,14 +340,14 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind key_type =
let%bind opt =
bind_fold_list aux None
@@ List.map Ast_typed.get_type_annotation
@@ List.map get_type_annotation
@@ List.map fst lst' in
trace_option (simple_error "empty map expression") opt
in
let%bind value_type =
let%bind opt =
bind_fold_list aux None
@@ List.map Ast_typed.get_type_annotation
@@ List.map get_type_annotation
@@ List.map snd lst' in
trace_option (simple_error "empty map expression") opt
in
@ -423,7 +370,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
ok O.{expression = E_lambda {binder;input_type;output_type;result;body} ; type_annotation}
| E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
let tv_lst = List.map get_annotation lst' in
let tv_lst = List.map get_type_annotation lst' in
let%bind (name', tv) = type_constant name tv_lst tv_opt in
let%bind type_annotation = check tv in
ok O.{expression = O.E_constant (name', lst') ; type_annotation}