Merge branch 'feature/default-environment' into 'dev'

Default environment with just "bool"

See merge request ligolang/ligo!586
This commit is contained in:
Pierre-Emmanuel Wulfman 2020-04-29 18:40:12 +00:00
commit 31858a7a24
44 changed files with 223 additions and 199 deletions

View File

@ -1425,7 +1425,7 @@ let%expect_test _ =
let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ;
[%expect {|
ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]] ]"}
ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]]\n- E[]\tT[bool -> sum[false -> unit , true -> unit]]]"}
If you're not sure how to fix this error, you can
@ -1465,7 +1465,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ;
[%expect {|
ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] ]","did_you_mean":"no suggestion"}
ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"no suggestion"}
If you're not sure how to fix this error, you can

View File

@ -93,7 +93,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * bool )","b":"( int * string )"}
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * sum[false -> unit , true -> unit] )","b":"( int * string )"}
If you're not sure how to fix this error, you can
@ -106,7 +106,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_4.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records: {"key_a":"c","key_b":"b","a":"record[a -> int , c -> bool , d -> string]","b":"record[a -> int , b -> string , c -> bool]"}
ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records: {"key_a":"c","key_b":"b","a":"record[a -> int , c -> sum[false -> unit , true -> unit] , d -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"}
If you're not sure how to fix this error, you can
@ -119,7 +119,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] ]","did_you_mean":"bool"}
ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"bool"}
If you're not sure how to fix this error, you can
@ -132,7 +132,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_6.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different type constructors: Expected these two constant type constructors to be the same, but they're different {"a":"string","b":"bool"}
ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different kinds: {"a":"string","b":"sum[false -> unit , true -> unit]"}
If you're not sure how to fix this error, you can
@ -145,7 +145,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_7.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> bool]"}
ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"}
If you're not sure how to fix this error, you can

4
src/environment/bool.ml Normal file
View File

@ -0,0 +1,4 @@
open Ast_typed
open Stage_common.Constant
let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})]

14
src/environment/dune Normal file
View File

@ -0,0 +1,14 @@
(library
(name environment)
(public_name ligo.environment)
(libraries
simple-utils
tezos-utils
ast_typed
stage_common
)
(preprocess
(pps ppx_let bisect_ppx --conditional)
)
(flags (:standard -open Simple_utils))
)

View File

@ -0,0 +1,11 @@
open Ast_typed
let merge e1 e2 =
let e1 = List.Ne.to_list e1 in
let e2 = List.Ne.to_list e2 in
List.Ne.of_list @@ e1 @ e2
let default = Environment.full_empty
let default = merge default Bool.environment

View File

