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

Merge branch 'feature/new-typer-rough-cleanup' into 'dev'

Browse Source 
Rough cleanup of the new typer

See merge request ligolang/ligo!561
This commit is contained in:
Suzanne Dupéron 2020-04-14 11:10:26 +00:00
commit 741bfcf9b4
18 changed files with 1154 additions and 1235 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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