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

Trying to merge new typer and new dev

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-10-09 00:51:29 -04:00
parent a0461d0622
commit 5de98259dc
10 changed files with 104 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
src/passes/4-typer/solver.ml
View File

@ -4,6 +4,7 @@ module Core = Typesystem.Core
module Wrap = struct
module I = Ast_simplified
module T = Ast_typed
module O = Core
type constraints = O.type_constraint list
@ -16,8 +17,8 @@ module Wrap = struct
(* let%bind state' = add_type state t in *)
(* return expr state' in *)
let rec type_expression_to_type_value : I.type_expression -> O.type_value = fun te ->
match te with
let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te ->
match te.type_value' with
| T_tuple types ->
P_constant (C_tuple, List.map type_expression_to_type_value types)
| T_sum kvmap ->
@ -42,16 +43,43 @@ module Wrap = struct
in
P_constant (csttag, List.map type_expression_to_type_value args)
let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
match te with
| T_tuple types ->
P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
| T_sum kvmap ->
P_constant (C_variant, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap)
| T_record kvmap ->
P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value_copypasted kvmap)
| T_function (arg , ret) ->
P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ arg ; ret ])
| T_variable type_name -> P_variable type_name
| T_constant (type_name , args) ->
let csttag = Core.(match type_name with
| "arrow" -> C_arrow
| "option" -> C_option
| "tuple" -> C_tuple
| "map" -> C_map
| "list" -> C_list
| "set" -> C_set
| "unit" -> C_unit
| "bool" -> C_bool
| "string" -> C_string
| _ -> failwith "unknown type constructor")
in
P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
(** TODO *)
let type_declaration : I.declaration -> constraints = fun td ->
match td with
| Declaration_type (name , te) ->
let pattern = type_expression_to_type_value te in
let pattern = type_expression_to_type_value_copypasted te in
[C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
| Declaration_constant (name, te, _) ->(
match te with
| Some (exp) ->
let pattern = type_expression_to_type_value exp in
let pattern = type_expression_to_type_value_copypasted exp in
[C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *)
| None ->
(** TODO *)
@ -62,12 +90,12 @@ module Wrap = struct
let type_name = Core.fresh_type_variable () in
[] , type_name
let variable : I.name -> I.type_expression -> (constraints * O.type_variable) = fun _name expr ->
let variable : I.name -> T.type_value -> (constraints * O.type_variable) = fun _name expr ->
let pattern = type_expression_to_type_value expr in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
let literal : I.type_expression -> (constraints * O.type_variable) = fun t ->
let literal : T.type_value -> (constraints * O.type_variable) = fun t ->
let pattern = type_expression_to_type_value t in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
@ -85,7 +113,7 @@ module Wrap = struct
*)
let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys ->
let patterns = List.map type_expression_to_type_value tys in
let patterns = List.map type_expression_to_type_value_copypasted tys in
let pattern = O.(P_constant (C_tuple , patterns)) in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
@ -129,8 +157,8 @@ module Wrap = struct
fun ~base ~key ->
let key_type = Core.fresh_type_variable () in
let element_type = Core.fresh_type_variable () in
let base' = type_expression_to_type_value base in
let key' = type_expression_to_type_value key in
let base' = type_expression_to_type_value_copypasted base in
let key' = type_expression_to_type_value_copypasted key in
let base_expected = mk_map_type key_type element_type in
let expr_type = Core.fresh_type_variable () in
O.[C_equation (base' , base_expected);
@ -140,9 +168,9 @@ module Wrap = struct
let constructor
: I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable)
= fun t_arg c_arg sum ->
let t_arg = type_expression_to_type_value t_arg in
let c_arg = type_expression_to_type_value c_arg in
let sum = type_expression_to_type_value sum in
let t_arg = type_expression_to_type_value_copypasted t_arg in
let c_arg = type_expression_to_type_value_copypasted c_arg in
let sum = type_expression_to_type_value_copypasted sum in
let whole_expr = Core.fresh_type_variable () in
[
C_equation (P_variable (whole_expr) , sum) ;
@ -150,7 +178,7 @@ module Wrap = struct
] , whole_expr
let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (I.t_record fields) in
let record_type = type_expression_to_type_value_copypasted (I.t_record fields) in
let whole_expr = Core.fresh_type_variable () in
[C_equation (P_variable whole_expr , record_type)] , whole_expr
@ -158,7 +186,7 @@ module Wrap = struct
fun ctor element_tys ->
let elttype = O.P_variable (Core.fresh_type_variable ()) in
let aux elt =
let elt' = type_expression_to_type_value elt
let elt' = type_expression_to_type_value_copypasted elt
in O.C_equation (elttype , elt') in
let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in
@ -174,10 +202,10 @@ module Wrap = struct
let k_type = O.P_variable (Core.fresh_type_variable ()) in
let v_type = O.P_variable (Core.fresh_type_variable ()) in
let aux_k (k , _v) =
let k' = type_expression_to_type_value k in
let k' = type_expression_to_type_value_copypasted k in
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value v in
let v' = type_expression_to_type_value_copypasted v in
O.C_equation (v_type , v') in
let equations_k = List.map aux_k kv_tys in
let equations_v = List.map aux_v kv_tys in
@ -189,16 +217,16 @@ module Wrap = struct
let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun f arg ->
let whole_expr = Core.fresh_type_variable () in
let f' = type_expression_to_type_value f in
let arg' = type_expression_to_type_value arg in
let f' = type_expression_to_type_value_copypasted f in
let arg' = type_expression_to_type_value_copypasted arg in
O.[
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
] , whole_expr
let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun ds ind ->
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
let ds' = type_expression_to_type_value_copypasted ds in
let ind' = type_expression_to_type_value_copypasted ind in
let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in
O.[
@ -208,8 +236,8 @@ module Wrap = struct
let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun a b ->
let a' = type_expression_to_type_value a in
let b' = type_expression_to_type_value b in
let a' = type_expression_to_type_value_copypasted a in
let b' = type_expression_to_type_value_copypasted b in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (a' , P_constant (C_unit , [])) ;
@ -218,8 +246,8 @@ module Wrap = struct
let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun expr body ->
let expr' = type_expression_to_type_value expr in
let body' = type_expression_to_type_value body in
let expr' = type_expression_to_type_value_copypasted expr in
let body' = type_expression_to_type_value_copypasted body in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (expr' , P_constant (C_bool , [])) ;
@ -229,11 +257,11 @@ module Wrap = struct
let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) =
fun rhs rhs_tv_opt result ->
let rhs' = type_expression_to_type_value rhs in
let result' = type_expression_to_type_value result in
let rhs' = type_expression_to_type_value_copypasted rhs in
let result' = type_expression_to_type_value_copypasted result in
let rhs_tv_opt' = match rhs_tv_opt with
None -> []
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value_copypasted annot)] in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (result' , P_variable whole_expr)
@ -241,8 +269,8 @@ module Wrap = struct
let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun v e ->
let v' = type_expression_to_type_value v in
let e' = type_expression_to_type_value e in
let v' = type_expression_to_type_value_copypasted v in
let e' = type_expression_to_type_value_copypasted e in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (v' , e') ;
@ -251,8 +279,8 @@ module Wrap = struct
let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) =
fun e annot ->
let e' = type_expression_to_type_value e in
let annot' = type_expression_to_type_value annot in
let e' = type_expression_to_type_value_copypasted e in
let annot' = type_expression_to_type_value_copypasted annot in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (e' , annot') ;
@ -262,7 +290,7 @@ module Wrap = struct
let matching : I.type_expression list -> (constraints * O.type_variable) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_values = (List.map type_expression_to_type_value es) in
let type_values = (List.map type_expression_to_type_value_copypasted es) in
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values
in cs, whole_expr
@ -280,12 +308,12 @@ module Wrap = struct
let unification_body = Core.fresh_type_variable () in
let arg' = match arg with
None -> []
| Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in
| Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value_copypasted arg)] in
let body' = match body with
None -> []
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value_copypasted body)]
in O.[
C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
C_equation (type_expression_to_type_value_copypasted fresh , P_variable unification_arg) ;
C_equation (P_variable whole_expr ,
P_constant (C_arrow , [P_variable unification_arg ;
P_variable unification_body]))

20
src/passes/4-typer/typer.ml
View File

@ -420,17 +420,17 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
to actually perform the recursive calls *)
(* Basic *)
| E_failwith expr -> (
let%bind (expr', state') = type_expression e state expr in
let (constraints , expr_type) = Wrap.failwith_ () in
let expr'' = e_failwith expr' in
return expr'' state' constraints expr_type
)
(* | E_failwith expr -> (
* let%bind (expr', state') = type_expression e state expr in
* let (constraints , expr_type) = Wrap.failwith_ () in
* let expr'' = e_failwith expr' in
* return expr'' state' constraints expr_type
* ) *)
| E_variable name -> (
let%bind tv' =
let%bind (tv' : Environment.element) =
trace_option (unbound_variable e name ae.location)
@@ Environment.get_opt name e in
let (constraints , expr_type) = Wrap.variable name tv'.type_expression in
let (constraints , expr_type) = Wrap.variable name tv'.type_value in
let expr' = e_variable name in
return expr' state constraints expr_type
)
@ -449,8 +449,8 @@ and type_expression : environment -> Solver.state -> I.expression -> (O.annotate
| E_literal (Literal_nat n) -> (
return_wrapped (e_nat n) state @@ Wrap.literal (t_nat ())
)
| E_literal (Literal_tez t) -> (
return_wrapped (e_tez t) state @@ Wrap.literal (t_tez ())
| E_literal (Literal_mutez t) -> (
return_wrapped (e_mutez t) state @@ Wrap.literal (t_mutez ())
)
| E_literal (Literal_address a) -> (
return_wrapped (e_address a) state @@ Wrap.literal (t_address ())

6
src/passes/6-transpiler/transpiler.ml
View File

@ -28,6 +28,11 @@ them. please report this to the developers." in
let content () = name in
error title content
let no_type_variable name =
let title () = "type variables can't be transpiled" in
let content () = name in
error title content
let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l)
let unsupported_pattern_matching kind location =
@ -102,6 +107,7 @@ open Errors
let rec transpile_type (t:AST.type_value) : type_value result =
match t.type_value' with
| T_variable name -> fail @@ no_type_variable name
| T_constant ("bool", []) -> ok (T_base Base_bool)
| T_constant ("int", []) -> ok (T_base Base_int)
| T_constant ("nat", []) -> ok (T_base Base_nat)

1
src/passes/6-transpiler/untranspiler.ml
View File

@ -203,3 +203,4 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
let m' = map_of_kv_list lst in
return (E_record m')
| T_function _ -> fail @@ bad_untranspile "function" v
| T_variable v -> return (E_variable v)

2
src/passes/operators/helpers.ml
View File

@ -113,7 +113,7 @@ module Typer = struct
List.exists (eq_2 (a , b)) [
t_int () ;
t_nat () ;
t_tez () ;
t_mutez () ;
t_string () ;
t_bytes () ;
t_address () ;

24
src/passes/operators/operators.ml
View File

@ -297,8 +297,8 @@ module Typer = struct
then ok @@ t_int () else
if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ()))
then ok @@ t_timestamp () else
if (eq_2 (a , b) (t_tez ()))
then ok @@ t_tez () else
if (eq_2 (a , b) (t_mutez ()))
then ok @@ t_mutez () else
fail (simple_error "Typing substraction, bad parameters.")
let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
@ -428,16 +428,16 @@ module Typer = struct
let unit = constant "UNIT" @@ t_unit ()
let amount = constant "AMOUNT" @@ t_tez ()
let amount = constant "AMOUNT" @@ t_mutez ()
let balance = constant "BALANCE" @@ t_tez ()
let balance = constant "BALANCE" @@ t_mutez ()
let address = constant "ADDRESS" @@ t_address ()
let now = constant "NOW" @@ t_timestamp ()
let transaction = typer_3 "CALL" @@ fun param amount contract ->
let%bind () = assert_t_tez amount in
let%bind () = assert_t_mutez amount in
let%bind contract_param = get_t_contract contract in
let%bind () = assert_type_value_eq (param , contract_param) in
ok @@ t_operation ()
@ -447,7 +447,7 @@ module Typer = struct
let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in
let%bind () = assert_eq_1 spendable (t_bool ()) in
let%bind () = assert_eq_1 delegatable (t_bool ()) in
let%bind () = assert_t_tez init_balance in
let%bind () = assert_t_mutez init_balance in
let%bind (arg , res) = get_t_function code in
let%bind (_param , storage) = get_t_pair arg in
let%bind (storage' , op_lst) = get_t_pair res in
@ -485,8 +485,8 @@ module Typer = struct
then ok @@ t_nat () else
if eq_2 (a , b) (t_int ())
then ok @@ t_int () else
if (eq_1 a (t_nat ()) && eq_1 b (t_tez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_tez ()))
then ok @@ t_tez () else
if (eq_1 a (t_nat ()) && eq_1 b (t_mutez ())) || (eq_1 b (t_nat ()) && eq_1 a (t_mutez ()))
then ok @@ t_mutez () else
simple_fail "Multiplying with wrong types"
let div = typer_2 "DIV" @@ fun a b ->
@ -494,8 +494,8 @@ module Typer = struct
then ok @@ t_nat () else
if eq_2 (a , b) (t_int ())
then ok @@ t_int () else
if eq_1 a (t_tez ()) && eq_1 b (t_nat ())
then ok @@ t_tez () else
if eq_1 a (t_mutez ()) && eq_1 b (t_nat ())
then ok @@ t_mutez () else
simple_fail "Dividing with wrong types"
let mod_ = typer_2 "MOD" @@ fun a b ->
@ -508,8 +508,8 @@ module Typer = struct
then ok @@ t_nat () else
if eq_2 (a , b) (t_int ())
then ok @@ t_int () else
if eq_2 (a , b) (t_tez ())
then ok @@ t_tez () else
if eq_2 (a , b) (t_mutez ())
then ok @@ t_mutez () else
if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
then ok @@ t_int () else
if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ()))

1
src/stages/ast_typed/PP.ml
View File

@ -14,6 +14,7 @@ let rec type_value' ppf (tv':type_value') : unit =
| 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
| T_variable name -> fprintf ppf "%s" name
and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value'

11
src/stages/ast_typed/combinators.ml
View File

@ -21,11 +21,12 @@ let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s
let t_mutez ?s () : type_value = make_t (T_constant ("tez", [])) s
let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) 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_variable t ?s () : type_value = make_t (T_variable t) s
let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s
let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
@ -82,7 +83,7 @@ let get_t_unit (t:type_value) : unit result = match t.type_value' with
| T_constant ("unit", []) -> ok ()
| _ -> simple_fail "not a unit"
let get_t_tez (t:type_value) : unit result = match t.type_value' with
let get_t_mutez (t:type_value) : unit result = match t.type_value' with
| T_constant ("tez", []) -> ok ()
| _ -> simple_fail "not a tez"
@ -179,7 +180,7 @@ let assert_t_map = fun t ->
let is_t_map = Function.compose to_bool get_t_map
let is_t_big_map = Function.compose to_bool get_t_big_map
let assert_t_tez : type_value -> unit result = get_t_tez
let assert_t_mutez : type_value -> unit result = get_t_mutez
let assert_t_key = get_t_key
let assert_t_signature = get_t_signature
let assert_t_key_hash = get_t_key_hash
@ -235,6 +236,8 @@ let e_nat n : expression = E_literal (Literal_nat n)
let e_mutez n : expression = E_literal (Literal_mutez n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_bytes s : expression = E_literal (Literal_bytes s)
let e_timestamp s : expression = E_literal (Literal_timestamp s)
let e_address s : expression = E_literal (Literal_address s)
let e_operation s : expression = E_literal (Literal_operation s)
let e_lambda l : expression = E_lambda l
@ -247,7 +250,7 @@ let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
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_mutez n = make_a_e (e_mutez n) (t_tez ())
let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ())
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_address s = make_a_e (e_address s) (t_address ())

2
src/stages/ast_typed/misc.ml
View File

@ -346,6 +346,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
let%bind _ = assert_type_value_eq (result, result') in
ok ()
| T_function _, _ -> fail @@ different_kinds a b
| T_variable x, T_variable y -> let _ = x == y in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding"
| T_variable _, _ -> 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

1
src/stages/ast_typed/types.ml
View File

@ -56,6 +56,7 @@ and type_value' =
| T_sum of tv_map
| T_record of tv_map
| T_constant of type_name * tv list
| T_variable of type_name
| T_function of (tv * tv)
and type_value = {