@ -255,7 +255,6 @@ C_STEPS_TO_QUOTA
(*interpreter*)
and eval_literal : Ast_typed.literal -> value result = function
| Literal_unit -> ok @@ V_Ct (C_unit)
| Literal_bool b -> ok @@ V_Ct (C_bool b)
| Literal_int i -> ok @@ V_Ct (C_int i)
| Literal_nat n -> ok @@ V_Ct (C_nat n)
| Literal_timestamp i -> ok @@ V_Ct (C_timestamp i)
@ -329,6 +328,8 @@ and eval : Ast_typed.expression -> env -> value result
arguments in
apply_operator cons_name operands'
)
| E_constructor { constructor = Constructor c ; element } when (String.equal c "true" || String.equal c "false")
&& element.expression_content = Ast_typed.e_unit () -> ok @@ V_Ct (C_bool (bool_of_string c))
| E_constructor { constructor = Constructor c ; element } ->
let%bind v' = eval element env in
ok @@ V_Construct (c,v')

View File

@ -76,7 +76,7 @@ them. please report this to the developers." in
error ~data title content
let wrong_mini_c_value expected_type actual =
let title () = "illed typed intermediary value" in
let title () = "transpiler: illed typed intermediary value" in
let content () = "type of intermediary value doesn't match what was expected" in
let data = [
("expected_type" , fun () -> expected_type) ;
@ -231,22 +231,23 @@ let transpile_constant' : AST.constant' -> constant' = function
let rec transpile_type (t:AST.type_expression) : type_value result =
match t.type_content with
| T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> ok (T_base TB_bool)
| t when (compare t (t_bool ()).type_content) = 0-> ok (T_base TB_bool)
| T_variable (name) -> fail @@ no_type_variable @@ name
| T_constant (TC_bool) -> ok (T_base TC_bool)
| T_constant (TC_int) -> ok (T_base TC_int)
| T_constant (TC_nat) -> ok (T_base TC_nat)
| T_constant (TC_mutez) -> ok (T_base TC_mutez)
| T_constant (TC_string) -> ok (T_base TC_string)
| T_constant (TC_bytes) -> ok (T_base TC_bytes)
| T_constant (TC_address) -> ok (T_base TC_address)
| T_constant (TC_timestamp) -> ok (T_base TC_timestamp)
| T_constant (TC_unit) -> ok (T_base TC_unit)
| T_constant (TC_operation) -> ok (T_base TC_operation)
| T_constant (TC_signature) -> ok (T_base TC_signature)
| T_constant (TC_key) -> ok (T_base TC_key)
| T_constant (TC_key_hash) -> ok (T_base TC_key_hash)
| T_constant (TC_chain_id) -> ok (T_base TC_chain_id)
| T_constant (TC_void) -> ok (T_base TC_void)
| T_constant (TC_int) -> ok (T_base TB_int)
| T_constant (TC_nat) -> ok (T_base TB_nat)
| T_constant (TC_mutez) -> ok (T_base TB_mutez)
| T_constant (TC_string) -> ok (T_base TB_string)
| T_constant (TC_bytes) -> ok (T_base TB_bytes)
| T_constant (TC_address) -> ok (T_base TB_address)
| T_constant (TC_timestamp) -> ok (T_base TB_timestamp)
| T_constant (TC_unit) -> ok (T_base TB_unit)
| T_constant (TC_operation) -> ok (T_base TB_operation)
| T_constant (TC_signature) -> ok (T_base TB_signature)
| T_constant (TC_key) -> ok (T_base TB_key)
| T_constant (TC_key_hash) -> ok (T_base TB_key_hash)
| T_constant (TC_chain_id) -> ok (T_base TB_chain_id)
| T_constant (TC_void) -> ok (T_base TB_void)
| T_operator (TC_contract x) ->
let%bind x' = transpile_type x in
ok (T_contract x')
@ -362,7 +363,6 @@ let record_access_to_lr : type_value -> type_value AST.label_map -> AST.label ->
ok lst
let rec transpile_literal : AST.literal -> value = fun l -> match l with
| Literal_bool b -> D_bool b
| Literal_int n -> D_int n
| Literal_nat n -> D_nat n
| Literal_timestamp n -> D_timestamp n
@ -411,6 +411,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
let%bind a = transpile_annotated_expression lamb in
let%bind b = transpile_annotated_expression args in
return @@ E_application (a, b)
| E_constructor {constructor=Constructor name;element} when (String.equal name "true"|| String.equal name "false") && element.expression_content = AST.e_unit () ->
return @@ E_literal (D_bool (bool_of_string name))
| E_constructor {constructor;element} -> (
let%bind param' = transpile_annotated_expression element in
let (param'_expr , param'_tv) = Combinators.Expression.(get_content param' , get_type param') in

View File

@ -19,7 +19,7 @@ them. please report this to the developers." in
error ~data title content
let wrong_mini_c_value expected_type actual =
let title () = "illed typed intermediary value" in
let title () = "untranspiler: illed typed intermediary value" in
let content () = "type of intermediary value doesn't match what was expected" in
let data = [
("expected_type" , fun () -> expected_type) ;
@ -44,6 +44,18 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
let open! AST in
let return e = ok (make_a_e_empty e t) in
match t.type_content with
| T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> (
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (e_bool b Environment.full_empty)
)
| t when (compare t (t_bool ()).type_content) = 0-> (
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (e_bool b Environment.full_empty)
)
| T_constant type_constant -> (
match type_constant with
| TC_unit -> (
@ -52,12 +64,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
get_unit v in
return (E_literal Literal_unit)
)
| TC_bool -> (
let%bind b =
trace_strong (wrong_mini_c_value "bool" v) @@
get_bool v in
return (E_literal (Literal_bool b))
)
| TC_int -> (
let%bind n =
trace_strong (wrong_mini_c_value "int" v) @@

View File

@ -117,7 +117,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
(* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons:
intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *)
let subst_binder2 y z expr' =
let dummy = T_base TC_unit in
let dummy = T_base TB_unit in
let hack = { content = E_closure { binder = z ; body = expr' } ;
type_value = dummy } in
match subst_binder y hack with
@ -199,7 +199,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
)
let%expect_test _ =
let dummy_type = T_base TC_unit in
let dummy_type = T_base TB_unit in
let wrap e = { content = e ; type_value = dummy_type } in
let show_subst ~body ~x ~expr =

View File

@ -59,24 +59,24 @@ module Ty = struct
let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) ()
let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) ()
let comparable_type_base : type_constant -> ex_comparable_ty result = fun tb ->
let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
let return x = ok @@ Ex_comparable_ty x in
match tb with
| TC_unit -> fail (not_comparable "unit")
| TC_void -> fail (not_comparable "void")
| TC_bool -> return bool_k
| TC_nat -> return nat_k
| TC_mutez -> return tez_k
| TC_int -> return int_k
| TC_string -> return string_k
| TC_address -> return address_k
| TC_timestamp -> return timestamp_k
| TC_bytes -> return bytes_k
| TC_operation -> fail (not_comparable "operation")
| TC_signature -> fail (not_comparable "signature")
| TC_key -> fail (not_comparable "key")
| TC_key_hash -> return key_hash_k
| TC_chain_id -> fail (not_comparable "chain_id")
| TB_unit -> fail (not_comparable "unit")
| TB_void -> fail (not_comparable "void")
| TB_bool -> return bool_k
| TB_nat -> return nat_k
| TB_mutez -> return tez_k
| TB_int -> return int_k
| TB_string -> return string_k
| TB_address -> return address_k
| TB_timestamp -> return timestamp_k
| TB_bytes -> return bytes_k
| TB_operation -> fail (not_comparable "operation")
| TB_signature -> fail (not_comparable "signature")
| TB_key -> fail (not_comparable "key")
| TB_key_hash -> return key_hash_k
| TB_chain_id -> fail (not_comparable "chain_id")
let comparable_leaf : type a. (a, _) comparable_struct -> (a , leaf) comparable_struct result =
fun a ->
@ -109,24 +109,24 @@ module Ty = struct
| T_option _ -> fail (not_comparable "option")
| T_contract _ -> fail (not_comparable "contract")
let base_type : type_constant -> ex_ty result = fun b ->
let base_type : type_base -> ex_ty result = fun b ->
let return x = ok @@ Ex_ty x in
match b with
| TC_unit -> return unit
| TC_void -> fail (not_compilable_type "void")
| TC_bool -> return bool
| TC_int -> return int
| TC_nat -> return nat
| TC_mutez -> return tez
| TC_string -> return string
| TC_address -> return address
| TC_timestamp -> return timestamp
| TC_bytes -> return bytes
| TC_operation -> return operation
| TC_signature -> return signature
| TC_key -> return key
| TC_key_hash -> return key_hash
| TC_chain_id -> return chain_id
| TB_unit -> return unit
| TB_void -> fail (not_compilable_type "void")
| TB_bool -> return bool
| TB_int -> return int
| TB_nat -> return nat
| TB_mutez -> return tez
| TB_string -> return string
| TB_address -> return address
| TB_timestamp -> return timestamp
| TB_bytes -> return bytes
| TB_operation -> return operation
| TB_signature -> return signature
| TB_key -> return key
| TB_key_hash -> return key_hash
| TB_chain_id -> return chain_id
let rec type_ : type_value -> ex_ty result =
function
@ -195,23 +195,23 @@ module Ty = struct
end
let base_type : type_constant -> O.michelson result =
let base_type : type_base -> O.michelson result =
function
| TC_unit -> ok @@ O.prim T_unit
| TC_void -> fail (Ty.not_compilable_type "void")
| TC_bool -> ok @@ O.prim T_bool
| TC_int -> ok @@ O.prim T_int
| TC_nat -> ok @@ O.prim T_nat
| TC_mutez -> ok @@ O.prim T_mutez
| TC_string -> ok @@ O.prim T_string
| TC_address -> ok @@ O.prim T_address
| TC_timestamp -> ok @@ O.prim T_timestamp
| TC_bytes -> ok @@ O.prim T_bytes
| TC_operation -> ok @@ O.prim T_operation
| TC_signature -> ok @@ O.prim T_signature
| TC_key -> ok @@ O.prim T_key
| TC_key_hash -> ok @@ O.prim T_key_hash
| TC_chain_id -> ok @@ O.prim T_chain_id
| TB_unit -> ok @@ O.prim T_unit
| TB_void -> fail (Ty.not_compilable_type "void")
| TB_bool -> ok @@ O.prim T_bool
| TB_int -> ok @@ O.prim T_int
| TB_nat -> ok @@ O.prim T_nat
| TB_mutez -> ok @@ O.prim T_mutez
| TB_string -> ok @@ O.prim T_string
| TB_address -> ok @@ O.prim T_address
| TB_timestamp -> ok @@ O.prim T_timestamp
| TB_bytes -> ok @@ O.prim T_bytes
| TB_operation -> ok @@ O.prim T_operation
| TB_signature -> ok @@ O.prim T_signature
| TB_key -> ok @@ O.prim T_key
| TB_key_hash -> ok @@ O.prim T_key_hash
| TB_chain_id -> ok @@ O.prim T_chain_id
let rec type_ : type_value -> O.michelson result =
function

View File

@ -768,11 +768,11 @@ and compile_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
match t with
| BoolExpr (False reg) -> (
let loc = Location.lift reg in
return @@ e_literal ~loc (Literal_bool false)
return @@ e_bool ~loc false
)
| BoolExpr (True reg) -> (
let loc = Location.lift reg in
return @@ e_literal ~loc (Literal_bool true)
return @@ e_bool ~loc true
)
| BoolExpr (Or b) ->
compile_binop "OR" b

View File

@ -487,11 +487,11 @@ and compile_logic_expression (t:Raw.logic_expr) : expression result =
match t with
| BoolExpr (False reg) -> (
let loc = Location.lift reg in
return @@ e_literal ~loc (Literal_bool false)
return @@ e_bool ~loc false
)
| BoolExpr (True reg) -> (
let loc = Location.lift reg in
return @@ e_literal ~loc (Literal_bool true)
return @@ e_bool ~loc true
)
| BoolExpr (Or b) ->
compile_binop "OR" b

View File

@ -14,7 +14,6 @@ let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
| Solver.Core.C_list -> "list"
| Solver.Core.C_set -> "set"
| Solver.Core.C_unit -> "unit"
| Solver.Core.C_bool -> "bool"
| Solver.Core.C_string -> "string"
| Solver.Core.C_nat -> "nat"
| Solver.Core.C_mutez -> "mutez"

View File

@ -8,6 +8,7 @@
ast_typed
operators
UnionFind
environment
)
(preprocess
(pps ppx_let)

View File

@ -387,93 +387,89 @@ let compare_simple_c_constant = function
| C_arrow -> (function
(* N/A -> 1 *)
| C_arrow -> 0
| C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_option -> (function
| C_arrow -> 1
| C_option -> 0
| C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_record -> (function
| C_arrow | C_option -> 1
| C_record -> 0
| C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_variant -> (function
| C_arrow | C_option | C_record -> 1
| C_variant -> 0
| C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_map -> (function
| C_arrow | C_option | C_record | C_variant -> 1
| C_map -> 0
| C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_big_map -> (function
| C_arrow | C_option | C_record | C_variant | C_map -> 1
| C_big_map -> 0
| C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_list -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map -> 1
| C_list -> 0
| C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_set -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1
| C_set -> 0
| C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_unit -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
| C_unit -> 0
| C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bool -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
| C_bool -> 0
| C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_string -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
| C_string -> 0
| C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_nat -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string -> 1
| C_nat -> 0
| C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_mutez -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat -> 1
| C_mutez -> 0
| C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_timestamp -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez -> 1
| C_timestamp -> 0
| C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_int -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp -> 1
| C_int -> 0
| C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_address -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
| C_address -> 0
| C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bytes -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
| C_bytes -> 0
| C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key_hash -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
| C_key_hash -> 0
| C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
| C_key -> 0
| C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_signature -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
| C_signature -> 0
| C_operation | C_contract | C_chain_id -> -1)
| C_operation -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
| C_operation -> 0
| C_contract | C_chain_id -> -1)
| C_contract -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
| C_contract -> 0
| C_chain_id -> -1)
| C_chain_id -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
| C_chain_id -> 0
(* N/A -> -1 *)
)
@ -492,7 +488,6 @@ let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag ->
| Core.C_list -> "list"
| Core.C_set -> "set"
| Core.C_unit -> "unit"
| Core.C_bool -> "bool"
| Core.C_string -> "string"
| Core.C_nat -> "nat"
| Core.C_mutez -> "mutez"

View File

@ -10,7 +10,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function
| TC_nat -> TC_nat
| TC_int -> TC_int
| TC_mutez -> TC_mutez
| TC_bool -> TC_bool
| TC_operation -> TC_operation
| TC_address -> TC_address
| TC_key -> TC_key

View File

@ -2,6 +2,7 @@ open Trace
module I = Ast_core
module O = Ast_typed
open O.Combinators
module DEnv = Environment
module Environment = O.Environment
module Solver = Solver
type environment = Environment.t
@ -233,9 +234,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
return expr' state constraints expr_type
)
| E_literal (Literal_bool b) -> (
return_wrapped (e_bool b) state @@ Wrap.literal (t_bool ())
)
| E_literal (Literal_string s) -> (
return_wrapped (e_string s) state @@ Wrap.literal (t_string ())
)
@ -481,7 +479,7 @@ let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply
ok (program, state)
let type_program (p : I.program) : (O.program * Solver.state) result =
let empty_env = Ast_typed.Environment.full_empty in
let empty_env = DEnv.default in
let empty_state = Solver.initial_state in
type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state

View File

@ -13,7 +13,6 @@ let unconvert_type_constant : O.type_constant -> I.type_constant = function
| TC_nat -> TC_nat
| TC_int -> TC_int
| TC_mutez -> TC_mutez
| TC_bool -> TC_bool
| TC_operation -> TC_operation
| TC_address -> TC_address
| TC_key -> TC_key
@ -219,7 +218,6 @@ let untype_literal (l:O.literal) : I.literal result =
match l with
| Literal_unit -> ok Literal_unit
| Literal_void -> ok Literal_void
| Literal_bool b -> ok (Literal_bool b)
| Literal_nat n -> ok (Literal_nat n)
| Literal_timestamp n -> ok (Literal_timestamp n)
| Literal_mutez n -> ok (Literal_mutez n)

View File

@ -47,7 +47,6 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
| T_constant (type_name) ->
let csttag = Core.(match type_name with
| TC_unit -> C_unit
| TC_bool -> C_bool
| TC_string -> C_string
| TC_nat -> C_nat
| TC_mutez -> C_mutez
@ -94,7 +93,6 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
| T_constant (type_name) ->
let csttag = Core.(match type_name with
| TC_unit -> C_unit
| TC_bool -> C_bool
| TC_string -> C_string
| _ -> failwith "unknown type constructor")
in
@ -278,7 +276,7 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
let body' = type_expression_to_type_value body in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (expr' , P_constant (C_bool , [])) ;
C_equation (expr' , P_variable (Stage_common.Constant.t_bool)) ;
C_equation (body' , P_constant (C_unit , [])) ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr

View File

@ -8,6 +8,7 @@
ast_typed
typer_new
operators
environment
)
(preprocess
(pps ppx_let)

View File

@ -4,6 +4,7 @@ module I = Ast_core
module O = Ast_typed
open O.Combinators
module DEnv = Environment
module Environment = O.Environment
module Solver = Typer_new.Solver
@ -226,7 +227,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function
| TC_nat -> TC_nat
| TC_int -> TC_int
| TC_mutez -> TC_mutez
| TC_bool -> TC_bool
| TC_operation -> TC_operation
| TC_address -> TC_address
| TC_key -> TC_key
@ -477,7 +477,7 @@ let rec type_program (p:I.program) : (O.program * Solver.state) result =
in
let%bind (_, lst) =
trace (fun () -> program_error p ()) @@
bind_fold_list aux (Environment.full_empty, []) p in
bind_fold_list aux (DEnv.default, []) p in
ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ()))
and type_declaration env (_placeholder_for_state_of_new_typer : Solver.state) : I.declaration -> (environment * Solver.state * O.declaration option) result = function
@ -689,8 +689,6 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
trace_option (unbound_variable e name ae.location)
@@ Environment.get_opt name e in
return (E_variable name) tv'.type_value
| E_literal (Literal_bool b) ->
return (E_literal (Literal_bool b)) (t_bool ())
| E_literal Literal_unit ->
return (E_literal (Literal_unit)) (t_unit ())
| E_literal Literal_void -> return (E_literal (Literal_void)) (t_unit ()) (* TODO : IS this really a t_unit ?*)
@ -1015,7 +1013,6 @@ let untype_literal (l:O.literal) : I.literal result =
match l with
| Literal_unit -> ok Literal_unit
| Literal_void -> ok Literal_void
| Literal_bool b -> ok (Literal_bool b)
| Literal_nat n -> ok (Literal_nat n)
| Literal_timestamp n -> ok (Literal_timestamp n)
| Literal_mutez n -> ok (Literal_mutez n)

View File

@ -43,7 +43,6 @@ module Concrete_to_imperative = struct
| "nat" -> Some TC_nat
| "int" -> Some TC_int
| "tez" -> Some TC_mutez
| "bool" -> Some TC_bool
| "operation" -> Some TC_operation
| "address" -> Some TC_address
| "key" -> Some TC_key

View File

@ -21,7 +21,7 @@ open Errors
let make_t ?(loc = Location.generated) type_content = {type_content; location=loc}
let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool)
let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string)
let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes)
let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int)
@ -88,7 +88,6 @@ let e_nat_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
let e_nat ?loc n : expression = e_nat_z ?loc @@ Z.of_int n
let e_timestamp_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
let e_timestamp ?loc n : expression = e_timestamp_z ?loc @@ Z.of_int n
let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b)
let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
let e_mutez_z ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@ -148,6 +147,8 @@ let e_while ?loc condition body = make_e ?loc @@ E_while {condition; body}
let e_for ?loc binder start final increment body = make_e ?loc @@ E_for {binder;start;final;increment;body}
let e_for_each ?loc binder collection collection_type body = make_e ?loc @@ E_for_each {binder;collection;collection_type;body}
let e_bool ?loc b : expression = e_constructor ?loc (string_of_bool b) (e_unit ())
let ez_match_variant (lst : ((string * string) * 'a) list) =
let lst = List.map (fun ((c,n),a) -> ((Constructor c, Var.of_name n), a) ) lst in
Match_variant (lst,())

View File

@ -34,9 +34,6 @@ open Errors
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 _ -> fail @@ different_literals "different bools" a b
| Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

View File

@ -27,7 +27,7 @@ let tuple_to_record lst =
let (_, lst ) = List.fold_left aux (0,[]) lst in
lst
let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool)
let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string)
let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes)
let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int)
@ -90,7 +90,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit)
let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n)
let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b)
let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@ -142,6 +141,8 @@ let e_map ?loc lst : expression = make_e ?loc @@ E_map lst
let e_big_map ?loc lst : expression = make_e ?loc @@ E_big_map lst
let e_look_up ?loc a b : expression = make_e ?loc @@ E_look_up (a,b)
let e_bool ?loc b : expression = e_constructor ?loc (Constructor (string_of_bool b)) (e_unit ())
let make_option_typed ?loc e t_opt =
match t_opt with
| None -> e

