diff --git a/gitlab-pages/docs/reference/current.md b/gitlab-pages/docs/reference/current.md index a08916711..58c668889 100644 --- a/gitlab-pages/docs/reference/current.md +++ b/gitlab-pages/docs/reference/current.md @@ -612,7 +612,12 @@ Cause the contract to fail with an error message. > ⚠ Using this currently requires in general a type annotation on the > `failwith` call. - + +Note that `Current.failwith` is deprecated. Use `Tezos.failwith` or `failwith` instead. + + +Note that `Current.failwith` is deprecated. Use `Tezos.failwith` or `failwith` instead. + @@ -713,10 +718,19 @@ val transaction : 'parameter -> mutez -> 'parameter contract -> operation let transaction: 'parameter -> mutez -> contract('parameter) -> operation -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`. + +Note that `transaction` is deprecated. Please use `Tezos.transaction` instead. + + +Note that `transaction` is deprecated. Please use `Tezos.transaction` instead. + + +Note that `transaction` is deprecated. Please use `Tezos.transaction` instead. + 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 -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. + + +Note that `set_delegate` is deprecated. Please use `Tezos.set_delegate` +instead. + + +Note that `Operation.set_delegate` is deprecated. Please use +`Tezos.set_delegate` instead. + + +Note that `Operation.set_delegate` is deprecated. Please use +`Tezos.set_delegate` instead. + 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, `None` is returned. + +Note that `get_contract` and `get_contract_opt` are deprecated. Please use +`Tezos.get_contract_opt` instead. + + +Note that `Operation.get_contract` and `Operation.get_contract_opt` are +deprecated. Please use `Tezos.get_contract_opt` instead. + + +Note that `Operation.get_contract` and `Operation.get_contract_opt` are +deprecated. Please use `Tezos.get_contract_opt` instead. + + function get_entrypoint_opt : string -> address -> option(contract('parameter)) @@ -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, `None` is returned. + + +Note that `get_entrypoint` and `get_entrypoint_opt` are deprecated. Please use +`Tezos.get_entrypoint_opt` instead. + + + +Note that `Operation.get_entrypoint` and `Operation.get_entrypoint_opt` are +deprecated. Please use `Tezos.get_entrypoint_opt` instead. + + + +Note that `Operation.get_entrypoint` and `Operation.get_entrypoint_opt` are +deprecated. Please use `Tezos.get_entrypoint_opt` instead. + \ No newline at end of file diff --git a/gitlab-pages/docs/reference/toplevel.md b/gitlab-pages/docs/reference/toplevel.md index ce19cfa08..b55f64286 100644 --- a/gitlab-pages/docs/reference/toplevel.md +++ b/gitlab-pages/docs/reference/toplevel.md @@ -22,6 +22,8 @@ let is_nat: int => option(nat) Convert an `int` to a `nat` if possible. +Note that `Michelson.is_nat` is deprecated. Please use `is_nat` instead. + function abs: int -> nat diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml index 7152d3e9b..0141af522 100644 --- a/src/bin/expect_tests/contract_tests.ml +++ b/src/bin/expect_tests/contract_tests.ml @@ -26,7 +26,7 @@ let%expect_test _ = run_ligo_bad [ "compile-storage" ; contract "coase.ligo" ; "main" ; "Buy_single (record card_to_buy = 1n end)" ] ; [%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 @@ -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" ] ; [%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 @@ -1117,7 +1117,7 @@ let%expect_test _ = let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ; [%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 @@ -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" ] ; [%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 @@ -1191,7 +1191,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "self_type_annotation.ligo" ; "main" ] ; [%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 @@ -1230,7 +1230,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract2.mligo" ; "main" ] ; [%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 @@ -1243,7 +1243,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "bad_contract3.mligo" ; "main" ] ; [%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 diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml index a52cd6e68..246762e60 100644 --- a/src/bin/expect_tests/typer_error_tests.ml +++ b/src/bin/expect_tests/typer_error_tests.ml @@ -29,7 +29,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_function_annotation_3.mligo"; "f"]; [%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 @@ -80,7 +80,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_2.mligo" ; "main" ] ; [%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 diff --git a/src/passes/1-parser/reasonligo/Parser.mly b/src/passes/1-parser/reasonligo/Parser.mly index 90819ab7a..e8dea1820 100644 --- a/src/passes/1-parser/reasonligo/Parser.mly +++ b/src/passes/1-parser/reasonligo/Parser.mly @@ -21,7 +21,6 @@ type 'a record_elements = { type 'a sequence_or_record = PaSequence of 'a sequence_elements | PaRecord of 'a record_elements -| PaSingleExpr of expr let (<@) f g x = f (g x) @@ -913,18 +912,26 @@ expr_with_let_expr: 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: - expr_with_let_expr ";" sep_or_term_list(expr_with_let_expr,";") { - let elts, _region = $3 in - let s_elts = Utils.nsepseq_cons $1 $2 elts - in PaSequence {s_elts; s_terminator=None} + sep_or_term_list(expr_with_let_expr,";") { + let elts, _region = $1 in + PaSequence {s_elts = elts; s_terminator=None} } -| field_assignment "," sep_or_term_list(field_assignment,",") { - let elts, _region = $3 in - let r_elts = Utils.nsepseq_cons $1 $2 elts - in PaRecord {r_elts; r_terminator = None} +| field_assignment more_field_assignments? { + match $2 with + | Some (comma, elts) -> + 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_in "}" { @@ -940,18 +947,25 @@ sequence_or_record: let value = {compound; ne_elements = r.r_elts; terminator = r.r_terminator} - in ERecord {region; value} - | PaSingleExpr e -> e } + in ERecord {region; value}} -field_assignment: - field_name { +field_assignment_punning: + (* This can only happen with multiple fields - + one item punning does NOT work in ReasonML *) + field_name { let value = { field_name = $1; assignment = ghost; 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 stop = expr_to_region $3 in let region = cover start stop in diff --git a/src/passes/1-parser/reasonligo/error.messages.checked-in b/src/passes/1-parser/reasonligo/error.messages.checked-in index 19c8fcfa2..c5aec0a5c 100644 --- a/src/passes/1-parser/reasonligo/error.messages.checked-in +++ b/src/passes/1-parser/reasonligo/error.messages.checked-in @@ -1150,11 +1150,130 @@ interactive_expr: LBRACE ELLIPSIS WILD +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 +## + + + +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 +## + + + +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 +## + + + +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 +## + + + +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 +## + + + +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 +## + + + 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: ## field_assignment @@ -1193,130 +1312,12 @@ interactive_expr: LBRACE Ident COLON VBAR -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 -## - - - -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 -## - - - -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 -## - - - -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 -## - - - -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 -## - - - -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 -## - - - interactive_expr: LBRACE Ident WILD ## ## 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 ] -## field_assignment -> Ident . [ COMMA ] -## field_assignment -> Ident . COLON expr [ COMMA ] +## field_assignment -> Ident . COLON expr [ RBRACE 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 ] ## ## The known suffix of the stack is as follows: @@ -1340,20 +1341,7 @@ interactive_expr: LBRACE VBAR interactive_expr: LBRACE WILD SEMI VBAR ## -## Ends in an error in state: 482. -## -## 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 -## - - - -interactive_expr: LBRACE WILD SEMI WILD SEMI VBAR -## -## Ends in an error in state: 487. +## Ends in an error in state: 488. ## ## 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 ] @@ -1364,9 +1352,9 @@ interactive_expr: LBRACE WILD SEMI WILD SEMI VBAR -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 ] ## 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 -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 . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] @@ -1410,9 +1398,9 @@ interactive_expr: LBRACE WILD SEMI WILD SEMI WILD VBAR -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 . SEMI nsepseq(expr_with_let_expr,SEMI) [ RBRACE ] @@ -1443,38 +1431,6 @@ interactive_expr: LBRACE WILD SEMI WILD VBAR -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 -## - - - interactive_expr: LBRACKET VBAR ## ## Ends in an error in state: 91. @@ -4149,4 +4105,5 @@ contract: WILD ## ## - \ No newline at end of file + + diff --git a/src/passes/8-typer-new/errors.ml b/src/passes/8-typer-new/errors.ml new file mode 100644 index 000000000..4205d11fb --- /dev/null +++ b/src/passes/8-typer-new/errors.ml @@ -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 () diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml index 7f06acc93..d7bbd220e 100644 --- a/src/passes/8-typer-new/solver.ml +++ b/src/passes/8-typer-new/solver.ml @@ -2,372 +2,8 @@ open Trace module Core = Typesystem.Core -module Wrap = struct - 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 - -end - -(* begin unionfind *) +module Wrap = Wrap +open Wrap module TypeVariable = struct diff --git a/src/passes/8-typer-new/todo_use_fold_generator.ml b/src/passes/8-typer-new/todo_use_fold_generator.ml new file mode 100644 index 000000000..8256f039e --- /dev/null +++ b/src/passes/8-typer-new/todo_use_fold_generator.ml @@ -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 diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml index a275dda33..2645f400a 100644 --- a/src/passes/8-typer-new/typer.ml +++ b/src/passes/8-typer-new/typer.ml @@ -1,451 +1,14 @@ open Trace - module I = Ast_core module O = Ast_typed open O.Combinators - module Environment = O.Environment - module Solver = Solver - type environment = Environment.t - -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 - +module Errors = Errors open Errors -let convert_constructor' (I.Constructor c) = O.Constructor c -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 -*) +open Todo_use_fold_generator (* Extract pairs of (name,type) in the declaration and add it to the environment @@ -597,26 +160,26 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu return (T_constant (convert_type_constant cst)) | T_operator opt -> let%bind opt = match opt with - | TC_set s -> - let%bind s = evaluate_type e s in - ok @@ O.TC_set (s) - | TC_option o -> - let%bind o = evaluate_type e o in - ok @@ O.TC_option (o) - | TC_list l -> - let%bind l = evaluate_type e l in - ok @@ O.TC_list (l) + | TC_set s -> + let%bind s = evaluate_type e s in + ok @@ O.TC_set (s) + | TC_option o -> + let%bind o = evaluate_type e o in + ok @@ O.TC_option (o) + | TC_list l -> + let%bind l = evaluate_type e l in + ok @@ O.TC_list (l) | TC_map (k,v) -> - let%bind k = evaluate_type e k in - let%bind v = evaluate_type e v in + let%bind k = evaluate_type e k in + let%bind v = evaluate_type e v in ok @@ O.TC_map {k;v} | TC_big_map (k,v) -> - let%bind k = evaluate_type e k in - let%bind v = evaluate_type e v in + let%bind k = evaluate_type e k in + let%bind v = evaluate_type e v in ok @@ O.TC_big_map {k;v} | TC_map_or_big_map (k,v) -> - let%bind k = evaluate_type e k in - let%bind v = evaluate_type e v in + let%bind k = evaluate_type e k in + let%bind v = evaluate_type e v in ok @@ O.TC_map_or_big_map {k;v} | TC_michelson_or (l,r) -> let%bind l = evaluate_type e l in @@ -662,12 +225,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression - to actually perform the recursive calls *) (* Basic *) - (* | E_failwith expr -> ( - * let%bind (expr', state') = type_expression e state expr in - * let (constraints , expr_type) = Wrap.failwith_ () in - * let expr'' = e_failwith expr' in - * return expr'' state' constraints expr_type - * ) *) | E_variable name -> ( let name'= name in 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 return expr' state constraints expr_type ) + | E_literal (Literal_bool b) -> ( 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) -> ( 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} -> ( let%bind (base' , state') = type_expression e state record 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 return_wrapped (E_record_update {record; path; update}) state (Wrap.record wrapped) (* 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} -> let%bind (f' , state') = type_expression e state lamb 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 (* 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} -> 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 *) @@ -866,6 +351,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression - let wrapped = 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 + | E_ascription {anno_expr;type_annotation} -> let%bind tv = evaluate_type e type_annotation 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 ) - (* 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 -> 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; ? *) state' wrapped + | E_recursive {fun_name;fun_type;lambda} -> let%bind fun_type = evaluate_type e fun_type 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 return (E_constant (name' , lst')) tv *) + and type_lambda e state { binder ; 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 wrapped = Solver.Wrap.lambda fresh input_type' output_type' in 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 = 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 ok(name, tv) -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" -(* 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 -*) +(* Apply type_declaration on every 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 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 ds' = match d'_opt with | 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 ok (e' , s' , ds') in let%bind (env' , state' , declarations) = trace (fun () -> program_error p ()) @@ 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) 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. *) type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state - (* -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 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 +let untype_type_expression = Untyper.untype_type_expression +let untype_expression = Untyper.untype_expression - (* here, maybe ensure that there are no invalid things in env' and state' ? *) - let () = ignore (env' , state') in - ok p' - -(* - 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',()) +(* These aliases are just here for quick navigation during debug, and can safely be removed later *) +let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * Solver.state * O.declaration option) result = type_declaration _env _state +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 +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 [@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) +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 [@warning "-32"] type_program (p : I.program) : (O.program * Solver.state) result = type_program p +let [@warning "-32"] type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.expression) Trace.result = type_expression_returns_state +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 diff --git a/src/passes/8-typer-new/typer.mli b/src/passes/8-typer-new/typer.mli index 6e24e7359..e5b91de0a 100644 --- a/src/passes/8-typer-new/typer.mli +++ b/src/passes/8-typer-new/typer.mli @@ -39,19 +39,11 @@ module Errors : sig end 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_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 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_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_expression : O.expression -> I.expression result -(* -val untype_matching : ('o -> 'i result) -> 'o O.matching -> ('i I.matching) result -*) diff --git a/src/passes/8-typer-new/untyper.ml b/src/passes/8-typer-new/untyper.ml new file mode 100644 index 000000000..0f0803f8e --- /dev/null +++ b/src/passes/8-typer-new/untyper.ml @@ -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',()) diff --git a/src/passes/8-typer-new/wrap.ml b/src/passes/8-typer-new/wrap.ml new file mode 100644 index 000000000..55e7c3257 --- /dev/null +++ b/src/passes/8-typer-new/wrap.ml @@ -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 diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index 9e493d00b..1cf4407ae 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -302,7 +302,6 @@ module Concrete_to_imperative = struct | "failwith" -> ok C_FAILWITH | "Operation.transaction" -> ok C_CALL (* Deprecated *) - | "Tezos.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_opt" -> ok C_CONTRACT_OPT (* Deprecated *) @@ -353,9 +352,9 @@ module Concrete_to_imperative = struct (* Loop module *) | "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 *) - | "Loop.stop" -> ok C_FOLD_STOP + | "Loop.stop" -> ok C_FOLD_STOP (* Deprecated *) | "stop" -> ok C_FOLD_STOP (* Deprecated *) (* Others *) diff --git a/src/stages/4-ast_typed/PP.ml b/src/stages/4-ast_typed/PP.ml index 0b8266a11..a5cf4c7f1 100644 --- a/src/stages/4-ast_typed/PP.ml +++ b/src/stages/4-ast_typed/PP.ml @@ -238,7 +238,7 @@ and type_operator : | TC_arrow {type1; type2} -> Format.asprintf "arrow (%a,%a)" f type1 f type2 | TC_contract te -> Format.asprintf "Contract (%a)" f te in - fprintf ppf "(TO_%s)" s + fprintf ppf "(type_operator: %s)" s (* end include Stage_common.PP *) let expression_variable ppf (ev : expression_variable) : unit = diff --git a/src/stages/4-ast_typed/PP_generic.ml b/src/stages/4-ast_typed/PP_generic.ml index 22ad1a2a1..47f4f2551 100644 --- a/src/stages/4-ast_typed/PP_generic.ml +++ b/src/stages/4-ast_typed/PP_generic.ml @@ -1,42 +1,89 @@ -open Types open Fold open Format +open PP_helpers -let print_program : formatter -> program -> unit = fun ppf p -> - ignore ppf ; - let assert_nostate _ = () in (* (needs_parens, state) = assert (not needs_parens && match state with None -> true | Some _ -> false) in *) - let nostate = false, "" in - let op = { - generic = (fun state info -> - assert_nostate state; - match info.node_instance.instance_kind with - | 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) ^ " }" - | VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_ }; cf_continue }; variant=_ } -> - (match cf_continue nostate with - | true, arg -> true, name ^ " (" ^ arg ^ ")" - | false, arg -> true, name ^ " " ^ arg) - | PolyInstance { poly=_; arguments=_; poly_continue } -> - (poly_continue nostate) - ); - type_variable = (fun _visitor state type_meta -> assert_nostate state; false , (ignore type_meta;"TODO:TYPE_META")) ; - type_meta = (fun _visitor state type_meta -> assert_nostate state; false , (ignore type_meta;"TODO:TYPE_META")) ; - bool = (fun _visitor state b -> assert_nostate state; false , if b then "true" else "false") ; - int = (fun _visitor state i -> assert_nostate state; false , string_of_int i) ; - string = (fun _visitor state str -> assert_nostate state; false , "\"" ^ str ^ "\"") ; - bytes = (fun _visitor state bytes -> assert_nostate state; false , (ignore bytes;"TODO:BYTES")) ; - packed_internal_operation = (fun _visitor state op -> assert_nostate state; false , (ignore op;"TODO:PACKED_INTERNAL_OPERATION")) ; - expression_variable = (fun _visitor state ev -> assert_nostate state; false , (ignore ev;"TODO:EXPRESSION_VARIABLE")) ; - constructor' = (fun _visitor state c -> assert_nostate state; false , (ignore c;"TODO:CONSTRUCTOR'")) ; - 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")) ; - label_map = (fun _visitor continue state lmap -> assert_nostate state; false , (ignore (continue,lmap);"TODO:label_map")) ; - list = (fun _visitor continue state lst -> - assert_nostate state; - false , "[ " ^ String.concat " ; " (List.map snd @@ List.map (continue nostate) lst) ^ " ]") ; - location_wrap = (fun _visitor continue state lwrap -> assert_nostate state; false , (ignore (continue,lwrap);"TODO:location_wrap")) ; - list_ne = (fun _visitor continue state list_ne -> assert_nostate state; false , (ignore (continue,list_ne);"TODO:location_wrap")) ; - } in - let (_ , state) = fold__program op nostate p in - Printf.printf "%s" state +let needs_parens = { + generic = (fun state info -> + match info.node_instance.instance_kind with + | RecordInstance _ -> false + | VariantInstance _ -> true + | PolyInstance { poly =_; arguments=_; poly_continue } -> + (poly_continue state) + ); + type_variable = (fun _ _ _ -> false) ; + bool = (fun _ _ _ -> false) ; + int = (fun _ _ _ -> false) ; + string = (fun _ _ _ -> false) ; + bytes = (fun _ _ _ -> false) ; + packed_internal_operation = (fun _ _ _ -> false) ; + expression_variable = (fun _ _ _ -> false) ; + constructor' = (fun _ _ _ -> false) ; + location = (fun _ _ _ -> false) ; + label = (fun _ _ _ -> false) ; + ast_core_type_expression = (fun _ _ _ -> true) ; + constructor_map = (fun _ _ _ _ -> false) ; + label_map = (fun _ _ _ _ -> false) ; + list = (fun _ _ _ _ -> false) ; + location_wrap = (fun _ _ _ _ -> false) ; + list_ne = (fun _ _ _ _ -> false) ; + option = (fun _visitor _continue _state o -> + match o with None -> false | Some _ -> true) ; + } + +let op ppf = { + generic = (fun () info -> + match info.node_instance.instance_kind with + | RecordInstance { fields } -> + let aux ppf (fld : 'x Adt_info.ctor_or_field_instance) = + fprintf ppf "%s = %a" fld.cf.name (fun _ppf -> fld.cf_continue) () in + fprintf ppf "{ %a }" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) fields + | VariantInstance { constructor ; _ } -> + if constructor.cf_new_fold needs_parens false + 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 diff --git a/src/stages/4-ast_typed/types.ml b/src/stages/4-ast_typed/types.ml index 28ffb6644..c2d06fa15 100644 --- a/src/stages/4-ast_typed/types.ml +++ b/src/stages/4-ast_typed/types.ml @@ -21,6 +21,7 @@ type type_constant = type te_cmap = type_expression constructor_map and te_lmap = type_expression label_map +and type_meta = ast_core_type_expression option and type_content = | T_sum of te_cmap diff --git a/src/stages/4-ast_typed/types_utils.ml b/src/stages/4-ast_typed/types_utils.ml index 24835256c..ffb1b683d 100644 --- a/src/stages/4-ast_typed/types_utils.ml +++ b/src/stages/4-ast_typed/types_utils.ml @@ -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 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 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 let%bind (state , l) = List.fold_left aux (ok (state , [])) l in 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) diff --git a/src/stages/adt_generator/generator.raku b/src/stages/adt_generator/generator.raku index f3938f900..6fc05e73b 100644 --- a/src/stages/adt_generator/generator.raku +++ b/src/stages/adt_generator/generator.raku @@ -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 return v = Simple_utils.Trace.ok v;;"; say "open $moduleName;;"; -say "module Adt_info = Adt_generator.Generic.Adt_info;;"; say ""; 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 "type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;;"; say ""; -say "type 'state fold_config ="; +say "type ('state , 'adt_info_node_instance_info) _fold_config ="; 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 '') for $adts.map({ $_ })[*;*].grep({$_ && $_ ne ''}).map({$_}).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 for $adts.grep({$_ ne $record && $_ ne $variant}).map({$_}).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 "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 'type blahblah = {'; @@ -256,7 +261,8 @@ for $adts.list -> $t say ""; say "let continue_info__$t__$c : type qstate . blahblah -> qstate fold_config -> {$c || 'unit'} -> qstate Adt_info.ctor_or_field_instance = fun blahblah visitor x -> \{"; say " cf = info__$t__$c;"; - say " cf_continue = fun state -> blahblah.fold__$t__$c blahblah visitor state x;"; + say " cf_continue = (fun state -> blahblah.fold__$t__$c blahblah visitor state x);"; + say " cf_new_fold = (fun visitor state -> blahblah.fold__$t__$c blahblah visitor state x);"; say '};;'; say ""; } say "(* info for node $t *)"; @@ -461,8 +467,8 @@ say '};;'; say ""; for $adts.list -> $t -{ say "let with__$t : _ = (fun node__$t op -> \{ op with $t = \{ op.$t with node__$t \} \});;"; - say "let with__$t__pre_state : _ = (fun node__$t__pre_state op -> \{ op with $t = \{ op.$t with node__$t__pre_state \} \});;"; - say "let with__$t__post_state : _ = (fun node__$t__post_state op -> \{ op with $t = \{ op.$t with node__$t__post_state \} \});;"; +{ say "let with__$t : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t op -> \{ op with $t = \{ op.$t with node__$t \} \});;"; + say "let with__$t__pre_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t__pre_state op -> \{ op with $t = \{ op.$t with node__$t__pre_state \} \});;"; + say "let with__$t__post_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t__post_state op -> \{ op with $t = \{ op.$t with node__$t__post_state \} \});;"; for $t.list -> $c - { say "let with__$t__$c : _ = (fun $t__$c op -> \{ op with $t = \{ op.$t with $t__$c \} \});;"; } } + { say "let with__$t__$c : _ -> _ fold_map_config -> _ fold_map_config = (fun $t__$c op -> \{ op with $t = \{ op.$t with $t__$c \} \});;"; } } diff --git a/src/stages/adt_generator/generic.ml b/src/stages/adt_generator/generic.ml index 7defcfbb2..c4f28821a 100644 --- a/src/stages/adt_generator/generic.ml +++ b/src/stages/adt_generator/generic.ml @@ -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 = | Record | Variant @@ -39,10 +39,11 @@ module Adt_info = struct and 'state ctor_or_field_instance = { 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; declaration_name : string; @@ -50,10 +51,10 @@ module Adt_info = struct } (* TODO: rename things a bit in this file. *) - type adt = node list - type 'state node_instance_info = { + and adt = node list + and 'state node_instance_info = { adt : adt ; 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 diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index 79fab238f..3b1e2441e 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -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_contract te -> Format.asprintf "Contract (%a)" f te in - fprintf ppf "(TO_%s)" s + fprintf ppf "(type_operator: %s)" s end diff --git a/src/test/adt_generator/use_a_fold.ml b/src/test/adt_generator/use_a_fold.ml index f49e42c7d..8cfd5aa3a 100644 --- a/src/test/adt_generator/use_a_fold.ml +++ b/src/test/adt_generator/use_a_fold.ml @@ -71,7 +71,7 @@ let () = match info.node_instance.instance_kind with | 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) ^ " }" - | 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 | true, arg -> true, name ^ " (" ^ arg ^ ")" | false, arg -> true, name ^ " " ^ arg) diff --git a/src/test/contracts/single_record_item.religo b/src/test/contracts/single_record_item.religo new file mode 100644 index 000000000..9a7216624 --- /dev/null +++ b/src/test/contracts/single_record_item.religo @@ -0,0 +1,5 @@ +type p = {x: int} + +let o = (p: int): p => { + x: p +} \ No newline at end of file diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 408f86d4c..ba51a7d3d 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -2328,6 +2328,10 @@ let tuple_list_religo () : unit result = let%bind _ = retype_file "./contracts/tuple_list.religo" in 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%bind program = type_file "./contracts/loop_bugs.ligo" 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 "loop_bugs (ligo)" loop_bugs_ligo ; test "tuple_list (religo)" tuple_list_religo ; + test "single_record_expr (religo)" single_record_expr_religo ; ] diff --git a/vendors/Preprocessor/.gitignore b/vendors/Preprocessor/.gitignore new file mode 100644 index 000000000..614b62428 --- /dev/null +++ b/vendors/Preprocessor/.gitignore @@ -0,0 +1 @@ +/Preprocessor.install