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

Merge

Browse Source
This commit is contained in:
Sander Spies 2020-04-14 13:11:44 +02:00
commit 3e447c40b7
25 changed files with 1394 additions and 1432 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
gitlab-pages/docs/reference/current.md
View File

@ -612,7 +612,12 @@ Cause the contract to fail with an error message.
> ⚠ Using this currently requires in general a type annotation on the > ⚠ Using this currently requires in general a type annotation on the
> `failwith` call. > `failwith` call.
<Syntax syntax="cameligo">
Note that `Current.failwith` is deprecated. Use `Tezos.failwith` or `failwith` instead.
</Syntax>
<Syntax syntax="reasonligo">
Note that `Current.failwith` is deprecated. Use `Tezos.failwith` or `failwith` instead.
</Syntax>
<Syntax syntax="pascaligo"> <Syntax syntax="pascaligo">
@ -713,10 +718,19 @@ val transaction : 'parameter -> mutez -> 'parameter contract -> operation
let transaction: 'parameter -> mutez -> contract('parameter) -> operation let transaction: 'parameter -> mutez -> contract('parameter) -> operation
</SyntaxTitle> </SyntaxTitle>
Create a transaction to a contract or account. Transfer `tez` to an account, or run code of another smart contract.
To indicate an account, use `unit` as `parameter`. To indicate an account, use `unit` as `parameter`.
<Syntax syntax="pascaligo">
Note that `transaction` is deprecated. Please use `Tezos.transaction` instead.
</Syntax>
<Syntax syntax="cameligo">
Note that `transaction` is deprecated. Please use `Tezos.transaction` instead.
</Syntax>
<Syntax syntax="reasonligo">
Note that `transaction` is deprecated. Please use `Tezos.transaction` instead.
</Syntax>
<SyntaxTitle syntax="pascaligo"> <SyntaxTitle syntax="pascaligo">
function set_delegate : option(key_hash) -> operation function set_delegate : option(key_hash) -> operation
@ -728,9 +742,28 @@ val set_delegate : key_hash option -> operation
let set_delegate: option(key_hash) => operation let set_delegate: option(key_hash) => operation
</SyntaxTitle> </SyntaxTitle>
Create a delegation. Modify the
(delegate)[http://tezos.gitlab.io/user/glossary.html?highlight=delegate#delegate]
of the current contract.
See also: http://tezos.gitlab.io/user/glossary.html?highlight=delegate#delegate The operation fails when:
- the delegate is the same as current delegate
- the keyhash is not of a registered delegate
Use `None` to withdraw the current delegate.
<Syntax syntax="pascaligo">
Note that `set_delegate` is deprecated. Please use `Tezos.set_delegate`
instead.
</Syntax>
<Syntax syntax="cameligo">
Note that `Operation.set_delegate` is deprecated. Please use
`Tezos.set_delegate` instead.
</Syntax>
<Syntax syntax="reasonligo">
Note that `Operation.set_delegate` is deprecated. Please use
`Tezos.set_delegate` instead.
</Syntax>
<SyntaxTitle syntax="pascaligo"> <SyntaxTitle syntax="pascaligo">
function get_contract_opt : address -> option(contract('parameter)) function get_contract_opt : address -> option(contract('parameter))
@ -747,6 +780,19 @@ Get a contract from an address.
When no contract is found or the contract doesn't match the type, When no contract is found or the contract doesn't match the type,
`None` is returned. `None` is returned.
<Syntax syntax="pascaligo">
Note that `get_contract` and `get_contract_opt` are deprecated. Please use
`Tezos.get_contract_opt` instead.
</Syntax>
<Syntax syntax="cameligo">
Note that `Operation.get_contract` and `Operation.get_contract_opt` are
deprecated. Please use `Tezos.get_contract_opt` instead.
</Syntax>
<Syntax syntax="reasonligo">
Note that `Operation.get_contract` and `Operation.get_contract_opt` are
deprecated. Please use `Tezos.get_contract_opt` instead.
</Syntax>
<SyntaxTitle syntax="pascaligo"> <SyntaxTitle syntax="pascaligo">
function get_entrypoint_opt : string -> address -> option(contract('parameter)) function get_entrypoint_opt : string -> address -> option(contract('parameter))
</SyntaxTitle> </SyntaxTitle>
@ -763,3 +809,18 @@ Entrypoints are written in the form of: `%entrypoint`.
When no contract is found or the contract doesn't match the type, When no contract is found or the contract doesn't match the type,
`None` is returned. `None` is returned.
<Syntax syntax="pascaligo">
Note that `get_entrypoint` and `get_entrypoint_opt` are deprecated. Please use
`Tezos.get_entrypoint_opt` instead.
</Syntax>
<Syntax syntax="cameligo">
Note that `Operation.get_entrypoint` and `Operation.get_entrypoint_opt` are
deprecated. Please use `Tezos.get_entrypoint_opt` instead.
</Syntax>
<Syntax syntax="reasonligo">
Note that `Operation.get_entrypoint` and `Operation.get_entrypoint_opt` are
deprecated. Please use `Tezos.get_entrypoint_opt` instead.
</Syntax>

2
gitlab-pages/docs/reference/toplevel.md
View File

@ -22,6 +22,8 @@ let is_nat: int => option(nat)
Convert an `int` to a `nat` if possible. Convert an `int` to a `nat` if possible.
Note that `Michelson.is_nat` is deprecated. Please use `is_nat` instead.
<SyntaxTitle syntax="pascaligo"> <SyntaxTitle syntax="pascaligo">
function abs: int -> nat function abs: int -> nat
</SyntaxTitle> </SyntaxTitle>

14
src/bin/expect_tests/contract_tests.ml
View File

@ -26,7 +26,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-storage" ; contract "coase.ligo" ; "main" ; "Buy_single (record card_to_buy = 1n end)" ] ; run_ligo_bad [ "compile-storage" ; contract "coase.ligo" ; "main" ; "Buy_single (record card_to_buy = 1n end)" ] ;
[%expect {| [%expect {|
ligo: different kinds: {"a":"record[card_patterns -> (TO_Map (nat,record[coefficient -> mutez , quantity -> nat])) ,\n cards -> (TO_Map (nat,record[card_owner -> address , card_pattern -> nat])) ,\n next_id -> nat]","b":"sum[Buy_single -> record[card_to_buy -> nat] ,\n Sell_single -> record[card_to_sell -> nat] ,\n Transfer_single -> record[card_to_transfer -> nat ,\n destination -> address]]"} ligo: different kinds: {"a":"record[card_patterns -> (type_operator: Map (nat,record[coefficient -> mutez , quantity -> nat])) ,\n cards -> (type_operator: Map (nat,record[card_owner -> address , card_pattern -> nat])) ,\n next_id -> nat]","b":"sum[Buy_single -> record[card_to_buy -> nat] ,\n Sell_single -> record[card_to_sell -> nat] ,\n Transfer_single -> record[card_to_transfer -> nat ,\n destination -> address]]"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -39,7 +39,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-parameter" ; contract "coase.ligo" ; "main" ; "record cards = (map end : cards) ; card_patterns = (map end : card_patterns) ; next_id = 3n ; end" ] ; run_ligo_bad [ "compile-parameter" ; contract "coase.ligo" ; "main" ; "record cards = (map end : cards) ; card_patterns = (map end : card_patterns) ; next_id = 3n ; end" ] ;
[%expect {| [%expect {|
ligo: different kinds: {"a":"sum[Buy_single -> record[card_to_buy -> nat] ,\n Sell_single -> record[card_to_sell -> nat] ,\n Transfer_single -> record[card_to_transfer -> nat ,\n destination -> address]]","b":"record[card_patterns -> (TO_Map (nat,record[coefficient -> mutez , quantity -> nat])) ,\n cards -> (TO_Map (nat,record[card_owner -> address , card_pattern -> nat])) ,\n next_id -> nat]"} ligo: different kinds: {"a":"sum[Buy_single -> record[card_to_buy -> nat] ,\n Sell_single -> record[card_to_sell -> nat] ,\n Transfer_single -> record[card_to_transfer -> nat ,\n destination -> address]]","b":"record[card_patterns -> (type_operator: Map (nat,record[coefficient -> mutez , quantity -> nat])) ,\n cards -> (type_operator: Map (nat,record[card_owner -> address , card_pattern -> nat])) ,\n next_id -> nat]"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1117,7 +1117,7 @@ let%expect_test _ =
let%expect_test _ = let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n let rhs#712 = #P in\n let p = rhs#712.0 in\n let s = rhs#712.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , store ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"} ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n let rhs#712 = #P in\n let p = rhs#712.0 in\n let s = rhs#712.1 in\n ( LIST_EMPTY() : (type_operator: list(operation)) , store ) ,\n NONE() : (type_operator: option(key_hash)) ,\n 300000000mutez ,\n \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1130,7 +1130,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8,
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n let rhs#715 = #P in\n let p = rhs#715.0 in\n let s = rhs#715.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , a ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"} ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n let rhs#715 = #P in\n let p = rhs#715.0 in\n let s = rhs#715.1 in\n ( LIST_EMPTY() : (type_operator: list(operation)) , a ) ,\n NONE() : (type_operator: option(key_hash)) ,\n 300000000mutez ,\n 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1191,7 +1191,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char
let%expect_test _ = let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "self_type_annotation.ligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "self_type_annotation.ligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "self_type_annotation.ligo", line 8, characters 41-64. bad self type: expected (TO_Contract (int)) but got (TO_Contract (nat)) {"location":"in file \"self_type_annotation.ligo\", line 8, characters 41-64"} ligo: in file "self_type_annotation.ligo", line 8, characters 41-64. bad self type: expected (type_operator: Contract (int)) but got (type_operator: Contract (nat)) {"location":"in file \"self_type_annotation.ligo\", line 8, characters 41-64"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1230,7 +1230,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract2.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract2.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "", line 0, characters 0-0. bad return type: expected (TO_list(operation)), got string {"location":"in file \"\", line 0, characters 0-0","entrypoint":"main"} ligo: in file "", line 0, characters 0-0. bad return type: expected (type_operator: list(operation)), got string {"location":"in file \"\", line 0, characters 0-0","entrypoint":"main"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -1243,7 +1243,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract3.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract3.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "", line 0, characters 0-0. badly typed contract: expected {int} and {string} to be the same in the entrypoint type {"location":"in file \"\", line 0, characters 0-0","entrypoint":"main","entrypoint_type":"( nat * int ) -> ( (TO_list(operation)) * string )"} ligo: in file "", line 0, characters 0-0. badly typed contract: expected {int} and {string} to be the same in the entrypoint type {"location":"in file \"\", line 0, characters 0-0","entrypoint":"main","entrypoint_type":"( nat * int ) -> ( (type_operator: list(operation)) * string )"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can

4
src/bin/expect_tests/typer_error_tests.ml
View File

@ -29,7 +29,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_function_annotation_3.mligo"; "f"]; run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_function_annotation_3.mligo"; "f"];
[%expect {| [%expect {|
ligo: in file "", line 0, characters 0-0. different kinds: {"a":"( (TO_list(operation)) * sum[Add -> int , Sub -> int] )","b":"sum[Add -> int , Sub -> int]"} ligo: in file "", line 0, characters 0-0. different kinds: {"a":"( (type_operator: list(operation)) * sum[Add -> int , Sub -> int] )","b":"sum[Add -> int , Sub -> int]"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can
@ -80,7 +80,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_2.mligo" ; "main" ] ; run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_2.mligo" ; "main" ] ;
[%expect {| [%expect {|
ligo: in file "error_typer_2.mligo", line 3, characters 24-39. different type constructors: Expected these two n-ary type constructors to be the same, but they're different {"a":"(TO_list(string))","b":"(TO_option(int))"} ligo: in file "error_typer_2.mligo", line 3, characters 24-39. different type constructors: Expected these two n-ary type constructors to be the same, but they're different {"a":"(type_operator: list(string))","b":"(type_operator: option(int))"}
If you're not sure how to fix this error, you can If you're not sure how to fix this error, you can

44
src/passes/1-parser/reasonligo/Parser.mly
View File

@ -21,7 +21,6 @@ type 'a record_elements = {
type 'a sequence_or_record = type 'a sequence_or_record =
PaSequence of 'a sequence_elements PaSequence of 'a sequence_elements
| PaRecord of 'a record_elements | PaRecord of 'a record_elements
| PaSingleExpr of expr
let (<@) f g x = f (g x) let (<@) f g x = f (g x)
@ -913,18 +912,26 @@ expr_with_let_expr:
expr { $1 } expr { $1 }
| let_expr(expr_with_let_expr) { $1 } | let_expr(expr_with_let_expr) { $1 }
more_field_assignments:
"," sep_or_term_list(field_assignment_punning,",") {
let elts, _region = $2 in
$1, elts
}
sequence_or_record_in: sequence_or_record_in:
expr_with_let_expr ";" sep_or_term_list(expr_with_let_expr,";") { sep_or_term_list(expr_with_let_expr,";") {
let elts, _region = $3 in let elts, _region = $1 in
let s_elts = Utils.nsepseq_cons $1 $2 elts PaSequence {s_elts = elts; s_terminator=None}
in PaSequence {s_elts; s_terminator=None}
} }
| field_assignment "," sep_or_term_list(field_assignment,",") { | field_assignment more_field_assignments? {
let elts, _region = $3 in match $2 with
let r_elts = Utils.nsepseq_cons $1 $2 elts | Some (comma, elts) ->
in PaRecord {r_elts; r_terminator = None} let r_elts = Utils.nsepseq_cons $1 comma elts in
PaRecord {r_elts; r_terminator = None}
| None ->
PaRecord {r_elts = ($1, []); r_terminator = None}
} }
| expr_with_let_expr ";"? { PaSingleExpr $1 }
sequence_or_record: sequence_or_record:
"{" sequence_or_record_in "}" { "{" sequence_or_record_in "}" {
@ -940,18 +947,25 @@ sequence_or_record:
let value = {compound; let value = {compound;
ne_elements = r.r_elts; ne_elements = r.r_elts;
terminator = r.r_terminator} terminator = r.r_terminator}
in ERecord {region; value} in ERecord {region; value}}
| PaSingleExpr e -> e }
field_assignment: field_assignment_punning:
(* This can only happen with multiple fields -
one item punning does NOT work in ReasonML *)
field_name { field_name {
let value = { let value = {
field_name = $1; field_name = $1;
assignment = ghost; assignment = ghost;
field_expr = EVar $1 } field_expr = EVar $1 }
in {$1 with value} in
{$1 with value}
} }
| field_name ":" expr { | field_assignment {
$1
}
field_assignment:
field_name ":" expr {
let start = $1.region in let start = $1.region in
let stop = expr_to_region $3 in let stop = expr_to_region $3 in
let region = cover start stop in let region = cover start stop in

303
src/passes/1-parser/reasonligo/error.messages.checked-in
View File

@ -1150,11 +1150,130 @@ interactive_expr: LBRACE ELLIPSIS WILD
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA Ident COLON Bytes VBAR
##
## Ends in an error in state: 477.
##
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning . [ RBRACE ]
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning . COMMA nsepseq(field_assignment_punning,COMMA) [ RBRACE ]
## nseq(__anonymous_0(field_assignment_punning,COMMA)) -> field_assignment_punning . COMMA seq(__anonymous_0(field_assignment_punning,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment_punning
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 155, spurious reduction of production call_expr_level_in -> core_expr
## In state 173, spurious reduction of production option(type_annotation_simple) ->
## In state 174, spurious reduction of production call_expr_level -> call_expr_level_in option(type_annotation_simple)
## In state 175, spurious reduction of production unary_expr_level -> call_expr_level
## In state 128, spurious reduction of production mult_expr_level -> unary_expr_level
## In state 152, spurious reduction of production add_expr_level -> mult_expr_level
## In state 183, spurious reduction of production cat_expr_level -> add_expr_level
## In state 204, spurious reduction of production comp_expr_level -> cat_expr_level
## In state 211, spurious reduction of production conj_expr_level -> comp_expr_level
## In state 218, spurious reduction of production disj_expr_level -> conj_expr_level
## In state 165, spurious reduction of production base_expr(expr) -> disj_expr_level
## In state 222, spurious reduction of production base_cond__open(expr) -> base_expr(expr)
## In state 223, spurious reduction of production expr -> base_cond__open(expr)
## In state 465, spurious reduction of production field_assignment -> Ident COLON expr
## In state 484, spurious reduction of production field_assignment_punning -> field_assignment
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA Ident COMMA Ident COLON Bytes VBAR
##
## Ends in an error in state: 481.
##
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning . [ RBRACE ]
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning . COMMA nsepseq(field_assignment_punning,COMMA) [ RBRACE ]
## seq(__anonymous_0(field_assignment_punning,COMMA)) -> field_assignment_punning . COMMA seq(__anonymous_0(field_assignment_punning,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment_punning
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 155, spurious reduction of production call_expr_level_in -> core_expr
## In state 173, spurious reduction of production option(type_annotation_simple) ->
## In state 174, spurious reduction of production call_expr_level -> call_expr_level_in option(type_annotation_simple)
## In state 175, spurious reduction of production unary_expr_level -> call_expr_level
## In state 128, spurious reduction of production mult_expr_level -> unary_expr_level
## In state 152, spurious reduction of production add_expr_level -> mult_expr_level
## In state 183, spurious reduction of production cat_expr_level -> add_expr_level
## In state 204, spurious reduction of production comp_expr_level -> cat_expr_level
## In state 211, spurious reduction of production conj_expr_level -> comp_expr_level
## In state 218, spurious reduction of production disj_expr_level -> conj_expr_level
## In state 165, spurious reduction of production base_expr(expr) -> disj_expr_level
## In state 222, spurious reduction of production base_cond__open(expr) -> base_expr(expr)
## In state 223, spurious reduction of production expr -> base_cond__open(expr)
## In state 465, spurious reduction of production field_assignment -> Ident COLON expr
## In state 484, spurious reduction of production field_assignment_punning -> field_assignment
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA Ident COMMA Ident COMMA WILD
##
## Ends in an error in state: 482.
##
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning COMMA . nsepseq(field_assignment_punning,COMMA) [ RBRACE ]
## seq(__anonymous_0(field_assignment_punning,COMMA)) -> field_assignment_punning COMMA . seq(__anonymous_0(field_assignment_punning,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment_punning COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA Ident COMMA WILD
##
## Ends in an error in state: 478.
##
## nsepseq(field_assignment_punning,COMMA) -> field_assignment_punning COMMA . nsepseq(field_assignment_punning,COMMA) [ RBRACE ]
## nseq(__anonymous_0(field_assignment_punning,COMMA)) -> field_assignment_punning COMMA . seq(__anonymous_0(field_assignment_punning,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment_punning COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA Ident WILD
##
## Ends in an error in state: 473.
##
## field_assignment -> Ident . COLON expr [ RBRACE COMMA ]
## field_assignment_punning -> Ident . [ RBRACE COMMA ]
##
## The known suffix of the stack is as follows:
## Ident
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes COMMA WILD
##
## Ends in an error in state: 472.
##
## more_field_assignments -> COMMA . sep_or_term_list(field_assignment_punning,COMMA) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COLON Bytes VBAR interactive_expr: LBRACE Ident COLON Bytes VBAR
## ##
## Ends in an error in state: 468. ## Ends in an error in state: 471.
## ##
## sequence_or_record_in -> field_assignment . COMMA sep_or_term_list(field_assignment,COMMA) [ RBRACE ] ## sequence_or_record_in -> field_assignment . option(more_field_assignments) [ RBRACE ]
## ##
## The known suffix of the stack is as follows: ## The known suffix of the stack is as follows:
## field_assignment ## field_assignment
@ -1193,130 +1312,12 @@ interactive_expr: LBRACE Ident COLON VBAR
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA Ident COLON Bytes VBAR
##
## Ends in an error in state: 474.
##
## nsepseq(field_assignment,COMMA) -> field_assignment . [ RBRACE ]
## nsepseq(field_assignment,COMMA) -> field_assignment . COMMA nsepseq(field_assignment,COMMA) [ RBRACE ]
## nseq(__anonymous_0(field_assignment,COMMA)) -> field_assignment . COMMA seq(__anonymous_0(field_assignment,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 155, spurious reduction of production call_expr_level_in -> core_expr
## In state 173, spurious reduction of production option(type_annotation_simple) ->
## In state 174, spurious reduction of production call_expr_level -> call_expr_level_in option(type_annotation_simple)
## In state 175, spurious reduction of production unary_expr_level -> call_expr_level
## In state 128, spurious reduction of production mult_expr_level -> unary_expr_level
## In state 152, spurious reduction of production add_expr_level -> mult_expr_level
## In state 183, spurious reduction of production cat_expr_level -> add_expr_level
## In state 204, spurious reduction of production comp_expr_level -> cat_expr_level
## In state 211, spurious reduction of production conj_expr_level -> comp_expr_level
## In state 218, spurious reduction of production disj_expr_level -> conj_expr_level
## In state 165, spurious reduction of production base_expr(expr) -> disj_expr_level
## In state 222, spurious reduction of production base_cond__open(expr) -> base_expr(expr)
## In state 223, spurious reduction of production expr -> base_cond__open(expr)
## In state 465, spurious reduction of production field_assignment -> Ident COLON expr
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA Ident COMMA Ident COLON Bytes VBAR
##
## Ends in an error in state: 478.
##
## nsepseq(field_assignment,COMMA) -> field_assignment . [ RBRACE ]
## nsepseq(field_assignment,COMMA) -> field_assignment . COMMA nsepseq(field_assignment,COMMA) [ RBRACE ]
## seq(__anonymous_0(field_assignment,COMMA)) -> field_assignment . COMMA seq(__anonymous_0(field_assignment,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 155, spurious reduction of production call_expr_level_in -> core_expr
## In state 173, spurious reduction of production option(type_annotation_simple) ->
## In state 174, spurious reduction of production call_expr_level -> call_expr_level_in option(type_annotation_simple)
## In state 175, spurious reduction of production unary_expr_level -> call_expr_level
## In state 128, spurious reduction of production mult_expr_level -> unary_expr_level
## In state 152, spurious reduction of production add_expr_level -> mult_expr_level
## In state 183, spurious reduction of production cat_expr_level -> add_expr_level
## In state 204, spurious reduction of production comp_expr_level -> cat_expr_level
## In state 211, spurious reduction of production conj_expr_level -> comp_expr_level
## In state 218, spurious reduction of production disj_expr_level -> conj_expr_level
## In state 165, spurious reduction of production base_expr(expr) -> disj_expr_level
## In state 222, spurious reduction of production base_cond__open(expr) -> base_expr(expr)
## In state 223, spurious reduction of production expr -> base_cond__open(expr)
## In state 465, spurious reduction of production field_assignment -> Ident COLON expr
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA Ident COMMA Ident COMMA WILD
##
## Ends in an error in state: 479.
##
## nsepseq(field_assignment,COMMA) -> field_assignment COMMA . nsepseq(field_assignment,COMMA) [ RBRACE ]
## seq(__anonymous_0(field_assignment,COMMA)) -> field_assignment COMMA . seq(__anonymous_0(field_assignment,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA Ident COMMA WILD
##
## Ends in an error in state: 475.
##
## nsepseq(field_assignment,COMMA) -> field_assignment COMMA . nsepseq(field_assignment,COMMA) [ RBRACE ]
## nseq(__anonymous_0(field_assignment,COMMA)) -> field_assignment COMMA . seq(__anonymous_0(field_assignment,COMMA)) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA Ident WILD
##
## Ends in an error in state: 470.
##
## field_assignment -> Ident . [ RBRACE COMMA ]
## field_assignment -> Ident . COLON expr [ RBRACE COMMA ]
##
## The known suffix of the stack is as follows:
## Ident
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident COMMA WILD
##
## Ends in an error in state: 469.
##
## sequence_or_record_in -> field_assignment COMMA . sep_or_term_list(field_assignment,COMMA) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## field_assignment COMMA
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE Ident WILD interactive_expr: LBRACE Ident WILD
## ##
## Ends in an error in state: 463. ## Ends in an error in state: 463.
## ##
## common_expr -> Ident . [ TIMES SLASH SEMI RBRACE PLUS Or NE Mod MINUS LT LPAR LE GT GE EQEQ COLON CAT BOOL_OR BOOL_AND ARROW ] ## common_expr -> Ident . [ TIMES SLASH SEMI RBRACE PLUS Or NE Mod MINUS LT LPAR LE GT GE EQEQ COLON CAT BOOL_OR BOOL_AND ARROW ]
## field_assignment -> Ident . [ COMMA ] ## field_assignment -> Ident . COLON expr [ RBRACE COMMA ]
## field_assignment -> Ident . COLON expr [ COMMA ]
## projection -> Ident . selection [ TIMES SLASH SEMI RBRACE PLUS Or NE Mod MINUS LT LPAR LE GT GE EQEQ COLON CAT BOOL_OR BOOL_AND ARROW ] ## projection -> Ident . selection [ TIMES SLASH SEMI RBRACE PLUS Or NE Mod MINUS LT LPAR LE GT GE EQEQ COLON CAT BOOL_OR BOOL_AND ARROW ]
## ##
## The known suffix of the stack is as follows: ## The known suffix of the stack is as follows:
@ -1340,20 +1341,7 @@ interactive_expr: LBRACE VBAR
interactive_expr: LBRACE WILD SEMI VBAR interactive_expr: LBRACE WILD SEMI VBAR
## ##
## Ends in an error in state: 482. ## Ends in an error in state: 488.
##
## option(SEMI) -> SEMI . [ RBRACE ]
## sequence_or_record_in -> expr_with_let_expr SEMI . sep_or_term_list(expr_with_let_expr,SEMI) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## expr_with_let_expr SEMI
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE WILD SEMI WILD SEMI VBAR
##
## Ends in an error in state: 487.
## ##
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr SEMI . nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr SEMI . nsepseq(expr_with_let_expr,SEMI) [ RBRACE ]
## nseq(__anonymous_0(expr_with_let_expr,SEMI)) -> expr_with_let_expr SEMI . seq(__anonymous_0(expr_with_let_expr,SEMI)) [ RBRACE ] ## nseq(__anonymous_0(expr_with_let_expr,SEMI)) -> expr_with_let_expr SEMI . seq(__anonymous_0(expr_with_let_expr,SEMI)) [ RBRACE ]
@ -1364,9 +1352,9 @@ interactive_expr: LBRACE WILD SEMI WILD SEMI VBAR
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE WILD SEMI WILD SEMI WILD SEMI VBAR interactive_expr: LBRACE WILD SEMI WILD SEMI VBAR
## ##
## Ends in an error in state: 491. ## Ends in an error in state: 492.
## ##
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr SEMI . nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr SEMI . nsepseq(expr_with_let_expr,SEMI) [ RBRACE ]
## seq(__anonymous_0(expr_with_let_expr,SEMI)) -> expr_with_let_expr SEMI . seq(__anonymous_0(expr_with_let_expr,SEMI)) [ RBRACE ] ## seq(__anonymous_0(expr_with_let_expr,SEMI)) -> expr_with_let_expr SEMI . seq(__anonymous_0(expr_with_let_expr,SEMI)) [ RBRACE ]
@ -1377,9 +1365,9 @@ interactive_expr: LBRACE WILD SEMI WILD SEMI WILD SEMI VBAR
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE WILD SEMI WILD SEMI WILD VBAR interactive_expr: LBRACE WILD SEMI WILD VBAR
## ##
## Ends in an error in state: 490. ## Ends in an error in state: 491.
## ##
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . [ RBRACE ]
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ]
@ -1410,9 +1398,9 @@ interactive_expr: LBRACE WILD SEMI WILD SEMI WILD VBAR
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE WILD SEMI WILD VBAR interactive_expr: LBRACE WILD VBAR
## ##
## Ends in an error in state: 486. ## Ends in an error in state: 487.
## ##
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . [ RBRACE ]
## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] ## nsepseq(expr_with_let_expr,SEMI) -> expr_with_let_expr . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ]
@ -1443,38 +1431,6 @@ interactive_expr: LBRACE WILD SEMI WILD VBAR
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACE WILD VBAR
##
## Ends in an error in state: 481.
##
## sequence_or_record_in -> expr_with_let_expr . SEMI sep_or_term_list(expr_with_let_expr,SEMI) [ RBRACE ]
## sequence_or_record_in -> expr_with_let_expr . option(SEMI) [ RBRACE ]
##
## The known suffix of the stack is as follows:
## expr_with_let_expr
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 155, spurious reduction of production call_expr_level_in -> core_expr
## In state 173, spurious reduction of production option(type_annotation_simple) ->
## In state 174, spurious reduction of production call_expr_level -> call_expr_level_in option(type_annotation_simple)
## In state 175, spurious reduction of production unary_expr_level -> call_expr_level
## In state 128, spurious reduction of production mult_expr_level -> unary_expr_level
## In state 152, spurious reduction of production add_expr_level -> mult_expr_level
## In state 183, spurious reduction of production cat_expr_level -> add_expr_level
## In state 204, spurious reduction of production comp_expr_level -> cat_expr_level
## In state 211, spurious reduction of production conj_expr_level -> comp_expr_level
## In state 218, spurious reduction of production disj_expr_level -> conj_expr_level
## In state 165, spurious reduction of production base_expr(expr) -> disj_expr_level
## In state 222, spurious reduction of production base_cond__open(expr) -> base_expr(expr)
## In state 223, spurious reduction of production expr -> base_cond__open(expr)
## In state 400, spurious reduction of production expr_with_let_expr -> expr
##
<YOUR SYNTAX ERROR MESSAGE HERE>
interactive_expr: LBRACKET VBAR interactive_expr: LBRACKET VBAR
## ##
## Ends in an error in state: 91. ## Ends in an error in state: 91.
@ -4150,3 +4106,4 @@ contract: WILD
## ##
<YOUR SYNTAX ERROR MESSAGE HERE> <YOUR SYNTAX ERROR MESSAGE HERE>

153
src/passes/8-typer-new/errors.ml Normal file
View File

@ -0,0 +1,153 @@
open Trace
module I = Ast_core
module O = Ast_typed
module Environment = O.Environment
type environment = Environment.t
let unbound_type_variable (e:environment) (tv:I.type_variable) () =
let title = (thunk "unbound type variable") in
let message () = "" in
let data = [
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
(* TODO: types don't have srclocs for now. *)
(* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
] in
error ~data title message ()
let unbound_variable (e:environment) (n:I.expression_variable) (loc:Location.t) () =
let name () = Format.asprintf "%a" I.PP.expression_variable n in
let title = (thunk ("unbound variable "^(name ()))) in
let message () = "" in
let data = [
("variable" , name) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_empty_variant : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "match with no cases") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_missing_case : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "missing case in match") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_redundant_case : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "redundant case in match") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let unbound_constructor (e:environment) (c:I.constructor') (loc:Location.t) () =
let title = (thunk "unbound constructor") in
let message () = "" in
let data = [
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
let title () = "wrong arity" in
let message () = "" in
let data = [
("function" , fun () -> Format.asprintf "%s" n) ;
("expected" , fun () -> Format.asprintf "%d" expected) ;
("actual" , fun () -> Format.asprintf "%d" actual) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
let title () = "matching tuple of different size" in
let message () = "" in
let data = [
("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
(* TODO: this should be a trace_info? *)
let program_error (p:I.program) () =
let message () = "" in
let title = (thunk "typing program") in
let data = [
("program" , fun () -> Format.asprintf "%a" I.PP.program p)
] in
error ~data title message ()
let constant_declaration_error (name: I.expression_variable) (ae:I.expr) (expected: O.type_expression option) () =
let title = (thunk "typing constant declaration") in
let message () = "" in
let data = [
("constant" , fun () -> Format.asprintf "%a" I.PP.expression_variable name) ; (* Todo : remove Stage_common*)
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
("expected" , fun () ->
match expected with
None -> "(no annotation for the expected type)"
| Some expected -> Format.asprintf "%a" O.PP.type_expression expected) ;
("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
] in
error ~data title message ()
let match_error : ?msg:string -> expected: I.matching_expr -> actual: O.type_expression -> Location.t -> unit -> _ =
fun ?(msg = "") ~expected ~actual loc () ->
let title = (thunk "typing match") in
let message () = msg in
let data = [
("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
(* let needs_annotation (e : I.expression) (case : string) () =
* let title = (thunk "this expression must be annotated with its type") in
* let message () = Format.asprintf "%s needs an annotation" case in
* let data = [
* ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
* ("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
* ] in
* error ~data title message () *)
(* let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
* let title = (thunk "type error") in
* let message () = msg in
* let data = [
* ("expected" , fun () -> Format.asprintf "%s" expected);
* ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual);
* ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
* ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
* ] in
* error ~data title message () *)
let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
let title = (thunk "type error") in
let message () = msg in
let data = [
("expected" , fun () -> Format.asprintf "%a" O.PP.type_expression expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()

368
src/passes/8-typer-new/solver.ml
View File

@ -2,372 +2,8 @@ open Trace
module Core = Typesystem.Core module Core = Typesystem.Core
module Wrap = struct module Wrap = Wrap
module I = Ast_core open Wrap
module T = Ast_typed
module O = Core
module Errors = struct
let unknown_type_constructor (ctor : string) (te : T.type_expression) () =
let title = (thunk "unknown type constructor") in
(* TODO: sanitize the "ctor" argument before displaying it. *)
let message () = ctor in
let data = [
("ctor" , fun () -> ctor) ;
("expression" , fun () -> Format.asprintf "%a" T.PP.type_expression te) ;
(* ("location" , fun () -> Format.asprintf "%a" Location.pp te.location) *) (* TODO *)
] in
error ~data title message ()
end
type constraints = O.type_constraint list
(* let add_type state t = *)
(* let constraints = Wrap.variable type_name t in *)
(* let%bind state' = aggregate_constraints state constraints in *)
(* ok state' in *)
(* let return_add_type ?(state = state) expr t = *)
(* let%bind state' = add_type state t in *)
(* return expr state' in *)
let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun te ->
match te.type_content with
| T_sum kvmap ->
let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
| T_record kvmap ->
let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_record, T.LMap.to_list @@ T.LMap.map type_expression_to_type_value kvmap)
| T_arrow {type1;type2} ->
P_constant (C_arrow, List.map type_expression_to_type_value [ type1 ; type2 ])
| T_variable (type_name) -> P_variable type_name
| 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
| TC_timestamp -> C_timestamp
| TC_int -> C_int
| TC_address -> C_address
| TC_bytes -> C_bytes
| TC_key_hash -> C_key_hash
| TC_key -> C_key
| TC_signature -> C_signature
| TC_operation -> C_operation
| TC_chain_id -> C_unit (* TODO : replace with chain_id *)
| TC_void -> C_unit (* TODO : replace with void *)
)
in
P_constant (csttag, [])
| T_operator (type_operator) ->
let (csttag, args) = Core.(match type_operator with
| TC_option o -> (C_option, [o])
| TC_set s -> (C_set, [s])
| TC_map { k ; v } -> (C_map, [k;v])
| TC_big_map { k ; v } -> (C_big_map, [k;v])
| TC_map_or_big_map { k ; v } -> (C_map, [k;v])
| TC_michelson_or { l; r } -> (C_michelson_or, [l;r])
| TC_arrow { type1 ; type2 } -> (C_arrow, [ type1 ; type2 ])
| TC_list l -> (C_list, [l])
| TC_contract c -> (C_contract, [c])
)
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.type_content with
| T_sum kvmap ->
let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
| T_record kvmap ->
let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_record, I.LMap.to_list @@ I.LMap.map type_expression_to_type_value_copypasted kvmap)
| T_arrow {type1;type2} ->
P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ type1 ; type2 ])
| T_variable type_name -> P_variable (type_name) (* eird stuff*)
| 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
P_constant (csttag,[])
| T_operator (type_name) ->
let (csttag, args) = Core.(match type_name with
| TC_option o -> (C_option , [o])
| TC_list l -> (C_list , [l])
| TC_set s -> (C_set , [s])
| TC_map ( k , v ) -> (C_map , [k;v])
| TC_big_map ( k , v ) -> (C_big_map, [k;v])
| TC_map_or_big_map ( k , v) -> (C_map, [k;v])
| TC_michelson_or ( k , v ) -> (C_michelson_or, [k;v])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
)
in
P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
let type_name = Core.fresh_type_variable () in
[] , type_name
let variable : I.expression_variable -> T.type_expression -> (constraints * T.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 : T.type_expression -> (constraints * T.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
(*
let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
let pattern = type_expression_to_type_value I.t_bool in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
let literal_string : unit -> (constraints * O.type_variable) = fun () ->
let pattern = type_expression_to_type_value I.t_string in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
*)
let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys ->
let patterns = List.map type_expression_to_type_value tys in
let pattern = O.(P_constant (C_record , patterns)) in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *)
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
(* let t_record = ('label:string, 'v) … -> record ('label : 'v) … with independent choices for each 'label and 'v *)
(* let t_variable = t_of_var_in_env *)
(* let t_access_int = record ('label:int , 'v) … -> 'label:int -> 'v *)
(* let t_access_string = record ('label:string , 'v) … -> 'label:string -> 'v *)
module Prim_types = struct
open Typesystem.Shorthands
let t_cons = forall "v" @@ fun v -> v --> list v --> list v (* was: list *)
let t_setcons = forall "v" @@ fun v -> v --> set v --> set v (* was: set *)
let t_mapcons = forall2 "k" "v" @@ fun k v -> (k * v) --> map k v --> map k v (* was: map *)
let t_failwith = forall "a" @@ fun a -> a
(* let t_literal_t = t *)
let t_literal_bool = bool
let t_literal_string = string
let t_application = forall2 "a" "b" @@ fun a b -> (a --> b) --> a --> b
let t_look_up = forall2 "ind" "v" @@ fun ind v -> map ind v --> ind --> option v
let t_sequence = forall "b" @@ fun b -> unit --> b --> b
let t_loop = bool --> unit --> unit
end
(* TODO: I think we should take an I.expression for the base+label *)
let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) =
let base' = type_expression_to_type_value base in
let expr_type = Core.fresh_type_variable () in
[O.C_access_label (base' , label , expr_type)] , expr_type
let constructor
: T.type_expression -> T.type_expression -> T.type_expression -> (constraints * T.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 whole_expr = Core.fresh_type_variable () in
[
C_equation (P_variable (whole_expr) , sum) ;
C_equation (t_arg , c_arg)
] , whole_expr
let record : T.type_expression T.label_map -> (constraints * T.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () in
[C_equation (P_variable whole_expr , record_type)] , whole_expr
let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
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
in O.C_equation (elttype , elt') in
let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype]))
] @ equations , whole_expr
let list = collection O.C_list
let set = collection O.C_set
let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
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
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value 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
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
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
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value 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
let whole_expr = Core.fresh_type_variable () in
O.[
(* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *)
C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let application : T.type_expression -> T.type_expression -> (constraints * T.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
O.[
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
] , whole_expr
let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun ds ind ->
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in
O.[
C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ;
C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
] , whole_expr
let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun a b ->
let a' = type_expression_to_type_value a in
let b' = type_expression_to_type_value b in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (a' , P_constant (C_unit , [])) ;
C_equation (b' , P_variable whole_expr)
] , whole_expr
let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun expr body ->
let expr' = type_expression_to_type_value expr in
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 (body' , P_constant (C_unit , [])) ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.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_tv_opt' = match rhs_tv_opt with
None -> []
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (result' , P_variable whole_expr)
] @ rhs_tv_opt', whole_expr
let recursive : T.type_expression -> (constraints * T.type_variable) =
fun fun_type ->
let fun_type = type_expression_to_type_value fun_type in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (fun_type, P_variable whole_expr)
], whole_expr
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun v e ->
let v' = type_expression_to_type_value v in
let e' = type_expression_to_type_value e in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (v' , e') ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun e annot ->
let e' = type_expression_to_type_value e in
let annot' = type_expression_to_type_value annot in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (e' , annot') ;
C_equation (e' , P_variable whole_expr)
] , whole_expr
let matching : T.type_expression list -> (constraints * T.type_variable) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_expressions = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_expressions
in cs, whole_expr
let fresh_binder () =
Core.fresh_type_variable ()
let lambda
: T.type_expression ->
T.type_expression option ->
T.type_expression option ->
(constraints * T.type_variable) =
fun fresh arg body ->
let whole_expr = Core.fresh_type_variable () in
let unification_arg = Core.fresh_type_variable () in
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
let body' = match body with
None -> []
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
in O.[
C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
C_equation (P_variable whole_expr ,
P_constant (C_arrow , [P_variable unification_arg ;
P_variable unification_body]))
] @ arg' @ body' , whole_expr
(* This is pretty much a wrapper for an n-ary function. *)
let constant : O.type_value -> T.type_expression list -> (constraints * T.type_variable) =
fun f args ->
let whole_expr = Core.fresh_type_variable () in
let args' = List.map type_expression_to_type_value args in
let args_tuple = O.P_constant (C_record , args') in
O.[
C_equation (f , P_constant (C_arrow , [args_tuple ; P_variable whole_expr]))
] , whole_expr
end
(* begin unionfind *)
module TypeVariable = module TypeVariable =
struct struct

136
src/passes/8-typer-new/todo_use_fold_generator.ml Normal file
View File

@ -0,0 +1,136 @@
module I = Ast_core
module O = Ast_typed
let convert_constructor' (I.Constructor c) = O.Constructor c
let convert_label (I.Label c) = O.Label c
let convert_type_constant : I.type_constant -> O.type_constant = function
| TC_unit -> TC_unit
| TC_string -> TC_string
| TC_bytes -> TC_bytes
| 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
| TC_key_hash -> TC_key_hash
| TC_chain_id -> TC_chain_id
| TC_signature -> TC_signature
| TC_timestamp -> TC_timestamp
| TC_void -> TC_void
let convert_constant' : I.constant' -> O.constant' = function
| C_INT -> C_INT
| C_UNIT -> C_UNIT
| C_NIL -> C_NIL
| C_NOW -> C_NOW
| C_IS_NAT -> C_IS_NAT
| C_SOME -> C_SOME
| C_NONE -> C_NONE
| C_ASSERTION -> C_ASSERTION
| C_ASSERT_INFERRED -> C_ASSERT_INFERRED
| C_FAILWITH -> C_FAILWITH
| C_UPDATE -> C_UPDATE
(* Loops *)
| C_ITER -> C_ITER
| C_FOLD_WHILE -> C_FOLD_WHILE
| C_FOLD_CONTINUE -> C_FOLD_CONTINUE
| C_FOLD_STOP -> C_FOLD_STOP
| C_LOOP_LEFT -> C_LOOP_LEFT
| C_LOOP_CONTINUE -> C_LOOP_CONTINUE
| C_LOOP_STOP -> C_LOOP_STOP
| C_FOLD -> C_FOLD
(* MATH *)
| C_NEG -> C_NEG
| C_ABS -> C_ABS
| C_ADD -> C_ADD
| C_SUB -> C_SUB
| C_MUL -> C_MUL
| C_EDIV -> C_EDIV
| C_DIV -> C_DIV
| C_MOD -> C_MOD
(* LOGIC *)
| C_NOT -> C_NOT
| C_AND -> C_AND
| C_OR -> C_OR
| C_XOR -> C_XOR
| C_LSL -> C_LSL
| C_LSR -> C_LSR
(* COMPARATOR *)
| C_EQ -> C_EQ
| C_NEQ -> C_NEQ
| C_LT -> C_LT
| C_GT -> C_GT
| C_LE -> C_LE
| C_GE -> C_GE
(* Bytes/ String *)
| C_SIZE -> C_SIZE
| C_CONCAT -> C_CONCAT
| C_SLICE -> C_SLICE
| C_BYTES_PACK -> C_BYTES_PACK
| C_BYTES_UNPACK -> C_BYTES_UNPACK
| C_CONS -> C_CONS
(* Pair *)
| C_PAIR -> C_PAIR
| C_CAR -> C_CAR
| C_CDR -> C_CDR
| C_LEFT -> C_LEFT
| C_RIGHT -> C_RIGHT
(* Set *)
| C_SET_EMPTY -> C_SET_EMPTY
| C_SET_LITERAL -> C_SET_LITERAL
| C_SET_ADD -> C_SET_ADD
| C_SET_REMOVE -> C_SET_REMOVE
| C_SET_ITER -> C_SET_ITER
| C_SET_FOLD -> C_SET_FOLD
| C_SET_MEM -> C_SET_MEM
(* List *)
| C_LIST_EMPTY -> C_LIST_EMPTY
| C_LIST_LITERAL -> C_LIST_LITERAL
| C_LIST_ITER -> C_LIST_ITER
| C_LIST_MAP -> C_LIST_MAP
| C_LIST_FOLD -> C_LIST_FOLD
(* Maps *)
| C_MAP -> C_MAP
| C_MAP_EMPTY -> C_MAP_EMPTY
| C_MAP_LITERAL -> C_MAP_LITERAL
| C_MAP_GET -> C_MAP_GET
| C_MAP_GET_FORCE -> C_MAP_GET_FORCE
| C_MAP_ADD -> C_MAP_ADD
| C_MAP_REMOVE -> C_MAP_REMOVE
| C_MAP_UPDATE -> C_MAP_UPDATE
| C_MAP_ITER -> C_MAP_ITER
| C_MAP_MAP -> C_MAP_MAP
| C_MAP_FOLD -> C_MAP_FOLD
| C_MAP_MEM -> C_MAP_MEM
| C_MAP_FIND -> C_MAP_FIND
| C_MAP_FIND_OPT -> C_MAP_FIND_OPT
(* Big Maps *)
| C_BIG_MAP -> C_BIG_MAP
| C_BIG_MAP_EMPTY -> C_BIG_MAP_EMPTY
| C_BIG_MAP_LITERAL -> C_BIG_MAP_LITERAL
(* Crypto *)
| C_SHA256 -> C_SHA256
| C_SHA512 -> C_SHA512
| C_BLAKE2b -> C_BLAKE2b
| C_HASH -> C_HASH
| C_HASH_KEY -> C_HASH_KEY
| C_CHECK_SIGNATURE -> C_CHECK_SIGNATURE
| C_CHAIN_ID -> C_CHAIN_ID
(* Blockchain *)
| C_CALL -> C_CALL
| C_CONTRACT -> C_CONTRACT
| C_CONTRACT_OPT -> C_CONTRACT_OPT
| C_CONTRACT_ENTRYPOINT -> C_CONTRACT_ENTRYPOINT
| C_CONTRACT_ENTRYPOINT_OPT -> C_CONTRACT_ENTRYPOINT_OPT
| C_AMOUNT -> C_AMOUNT
| C_BALANCE -> C_BALANCE
| C_SOURCE -> C_SOURCE
| C_SENDER -> C_SENDER
| C_ADDRESS -> C_ADDRESS
| C_SELF -> C_SELF
| C_SELF_ADDRESS -> C_SELF_ADDRESS
| C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
| C_SET_DELEGATE -> C_SET_DELEGATE
| C_CREATE_CONTRACT -> C_CREATE_CONTRACT

801
src/passes/8-typer-new/typer.ml
View File

@ -1,451 +1,14 @@
open Trace open Trace
module I = Ast_core module I = Ast_core
module O = Ast_typed module O = Ast_typed
open O.Combinators open O.Combinators
module Environment = O.Environment module Environment = O.Environment
module Solver = Solver module Solver = Solver
type environment = Environment.t type environment = Environment.t
module Errors = Errors
module Errors = struct
let unbound_type_variable (e:environment) (tv:I.type_variable) () =
let title = (thunk "unbound type variable") in
let message () = "" in
let data = [
("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ;
(* TODO: types don't have srclocs for now. *)
(* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *)
("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
] in
error ~data title message ()
let unbound_variable (e:environment) (n:I.expression_variable) (loc:Location.t) () =
let name () = Format.asprintf "%a" I.PP.expression_variable n in
let title = (thunk ("unbound variable "^(name ()))) in
let message () = "" in
let data = [
("variable" , name) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_empty_variant : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "match with no cases") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_missing_case : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "missing case in match") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_redundant_case : I.matching_expr -> Location.t -> unit -> _ =
fun matching loc () ->
let title = (thunk "redundant case in match") in
let message () = "" in
let data = [
("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let unbound_constructor (e:environment) (c:I.constructor') (loc:Location.t) () =
let title = (thunk "unbound constructor") in
let message () = "" in
let data = [
("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c) ;
("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () =
let title () = "wrong arity" in
let message () = "" in
let data = [
("function" , fun () -> Format.asprintf "%s" n) ;
("expected" , fun () -> Format.asprintf "%d" expected) ;
("actual" , fun () -> Format.asprintf "%d" actual) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () =
let title () = "matching tuple of different size" in
let message () = "" in
let data = [
("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ;
("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
(* TODO: this should be a trace_info? *)
let program_error (p:I.program) () =
let message () = "" in
let title = (thunk "typing program") in
let data = [
("program" , fun () -> Format.asprintf "%a" I.PP.program p)
] in
error ~data title message ()
let constant_declaration_error (name: I.expression_variable) (ae:I.expr) (expected: O.type_expression option) () =
let title = (thunk "typing constant declaration") in
let message () = "" in
let data = [
("constant" , fun () -> Format.asprintf "%a" I.PP.expression_variable name) ; (* Todo : remove Stage_common*)
("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
("expected" , fun () ->
match expected with
None -> "(no annotation for the expected type)"
| Some expected -> Format.asprintf "%a" O.PP.type_expression expected) ;
("location" , fun () -> Format.asprintf "%a" Location.pp ae.location)
] in
error ~data title message ()
let match_error : ?msg:string -> expected: I.matching_expr -> actual: O.type_expression -> Location.t -> unit -> _ =
fun ?(msg = "") ~expected ~actual loc () ->
let title = (thunk "typing match") in
let message () = msg in
let data = [
("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
(* let needs_annotation (e : I.expression) (case : string) () =
* let title = (thunk "this expression must be annotated with its type") in
* let message () = Format.asprintf "%s needs an annotation" case in
* let data = [
* ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ;
* ("location" , fun () -> Format.asprintf "%a" Location.pp e.location)
* ] in
* error ~data title message () *)
(* let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
* let title = (thunk "type error") in
* let message () = msg in
* let data = [
* ("expected" , fun () -> Format.asprintf "%s" expected);
* ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual);
* ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
* ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
* ] in
* error ~data title message () *)
let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
let title = (thunk "type error") in
let message () = msg in
let data = [
("expected" , fun () -> Format.asprintf "%a" O.PP.type_expression expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual);
("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in
error ~data title message ()
end
open Errors open Errors
let convert_constructor' (I.Constructor c) = O.Constructor c open Todo_use_fold_generator
let unconvert_constructor' (O.Constructor c) = I.Constructor c
let convert_label (I.Label c) = O.Label c
let unconvert_label (O.Label c) = I.Label c
let convert_type_constant : I.type_constant -> O.type_constant = function
| TC_unit -> TC_unit
| TC_string -> TC_string
| TC_bytes -> TC_bytes
| 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
| TC_key_hash -> TC_key_hash
| TC_chain_id -> TC_chain_id
| TC_signature -> TC_signature
| TC_timestamp -> TC_timestamp
| TC_void -> TC_void
let unconvert_type_constant : O.type_constant -> I.type_constant = function
| TC_unit -> TC_unit
| TC_string -> TC_string
| TC_bytes -> TC_bytes
| 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
| TC_key_hash -> TC_key_hash
| TC_chain_id -> TC_chain_id
| TC_signature -> TC_signature
| TC_timestamp -> TC_timestamp
| TC_void -> TC_void
let convert_constant' : I.constant' -> O.constant' = function
| C_INT -> C_INT
| C_UNIT -> C_UNIT
| C_NIL -> C_NIL
| C_NOW -> C_NOW
| C_IS_NAT -> C_IS_NAT
| C_SOME -> C_SOME
| C_NONE -> C_NONE
| C_ASSERTION -> C_ASSERTION
| C_ASSERT_INFERRED -> C_ASSERT_INFERRED
| C_FAILWITH -> C_FAILWITH
| C_UPDATE -> C_UPDATE
(* Loops *)
| C_ITER -> C_ITER
| C_FOLD_WHILE -> C_FOLD_WHILE
| C_FOLD_CONTINUE -> C_FOLD_CONTINUE
| C_FOLD_STOP -> C_FOLD_STOP
| C_LOOP_LEFT -> C_LOOP_LEFT
| C_LOOP_CONTINUE -> C_LOOP_CONTINUE
| C_LOOP_STOP -> C_LOOP_STOP
| C_FOLD -> C_FOLD
(* MATH *)
| C_NEG -> C_NEG
| C_ABS -> C_ABS
| C_ADD -> C_ADD
| C_SUB -> C_SUB
| C_MUL -> C_MUL
| C_EDIV -> C_EDIV
| C_DIV -> C_DIV
| C_MOD -> C_MOD
(* LOGIC *)
| C_NOT -> C_NOT
| C_AND -> C_AND
| C_OR -> C_OR
| C_XOR -> C_XOR
| C_LSL -> C_LSL
| C_LSR -> C_LSR
(* COMPARATOR *)
| C_EQ -> C_EQ
| C_NEQ -> C_NEQ
| C_LT -> C_LT
| C_GT -> C_GT
| C_LE -> C_LE
| C_GE -> C_GE
(* Bytes/ String *)
| C_SIZE -> C_SIZE
| C_CONCAT -> C_CONCAT
| C_SLICE -> C_SLICE
| C_BYTES_PACK -> C_BYTES_PACK
| C_BYTES_UNPACK -> C_BYTES_UNPACK
| C_CONS -> C_CONS
(* Pair *)
| C_PAIR -> C_PAIR
| C_CAR -> C_CAR
| C_CDR -> C_CDR
| C_LEFT -> C_LEFT
| C_RIGHT -> C_RIGHT
(* Set *)
| C_SET_EMPTY -> C_SET_EMPTY
| C_SET_LITERAL -> C_SET_LITERAL
| C_SET_ADD -> C_SET_ADD
| C_SET_REMOVE -> C_SET_REMOVE
| C_SET_ITER -> C_SET_ITER
| C_SET_FOLD -> C_SET_FOLD
| C_SET_MEM -> C_SET_MEM
(* List *)
| C_LIST_EMPTY -> C_LIST_EMPTY
| C_LIST_LITERAL -> C_LIST_LITERAL
| C_LIST_ITER -> C_LIST_ITER
| C_LIST_MAP -> C_LIST_MAP
| C_LIST_FOLD -> C_LIST_FOLD
(* Maps *)
| C_MAP -> C_MAP
| C_MAP_EMPTY -> C_MAP_EMPTY
| C_MAP_LITERAL -> C_MAP_LITERAL
| C_MAP_GET -> C_MAP_GET
| C_MAP_GET_FORCE -> C_MAP_GET_FORCE
| C_MAP_ADD -> C_MAP_ADD
| C_MAP_REMOVE -> C_MAP_REMOVE
| C_MAP_UPDATE -> C_MAP_UPDATE
| C_MAP_ITER -> C_MAP_ITER
| C_MAP_MAP -> C_MAP_MAP
| C_MAP_FOLD -> C_MAP_FOLD
| C_MAP_MEM -> C_MAP_MEM
| C_MAP_FIND -> C_MAP_FIND
| C_MAP_FIND_OPT -> C_MAP_FIND_OPT
(* Big Maps *)
| C_BIG_MAP -> C_BIG_MAP
| C_BIG_MAP_EMPTY -> C_BIG_MAP_EMPTY
| C_BIG_MAP_LITERAL -> C_BIG_MAP_LITERAL
(* Crypto *)
| C_SHA256 -> C_SHA256
| C_SHA512 -> C_SHA512
| C_BLAKE2b -> C_BLAKE2b
| C_HASH -> C_HASH
| C_HASH_KEY -> C_HASH_KEY
| C_CHECK_SIGNATURE -> C_CHECK_SIGNATURE
| C_CHAIN_ID -> C_CHAIN_ID
(* Blockchain *)
| C_CALL -> C_CALL
| C_CONTRACT -> C_CONTRACT
| C_CONTRACT_OPT -> C_CONTRACT_OPT
| C_CONTRACT_ENTRYPOINT -> C_CONTRACT_ENTRYPOINT
| C_CONTRACT_ENTRYPOINT_OPT -> C_CONTRACT_ENTRYPOINT_OPT
| C_AMOUNT -> C_AMOUNT
| C_BALANCE -> C_BALANCE
| C_SOURCE -> C_SOURCE
| C_SENDER -> C_SENDER
| C_ADDRESS -> C_ADDRESS
| C_SELF -> C_SELF
| C_SELF_ADDRESS -> C_SELF_ADDRESS
| C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
| C_SET_DELEGATE -> C_SET_DELEGATE
| C_CREATE_CONTRACT -> C_CREATE_CONTRACT
let unconvert_constant' : O.constant' -> I.constant' = function
| C_INT -> C_INT
| C_UNIT -> C_UNIT
| C_NIL -> C_NIL
| C_NOW -> C_NOW
| C_IS_NAT -> C_IS_NAT
| C_SOME -> C_SOME
| C_NONE -> C_NONE
| C_ASSERTION -> C_ASSERTION
| C_ASSERT_INFERRED -> C_ASSERT_INFERRED
| C_FAILWITH -> C_FAILWITH
| C_UPDATE -> C_UPDATE
(* Loops *)
| C_ITER -> C_ITER
| C_FOLD_WHILE -> C_FOLD_WHILE
| C_FOLD_CONTINUE -> C_FOLD_CONTINUE
| C_FOLD_STOP -> C_FOLD_STOP
| C_LOOP_LEFT -> C_LOOP_LEFT
| C_LOOP_CONTINUE -> C_LOOP_CONTINUE
| C_LOOP_STOP -> C_LOOP_STOP
| C_FOLD -> C_FOLD
(* MATH *)
| C_NEG -> C_NEG
| C_ABS -> C_ABS
| C_ADD -> C_ADD
| C_SUB -> C_SUB
| C_MUL -> C_MUL
| C_EDIV -> C_EDIV
| C_DIV -> C_DIV
| C_MOD -> C_MOD
(* LOGIC *)
| C_NOT -> C_NOT
| C_AND -> C_AND
| C_OR -> C_OR
| C_XOR -> C_XOR
| C_LSL -> C_LSL
| C_LSR -> C_LSR
(* COMPARATOR *)
| C_EQ -> C_EQ
| C_NEQ -> C_NEQ
| C_LT -> C_LT
| C_GT -> C_GT
| C_LE -> C_LE
| C_GE -> C_GE
(* Bytes/ String *)
| C_SIZE -> C_SIZE
| C_CONCAT -> C_CONCAT
| C_SLICE -> C_SLICE
| C_BYTES_PACK -> C_BYTES_PACK
| C_BYTES_UNPACK -> C_BYTES_UNPACK
| C_CONS -> C_CONS
(* Pair *)
| C_PAIR -> C_PAIR
| C_CAR -> C_CAR
| C_CDR -> C_CDR
| C_LEFT -> C_LEFT
| C_RIGHT -> C_RIGHT
(* Set *)
| C_SET_EMPTY -> C_SET_EMPTY
| C_SET_LITERAL -> C_SET_LITERAL
| C_SET_ADD -> C_SET_ADD
| C_SET_REMOVE -> C_SET_REMOVE
| C_SET_ITER -> C_SET_ITER
| C_SET_FOLD -> C_SET_FOLD
| C_SET_MEM -> C_SET_MEM
(* List *)
| C_LIST_EMPTY -> C_LIST_EMPTY
| C_LIST_LITERAL -> C_LIST_LITERAL
| C_LIST_ITER -> C_LIST_ITER
| C_LIST_MAP -> C_LIST_MAP
| C_LIST_FOLD -> C_LIST_FOLD
(* Maps *)
| C_MAP -> C_MAP
| C_MAP_EMPTY -> C_MAP_EMPTY
| C_MAP_LITERAL -> C_MAP_LITERAL
| C_MAP_GET -> C_MAP_GET
| C_MAP_GET_FORCE -> C_MAP_GET_FORCE
| C_MAP_ADD -> C_MAP_ADD
| C_MAP_REMOVE -> C_MAP_REMOVE
| C_MAP_UPDATE -> C_MAP_UPDATE
| C_MAP_ITER -> C_MAP_ITER
| C_MAP_MAP -> C_MAP_MAP
| C_MAP_FOLD -> C_MAP_FOLD
| C_MAP_MEM -> C_MAP_MEM
| C_MAP_FIND -> C_MAP_FIND
| C_MAP_FIND_OPT -> C_MAP_FIND_OPT
(* Big Maps *)
| C_BIG_MAP -> C_BIG_MAP
| C_BIG_MAP_EMPTY -> C_BIG_MAP_EMPTY
| C_BIG_MAP_LITERAL -> C_BIG_MAP_LITERAL
(* Crypto *)
| C_SHA256 -> C_SHA256
| C_SHA512 -> C_SHA512
| C_BLAKE2b -> C_BLAKE2b
| C_HASH -> C_HASH
| C_HASH_KEY -> C_HASH_KEY
| C_CHECK_SIGNATURE -> C_CHECK_SIGNATURE
| C_CHAIN_ID -> C_CHAIN_ID
(* Blockchain *)
| C_CALL -> C_CALL
| C_CONTRACT -> C_CONTRACT
| C_CONTRACT_OPT -> C_CONTRACT_OPT
| C_CONTRACT_ENTRYPOINT -> C_CONTRACT_ENTRYPOINT
| C_CONTRACT_ENTRYPOINT_OPT -> C_CONTRACT_ENTRYPOINT_OPT
| C_AMOUNT -> C_AMOUNT
| C_BALANCE -> C_BALANCE
| C_SOURCE -> C_SOURCE
| C_SENDER -> C_SENDER
| C_ADDRESS -> C_ADDRESS
| C_SELF -> C_SELF
| C_SELF_ADDRESS -> C_SELF_ADDRESS
| C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
| C_SET_DELEGATE -> C_SET_DELEGATE
| C_CREATE_CONTRACT -> C_CREATE_CONTRACT
(*
let rec type_program (p:I.program) : O.program result =
let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
let%bind ed' = (bind_map_location (type_declaration e)) d in
let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
let (e', d') = Location.unwrap ed' in
match d' with
| None -> ok (e', acc)
| Some d' -> ok (e', loc ed' d' :: acc)
in
let%bind (_, lst) =
trace (fun () -> program_error p ()) @@
bind_fold_list aux (Environment.full_empty, []) p in
ok @@ List.rev lst
*)
(* (*
Extract pairs of (name,type) in the declaration and add it to the environment Extract pairs of (name,type) in the declaration and add it to the environment
@ -662,12 +225,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
to actually perform the recursive calls *) to actually perform the recursive calls *)
(* Basic *) (* 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_variable name -> ( | E_variable name -> (
let name'= name in let name'= name in
let%bind (tv' : Environment.element) = let%bind (tv' : Environment.element) =
@ -677,6 +234,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
let expr' = e_variable name' in let expr' = e_variable name' in
return expr' state constraints expr_type return expr' state constraints expr_type
) )
| E_literal (Literal_bool b) -> ( | E_literal (Literal_bool b) -> (
return_wrapped (e_bool b) state @@ Wrap.literal (t_bool ()) return_wrapped (e_bool b) state @@ Wrap.literal (t_bool ())
) )
@ -722,12 +280,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
| E_literal (Literal_void) -> ( | E_literal (Literal_void) -> (
failwith "TODO: missing implementation for literal void" failwith "TODO: missing implementation for literal void"
) )
(* | E_literal (Literal_string s) -> (
* L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
* match Option.map Ast_typed.get_type' tv_opt with
* | Some (T_constant ("address" , [])) -> return (E_literal (Literal_address s)) (t_address ())
* | _ -> return (E_literal (Literal_string s)) (t_string ())
* ) *)
| E_record_accessor {record;path} -> ( | E_record_accessor {record;path} -> (
let%bind (base' , state') = type_expression e state record in let%bind (base' , state') = type_expression e state record in
let path = convert_label path in let path = convert_label path in
@ -781,50 +334,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
let%bind () = O.assert_type_expression_eq (tv, get_type_expression update) in let%bind () = O.assert_type_expression_eq (tv, get_type_expression update) in
return_wrapped (E_record_update {record; path; update}) state (Wrap.record wrapped) return_wrapped (E_record_update {record; path; update}) state (Wrap.record wrapped)
(* Data-structure *) (* Data-structure *)
(* | E_lambda {
* binder ;
* input_type ;
* output_type ;
* result ;
* } -> (
* let%bind input_type =
* let%bind input_type =
* (\* Hack to take care of let_in introduced by `simplify/cameligo.ml` in ECase's hack *\)
* let default_action e () = fail @@ (needs_annotation e "the returned value") in
* match input_type with
* | Some ty -> ok ty
* | None -> (
* match result.expression with
* | I.E_let_in li -> (
* match li.rhs.expression with
* | I.E_variable name when name = (fst binder) -> (
* match snd li.binder with
* | Some ty -> ok ty
* | None -> default_action li.rhs ()
* )
* | _ -> default_action li.rhs ()
* )
* | _ -> default_action result ()
* )
* in
* evaluate_type e input_type in
* let%bind output_type =
* bind_map_option (evaluate_type e) output_type
* in
* let e' = Environment.add_ez_binder (fst binder) input_type e in
* let%bind body = type_expression ?tv_opt:output_type e' result in
* let output_type = body.type_annotation in
* return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ())
* ) *)
(* | E_constant (name, lst) ->
* let%bind lst' = bind_list @@ List.map (type_expression e) lst in
* let tv_lst = List.map get_type_annotation lst' in
* let%bind (name', tv) =
* type_constant name tv_lst tv_opt ae.location in
* return (E_constant (name' , lst')) tv *)
| E_application {lamb;args} -> | E_application {lamb;args} ->
let%bind (f' , state') = type_expression e state lamb in let%bind (f' , state') = type_expression e state lamb in
let%bind (args , state'') = type_expression e state' args in let%bind (args , state'') = type_expression e state' args in
@ -832,30 +341,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
return_wrapped (E_application {lamb=f';args}) state'' wrapped return_wrapped (E_application {lamb=f';args}) state'' wrapped
(* Advanced *) (* Advanced *)
(* | E_matching (ex, m) -> (
* let%bind ex' = type_expression e ex in
* let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
* let tvs =
* let aux (cur:O.value O.matching) =
* match cur with
* | Match_bool { match_true ; match_false } -> [ match_true ; match_false ]
* | Match_list { match_nil ; match_cons = ((_ , _) , match_cons) } -> [ match_nil ; match_cons ]
* | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ]
* | Match_tuple (_ , match_tuple) -> [ match_tuple ]
* | Match_variant (lst , _) -> List.map snd lst in
* List.map get_type_annotation @@ aux m' in
* let aux prec cur =
* let%bind () =
* match prec with
* | None -> ok ()
* | Some cur' -> Ast_typed.assert_type_value_eq (cur , cur') in
* ok (Some cur) in
* let%bind tv_opt = bind_fold_list aux None tvs in
* let%bind tv =
* trace_option (match_empty_variant m ae.location) @@
* tv_opt in
* return (O.E_matching (ex', m')) tv
* ) *)
| E_let_in {let_binder ; rhs ; let_result; inline} -> | E_let_in {let_binder ; rhs ; let_result; inline} ->
let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd let_binder) in let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd let_binder) in
(* TODO: the binder annotation should just be an annotation node *) (* TODO: the binder annotation should just be an annotation node *)
@ -866,6 +351,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
let wrapped = let wrapped =
Wrap.let_in rhs.type_expression rhs_tv_opt let_result.type_expression in Wrap.let_in rhs.type_expression rhs_tv_opt let_result.type_expression in
return_wrapped (E_let_in {let_binder; rhs; let_result; inline}) state'' wrapped return_wrapped (E_let_in {let_binder; rhs; let_result; inline}) state'' wrapped
| E_ascription {anno_expr;type_annotation} -> | E_ascription {anno_expr;type_annotation} ->
let%bind tv = evaluate_type e type_annotation in let%bind tv = evaluate_type e type_annotation in
let%bind (expr' , state') = type_expression e state anno_expr in let%bind (expr' , state') = type_expression e state anno_expr in
@ -899,38 +385,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
return_wrapped (O.E_matching {matchee=ex';cases=m'}) state'' wrapped return_wrapped (O.E_matching {matchee=ex';cases=m'}) state'' wrapped
) )
(* match m with *)
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
(* | I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> ( *)
(* let%bind fw = I.get_e_failwith match_true in *)
(* let%bind fw' = type_expression e fw in *)
(* let%bind mf' = type_expression e match_false in *)
(* let t = get_type_annotation ex' in *)
(* let%bind () = *)
(* trace_strong (match_error ~expected:m ~actual:t ae.location) *)
(* @@ assert_t_bool t in *)
(* let%bind () = *)
(* trace_strong (match_error *)
(* ~msg:"matching not-unit on an assert" *)
(* ~expected:m *)
(* ~actual:t *)
(* ae.location) *)
(* @@ assert_t_unit (get_type_annotation mf') in *)
(* let mt' = make_a_e *)
(* (E_constant ("ASSERT_INFERRED" , [ex' ; fw'])) *)
(* (t_unit ()) *)
(* e *)
(* in *)
(* let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in *)
(* return (O.E_matching (ex' , m')) (t_unit ()) *)
(* ) *)
(* | _ -> ( … ) *)
| E_lambda lambda -> | E_lambda lambda ->
let%bind (lambda,state',wrapped) = type_lambda e state lambda in let%bind (lambda,state',wrapped) = type_lambda e state lambda in
return_wrapped (E_lambda lambda) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *) return_wrapped (E_lambda lambda) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
state' wrapped state' wrapped
| E_recursive {fun_name;fun_type;lambda} -> | E_recursive {fun_name;fun_type;lambda} ->
let%bind fun_type = evaluate_type e fun_type in let%bind fun_type = evaluate_type e fun_type in
let e = Environment.add_ez_binder fun_name fun_type e in let e = Environment.add_ez_binder fun_name fun_type e in
@ -958,6 +417,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
type_constant name tv_lst tv_opt ae.location in type_constant name tv_lst tv_opt ae.location in
return (E_constant (name' , lst')) tv return (E_constant (name' , lst')) tv
*) *)
and type_lambda e state { and type_lambda e state {
binder ; binder ;
input_type ; input_type ;
@ -974,7 +434,6 @@ and type_lambda e state {
let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
ok (({binder;result}:O.lambda),state',wrapped) ok (({binder;result}:O.lambda),state',wrapped)
(* Advanced *)
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result = and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
let name = convert_constant' name in let name = convert_constant' name in
@ -982,42 +441,20 @@ and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type
let%bind tv = typer lst tv_opt in let%bind tv = typer lst tv_opt in
ok(name, tv) ok(name, tv)
let untype_type_value (t:O.type_expression) : (I.type_expression) result = (* Apply type_declaration on every node of the AST_core from the root p *)
match t.type_meta with
| Some s -> ok s
| _ -> fail @@ internal_assertion_failure "trying to untype generated type"
(* let type_statement : environment -> I.declaration -> Solver.state -> (environment * O.declaration * Solver.state) result = fun env declaration state -> *)
(* match declaration with *)
(* | I.Declaration_type td -> ( *)
(* let%bind (env', state', declaration') = type_declaration env state td in *)
(* let%bind toto = Solver.aggregate_constraints state' constraints in *)
(* let declaration' = match declaration' with None -> Pervasives.failwith "TODO" | Some x -> x in *)
(* ok (env' , declaration' , toto) *)
(* ) *)
(* | I.Declaration_constant ((_ , _ , expr) as cd) -> ( *)
(* let%bind state' = type_expression expr in *)
(* let constraints = constant_declaration cd in *)
(* Solver.aggregate_constraints state' constraints *)
(* ) *)
(* TODO: we ended up with two versions of type_program… ??? *)
(*
Apply type_declaration on all the node of the AST_core from the root p
*)
let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result =
let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
let ds' = match d'_opt with let ds' = match d'_opt with
| None -> ds | None -> ds
| Some d' -> ds @ [Location.wrap ~loc:(Location.get_location d) d'] (* take O(n) insted of O(1) *) | Some d' -> Location.wrap ~loc:(Location.get_location d) d' :: ds
in in
ok (e' , s' , ds') ok (e' , s' , ds')
in in
let%bind (env' , state' , declarations) = let%bind (env' , state' , declarations) =
trace (fun () -> program_error p ()) @@ trace (fun () -> program_error p ()) @@
bind_fold_list aux (env , state , []) p in bind_fold_list aux (env , state , []) p in
let () = ignore (env' , state') in let declarations = List.rev declarations in (* Common hack to have O(1) append: prepend and then reverse *)
ok (env', state', declarations) ok (env', state', declarations)
let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result = let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result =
@ -1059,208 +496,18 @@ let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt :
let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state
(* let untype_type_expression = Untyper.untype_type_expression
TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity let untype_expression = Untyper.untype_expression
*)
let type_program' : I.program -> O.program result = fun p ->
let initial_state = Solver.initial_state in
let initial_env = Environment.full_empty in
let aux (env, state) (statement : I.declaration Location.wrap) =
let statement' = statement.wrap_content in (* TODO *)
let%bind (env' , state' , declaration') = type_declaration env state statement' in
let declaration'' = match declaration' with
None -> None
| Some x -> Some (Location.wrap ~loc:Location.(statement.location) x) in
ok ((env' , state') , declaration'')
in
let%bind ((env' , state') , p') = bind_fold_map_list aux (initial_env, initial_state) p in
let p' = List.fold_left (fun l e -> match e with None -> l | Some x -> x :: l) [] p' in
(* here, maybe ensure that there are no invalid things in env' and state' ? *) (* These aliases are just here for quick navigation during debug, and can safely be removed later *)
let () = ignore (env' , state') in let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * Solver.state * O.declaration option) result = type_declaration _env _state
ok p' and [@warning "-32"] type_match : environment -> Solver.state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * Solver.state) result = type_match
and [@warning "-32"] evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result = evaluate_type e t
(* and [@warning "-32"] type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result = type_expression
Tranform a Ast_typed type_expression into an ast_core type_expression and [@warning "-32"] type_lambda e state lam = type_lambda e state lam
*) and [@warning "-32"] type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result = type_constant name lst tv_opt
let rec untype_type_expression (t:O.type_expression) : (I.type_expression) result = let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = type_program_returns_state (env, state, p)
(* TODO: or should we use t.core if present? *) let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state
let%bind t = match t.type_content with let [@warning "-32"] type_program (p : I.program) : (O.program * Solver.state) result = type_program p
| O.T_sum x -> let [@warning "-32"] type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.expression) Trace.result = type_expression_returns_state
let aux k v acc = let [@warning "-32"] type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * Solver.state) result = type_expression_subst env state ?tv_opt e
let%bind acc = acc in
let%bind v' = untype_type_expression v in
ok @@ I.CMap.add (unconvert_constructor' k) v' acc in
let%bind x' = O.CMap.fold aux x (ok I.CMap.empty) in
ok @@ I.T_sum x'
| O.T_record x ->
let aux k v acc =
let%bind acc = acc in
let%bind v' = untype_type_expression v in
ok @@ I.LMap.add (unconvert_label k) v' acc in
let%bind x' = O.LMap.fold aux x (ok I.LMap.empty) in
ok @@ I.T_record x'
| O.T_constant (tag) ->
ok @@ I.T_constant (unconvert_type_constant tag)
| O.T_variable (name) -> ok @@ I.T_variable (name) (* TODO: is this the right conversion? *)
| O.T_arrow {type1;type2} ->
let%bind type1 = untype_type_expression type1 in
let%bind type2 = untype_type_expression type2 in
ok @@ I.T_arrow {type1;type2}
| O.T_operator (type_name) ->
let%bind type_name = match type_name with
| O.TC_option t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_option t'
| O.TC_list t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_list t'
| O.TC_set t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_set t'
| O.TC_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_map (k,v)
| O.TC_big_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_big_map (k,v)
| O.TC_map_or_big_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_map_or_big_map (k,v)
| O.TC_michelson_or {l;r} ->
let%bind l = untype_type_expression l in
let%bind r = untype_type_expression r in
ok @@ I.TC_michelson_or (l,r)
| O.TC_arrow { type1=arg ; type2=ret } ->
let%bind arg' = untype_type_expression arg in
let%bind ret' = untype_type_expression ret in
ok @@ I.TC_arrow ( arg' , ret' )
| O.TC_contract c->
let%bind c = untype_type_expression c in
ok @@ I.TC_contract c
in
ok @@ I.T_operator (type_name)
in
ok @@ I.make_t t
(* match t.core with *)
(* | Some s -> ok s *)
(* | _ -> fail @@ internal_assertion_failure "trying to untype generated type" *)
(*
Tranform a Ast_typed literal into an ast_core literal
*)
let untype_literal (l:O.literal) : I.literal result =
let open I in
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)
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
| Literal_key s -> ok (Literal_key s)
| Literal_key_hash s -> ok (Literal_key_hash s)
| Literal_chain_id s -> ok (Literal_chain_id s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s)
| Literal_operation s -> ok (Literal_operation s)
(*
Tranform a Ast_typed expression into an ast_core matching
*)
let rec untype_expression (e:O.expression) : (I.expression) result =
let open I in
let return e = ok e in
match e.expression_content with
| E_literal l ->
let%bind l = untype_literal l in
return (e_literal l)
| E_constant {cons_name;arguments} ->
let%bind lst' = bind_map_list untype_expression arguments in
return (e_constant (unconvert_constant' cons_name) lst')
| E_variable (n) ->
return (e_variable (n))
| E_application {lamb;args} ->
let%bind f' = untype_expression lamb in
let%bind arg' = untype_expression args in
return (e_application f' arg')
| E_lambda lambda ->
let%bind lambda = untype_lambda e.type_expression lambda in
let {binder;input_type;output_type;result} = lambda in
return (e_lambda (binder) (input_type) (output_type) result)
| E_constructor {constructor; element} ->
let%bind p' = untype_expression element in
let Constructor n = constructor in
return (e_constructor n p')
| E_record r ->
let r = O.LMap.to_kv_list r in
let%bind r' = bind_map_list (fun (O.Label k,e) -> let%bind e = untype_expression e in ok (I.Label k,e)) r in
return (e_record @@ LMap.of_list r')
| E_record_accessor {record; path} ->
let%bind r' = untype_expression record in
let Label s = path in
return (e_record_accessor r' s)
| E_record_update {record; path; update} ->
let%bind r' = untype_expression record in
let%bind e = untype_expression update in
return (e_record_update r' (unconvert_label path) e)
| E_matching {matchee;cases} ->
let%bind ae' = untype_expression matchee in
let%bind m' = untype_matching untype_expression cases in
return (e_matching ae' m')
(* | E_failwith ae ->
* let%bind ae' = untype_expression ae in
* return (e_failwith ae') *)
| E_let_in {let_binder; rhs;let_result; inline} ->
let%bind tv = untype_type_value rhs.type_expression in
let%bind rhs = untype_expression rhs in
let%bind result = untype_expression let_result in
return (e_let_in (let_binder , (Some tv)) inline rhs result)
| E_recursive {fun_name; fun_type; lambda} ->
let%bind lambda = untype_lambda fun_type lambda in
let%bind fun_type = untype_type_expression fun_type in
return @@ e_recursive fun_name fun_type lambda
and untype_lambda ty {binder; result} : I.lambda result =
let%bind io = get_t_function ty in
let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
let%bind result = untype_expression result in
ok ({binder;input_type = Some input_type; output_type = Some output_type; result}: I.lambda)
(*
Tranform a Ast_typed matching into an ast_core matching
*)
and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
let open I in
match m with
| Match_bool {match_true ; match_false} ->
let%bind match_true = f match_true in
let%bind match_false = f match_false in
ok @@ Match_bool {match_true ; match_false}
| Match_tuple { vars ; body ; tvs=_ } ->
let%bind b = f body in
ok @@ I.Match_tuple ((vars, b),[])
| Match_option {match_none ; match_some = {opt; body;tv=_}} ->
let%bind match_none = f match_none in
let%bind some = f body in
let match_some = opt, some, () in
ok @@ Match_option {match_none ; match_some}
| Match_list {match_nil ; match_cons = {hd;tl;body;tv=_}} ->
let%bind match_nil = f match_nil in
let%bind cons = f body in
let match_cons = hd , tl , cons, () in
ok @@ Match_list {match_nil ; match_cons}
| Match_variant { cases ; tv=_ } ->
let aux ({constructor;pattern;body} : O.matching_content_case) =
let%bind body = f body in
ok ((unconvert_constructor' constructor,pattern),body) in
let%bind lst' = bind_map_list aux cases in
ok @@ Match_variant (lst',())

10
src/passes/8-typer-new/typer.mli
View File

@ -39,19 +39,11 @@ module Errors : sig
end end
val type_program : I.program -> (O.program * Solver.state) result val type_program : I.program -> (O.program * Solver.state) result
val type_program' : I.program -> (O.program) result (* TODO: merge with type_program *)
val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result
(* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
val evaluate_type : environment -> I.type_expression -> O.type_expression result val evaluate_type : environment -> I.type_expression -> O.type_expression result
val type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result val type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result
val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result
val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result
(*
val untype_type_value : O.type_value -> (I.type_expression) result
val untype_literal : O.literal -> I.literal result
*)
val untype_type_expression : O.type_expression -> I.type_expression result val untype_type_expression : O.type_expression -> I.type_expression result
val untype_expression : O.expression -> I.expression result val untype_expression : O.expression -> I.expression result
(*
val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result
*)

328
src/passes/8-typer-new/untyper.ml Normal file
View File

@ -0,0 +1,328 @@
open Trace
module I = Ast_core
module O = Ast_typed
open O.Combinators
let unconvert_constructor' (O.Constructor c) = I.Constructor c
let unconvert_label (O.Label c) = I.Label c
let unconvert_type_constant : O.type_constant -> I.type_constant = function
| TC_unit -> TC_unit
| TC_string -> TC_string
| TC_bytes -> TC_bytes
| 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
| TC_key_hash -> TC_key_hash
| TC_chain_id -> TC_chain_id
| TC_signature -> TC_signature
| TC_timestamp -> TC_timestamp
| TC_void -> TC_void
let unconvert_constant' : O.constant' -> I.constant' = function
| C_INT -> C_INT
| C_UNIT -> C_UNIT
| C_NIL -> C_NIL
| C_NOW -> C_NOW
| C_IS_NAT -> C_IS_NAT
| C_SOME -> C_SOME
| C_NONE -> C_NONE
| C_ASSERTION -> C_ASSERTION
| C_ASSERT_INFERRED -> C_ASSERT_INFERRED
| C_FAILWITH -> C_FAILWITH
| C_UPDATE -> C_UPDATE
(* Loops *)
| C_ITER -> C_ITER
| C_FOLD_WHILE -> C_FOLD_WHILE
| C_FOLD_CONTINUE -> C_FOLD_CONTINUE
| C_FOLD_STOP -> C_FOLD_STOP
| C_LOOP_LEFT -> C_LOOP_LEFT
| C_LOOP_CONTINUE -> C_LOOP_CONTINUE
| C_LOOP_STOP -> C_LOOP_STOP
| C_FOLD -> C_FOLD
(* MATH *)
| C_NEG -> C_NEG
| C_ABS -> C_ABS
| C_ADD -> C_ADD
| C_SUB -> C_SUB
| C_MUL -> C_MUL
| C_DIV -> C_DIV
| C_EDIV -> C_EDIV
| C_MOD -> C_MOD
(* LOGIC *)
| C_NOT -> C_NOT
| C_AND -> C_AND
| C_OR -> C_OR
| C_XOR -> C_XOR
| C_LSL -> C_LSL
| C_LSR -> C_LSR
(* COMPARATOR *)
| C_EQ -> C_EQ
| C_NEQ -> C_NEQ
| C_LT -> C_LT
| C_GT -> C_GT
| C_LE -> C_LE
| C_GE -> C_GE
(* Bytes/ String *)
| C_SIZE -> C_SIZE
| C_CONCAT -> C_CONCAT
| C_SLICE -> C_SLICE
| C_BYTES_PACK -> C_BYTES_PACK
| C_BYTES_UNPACK -> C_BYTES_UNPACK
| C_CONS -> C_CONS
(* Pair *)
| C_PAIR -> C_PAIR
| C_CAR -> C_CAR
| C_CDR -> C_CDR
| C_LEFT -> C_LEFT
| C_RIGHT -> C_RIGHT
(* Set *)
| C_SET_EMPTY -> C_SET_EMPTY
| C_SET_LITERAL -> C_SET_LITERAL
| C_SET_ADD -> C_SET_ADD
| C_SET_REMOVE -> C_SET_REMOVE
| C_SET_ITER -> C_SET_ITER
| C_SET_FOLD -> C_SET_FOLD
| C_SET_MEM -> C_SET_MEM
(* List *)
| C_LIST_EMPTY -> C_LIST_EMPTY
| C_LIST_LITERAL -> C_LIST_LITERAL
| C_LIST_ITER -> C_LIST_ITER
| C_LIST_MAP -> C_LIST_MAP
| C_LIST_FOLD -> C_LIST_FOLD
(* Maps *)
| C_MAP -> C_MAP
| C_MAP_EMPTY -> C_MAP_EMPTY
| C_MAP_LITERAL -> C_MAP_LITERAL
| C_MAP_GET -> C_MAP_GET
| C_MAP_GET_FORCE -> C_MAP_GET_FORCE
| C_MAP_ADD -> C_MAP_ADD
| C_MAP_REMOVE -> C_MAP_REMOVE
| C_MAP_UPDATE -> C_MAP_UPDATE
| C_MAP_ITER -> C_MAP_ITER
| C_MAP_MAP -> C_MAP_MAP
| C_MAP_FOLD -> C_MAP_FOLD
| C_MAP_MEM -> C_MAP_MEM
| C_MAP_FIND -> C_MAP_FIND
| C_MAP_FIND_OPT -> C_MAP_FIND_OPT
(* Big Maps *)
| C_BIG_MAP -> C_BIG_MAP
| C_BIG_MAP_EMPTY -> C_BIG_MAP_EMPTY
| C_BIG_MAP_LITERAL -> C_BIG_MAP_LITERAL
(* Crypto *)
| C_SHA256 -> C_SHA256
| C_SHA512 -> C_SHA512
| C_BLAKE2b -> C_BLAKE2b
| C_HASH -> C_HASH
| C_HASH_KEY -> C_HASH_KEY
| C_CHECK_SIGNATURE -> C_CHECK_SIGNATURE
| C_CHAIN_ID -> C_CHAIN_ID
(* Blockchain *)
| C_CALL -> C_CALL
| C_CONTRACT -> C_CONTRACT
| C_CONTRACT_OPT -> C_CONTRACT_OPT
| C_CONTRACT_ENTRYPOINT -> C_CONTRACT_ENTRYPOINT
| C_CONTRACT_ENTRYPOINT_OPT -> C_CONTRACT_ENTRYPOINT_OPT
| C_AMOUNT -> C_AMOUNT
| C_BALANCE -> C_BALANCE
| C_SOURCE -> C_SOURCE
| C_SENDER -> C_SENDER
| C_ADDRESS -> C_ADDRESS
| C_SELF -> C_SELF
| C_SELF_ADDRESS -> C_SELF_ADDRESS
| C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
| C_SET_DELEGATE -> C_SET_DELEGATE
| C_CREATE_CONTRACT -> C_CREATE_CONTRACT
let untype_type_value (t:O.type_expression) : (I.type_expression) result =
match t.type_meta with
| Some s -> ok s
| _ -> fail @@ internal_assertion_failure "trying to untype generated type"
(*
Tranform a Ast_typed type_expression into an ast_core type_expression
*)
let rec untype_type_expression (t:O.type_expression) : (I.type_expression) result =
(* TODO: or should we use t.core if present? *)
let%bind t = match t.type_content with
| O.T_sum x ->
let aux k v acc =
let%bind acc = acc in
let%bind v' = untype_type_expression v in
ok @@ I.CMap.add (unconvert_constructor' k) v' acc in
let%bind x' = O.CMap.fold aux x (ok I.CMap.empty) in
ok @@ I.T_sum x'
| O.T_record x ->
let aux k v acc =
let%bind acc = acc in
let%bind v' = untype_type_expression v in
ok @@ I.LMap.add (unconvert_label k) v' acc in
let%bind x' = O.LMap.fold aux x (ok I.LMap.empty) in
ok @@ I.T_record x'
| O.T_constant (tag) ->
ok @@ I.T_constant (unconvert_type_constant tag)
| O.T_variable (name) -> ok @@ I.T_variable (name) (* TODO: is this the right conversion? *)
| O.T_arrow {type1;type2} ->
let%bind type1 = untype_type_expression type1 in
let%bind type2 = untype_type_expression type2 in
ok @@ I.T_arrow {type1;type2}
| O.T_operator (type_name) ->
let%bind type_name = match type_name with
| O.TC_option t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_option t'
| O.TC_list t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_list t'
| O.TC_set t ->
let%bind t' = untype_type_expression t in
ok @@ I.TC_set t'
| O.TC_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_map (k,v)
| O.TC_big_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_big_map (k,v)
| O.TC_map_or_big_map {k;v} ->
let%bind k = untype_type_expression k in
let%bind v = untype_type_expression v in
ok @@ I.TC_map_or_big_map (k,v)
| O.TC_michelson_or {l;r} ->
let%bind l = untype_type_expression l in
let%bind r = untype_type_expression r in
ok @@ I.TC_michelson_or (l,r)
| O.TC_arrow { type1=arg ; type2=ret } ->
let%bind arg' = untype_type_expression arg in
let%bind ret' = untype_type_expression ret in
ok @@ I.TC_arrow ( arg' , ret' )
| O.TC_contract c->
let%bind c = untype_type_expression c in
ok @@ I.TC_contract c
in
ok @@ I.T_operator (type_name)
in
ok @@ I.make_t t
(* match t.core with *)
(* | Some s -> ok s *)
(* | _ -> fail @@ internal_assertion_failure "trying to untype generated type" *)
(*
Tranform a Ast_typed literal into an ast_core literal
*)
let untype_literal (l:O.literal) : I.literal result =
let open I in
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)
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
| Literal_key s -> ok (Literal_key s)
| Literal_key_hash s -> ok (Literal_key_hash s)
| Literal_chain_id s -> ok (Literal_chain_id s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s)
| Literal_operation s -> ok (Literal_operation s)
(*
Tranform a Ast_typed expression into an ast_core matching
*)
let rec untype_expression (e:O.expression) : (I.expression) result =
let open I in
let return e = ok e in
match e.expression_content with
| E_literal l ->
let%bind l = untype_literal l in
return (e_literal l)
| E_constant {cons_name;arguments} ->
let%bind lst' = bind_map_list untype_expression arguments in
return (e_constant (unconvert_constant' cons_name) lst')
| E_variable (n) ->
return (e_variable (n))
| E_application {lamb;args} ->
let%bind f' = untype_expression lamb in
let%bind arg' = untype_expression args in
return (e_application f' arg')
| E_lambda lambda ->
let%bind lambda = untype_lambda e.type_expression lambda in
let {binder;input_type;output_type;result} = lambda in
return (e_lambda (binder) (input_type) (output_type) result)
| E_constructor {constructor; element} ->
let%bind p' = untype_expression element in
let Constructor n = constructor in
return (e_constructor n p')
| E_record r ->
let r = O.LMap.to_kv_list r in
let%bind r' = bind_map_list (fun (O.Label k,e) -> let%bind e = untype_expression e in ok (I.Label k,e)) r in
return (e_record @@ LMap.of_list r')
| E_record_accessor {record; path} ->
let%bind r' = untype_expression record in
let Label s = path in
return (e_record_accessor r' s)
| E_record_update {record; path; update} ->
let%bind r' = untype_expression record in
let%bind e = untype_expression update in
return (e_record_update r' (unconvert_label path) e)
| E_matching {matchee;cases} ->
let%bind ae' = untype_expression matchee in
let%bind m' = untype_matching untype_expression cases in
return (e_matching ae' m')
(* | E_failwith ae ->
* let%bind ae' = untype_expression ae in
* return (e_failwith ae') *)
| E_let_in {let_binder; rhs;let_result; inline} ->
let%bind tv = untype_type_value rhs.type_expression in
let%bind rhs = untype_expression rhs in
let%bind result = untype_expression let_result in
return (e_let_in (let_binder , (Some tv)) inline rhs result)
| E_recursive {fun_name; fun_type; lambda} ->
let%bind lambda = untype_lambda fun_type lambda in
let%bind fun_type = untype_type_expression fun_type in
return @@ e_recursive fun_name fun_type lambda
and untype_lambda ty {binder; result} : I.lambda result =
let%bind io = get_t_function ty in
let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
let%bind result = untype_expression result in
ok ({binder;input_type = Some input_type; output_type = Some output_type; result}: I.lambda)
(*
Tranform a Ast_typed matching into an ast_core matching
*)
and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
let open I in
match m with
| Match_bool {match_true ; match_false} ->
let%bind match_true = f match_true in
let%bind match_false = f match_false in
ok @@ Match_bool {match_true ; match_false}
| Match_tuple { vars ; body ; tvs=_ } ->
let%bind b = f body in
ok @@ I.Match_tuple ((vars, b),[])
| Match_option {match_none ; match_some = {opt; body;tv=_}} ->
let%bind match_none = f match_none in
let%bind some = f body in
let match_some = opt, some, () in
ok @@ Match_option {match_none ; match_some}
| Match_list {match_nil ; match_cons = {hd;tl;body;tv=_}} ->
let%bind match_nil = f match_nil in
let%bind cons = f body in
let match_cons = hd , tl , cons, () in
ok @@ Match_list {match_nil ; match_cons}
| Match_variant { cases ; tv=_ } ->
let aux ({constructor;pattern;body} : O.matching_content_case) =
let%bind body = f body in
ok ((unconvert_constructor' constructor,pattern),body) in
let%bind lst' = bind_map_list aux cases in
ok @@ Match_variant (lst',())

364
src/passes/8-typer-new/wrap.ml Normal file
View File

@ -0,0 +1,364 @@
open Trace
module Core = Typesystem.Core
module I = Ast_core
module T = Ast_typed
module O = Core
module Errors = struct
let unknown_type_constructor (ctor : string) (te : T.type_expression) () =
let title = (thunk "unknown type constructor") in
(* TODO: sanitize the "ctor" argument before displaying it. *)
let message () = ctor in
let data = [
("ctor" , fun () -> ctor) ;
("expression" , fun () -> Format.asprintf "%a" T.PP.type_expression te) ;
(* ("location" , fun () -> Format.asprintf "%a" Location.pp te.location) *) (* TODO *)
] in
error ~data title message ()
end
type constraints = O.type_constraint list
(* let add_type state t = *)
(* let constraints = Wrap.variable type_name t in *)
(* let%bind state' = aggregate_constraints state constraints in *)
(* ok state' in *)
(* let return_add_type ?(state = state) expr t = *)
(* let%bind state' = add_type state t in *)
(* return expr state' in *)
let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun te ->
match te.type_content with
| T_sum kvmap ->
let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
| T_record kvmap ->
let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_record, T.LMap.to_list @@ T.LMap.map type_expression_to_type_value kvmap)
| T_arrow {type1;type2} ->
P_constant (C_arrow, List.map type_expression_to_type_value [ type1 ; type2 ])
| T_variable (type_name) -> P_variable type_name
| 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
| TC_timestamp -> C_timestamp
| TC_int -> C_int
| TC_address -> C_address
| TC_bytes -> C_bytes
| TC_key_hash -> C_key_hash
| TC_key -> C_key
| TC_signature -> C_signature
| TC_operation -> C_operation
| TC_chain_id -> C_unit (* TODO : replace with chain_id *)
| TC_void -> C_unit (* TODO : replace with void *)
)
in
P_constant (csttag, [])
| T_operator (type_operator) ->
let (csttag, args) = Core.(match type_operator with
| TC_option o -> (C_option, [o])
| TC_set s -> (C_set, [s])
| TC_map { k ; v } -> (C_map, [k;v])
| TC_big_map { k ; v } -> (C_big_map, [k;v])
| TC_map_or_big_map { k ; v } -> (C_map, [k;v])
| TC_michelson_or { l; r } -> (C_michelson_or, [l;r])
| TC_arrow { type1 ; type2 } -> (C_arrow, [ type1 ; type2 ])
| TC_list l -> (C_list, [l])
| TC_contract c -> (C_contract, [c])
)
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.type_content with
| T_sum kvmap ->
let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
| T_record kvmap ->
let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in
P_constant (C_record, I.LMap.to_list @@ I.LMap.map type_expression_to_type_value_copypasted kvmap)
| T_arrow {type1;type2} ->
P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ type1 ; type2 ])
| T_variable type_name -> P_variable (type_name) (* eird stuff*)
| 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
P_constant (csttag,[])
| T_operator (type_name) ->
let (csttag, args) = Core.(match type_name with
| TC_option o -> (C_option , [o])
| TC_list l -> (C_list , [l])
| TC_set s -> (C_set , [s])
| TC_map ( k , v ) -> (C_map , [k;v])
| TC_big_map ( k , v ) -> (C_big_map, [k;v])
| TC_map_or_big_map ( k , v) -> (C_map, [k;v])
| TC_michelson_or ( k , v ) -> (C_michelson_or, [k;v])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
)
in
P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
let type_name = Core.fresh_type_variable () in
[] , type_name
let variable : I.expression_variable -> T.type_expression -> (constraints * T.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 : T.type_expression -> (constraints * T.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
(*
let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
let pattern = type_expression_to_type_value I.t_bool in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
let literal_string : unit -> (constraints * O.type_variable) = fun () ->
let pattern = type_expression_to_type_value I.t_string in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
*)
let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys ->
let patterns = List.map type_expression_to_type_value tys in
let pattern = O.(P_constant (C_record , patterns)) in
let type_name = Core.fresh_type_variable () in
[C_equation (P_variable (type_name) , pattern)] , type_name
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *)
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
(* let t_record = ('label:string, 'v) … -> record ('label : 'v) … with independent choices for each 'label and 'v *)
(* let t_variable = t_of_var_in_env *)
(* let t_access_int = record ('label:int , 'v) … -> 'label:int -> 'v *)
(* let t_access_string = record ('label:string , 'v) … -> 'label:string -> 'v *)
module Prim_types = struct
open Typesystem.Shorthands
let t_cons = forall "v" @@ fun v -> v --> list v --> list v (* was: list *)
let t_setcons = forall "v" @@ fun v -> v --> set v --> set v (* was: set *)
let t_mapcons = forall2 "k" "v" @@ fun k v -> (k * v) --> map k v --> map k v (* was: map *)
let t_failwith = forall "a" @@ fun a -> a
(* let t_literal_t = t *)
let t_literal_bool = bool
let t_literal_string = string
let t_application = forall2 "a" "b" @@ fun a b -> (a --> b) --> a --> b
let t_look_up = forall2 "ind" "v" @@ fun ind v -> map ind v --> ind --> option v
let t_sequence = forall "b" @@ fun b -> unit --> b --> b
let t_loop = bool --> unit --> unit
end
(* TODO: I think we should take an I.expression for the base+label *)
let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) =
let base' = type_expression_to_type_value base in
let expr_type = Core.fresh_type_variable () in
[O.C_access_label (base' , label , expr_type)] , expr_type
let constructor
: T.type_expression -> T.type_expression -> T.type_expression -> (constraints * T.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 whole_expr = Core.fresh_type_variable () in
[
C_equation (P_variable (whole_expr) , sum) ;
C_equation (t_arg , c_arg)
] , whole_expr
let record : T.type_expression T.label_map -> (constraints * T.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () in
[C_equation (P_variable whole_expr , record_type)] , whole_expr
let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
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
in O.C_equation (elttype , elt') in
let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype]))
] @ equations , whole_expr
let list = collection O.C_list
let set = collection O.C_set
let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
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
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value 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
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
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
O.C_equation (k_type , k') in
let aux_v (_k , v) =
let v' = type_expression_to_type_value 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
let whole_expr = Core.fresh_type_variable () in
O.[
(* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *)
C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type]))
] @ equations_k @ equations_v , whole_expr
let application : T.type_expression -> T.type_expression -> (constraints * T.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
O.[
C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr]))
] , whole_expr
let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun ds ind ->
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in
O.[
C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ;
C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v]))
] , whole_expr
let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun a b ->
let a' = type_expression_to_type_value a in
let b' = type_expression_to_type_value b in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (a' , P_constant (C_unit , [])) ;
C_equation (b' , P_variable whole_expr)
] , whole_expr
let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun expr body ->
let expr' = type_expression_to_type_value expr in
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 (body' , P_constant (C_unit , [])) ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.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_tv_opt' = match rhs_tv_opt with
None -> []
| Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (result' , P_variable whole_expr)
] @ rhs_tv_opt', whole_expr
let recursive : T.type_expression -> (constraints * T.type_variable) =
fun fun_type ->
let fun_type = type_expression_to_type_value fun_type in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (fun_type, P_variable whole_expr)
], whole_expr
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun v e ->
let v' = type_expression_to_type_value v in
let e' = type_expression_to_type_value e in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (v' , e') ;
C_equation (P_variable whole_expr , P_constant (C_unit , []))
] , whole_expr
let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
fun e annot ->
let e' = type_expression_to_type_value e in
let annot' = type_expression_to_type_value annot in
let whole_expr = Core.fresh_type_variable () in
O.[
C_equation (e' , annot') ;
C_equation (e' , P_variable whole_expr)
] , whole_expr
let matching : T.type_expression list -> (constraints * T.type_variable) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_expressions = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_expressions
in cs, whole_expr
let fresh_binder () =
Core.fresh_type_variable ()
let lambda
: T.type_expression ->
T.type_expression option ->
T.type_expression option ->
(constraints * T.type_variable) =
fun fresh arg body ->
let whole_expr = Core.fresh_type_variable () in
let unification_arg = Core.fresh_type_variable () in
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
let body' = match body with
None -> []
| Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)]
in O.[
C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
C_equation (P_variable whole_expr ,
P_constant (C_arrow , [P_variable unification_arg ;
P_variable unification_body]))
] @ arg' @ body' , whole_expr
(* This is pretty much a wrapper for an n-ary function. *)
let constant : O.type_value -> T.type_expression list -> (constraints * T.type_variable) =
fun f args ->
let whole_expr = Core.fresh_type_variable () in
let args' = List.map type_expression_to_type_value args in
let args_tuple = O.P_constant (C_record , args') in
O.[
C_equation (f , P_constant (C_arrow , [args_tuple ; P_variable whole_expr]))
] , whole_expr

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

@ -302,7 +302,6 @@ module Concrete_to_imperative = struct
| "failwith" -> ok C_FAILWITH | "failwith" -> ok C_FAILWITH
| "Operation.transaction" -> ok C_CALL (* Deprecated *) | "Operation.transaction" -> ok C_CALL (* Deprecated *)
| "Tezos.set_delegate" -> ok C_SET_DELEGATE (* Deprecated *)
| "Operation.set_delegate" -> ok C_SET_DELEGATE (* Deprecated *) | "Operation.set_delegate" -> ok C_SET_DELEGATE (* Deprecated *)
| "Operation.get_contract" -> ok C_CONTRACT (* Deprecated *) | "Operation.get_contract" -> ok C_CONTRACT (* Deprecated *)
| "Operation.get_contract_opt" -> ok C_CONTRACT_OPT (* Deprecated *) | "Operation.get_contract_opt" -> ok C_CONTRACT_OPT (* Deprecated *)
@ -353,9 +352,9 @@ module Concrete_to_imperative = struct
(* Loop module *) (* Loop module *)
| "Loop.fold_while" -> ok C_FOLD_WHILE (* Deprecated *) | "Loop.fold_while" -> ok C_FOLD_WHILE (* Deprecated *)
| "Loop.resume" -> ok C_FOLD_CONTINUE | "Loop.resume" -> ok C_FOLD_CONTINUE (* Deprecated *)
| "continue" -> ok C_FOLD_CONTINUE (* Deprecated *) | "continue" -> ok C_FOLD_CONTINUE (* Deprecated *)
| "Loop.stop" -> ok C_FOLD_STOP | "Loop.stop" -> ok C_FOLD_STOP (* Deprecated *)
| "stop" -> ok C_FOLD_STOP (* Deprecated *) | "stop" -> ok C_FOLD_STOP (* Deprecated *)
(* Others *) (* Others *)

2
src/stages/4-ast_typed/PP.ml
View File

@ -238,7 +238,7 @@ and type_operator :
| TC_arrow {type1; type2} -> Format.asprintf "arrow (%a,%a)" f type1 f type2 | TC_arrow {type1; type2} -> Format.asprintf "arrow (%a,%a)" f type1 f type2
| TC_contract te -> Format.asprintf "Contract (%a)" f te | TC_contract te -> Format.asprintf "Contract (%a)" f te
in in
fprintf ppf "(TO_%s)" s fprintf ppf "(type_operator: %s)" s
(* end include Stage_common.PP *) (* end include Stage_common.PP *)
let expression_variable ppf (ev : expression_variable) : unit = let expression_variable ppf (ev : expression_variable) : unit =

125
src/stages/4-ast_typed/PP_generic.ml
View File

@ -1,42 +1,89 @@
open Types
open Fold open Fold
open Format open Format
open PP_helpers
let print_program : formatter -> program -> unit = fun ppf p -> let needs_parens = {
ignore ppf ; generic = (fun state info ->
let assert_nostate _ = () in (* (needs_parens, state) = assert (not needs_parens && match state with None -> true | Some _ -> false) in *) match info.node_instance.instance_kind with
let nostate = false, "" in | RecordInstance _ -> false
let op = { | VariantInstance _ -> true
generic = (fun state info -> | PolyInstance { poly =_; arguments=_; poly_continue } ->
assert_nostate state; (poly_continue state)
match info.node_instance.instance_kind with );
| RecordInstance { fields } -> type_variable = (fun _ _ _ -> false) ;
false, "{ " ^ String.concat " ; " (List.map (fun (fld : 'x Adt_info.ctor_or_field_instance) -> fld.cf.name ^ " = " ^ snd (fld.cf_continue nostate)) fields) ^ " }" bool = (fun _ _ _ -> false) ;
| VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_ }; cf_continue }; variant=_ } -> int = (fun _ _ _ -> false) ;
(match cf_continue nostate with string = (fun _ _ _ -> false) ;
| true, arg -> true, name ^ " (" ^ arg ^ ")" bytes = (fun _ _ _ -> false) ;
| false, arg -> true, name ^ " " ^ arg) packed_internal_operation = (fun _ _ _ -> false) ;
| PolyInstance { poly=_; arguments=_; poly_continue } -> expression_variable = (fun _ _ _ -> false) ;
(poly_continue nostate) constructor' = (fun _ _ _ -> false) ;
); location = (fun _ _ _ -> false) ;
type_variable = (fun _visitor state type_meta -> assert_nostate state; false , (ignore type_meta;"TODO:TYPE_META")) ; label = (fun _ _ _ -> false) ;
type_meta = (fun _visitor state type_meta -> assert_nostate state; false , (ignore type_meta;"TODO:TYPE_META")) ; ast_core_type_expression = (fun _ _ _ -> true) ;
bool = (fun _visitor state b -> assert_nostate state; false , if b then "true" else "false") ; constructor_map = (fun _ _ _ _ -> false) ;
int = (fun _visitor state i -> assert_nostate state; false , string_of_int i) ; label_map = (fun _ _ _ _ -> false) ;
string = (fun _visitor state str -> assert_nostate state; false , "\"" ^ str ^ "\"") ; list = (fun _ _ _ _ -> false) ;
bytes = (fun _visitor state bytes -> assert_nostate state; false , (ignore bytes;"TODO:BYTES")) ; location_wrap = (fun _ _ _ _ -> false) ;
packed_internal_operation = (fun _visitor state op -> assert_nostate state; false , (ignore op;"TODO:PACKED_INTERNAL_OPERATION")) ; list_ne = (fun _ _ _ _ -> false) ;
expression_variable = (fun _visitor state ev -> assert_nostate state; false , (ignore ev;"TODO:EXPRESSION_VARIABLE")) ; option = (fun _visitor _continue _state o ->
constructor' = (fun _visitor state c -> assert_nostate state; false , (ignore c;"TODO:CONSTRUCTOR'")) ; match o with None -> false | Some _ -> true) ;
location = (fun _visitor state loc -> assert_nostate state; false , (ignore loc;"TODO:LOCATION'")) ; }
label = (fun _visitor state (Label lbl) -> assert_nostate state; true, "Label " ^ lbl) ;
constructor_map = (fun _visitor continue state cmap -> assert_nostate state; false , (ignore (continue,cmap);"TODO:constructor_map")) ; let op ppf = {
label_map = (fun _visitor continue state lmap -> assert_nostate state; false , (ignore (continue,lmap);"TODO:label_map")) ; generic = (fun () info ->
list = (fun _visitor continue state lst -> match info.node_instance.instance_kind with
assert_nostate state; | RecordInstance { fields } ->
false , "[ " ^ String.concat " ; " (List.map snd @@ List.map (continue nostate) lst) ^ " ]") ; let aux ppf (fld : 'x Adt_info.ctor_or_field_instance) =
location_wrap = (fun _visitor continue state lwrap -> assert_nostate state; false , (ignore (continue,lwrap);"TODO:location_wrap")) ; fprintf ppf "%s = %a" fld.cf.name (fun _ppf -> fld.cf_continue) () in
list_ne = (fun _visitor continue state list_ne -> assert_nostate state; false , (ignore (continue,list_ne);"TODO:location_wrap")) ; fprintf ppf "{ %a }" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) fields
} in | VariantInstance { constructor ; _ } ->
let (_ , state) = fold__program op nostate p in if constructor.cf_new_fold needs_parens false
Printf.printf "%s" state then fprintf ppf "%s (%a)" constructor.cf.name (fun _ppf -> constructor.cf_continue) ()
else fprintf ppf "%s %a" constructor.cf.name (fun _ppf -> constructor.cf_continue) ()
| PolyInstance { poly=_; arguments=_; poly_continue } ->
(poly_continue ())
);
type_variable = (fun _visitor () type_variable -> fprintf ppf "%a" Var.pp type_variable) ;
bool = (fun _visitor () b -> fprintf ppf "%s" (if b then "true" else "false")) ;
int = (fun _visitor () i -> fprintf ppf "%d" i) ;
string = (fun _visitor () str -> fprintf ppf "\"%s\"" str) ;
bytes = (fun _visitor () _bytes -> fprintf ppf "bytes...") ;
packed_internal_operation = (fun _visitor () _op -> fprintf ppf "Operation(...bytes)") ;
expression_variable = (fun _visitor () ev -> fprintf ppf "%a" Var.pp ev) ;
constructor' = (fun _visitor () (Constructor c) -> fprintf ppf "Constructor %s" c) ;
location = (fun _visitor () loc -> fprintf ppf "%a" Location.pp loc) ;
label = (fun _visitor () (Label lbl) -> fprintf ppf "Label %s" lbl) ;
ast_core_type_expression = (fun _visitor () te -> fprintf ppf "%a" Ast_core.PP.type_expression te) ;
constructor_map = (fun _visitor continue () cmap ->
let lst = List.sort (fun (Constructor a, _) (Constructor b, _) -> String.compare a b) (CMap.bindings cmap) in
let aux ppf (Constructor k, v) =
fprintf ppf "(Constructor %s, %a)" k (fun _ppf -> continue ()) v in
fprintf ppf "CMap [ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst);
label_map = (fun _visitor continue () lmap ->
let lst = List.sort (fun (Label a, _) (Label b, _) -> String.compare a b) (LMap.bindings lmap) in
let aux ppf (Label k, v) =
fprintf ppf "(Constructor %s, %a)" k (fun _ppf -> continue ()) v in
fprintf ppf "LMap [ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst);
list = (fun _visitor continue () lst ->
let aux ppf elt =
fprintf ppf "%a" (fun _ppf -> continue ()) elt in
fprintf ppf "[ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst);
location_wrap = (fun _visitor continue () lwrap ->
let ({ wrap_content; location } : _ Location.wrap) = lwrap in
fprintf ppf "{ wrap_content = %a ; location = %a }" (fun _ppf -> continue ()) wrap_content Location.pp location);
list_ne = (fun _visitor continue () (first, lst) ->
let aux ppf elt =
fprintf ppf "%a" (fun _ppf -> continue ()) elt in
fprintf ppf "[ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) (first::lst));
option = (fun _visitor continue () o ->
match o with
| None -> fprintf ppf "None"
| Some v -> fprintf ppf "%a" (fun _ppf -> continue ()) v) ;
}
let print : (unit fold_config -> unit -> 'a -> unit) -> formatter -> 'a -> unit = fun fold ppf v ->
fold (op ppf) () v
let program = print fold__program
let type_expression = print fold__type_expression

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

@ -21,6 +21,7 @@ type type_constant =
type te_cmap = type_expression constructor_map type te_cmap = type_expression constructor_map
and te_lmap = type_expression label_map and te_lmap = type_expression label_map
and type_meta = ast_core_type_expression option
and type_content = and type_content =
| T_sum of te_cmap | T_sum of te_cmap

9
src/stages/4-ast_typed/types_utils.ml
View File

@ -21,7 +21,8 @@ module LMap = Map.Make( struct type t = label let compare (Label a) (Label b) =
type 'a label_map = 'a LMap.t type 'a label_map = 'a LMap.t
type 'a constructor_map = 'a CMap.t type 'a constructor_map = 'a CMap.t
type type_meta = S.type_expression option type ast_core_type_expression = S.type_expression
type 'a location_wrap = 'a Location.wrap type 'a location_wrap = 'a Location.wrap
type 'a list_ne = 'a List.Ne.t type 'a list_ne = 'a List.Ne.t
@ -69,3 +70,9 @@ let fold_map__list_ne : type a state new_a . (state -> a -> (state * new_a) resu
ok (state , new_element :: l) in ok (state , new_element :: l) in
let%bind (state , l) = List.fold_left aux (ok (state , [])) l in let%bind (state , l) = List.fold_left aux (ok (state , [])) l in
ok (state , (new_first , l)) ok (state , (new_first , l))
let fold_map__option : type a state new_a . (state -> a -> (state * new_a) result) -> state -> a option -> (state * new_a option) Simple_utils.Trace.result =
fun f state o ->
match o with
| None -> ok (state, None)
| Some v -> let%bind state, v = f state v in ok (state, Some v)

26
src/stages/adt_generator/generator.raku
View File

@ -147,7 +147,6 @@ say "type 'a monad = 'a Simple_utils.Trace.result;;";
say "let (>>?) v f = Simple_utils.Trace.bind f v;;"; say "let (>>?) v f = Simple_utils.Trace.bind f v;;";
say "let return v = Simple_utils.Trace.ok v;;"; say "let return v = Simple_utils.Trace.ok v;;";
say "open $moduleName;;"; say "open $moduleName;;";
say "module Adt_info = Adt_generator.Generic.Adt_info;;";
say ""; say "";
say "(* must be provided by one of the open or include statements: *)"; say "(* must be provided by one of the open or include statements: *)";
@ -224,16 +223,22 @@ say '};;';
say "(* map from node names to their generic folds *)"; say "(* map from node names to their generic folds *)";
say "type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;;"; say "type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;;";
say ""; say "";
say "type 'state fold_config ="; say "type ('state , 'adt_info_node_instance_info) _fold_config =";
say ' {'; say ' {';
say " generic : 'state -> 'state Adt_info.node_instance_info -> 'state;"; say " generic : 'state -> 'adt_info_node_instance_info -> 'state;";
# look for builtins, filtering out the "implicit unit-like fake argument of emtpy constructors" (represented by '') # look for builtins, filtering out the "implicit unit-like fake argument of emtpy constructors" (represented by '')
for $adts.map({ $_<ctorsOrFields> })[*;*].grep({$_<isBuiltin> && $_<type> ne ''}).map({$_<type>}).unique -> $builtin for $adts.map({ $_<ctorsOrFields> })[*;*].grep({$_<isBuiltin> && $_<type> ne ''}).map({$_<type>}).unique -> $builtin
{ say " $builtin : 'state fold_config -> 'state -> $builtin -> 'state;"; } { say " $builtin : ('state , 'adt_info_node_instance_info) _fold_config -> 'state -> $builtin -> 'state;"; }
# look for built-in polymorphic types # look for built-in polymorphic types
for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).unique -> $poly for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).unique -> $poly
{ say " $poly : 'a . 'state fold_config -> ('state -> 'a -> 'state) -> 'state -> 'a $poly -> 'state;"; } { say " $poly : 'a . ('state , 'adt_info_node_instance_info) _fold_config -> ('state -> 'a -> 'state) -> 'state -> 'a $poly -> 'state;"; }
say ' };;'; say ' };;';
say "module Arg = struct";
say " type nonrec ('state , 'adt_info_node_instance_info) fold_config = ('state , 'adt_info_node_instance_info) _fold_config;;";
say "end;;";
say "module Adt_info = Adt_generator.Generic.Adt_info (Arg);;";
say "include Adt_info;;";
say "type 'state fold_config = ('state , 'state Adt_info.node_instance_info) _fold_config;;";
say ""; say "";
say 'type blahblah = {'; say 'type blahblah = {';
@ -256,7 +261,8 @@ for $adts.list -> $t
say ""; say "";
say "let continue_info__$t<name>__$c<name> : type qstate . blahblah -> qstate fold_config -> {$c<type> || 'unit'} -> qstate Adt_info.ctor_or_field_instance = fun blahblah visitor x -> \{"; say "let continue_info__$t<name>__$c<name> : type qstate . blahblah -> qstate fold_config -> {$c<type> || 'unit'} -> qstate Adt_info.ctor_or_field_instance = fun blahblah visitor x -> \{";
say " cf = info__$t<name>__$c<name>;"; say " cf = info__$t<name>__$c<name>;";
say " cf_continue = fun state -> blahblah.fold__$t<name>__$c<name> blahblah visitor state x;"; say " cf_continue = (fun state -> blahblah.fold__$t<name>__$c<name> blahblah visitor state x);";
say " cf_new_fold = (fun visitor state -> blahblah.fold__$t<name>__$c<name> blahblah visitor state x);";
say '};;'; say '};;';
say ""; } say ""; }
say "(* info for node $t<name> *)"; say "(* info for node $t<name> *)";
@ -461,8 +467,8 @@ say '};;';
say ""; say "";
for $adts.list -> $t for $adts.list -> $t
{ say "let with__$t<name> : _ = (fun node__$t<name> op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name> \} \});;"; { say "let with__$t<name> : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name> op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name> \} \});;";
say "let with__$t<name>__pre_state : _ = (fun node__$t<name>__pre_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__pre_state \} \});;"; say "let with__$t<name>__pre_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name>__pre_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__pre_state \} \});;";
say "let with__$t<name>__post_state : _ = (fun node__$t<name>__post_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__post_state \} \});;"; say "let with__$t<name>__post_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name>__post_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__post_state \} \});;";
for $t<ctorsOrFields>.list -> $c for $t<ctorsOrFields>.list -> $c
{ say "let with__$t<name>__$c<name> : _ = (fun $t<name>__$c<name> op -> \{ op with $t<name> = \{ op.$t<name> with $t<name>__$c<name> \} \});;"; } } { say "let with__$t<name>__$c<name> : _ -> _ fold_map_config -> _ fold_map_config = (fun $t<name>__$c<name> op -> \{ op with $t<name> = \{ op.$t<name> with $t<name>__$c<name> \} \});;"; } }

13
src/stages/adt_generator/generic.ml
View File

@ -1,4 +1,4 @@
module Adt_info = struct module Adt_info (M : sig type ('state , 'adt_info_node_instance_info) fold_config end) = struct
type kind = type kind =
| Record | Record
| Variant | Variant
@ -39,10 +39,11 @@ module Adt_info = struct
and 'state ctor_or_field_instance = and 'state ctor_or_field_instance =
{ {
cf : ctor_or_field; cf : ctor_or_field;
cf_continue : 'state -> 'state cf_continue : 'state -> 'state;
cf_new_fold : 'state . ('state, ('state node_instance_info)) M.fold_config -> 'state -> 'state;
} }
type node = and node =
{ {
kind : kind; kind : kind;
declaration_name : string; declaration_name : string;
@ -50,10 +51,10 @@ module Adt_info = struct
} }
(* TODO: rename things a bit in this file. *) (* TODO: rename things a bit in this file. *)
type adt = node list and adt = node list
type 'state node_instance_info = { and 'state node_instance_info = {
adt : adt ; adt : adt ;
node_instance : 'state instance ; node_instance : 'state instance ;
} }
type 'state ctor_or_field_instance_info = adt * node * 'state ctor_or_field_instance and 'state ctor_or_field_instance_info = adt * node * 'state ctor_or_field_instance
end end

2
src/stages/common/PP.ml
View File

@ -235,5 +235,5 @@ module Ast_PP_type (PARAMETER : AST_PARAMETER_TYPE) = struct
| TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v
| TC_contract te -> Format.asprintf "Contract (%a)" f te | TC_contract te -> Format.asprintf "Contract (%a)" f te
in in
fprintf ppf "(TO_%s)" s fprintf ppf "(type_operator: %s)" s
end end

2
src/test/adt_generator/use_a_fold.ml
View File

@ -71,7 +71,7 @@ let () =
match info.node_instance.instance_kind with match info.node_instance.instance_kind with
| RecordInstance { fields } -> | RecordInstance { fields } ->
false, "{ " ^ String.concat " ; " (List.map (fun (fld : 'x Adt_info.ctor_or_field_instance) -> fld.cf.name ^ " = " ^ snd (fld.cf_continue nostate)) fields) ^ " }" false, "{ " ^ String.concat " ; " (List.map (fun (fld : 'x Adt_info.ctor_or_field_instance) -> fld.cf.name ^ " = " ^ snd (fld.cf_continue nostate)) fields) ^ " }"
| VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_ }; cf_continue }; variant=_ } -> | VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_ }; cf_continue; cf_new_fold=_ }; variant=_ } ->
(match cf_continue nostate with (match cf_continue nostate with
| true, arg -> true, name ^ " (" ^ arg ^ ")" | true, arg -> true, name ^ " (" ^ arg ^ ")"
| false, arg -> true, name ^ " " ^ arg) | false, arg -> true, name ^ " " ^ arg)

5
src/test/contracts/single_record_item.religo Normal file
View File

@ -0,0 +1,5 @@
type p = {x: int}
let o = (p: int): p => {
x: p
}

5
src/test/integration_tests.ml
View File

@ -2328,6 +2328,10 @@ let tuple_list_religo () : unit result =
let%bind _ = retype_file "./contracts/tuple_list.religo" in let%bind _ = retype_file "./contracts/tuple_list.religo" in
ok () ok ()
let single_record_expr_religo () : unit result =
let%bind _ = retype_file "./contracts/single_record_item.religo" in
ok ()
let loop_bugs_ligo () : unit result = let loop_bugs_ligo () : unit result =
let%bind program = type_file "./contracts/loop_bugs.ligo" in let%bind program = type_file "./contracts/loop_bugs.ligo" in
let input = e_unit () in let input = e_unit () in
@ -2515,4 +2519,5 @@ let main = test_suite "Integration (End to End)" [
test "no semicolon (religo)" no_semicolon_religo ; test "no semicolon (religo)" no_semicolon_religo ;
test "loop_bugs (ligo)" loop_bugs_ligo ; test "loop_bugs (ligo)" loop_bugs_ligo ;
test "tuple_list (religo)" tuple_list_religo ; test "tuple_list (religo)" tuple_list_religo ;
test "single_record_expr (religo)" single_record_expr_religo ;
] ]

1
vendors/Preprocessor/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
/Preprocessor.install