View File

@ -34,9 +34,6 @@ open Errors
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 _ -> fail @@ different_literals "different bools" a b
| Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

View File

@ -27,7 +27,7 @@ let tuple_to_record lst =
let (_, lst ) = List.fold_left aux (0,[]) lst in
lst
let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool)
let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string)
let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes)
let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int)
@ -87,7 +87,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit)
let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n)
let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b)
let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
@ -126,6 +125,8 @@ let e_record_update ?loc record path update = make_e ?loc @@ E_record_update {re
let e_annotation ?loc anno_expr ty = make_e ?loc @@ E_ascription {anno_expr; type_annotation = ty}
let e_bool ?loc b : expression = e_constructor ?loc (string_of_bool b) (e_unit ())
let make_option_typed ?loc e t_opt =
match t_opt with
| None -> e

View File

@ -34,9 +34,6 @@ open Errors
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 _ -> fail @@ different_literals "different bools" a b
| Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

View File

@ -180,7 +180,6 @@ let literal ppf (l : literal) =
match l with
| Literal_unit -> fprintf ppf "unit"
| Literal_void -> fprintf ppf "void"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int z -> fprintf ppf "%a" Z.pp_print z
| Literal_nat z -> fprintf ppf "+%a" Z.pp_print z
| Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z
@ -205,7 +204,6 @@ let s =
| TC_nat -> "nat"
| TC_int -> "int"
| TC_mutez -> "mutez"
| TC_bool -> "bool"
| TC_operation -> "operation"
| TC_address -> "address"
| TC_key -> "key"

View File

@ -34,7 +34,6 @@ let make_n_t type_name type_value = { type_name ; type_value }
let t_signature ?loc ?s () : type_expression = make_t ?loc (T_constant TC_signature) s
let t_chain_id ?loc ?s () : type_expression = make_t ?loc (T_constant TC_chain_id) s
let t_bool ?loc ?s () : type_expression = make_t ?loc (T_constant TC_bool) s
let t_string ?loc ?s () : type_expression = make_t ?loc (T_constant TC_string) s
let t_bytes ?loc ?s () : type_expression = make_t ?loc (T_constant TC_bytes) s
let t_key ?loc ?s () : type_expression = make_t ?loc (T_constant TC_key) s
@ -67,10 +66,13 @@ let t_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_big_map { k ; v })) s
let t_map_or_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map_or_big_map { k ; v })) s
let t_sum m ?loc ?s () : type_expression = make_t ?loc (T_sum m) s
let make_t_ez_sum ?loc (lst:(constructor' * ctor_content) list) : type_expression =
let make_t_ez_sum ?loc ?s (lst:(constructor' * ctor_content) list) : type_expression =
let aux prev (k, v) = CMap.add k v prev in
let map = List.fold_left aux CMap.empty lst in
make_t ?loc (T_sum map) None
make_t ?loc (T_sum map) s
let t_bool ?loc ?s () : type_expression = make_t_ez_sum ?loc ?s
[(Constructor "true", {ctor_type=t_unit ();michelson_annotation=None});(Constructor "false", {ctor_type=t_unit ();michelson_annotation=None})]
let t_function param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
let t_shallow_closure param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
@ -90,7 +92,8 @@ let get_lambda_with_type e =
| _ -> simple_fail "not a lambda with functional type"
let get_t_bool (t:type_expression) : unit result = match t.type_content with
| T_constant (TC_bool) -> ok ()
| T_variable v when Var.equal v Stage_common.Constant.t_bool -> ok ()
| t when (compare t (t_bool ()).type_content) = 0-> ok ()
| _ -> fail @@ Errors.not_a_x_type "bool" t ()
let get_t_int (t:type_expression) : unit result = match t.type_content with
@ -286,7 +289,6 @@ let e_unit () : expression_content = E_literal (Literal_unit)
let e_int n : expression_content = E_literal (Literal_int n)
let e_nat n : expression_content = E_literal (Literal_nat n)
let e_mutez n : expression_content = E_literal (Literal_mutez n)
let e_bool b : expression_content = E_literal (Literal_bool b)
let e_string s : expression_content = E_literal (Literal_string s)
let e_bytes s : expression_content = E_literal (Literal_bytes s)
let e_timestamp s : expression_content = E_literal (Literal_timestamp s)
@ -302,11 +304,15 @@ let e_application lamb args : expression_content = E_application {lamb;args}
let e_variable v : expression_content = E_variable v
let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; let_result; inline }
let e_constructor constructor element: expression_content = E_constructor {constructor;element}
let e_bool b env : expression_content = e_constructor (Constructor (string_of_bool b)) (make_e (e_unit ())(t_unit()) env)
let e_a_unit = make_e (e_unit ()) (t_unit ())
let e_a_int n = make_e (e_int n) (t_int ())
let e_a_nat n = make_e (e_nat n) (t_nat ())
let e_a_mutez n = make_e (e_mutez n) (t_mutez ())
let e_a_bool b = make_e (e_bool b) (t_bool ())
let e_a_bool b = fun env -> make_e (e_bool b env) (t_bool ()) env
let e_a_string s = make_e (e_string s) (t_string ())
let e_a_address s = make_e (e_address s) (t_address ())
let e_a_pair a b = make_e (e_pair a b)
@ -326,6 +332,7 @@ let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y)
let e_a_let_in binder expr body attributes = make_e (e_let_in binder expr body attributes) (get_type_expression body)
let get_a_int (t:expression) =
match t.expression_content with
| E_literal (Literal_int n) -> ok n
@ -338,7 +345,7 @@ let get_a_unit (t:expression) =
let get_a_bool (t:expression) =
match t.expression_content with
| E_literal (Literal_bool b) -> ok b
| E_constructor {constructor=Constructor name;element} when (String.equal name "true" || String.equal name "false") && element.expression_content = e_unit () -> ok (bool_of_string name)
| _ -> simple_fail "not a bool"

View File

@ -33,7 +33,7 @@ val t_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_e
val t_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression
val t_map_or_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression
val t_sum : Types.te_cmap -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
val make_t_ez_sum : ?loc:Location.t -> ( constructor' * ctor_content ) list -> type_expression
val make_t_ez_sum : ?loc:Location.t -> ?s:S.type_expression -> ( constructor' * ctor_content ) list -> type_expression
val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
val get_type_expression : expression -> type_expression
@ -114,7 +114,7 @@ val e_unit : unit -> expression_content
val e_int : Z.t -> expression_content
val e_nat : Z.t -> expression_content
val e_mutez : Z.t -> expression_content
val e_bool : bool -> expression_content
val e_bool : bool -> full_environment -> expression_content
val e_string : string -> expression_content
val e_bytes : bytes -> expression_content
val e_timestamp : Z.t -> expression_content

View File

@ -47,7 +47,6 @@ let type_expression'_of_string = function
| "TC_nat" , [] -> ok @@ T_constant(TC_nat)
| "TC_int" , [] -> ok @@ T_constant(TC_int)
| "TC_mutez" , [] -> ok @@ T_constant(TC_mutez)
| "TC_bool" , [] -> ok @@ T_constant(TC_bool)
| "TC_operation" , [] -> ok @@ T_constant(TC_operation)
| "TC_address" , [] -> ok @@ T_constant(TC_address)
| "TC_key" , [] -> ok @@ T_constant(TC_key)
@ -77,7 +76,6 @@ let string_of_type_constant = function
| TC_nat -> "TC_nat", []
| TC_int -> "TC_int", []
| TC_mutez -> "TC_mutez", []
| TC_bool -> "TC_bool", []
| TC_operation -> "TC_operation", []
| TC_address -> "TC_address", []
| TC_key -> "TC_key", []

View File

@ -407,9 +407,6 @@ let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_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 _ -> fail @@ different_literals "booleans" a b
| Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b

View File

@ -9,7 +9,6 @@ type type_constant =
| TC_nat
| TC_int
| TC_mutez
| TC_bool
| TC_operation
| TC_address
| TC_key
@ -77,7 +76,6 @@ and type_expression = {
type literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of z
| Literal_nat of z
| Literal_timestamp of z

View File

@ -29,23 +29,23 @@ and environment_element ppf ((n, tv) : environment_element) =
and environment ppf (x:environment) =
fprintf ppf "Env[%a]" (list_sep_d environment_element) x
and type_constant ppf (tc:type_constant) : unit =
let s = match tc with
| TC_unit -> "unit"
| TC_string -> "string"
| TC_bytes -> "bytes"
| TC_nat -> "nat"
| TC_int -> "int"
| TC_mutez -> "mutez"
| TC_bool -> "bool"
| TC_operation -> "operation"
| TC_address -> "address"
| TC_key -> "key"
| TC_key_hash -> "key_hash"
| TC_signature -> "signature"
| TC_timestamp -> "timestamp"
| TC_chain_id -> "chain_id"
| TC_void -> "void"
and type_constant ppf (tb:type_base) : unit =
let s = match tb with
| TB_unit -> "unit"
| TB_string -> "string"
| TB_bytes -> "bytes"
| TB_nat -> "nat"
| TB_int -> "int"
| TB_mutez -> "mutez"
| TB_bool -> "bool"
| TB_operation -> "operation"
| TB_address -> "address"
| TB_key -> "key"
| TB_key_hash -> "key_hash"
| TB_signature -> "signature"
| TB_timestamp -> "timestamp"
| TB_chain_id -> "chain_id"
| TB_void -> "void"
in
fprintf ppf "(TC %s)" s
@ -255,7 +255,7 @@ let%expect_test _ =
let%expect_test _ =
let pp = expression' Format.std_formatter in
let dummy_type = T_base TC_unit in
let dummy_type = T_base TB_unit in
let wrap e = { content = e ; type_value = dummy_type } in
pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ;
[%expect{|

View File

@ -152,7 +152,7 @@ let get_t_contract t = match t with
| _ -> fail @@ wrong_type "contract" t
let get_t_operation t = match t with
| T_base TC_operation -> ok t
| T_base TB_operation -> ok t
| _ -> fail @@ wrong_type "operation" t
let get_operation (v:value) = match v with
@ -160,9 +160,9 @@ let get_operation (v:value) = match v with
| _ -> simple_fail "not an operation"
let t_int : type_value = T_base TC_int
let t_unit : type_value = T_base TC_unit
let t_nat : type_value = T_base TC_nat
let t_int : type_value = T_base TB_int
let t_unit : type_value = T_base TB_unit
let t_nat : type_value = T_base TB_nat
let t_function x y : type_value = T_function ( x , y )
let t_pair x y : type_value = T_pair ( x , y )

View File

@ -1,4 +1,3 @@
include Stage_common.Types
type 'a annotated = string option * 'a
@ -7,7 +6,7 @@ type type_value =
| T_pair of (type_value annotated * type_value annotated)
| T_or of (type_value annotated * type_value annotated)
| T_function of (type_value * type_value)
| T_base of type_constant
| T_base of type_base
| T_map of (type_value * type_value)
| T_big_map of (type_value * type_value)
| T_list of type_value
@ -15,6 +14,23 @@ type type_value =
| T_contract of type_value
| T_option of type_value
and type_base =
| TB_unit
| TB_bool
| TB_string
| TB_bytes
| TB_nat
| TB_int
| TB_mutez
| TB_operation
| TB_address
| TB_key
| TB_key_hash
| TB_chain_id
| TB_signature
| TB_timestamp
| TB_void
and environment_element = expression_variable * type_value
and environment = environment_element list

View File

@ -130,7 +130,6 @@ let literal ppf (l : literal) =
match l with
| Literal_unit -> fprintf ppf "unit"
| Literal_void -> fprintf ppf "void"
| Literal_bool b -> fprintf ppf "%b" b
| Literal_int z -> fprintf ppf "%a" Z.pp_print z
| Literal_nat z -> fprintf ppf "+%a" Z.pp_print z
| Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z
@ -155,7 +154,6 @@ let s =
| TC_nat -> "nat"
| TC_int -> "int"
| TC_mutez -> "mutez"
| TC_bool -> "bool"
| TC_operation -> "operation"
| TC_address -> "address"
| TC_key -> "key"

View File

@ -0,0 +1,2 @@
open Types
let t_bool : type_variable = Var.of_name "bool"

View File

@ -20,7 +20,6 @@ type 'a constructor_map = 'a CMap.t
| TC_nat
| TC_int
| TC_mutez
| TC_bool
| TC_operation
| TC_address
| TC_key
@ -112,7 +111,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
| "TC_nat" , [] -> ok @@ T_constant(TC_nat)
| "TC_int" , [] -> ok @@ T_constant(TC_int)
| "TC_mutez" , [] -> ok @@ T_constant(TC_mutez)
| "TC_bool" , [] -> ok @@ T_constant(TC_bool)
| "TC_operation" , [] -> ok @@ T_constant(TC_operation)
| "TC_address" , [] -> ok @@ T_constant(TC_address)
| "TC_key" , [] -> ok @@ T_constant(TC_key)
@ -142,7 +140,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
| TC_nat -> "TC_nat", []
| TC_int -> "TC_int", []
| TC_mutez -> "TC_mutez", []
| TC_bool -> "TC_bool", []
| TC_operation -> "TC_operation", []
| TC_address -> "TC_address", []
| TC_key -> "TC_key", []
@ -162,7 +159,6 @@ end
type literal =
| Literal_unit
| Literal_bool of bool
| Literal_int of Z.t
| Literal_nat of Z.t
| Literal_timestamp of Z.t

View File

@ -18,7 +18,6 @@ type constant_tag =
| C_list (* * -> * *)
| C_set (* * -> * *)
| C_unit (* * *)
| C_bool (* * *)
| C_string (* * *)
| C_nat (* * *)
| C_mutez (* * *)
@ -87,7 +86,6 @@ let type_expression'_of_simple_c_constant = function
| C_nat , [] -> ok @@ Ast_typed.T_constant(TC_nat)
| C_int , [] -> ok @@ Ast_typed.T_constant(TC_int)
| C_mutez , [] -> ok @@ Ast_typed.T_constant(TC_mutez)
| C_bool , [] -> ok @@ Ast_typed.T_constant(TC_bool)
| C_operation , [] -> ok @@ Ast_typed.T_constant(TC_operation)
| C_address , [] -> ok @@ Ast_typed.T_constant(TC_address)
| C_key , [] -> ok @@ Ast_typed.T_constant(TC_key)
@ -95,5 +93,5 @@ let type_expression'_of_simple_c_constant = function
| C_chain_id , [] -> ok @@ Ast_typed.T_constant(TC_chain_id)
| C_signature , [] -> ok @@ Ast_typed.T_constant(TC_signature)
| C_timestamp , [] -> ok @@ Ast_typed.T_constant(TC_timestamp)
| (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_bool | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ ->
| (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ ->
failwith "internal error: wrong number of arguments for type constant"

View File

@ -119,7 +119,6 @@ module Substitution = struct
| T.Literal_void ->
let () = ignore @@ substs in
ok @@ T.Literal_void
| (T.Literal_bool _ as x)
| (T.Literal_int _ as x)
| (T.Literal_nat _ as x)
| (T.Literal_timestamp _ as x)

View File

@ -53,7 +53,7 @@ let map k v = P_constant (C_map , [k; v])
let unit = P_constant (C_unit , [])
let list t = P_constant (C_list , [t])
let set t = P_constant (C_set , [t])
let bool = P_constant (C_bool , [])
let bool = P_variable (Stage_common.Constant.t_bool)
let string = P_constant (C_string , [])
let nat = P_constant (C_nat , [])
let mutez = P_constant (C_mutez , [])

View File

@ -20,7 +20,7 @@ let int () : unit result =
ok ()
module TestExpressions = struct
let test_expression ?(env = Typer.Environment.full_empty)
let test_expression ?(env = Environment.default)
?(state = Typer.Solver.initial_state)
(expr : expression)
(test_expected_ty : Typed.type_expression) =