diff --git a/gitlab-pages/docs/api/cheat-sheet.md b/gitlab-pages/docs/api/cheat-sheet.md index 920ae6376..8f8baebdb 100644 --- a/gitlab-pages/docs/api/cheat-sheet.md +++ b/gitlab-pages/docs/api/cheat-sheet.md @@ -4,6 +4,9 @@ title: Cheat Sheet ---
+ @@ -67,11 +70,42 @@ title: Cheat Sheet |Variants|
type action =
| Increment of int
| Decrement of int
| |Variant *(pattern)* matching|
let a: action = Increment 5
match a with
| Increment n -> n + 1
| Decrement n -> n - 1
| |Records|
type person = {
  age: int ;
  name: string ;
}

let john : person = {
  age = 18;
  name = "John Doe";
}

let name: string = john.name
| -|Maps|
type prices = (nat, tez) map

let prices : prices = Map.literal [
  (10n, 60mutez);
  (50n, 30mutez);
  (100n, 10mutez)
]

let price: tez option = Map.find 50n prices

let prices: prices = Map.update 200n 5mutez prices
| +|Maps|
type prices = (nat, tez) map

let prices : prices = Map.literal [
  (10n, 60mutez);
  (50n, 30mutez);
  (100n, 10mutez)
]

let price: tez option = Map.find_opt 50n prices

let prices: prices = Map.update 200n (Some 5mutez) prices
| |Contracts & Accounts|
let destination_address : address = "tz1..."
let contract : unit contract = 
 Operation.get_contract destination_address
| -|Transactions|
let payment : operation = 
 Operation.transaction (unit, receiver, amount)
| +|Transactions|
let payment : operation = 
 Operation.transaction unit amount receiver
| |Exception/Failure|`failwith("Your descriptive error message for the user goes here.")`| + + +|Primitive |Example| +|--- |---| +|Strings | `"Tezos"`| +|Characters | `"t"`| +|Integers | `42`, `7`| +|Natural numbers | `42n`, `7n`| +|Unit| `unit`| +|Boolean|
let has_drivers_license: bool = false;
let adult: bool = true;
| +|Boolean Logic|
(not true) = false = (false && true) = (false || false)
| +|Mutez (micro tez)| `42mutez`, `7mutez` | +|Address | `("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address)`, `("KT1JepfBfMSqkQyf9B1ndvURghGsSB8YCLMD": address)`| +|Addition |`3 + 4`, `3n + 4n`| +|Multiplication & Division| `3 * 4`, `3n * 4n`, `10 / 5`, `10n / 5n`| +|Modulo| `10 mod 3`| +|Tuples| 
type name = (string, string);
let winner: name = ("John", "Doe");
let first_name: string = winner[0];
let last_name: string = winner[1];
| +|Types|`type age = int;`, `type name = string;` | +|Includes|```#include "library.mligo"```| +|Functions |
let add = (a: int, b: int) : int => a + b;
| +| If Statement | 
let new_id: int = if (age < 16) {
  failwith("Too young to drive."); 
 } else { prev_id + 1; }
| +|Options|
type middle_name = option(string);
let middle_name : middle_name = Some("Foo");
let middle_name : middle_name = None;
| +|Variable Binding | ```let age: int = 5;```| +|Type Annotations| ```("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address)```| +|Variants|
type action =
| Increment(int)
| Decrement(int);
| +|Variant *(pattern)* matching|
let a: action = Increment(5);
switch(a) {
| Increment(n) => n + 1
| Decrement(n) => n - 1;
 }
| +|Records|
type person = {
  age: int,
  name: string
}

let john : person = {
  age: 18,
  name: "John Doe"
};

let name: string = john.name;
| +|Maps|
type prices = map(nat, tez);

let prices : prices = Map.literal([
  (10n, 60mutez),
  (50n, 30mutez),
  (100n, 10mutez)
]);

let price: option(tez) = Map.find_opt(50n, prices);

let prices: prices = Map.update(200n, Some (5mutez), prices);
| +|Contracts & Accounts|
let destination_address : address = "tz1...";
let contract : contract(unit) = 
 Operation.get_contract(destination_address);
| +|Transactions|
let payment : operation = 
 Operation.transaction (unit, amount, receiver);
| +|Exception/Failure|`failwith("Your descriptive error message for the user goes here.");`| diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml index 67429e040..511831b28 100644 --- a/src/bin/expect_tests/typer_error_tests.ml +++ b/src/bin/expect_tests/typer_error_tests.ml @@ -41,7 +41,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"} + ligo: in file "error_typer_3.mligo", line 3, characters 34-53. different number of arguments to type constructors: Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the TC_tuple type constructor, but they have 3 and 2 arguments, respectively) {"a":"(TO_tuple[int , string , bool])","b":"(TO_tuple[int , string])","op":"TC_tuple","len_a":"3","len_b":"2"} If you're not sure how to fix this error, you can diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml index 4d99be97a..8b95d9a2d 100644 --- a/src/main/compile/of_mini_c.ml +++ b/src/main/compile/of_mini_c.ml @@ -9,15 +9,13 @@ let compile_contract : expression -> Compiler.compiled_expression result = fun e let%bind body = Compiler.Program.translate_function_body body [] input_ty in let expr = Self_michelson.optimize body in let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in - let open! Compiler.Program in - ok { expr_ty ; expr } + ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression) let compile_expression : expression -> Compiler.compiled_expression result = fun e -> let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in let expr = Self_michelson.optimize expr in let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in - let open! Compiler.Program in - ok { expr_ty ; expr } + ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression) let aggregate_and_compile = fun program form -> let%bind aggregated = aggregate_entry program form in diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml index 243ecd586..6d98bccc5 100644 --- a/src/main/compile/of_simplified.ml +++ b/src/main/compile/of_simplified.ml @@ -7,14 +7,15 @@ let compile (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solv let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression) : (Ast_typed.value * Typer.Solver.state) result = - Typer.type_expression env state ae + let () = Typer.Solver.discard_state state in + Typer.type_expression_subst env state ae let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result = let name = Var.of_name entry_point in let entry_point_var : Ast_simplified.expression = { expression = Ast_simplified.E_variable name ; location = Virtual "generated entry-point variable" } in - let applied : Ast_simplified.expression = + let applied : Ast_simplified.expression = { expression = Ast_simplified.E_application (entry_point_var, param) ; location = Virtual "generated application" } in ok applied diff --git a/src/main/compile/of_typed.ml b/src/main/compile/of_typed.ml index a69f32c9d..c1b2930ef 100644 --- a/src/main/compile/of_typed.ml +++ b/src/main/compile/of_typed.ml @@ -14,7 +14,7 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As match entry_point.type_annotation.type_value' with | T_arrow (args,_) -> ( match args.type_value' with - | T_tuple [param_exp;storage_exp] -> ( + | T_operator (TC_tuple [param_exp;storage_exp]) -> ( match c with | Check_parameter -> assert_type_value_eq (param_exp, param.type_annotation) | Check_storage -> assert_type_value_eq (storage_exp, param.type_annotation) @@ -24,4 +24,4 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As | _ -> dummy_fail ) let pretty_print ppf program = - Ast_typed.PP.program ppf program \ No newline at end of file + Ast_typed.PP.program ppf program diff --git a/src/passes/1-parser/cameligo/AST.ml b/src/passes/1-parser/cameligo/AST.ml index d00cf9cd7..551d82077 100644 --- a/src/passes/1-parser/cameligo/AST.ml +++ b/src/passes/1-parser/cameligo/AST.ml @@ -333,10 +333,15 @@ and update = { lbrace : lbrace; record : path; kwd_with : kwd_with; - updates : record reg; + updates : field_path_assign reg ne_injection reg; rbrace : rbrace; } +and field_path_assign = { + field_path : (field_name, dot) nsepseq; + assignment : equal; + field_expr : expr +} and path = Name of variable | Path of projection reg diff --git a/src/passes/1-parser/cameligo/Parser.mly b/src/passes/1-parser/cameligo/Parser.mly index e6cc6f903..8becc88f5 100644 --- a/src/passes/1-parser/cameligo/Parser.mly +++ b/src/passes/1-parser/cameligo/Parser.mly @@ -627,7 +627,7 @@ record_expr: in {region; value} } update_record: - "{" path "with" sep_or_term_list(field_assignment,";") "}" { + "{" path "with" sep_or_term_list(field_path_assignment,";") "}" { let region = cover $1 $5 in let ne_elements, terminator = $4 in let value = { @@ -641,6 +641,14 @@ update_record: rbrace = $5} in {region; value} } +field_path_assignment : + nsepseq(field_name,".") "=" expr { + let region = cover (nsepseq_to_region (fun x -> x.region) $1) (expr_to_region $3) in + let value = {field_path = $1; + assignment = $2; + field_expr = $3} + in {region; value}} + field_assignment: field_name "=" expr { let start = $1.region in diff --git a/src/passes/1-parser/cameligo/ParserLog.ml b/src/passes/1-parser/cameligo/ParserLog.ml index e0b7fd09b..aa847e245 100644 --- a/src/passes/1-parser/cameligo/ParserLog.ml +++ b/src/passes/1-parser/cameligo/ParserLog.ml @@ -188,7 +188,7 @@ and print_update state {value; _} = print_token state lbrace "{"; print_path state record; print_token state kwd_with "with"; - print_record_expr state updates; + print_ne_injection state print_field_path_assign updates; print_token state rbrace "}" and print_path state = function @@ -513,6 +513,12 @@ and print_field_assign state {value; _} = print_token state assignment "="; print_expr state field_expr +and print_field_path_assign state {value; _} = + let {field_path; assignment; field_expr} = value in + print_nsepseq state "." print_var field_path; + print_token state assignment "="; + print_expr state field_expr + and print_sequence state seq = print_injection state print_expr seq @@ -905,7 +911,7 @@ and pp_projection state proj = and pp_update state update = pp_path state update.record; - pp_ne_injection pp_field_assign state update.updates.value + pp_ne_injection pp_field_path_assign state update.updates.value and pp_path state = function Name name -> @@ -928,6 +934,12 @@ and pp_field_assign state {value; _} = pp_ident (state#pad 2 0) value.field_name; pp_expr (state#pad 2 1) value.field_expr +and pp_field_path_assign state {value; _} = + pp_node state ""; + let path = Utils.nsepseq_to_list value.field_path in + List.iter (pp_ident (state#pad 2 0)) path; + pp_expr (state#pad 2 1) value.field_expr + and pp_constr_expr state = function ENone region -> pp_loc_node state "ENone" region diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml index 5f95dc3e5..27dfdd585 100644 --- a/src/passes/1-parser/pascaligo/AST.ml +++ b/src/passes/1-parser/pascaligo/AST.ml @@ -577,7 +577,13 @@ and projection = { and update = { record : path; kwd_with : kwd_with; - updates : record reg; + updates : field_path_assign reg ne_injection reg +} + +and field_path_assign = { + field_path : (field_name, dot) nsepseq; + equal : equal; + field_expr : expr } and selection = diff --git a/src/passes/1-parser/pascaligo/Parser.mly b/src/passes/1-parser/pascaligo/Parser.mly index 9b41ba242..55ac2262e 100644 --- a/src/passes/1-parser/pascaligo/Parser.mly +++ b/src/passes/1-parser/pascaligo/Parser.mly @@ -937,7 +937,7 @@ record_expr: in {region; value} } update_record: - path "with" ne_injection("record",field_assignment){ + path "with" ne_injection("record",field_path_assignment){ let region = cover (path_to_region $1) $3.region in let value = { record = $1; @@ -954,6 +954,14 @@ field_assignment: field_expr = $3} in {region; value} } +field_path_assignment: + nsepseq(field_name,".") "=" expr { + let region = cover (nsepseq_to_region (fun x -> x.region) $1) (expr_to_region $3) + and value = {field_path = $1; + equal = $2; + field_expr = $3} + in {region; value} } + fun_call: fun_name arguments { let region = cover $1.region $2.region diff --git a/src/passes/1-parser/pascaligo/ParserLog.ml b/src/passes/1-parser/pascaligo/ParserLog.ml index 06c42718a..d423006f2 100644 --- a/src/passes/1-parser/pascaligo/ParserLog.ml +++ b/src/passes/1-parser/pascaligo/ParserLog.ml @@ -603,11 +603,18 @@ and print_field_assign state {value; _} = print_token state equal "="; print_expr state field_expr -and print_update_expr state {value; _} = +and print_field_path_assign state {value; _} = + let {field_path; equal; field_expr} = value in + print_nsepseq state "field_path" print_var field_path; + print_token state equal "="; + print_expr state field_expr + +and print_update_expr state {value; _} = let {record; kwd_with; updates} = value in print_path state record; print_token state kwd_with "with"; - print_record_expr state updates + print_ne_injection state "updates field" print_field_path_assign updates + and print_projection state {value; _} = let {struct_name; selector; field_path} = value in @@ -1215,7 +1222,7 @@ and pp_projection state proj = and pp_update state update = pp_path state update.record; - pp_ne_injection pp_field_assign state update.updates.value + pp_ne_injection pp_field_path_assign state update.updates.value and pp_selection state = function FieldName name -> @@ -1320,6 +1327,12 @@ and pp_field_assign state {value; _} = pp_ident (state#pad 2 0) value.field_name; pp_expr (state#pad 2 1) value.field_expr +and pp_field_path_assign state {value; _} = + pp_node state ""; + let path = Utils.nsepseq_to_list value.field_path in + List.iter (pp_ident (state#pad 2 0)) path; + pp_expr (state#pad 2 1) value.field_expr + and pp_map_patch state patch = pp_path (state#pad 2 0) patch.path; pp_ne_injection pp_binding state patch.map_inj.value diff --git a/src/passes/1-parser/reasonligo/Parser.mly b/src/passes/1-parser/reasonligo/Parser.mly index 12f2e7f42..142a29313 100644 --- a/src/passes/1-parser/reasonligo/Parser.mly +++ b/src/passes/1-parser/reasonligo/Parser.mly @@ -812,7 +812,7 @@ path : | projection { Path $1} update_record : - "{""..."path "," sep_or_term_list(field_assignment,",") "}" { + "{""..."path "," sep_or_term_list(field_path_assignment,",") "}" { let region = cover $1 $6 in let ne_elements, terminator = $5 in let value = { @@ -873,3 +873,21 @@ field_assignment: assignment = $2; field_expr = $3} in {region; value} } + +field_path_assignment: + field_name { + let value = { + field_path = ($1,[]); + assignment = ghost; + field_expr = EVar $1 } + in {$1 with value} + } +| nsepseq(field_name,".") ":" expr { + let start = nsepseq_to_region (fun x -> x.region) $1 in + let stop = expr_to_region $3 in + let region = cover start stop in + let value = { + field_path = $1; + assignment = $2; + field_expr = $3} + in {region; value} } diff --git a/src/passes/2-simplify/cameligo.ml b/src/passes/2-simplify/cameligo.ml index 917d001bf..dcbf94693 100644 --- a/src/passes/2-simplify/cameligo.ml +++ b/src/passes/2-simplify/cameligo.ml @@ -246,7 +246,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result | [hd] -> simpl_type_expression hd | lst -> let%bind lst = bind_map_list simpl_type_expression lst in - ok @@ make_t @@ T_tuple lst + ok @@ make_t @@ T_operator (TC_tuple lst) let rec simpl_expression : Raw.expr -> expr result = fun t -> @@ -291,14 +291,23 @@ let rec simpl_expression : | _ -> e_accessor (e_variable (Var.of_name name)) path in let updates = u.updates.value.ne_elements in let%bind updates' = - let aux (f:Raw.field_assign Raw.reg) = + let aux (f:Raw.field_path_assign Raw.reg) = let (f,_) = r_split f in let%bind expr = simpl_expression f.field_expr in - ok (f.field_name.value, expr) + ok ( List.map (fun (x: _ Raw.reg) -> x.value) (npseq_to_list f.field_path), expr) in bind_map_list aux @@ npseq_to_list updates in - return @@ e_update ~loc record updates' + let aux ur (path, expr) = + let rec aux record = function + | [] -> failwith "error in parsing" + | hd :: [] -> ok @@ e_update ~loc record hd expr + | hd :: tl -> + let%bind expr = (aux (e_accessor ~loc record [Access_record hd]) tl) in + ok @@ e_update ~loc record hd expr + in + aux ur path in + bind_fold_list aux record updates' in trace (simplifying_expr t) @@ diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 113ab7c63..e8c72ce9a 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -267,7 +267,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result | [hd] -> simpl_type_expression hd | lst -> let%bind lst = bind_list @@ List.map simpl_type_expression lst in - ok @@ make_t @@ T_tuple lst + ok @@ make_t @@ T_operator (TC_tuple lst) let simpl_projection : Raw.projection Region.reg -> _ = fun p -> let (p' , loc) = r_split p in @@ -473,14 +473,23 @@ and simpl_update = fun (u:Raw.update Region.reg) -> | _ -> e_accessor (e_variable (Var.of_name name)) path in let updates = u.updates.value.ne_elements in let%bind updates' = - let aux (f:Raw.field_assign Raw.reg) = + let aux (f:Raw.field_path_assign Raw.reg) = let (f,_) = r_split f in let%bind expr = simpl_expression f.field_expr in - ok (f.field_name.value, expr) + ok ( List.map (fun (x: _ Raw.reg) -> x.value) (npseq_to_list f.field_path), expr) in bind_map_list aux @@ npseq_to_list updates in - ok @@ e_update ~loc record updates' + let aux ur (path, expr) = + let rec aux record = function + | [] -> failwith "error in parsing" + | hd :: [] -> ok @@ e_update ~loc record hd expr + | hd :: tl -> + let%bind expr = (aux (e_accessor ~loc record [Access_record hd]) tl) in + ok @@ e_update ~loc record hd expr + in + aux ur path in + bind_fold_list aux record updates' and simpl_logic_expression (t:Raw.logic_expr) : expression result = let return x = ok x in @@ -654,7 +663,7 @@ and simpl_fun_decl : let arguments_name = Var.of_name "arguments" in let%bind params = bind_map_list simpl_param lst in let (binder , input_type) = - let type_expression = T_tuple (List.map snd params) in + let type_expression = t_tuple (List.map snd params) in (arguments_name , type_expression) in let%bind tpl_declarations = let aux = fun i x -> @@ -673,8 +682,8 @@ and simpl_fun_decl : let aux prec cur = cur (Some prec) in bind_fold_right_list aux result body in let expression = - e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in - let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in + e_lambda ~loc binder (Some input_type) (Some output_type) result in + let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in ok ((Var.of_name fun_name.value, type_annotation), expression) ) ) @@ -708,7 +717,7 @@ and simpl_fun_expression : let arguments_name = Var.of_name "arguments" in let%bind params = bind_map_list simpl_param lst in let (binder , input_type) = - let type_expression = T_tuple (List.map snd params) in + let type_expression = t_tuple (List.map snd params) in (arguments_name , type_expression) in let%bind tpl_declarations = let aux = fun i x -> @@ -727,8 +736,8 @@ and simpl_fun_expression : let aux prec cur = cur (Some prec) in bind_fold_right_list aux result body in let expression = - e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in - let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in + e_lambda ~loc binder (Some (input_type)) (Some output_type) result in + let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in ok (type_annotation, expression) ) ) diff --git a/src/passes/3-self_ast_simplified/helpers.ml b/src/passes/3-self_ast_simplified/helpers.ml index fc4346147..47b06e9b9 100644 --- a/src/passes/3-self_ast_simplified/helpers.ml +++ b/src/passes/3-self_ast_simplified/helpers.ml @@ -41,13 +41,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini let%bind res = bind_fold_lmap aux (ok init') m in ok res ) - | E_update {record;updates} -> ( + | E_update {record;update=(_,expr)} -> ( let%bind res = self init' record in - let aux res (_, expr) = - let%bind res = fold_expression self res expr in - ok res - in - let%bind res = bind_fold_list aux res updates in + let%bind res = fold_expression self res expr in ok res ) | E_let_in { binder = _ ; rhs ; result } -> ( @@ -140,10 +136,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e -> let%bind m' = bind_map_lmap self m in return @@ E_record m' ) - | E_update {record; updates} -> ( + | E_update {record; update=(l,expr)} -> ( let%bind record = self record in - let%bind updates = bind_map_list (fun(l,e) -> let%bind e = self e in ok (l,e)) updates in - return @@ E_update {record;updates} + let%bind expr = self expr in + return @@ E_update {record;update=(l,expr)} ) | E_constructor (name , e) -> ( let%bind e' = self e in diff --git a/src/passes/4-typer-new/PP.ml b/src/passes/4-typer-new/PP.ml new file mode 100644 index 000000000..a8829aef3 --- /dev/null +++ b/src/passes/4-typer-new/PP.ml @@ -0,0 +1,54 @@ +open Solver +open Format + +let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf -> + function + |SC_Constructor { tv; c_tag; tv_list=_ } -> + let ct = match c_tag with + | Solver.Core.C_arrow -> "arrow" + | Solver.Core.C_option -> "option" + | Solver.Core.C_tuple -> "tuple" + | Solver.Core.C_record -> failwith "record" + | Solver.Core.C_variant -> failwith "variant" + | Solver.Core.C_map -> "map" + | Solver.Core.C_big_map -> "big_map" + | Solver.Core.C_list -> "list" + | Solver.Core.C_set -> "set" + | Solver.Core.C_unit -> "unit" + | Solver.Core.C_bool -> "bool" + | Solver.Core.C_string -> "string" + | Solver.Core.C_nat -> "nat" + | Solver.Core.C_mutez -> "mutez" + | Solver.Core.C_timestamp -> "timestamp" + | Solver.Core.C_int -> "int" + | Solver.Core.C_address -> "address" + | Solver.Core.C_bytes -> "bytes" + | Solver.Core.C_key_hash -> "key_hash" + | Solver.Core.C_key -> "key" + | Solver.Core.C_signature -> "signature" + | Solver.Core.C_operation -> "operation" + | Solver.Core.C_contract -> "contract" + | Solver.Core.C_chain_id -> "chain_id" + in + fprintf ppf "CTOR %a %s()" Var.pp tv ct + |SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b + |SC_Poly _ -> fprintf ppf "Poly" + |SC_Typeclass _ -> fprintf ppf "TC" + +let all_constraints ppf ac = + fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac + +let aliases ppf (al : unionfind) = + fprintf ppf "ALIASES %a" UF.print al + +let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs -> + let { all_constraints = a ; aliases = b ; _ } = structured_dbs in + fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b + +let already_selected : _ -> already_selected -> unit = fun ppf already_selected -> + let _ = already_selected in + fprintf ppf "ALREADY_SELECTED" + +let state : _ -> state -> unit = fun ppf state -> + let { structured_dbs=a ; already_selected=b } = state in + fprintf ppf "STATE %a %a" structured_dbs a already_selected b diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml index 2adac9659..4f9c96388 100644 --- a/src/passes/4-typer-new/solver.ml +++ b/src/passes/4-typer-new/solver.ml @@ -34,8 +34,6 @@ module Wrap = struct let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te -> match te.type_value' with - | T_tuple types -> - P_constant (C_tuple, List.map type_expression_to_type_value types) | T_sum kvmap -> P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap) | T_record kvmap -> @@ -64,21 +62,20 @@ module Wrap = struct 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_list l -> (C_list, [l]) - | TC_contract c -> (C_contract, [c]) + | 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_list l -> (C_list, [l]) + | TC_contract c -> (C_contract, [c]) + | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ]) + | TC_tuple lst -> (C_tuple, lst) ) 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_expression' with - | T_tuple types -> - P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types) | T_sum kvmap -> P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap) | T_record kvmap -> @@ -96,12 +93,14 @@ module Wrap = struct 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_contract c -> (C_contract, [c]) + | 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_contract c -> (C_contract, [c]) + | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ]) + | TC_tuple lst -> (C_tuple, lst) ) in P_constant (csttag, List.map type_expression_to_type_value_copypasted args) @@ -350,7 +349,7 @@ end module TypeVariable = struct type t = Core.type_variable - let compare a b= Var.compare a b + let compare a b = Var.compare a b let to_string = (fun s -> Format.asprintf "%a" Var.pp s) end @@ -475,44 +474,69 @@ module UnionFindWrapper = struct in let dbs = { dbs with grouped_by_variable } in dbs - let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs = + + let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs = fun variable_a variable_b dbs -> + (* get old representant for variable_a *) let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in let dbs = { dbs with aliases } in + (* get old representant for variable_b *) let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in let dbs = { dbs with aliases } in - let default d = function None -> d | Some y -> y in - let get_constraints ab = - TypeVariableMap.find_opt ab dbs.grouped_by_variable - |> default { constructor = [] ; poly = [] ; tc = [] } in - let constraints_a = get_constraints variable_repr_a in - let constraints_b = get_constraints variable_repr_b in - let all_constraints = { - constructor = constraints_a.constructor @ constraints_b.constructor ; - poly = constraints_a.poly @ constraints_b.poly ; - tc = constraints_a.tc @ constraints_b.tc ; - } in - let grouped_by_variable = - TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in - let dbs = { dbs with grouped_by_variable} in - let grouped_by_variable = - TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in - let dbs = { dbs with grouped_by_variable} in - dbs + + (* alias variable_a and variable_b together *) + let aliases = UF.alias variable_a variable_b dbs.aliases in + let dbs = { dbs with aliases } in + + (* Replace the two entries in grouped_by_variable by a single one *) + ( + let get_constraints ab = + match TypeVariableMap.find_opt ab dbs.grouped_by_variable with + | Some x -> x + | None -> { constructor = [] ; poly = [] ; tc = [] } in + let constraints_a = get_constraints variable_repr_a in + let constraints_b = get_constraints variable_repr_b in + let all_constraints = { + constructor = constraints_a.constructor @ constraints_b.constructor ; + poly = constraints_a.poly @ constraints_b.poly ; + tc = constraints_a.tc @ constraints_b.tc ; + } in + let grouped_by_variable = + TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in + let dbs = { dbs with grouped_by_variable} in + let grouped_by_variable = + TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in + let dbs = { dbs with grouped_by_variable} in + dbs + ) end (* sub-sub component: constraint normalizer: remove dupes and give structure * right now: union-find of unification vars * later: better database-like organisation of knowledge *) -(* Each normalizer returns a *) -(* If implemented in a language with decent sets, should be 'b set not 'b list. *) +(* Each normalizer returns an updated database (after storing the + incoming constraint) and a list of constraints, used when the + normalizer rewrites the constraints e.g. into simpler ones. *) +(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *) type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list) +(** Updates the dbs.all_constraints field when new constraints are + discovered. + + This field contains a list of all the constraints, without any form of + grouping or sorting. *) let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> ({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint]) +(** Updates the dbs.grouped_by_variable field when new constraints are + discovered. + + This field contains a map from type variables to lists of + constraints that are related to that variable (in other words, the + key appears in the equation). + *) let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> let store_constraint tvars constraints = @@ -520,16 +544,18 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si UnionFindWrapper.add_constraints_related_to tvar constraints dbs in List.fold_left aux dbs tvars in - let merge_constraints a b = - UnionFindWrapper.merge_variables a b dbs in let dbs = match new_constraint with SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []} | SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]} | SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []} - | SC_Alias (a , b) -> merge_constraints a b + | SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs in (dbs , [new_constraint]) -(* Stores the first assinment ('a = ctor('b, …)) seen *) +(** Stores the first assinment ('a = ctor('b, …)) that is encountered. + + Subsequent ('a = ctor('b2, …)) with the same 'a are ignored. + + TOOD: are we checking somewhere that 'b … = 'b2 … ? *) let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> match new_constraint with @@ -540,9 +566,14 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor | _ -> (dbs , [new_constraint]) +(** Evaluates a type-leval application. For now, only supports + immediate beta-reduction at the root of the type. *) let type_level_eval : type_value -> type_value * type_constraint list = fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv +(** Checks that a type-level application has been fully reduced. For + now, only some simple cases like applications of `forall` + failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *) @@ -552,6 +583,14 @@ let check_applied ((reduced, _new_constraints) as x) = (* TODO: at some point there may be uses of named type aliases (type foo = int; let x : foo = 42). These should be inlined. *) +(** This function converts constraints from type_constraint to + type_constraint_simpl. The former has more possible cases, and the + latter uses a more minimalistic constraint language. + + It does not modify the dbs, and only rewrites the constraint + + TODO: update the code to show that the dbs are always copied as-is + *) let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer = fun dbs new_constraint -> let insert_fresh a b = diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml index 537a4c485..ba9e10bd0 100644 --- a/src/passes/4-typer-new/typer.ml +++ b/src/passes/4-typer-new/typer.ml @@ -334,9 +334,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = let%bind a' = evaluate_type e a in let%bind b' = evaluate_type e b in return (T_arrow (a', b')) - | T_tuple lst -> - let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - return (T_tuple lst') | T_sum m -> let aux k v prev = let%bind prev' = prev in @@ -382,6 +379,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = | TC_contract c -> let%bind c = evaluate_type e c in ok @@ O.TC_contract c + | TC_arrow ( arg , ret ) -> + let%bind arg' = evaluate_type e arg in + let%bind ret' = evaluate_type e ret in + ok @@ O.TC_arrow ( arg' , ret' ) + | TC_tuple lst -> + let%bind lst' = bind_map_list (evaluate_type e) lst in + ok @@ O.TC_tuple lst' in return (T_operator (opt)) @@ -469,10 +473,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e return_wrapped (e_operation o) state @@ Wrap.literal (t_operation ()) ) | E_literal (Literal_unit) -> ( - return_wrapped (e_unit) state @@ Wrap.literal (t_unit ()) + return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ()) ) | E_skip -> ( - failwith "TODO: missing implementation for E_skip" + (* E_skip just returns unit *) + return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ()) ) (* | E_literal (Literal_string s) -> ( * L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ; @@ -516,7 +521,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e trace_option error @@ Environment.get_constructor c e in let%bind (expr' , state') = type_expression e state expr in - let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in return_wrapped (E_constructor (c , expr')) state' wrapped @@ -529,27 +533,22 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e let%bind (m' , state') = I.bind_fold_lmap aux (ok (I.LMap.empty , state)) m in let wrapped = Wrap.record (I.LMap.map get_type_annotation m') in return_wrapped (E_record m') state' wrapped - | E_update {record; updates} -> + | E_update {record; update=(k,expr)} -> let%bind (record, state) = type_expression e state record in - let aux (lst,state) (k, expr) = - let%bind (expr', state) = type_expression e state expr in - ok ((k,expr')::lst, state) - in - let%bind (updates, state) = bind_fold_list aux ([], state) updates in + let%bind (expr,state) = type_expression e state expr in let wrapped = get_type_annotation record in - let%bind wrapped = match wrapped.type_value' with - | T_record record -> - let aux (k, e) = + let%bind (wrapped,tv) = + match wrapped.type_value' with + | T_record record -> ( let field_op = I.LMap.find_opt k record in match field_op with + | Some tv -> ok (record,tv) | None -> failwith @@ Format.asprintf "field %a is not part of record" Stage_common.PP.label k - | Some tv -> O.assert_type_value_eq (tv, get_type_annotation e) - in - let%bind () = bind_iter_list aux updates in - ok (record) - | _ -> failwith "Update an expression which is not a record" + ) + | _ -> failwith "Update an expression which is not a record" in - return_wrapped (E_record_update (record, updates)) state (Wrap.record wrapped) + let%bind () = O.assert_type_value_eq (tv, get_type_annotation expr) in + return_wrapped (E_record_update (record, (k,expr))) state (Wrap.record wrapped) (* Data-structure *) (* @@ -937,9 +936,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result = (* Apply type_declaration on all the node of the AST_simplified from the root p *) -let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result = - let env = Ast_typed.Environment.full_empty in - let state = Solver.initial_state in +let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in let ds' = match d'_opt with @@ -954,51 +951,45 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p let () = ignore (env' , state') in ok (env', state', declarations) -(* module TSMap = TMap(Solver.TypeVariable) *) - -(* let c_tag_to_string : Solver.Core.constant_tag -> string = function - * | Solver.Core.C_arrow -> "arrow" - * | Solver.Core.C_option -> "option" - * | Solver.Core.C_tuple -> "tuple" - * | Solver.Core.C_record -> failwith "record" - * | Solver.Core.C_variant -> failwith "variant" - * | Solver.Core.C_map -> "map" - * | Solver.Core.C_big_map -> "big" - * | Solver.Core.C_list -> "list" - * | Solver.Core.C_set -> "set" - * | Solver.Core.C_unit -> "unit" - * | Solver.Core.C_bool -> "bool" - * | Solver.Core.C_string -> "string" - * | Solver.Core.C_nat -> "nat" - * | Solver.Core.C_mutez -> "mutez" - * | Solver.Core.C_timestamp -> "timestamp" - * | Solver.Core.C_int -> "int" - * | Solver.Core.C_address -> "address" - * | Solver.Core.C_bytes -> "bytes" - * | Solver.Core.C_key_hash -> "key_hash" - * | Solver.Core.C_key -> "key" - * | Solver.Core.C_signature -> "signature" - * | Solver.Core.C_operation -> "operation" - * | Solver.Core.C_contract -> "contract" - * | Solver.Core.C_chain_id -> "chain_id" *) - -let type_program (p : I.program) : (O.program * Solver.state) result = - let%bind (env, state, program) = type_program_returns_state p in +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%bind (env, state, program) = type_xyz_returns_state env_state_node in let subst_all = + let aliases = state.structured_dbs.aliases in let assignments = state.structured_dbs.assignments in - let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) = - let%bind p = p in - let Solver.{ tv ; c_tag ; tv_list } = expr in + let substs : variable: I.type_variable -> _ = fun ~variable -> + to_option @@ + let%bind root = + trace_option (simple_error (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@ + (* TODO: after upgrading UnionFind, this will be an option, not an exception. *) + try Some (Solver.UF.repr variable aliases) with Not_found -> None in + let%bind assignment = + trace_option (simple_error (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@ + (Solver.TypeVariableMap.find_opt root assignments) in + let Solver.{ tv ; c_tag ; tv_list } = assignment in let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in - Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in - (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *) - let p = Solver.TypeVariableMap.fold aux assignments (ok program) in + ok @@ expr + in + let p = apply_substs ~substs program in p in let%bind program = subst_all in let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (program, state) +let type_program (p : I.program) : (O.program * Solver.state) result = + let empty_env = Ast_typed.Environment.full_empty in + let empty_state = Solver.initial_state in + type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state + +let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.annotated_expression) Trace.result = + fun (env, state, e) -> + let%bind (e , state) = type_expression env state e in + ok (env, state, e) + +let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_value option) (e : I.expression) : (O.annotated_expression * Solver.state) result = + 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_annotated_expression type_expression_returns_state + (* TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity *) @@ -1026,9 +1017,6 @@ let type_program' : I.program -> O.program result = fun p -> let rec untype_type_expression (t:O.type_value) : (I.type_expression) result = (* TODO: or should we use t.simplified if present? *) let%bind t = match t.type_value' with - | O.T_tuple x -> - let%bind x' = bind_map_list untype_type_expression x in - ok @@ I.T_tuple x' | O.T_sum x -> let%bind x' = I.bind_map_cmap untype_type_expression x in ok @@ I.T_sum x' @@ -1064,6 +1052,13 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result = | O.TC_contract c-> let%bind c = untype_type_expression c in ok @@ I.TC_contract c + | O.TC_arrow ( arg , 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_tuple lst -> + let%bind lst' = bind_map_list untype_type_expression lst in + ok @@ I.TC_tuple lst' in ok @@ I.T_operator (type_name) in @@ -1139,14 +1134,11 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result = | E_record_accessor (r, Label s) -> let%bind r' = untype_expression r in return (e_accessor r' [Access_record s]) - | E_record_update (r, updates) -> + | E_record_update (r, (l,e)) -> let%bind r' = untype_expression r in - let aux (Label l,e) = - let%bind e = untype_expression e in - ok (l, e) - in - let%bind updates = bind_map_list aux updates in - return (e_update r' updates) + let%bind e = untype_expression e in + let Label l = l in + return (e_update r' l e) | E_map m -> let%bind m' = bind_map_list (bind_map_pair untype_expression) m in return (e_map m') diff --git a/src/passes/4-typer-new/typer.mli b/src/passes/4-typer-new/typer.mli index 07c28338b..379b31b1e 100644 --- a/src/passes/4-typer-new/typer.mli +++ b/src/passes/4-typer-new/typer.mli @@ -44,6 +44,7 @@ val type_declaration : environment -> Solver.state -> I.declaration -> (environm (* 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_value result val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result +val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result val type_constant : I.constant -> O.type_value list -> O.type_value option -> (O.constant * O.type_value) result (* val untype_type_value : O.type_value -> (I.type_expression) result diff --git a/src/passes/4-typer-old/typer.ml b/src/passes/4-typer-old/typer.ml index 1b9f90fbd..8c43ade15 100644 --- a/src/passes/4-typer-old/typer.ml +++ b/src/passes/4-typer-old/typer.ml @@ -327,9 +327,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = let%bind a' = evaluate_type e a in let%bind b' = evaluate_type e b in return (T_arrow (a', b')) - | T_tuple lst -> - let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in - return (T_tuple lst') | T_sum m -> let aux k v prev = let%bind prev' = prev in @@ -375,6 +372,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = | TC_contract c -> let%bind c = evaluate_type e c in ok @@ I.TC_contract c + | TC_arrow ( arg , ret ) -> + let%bind arg' = evaluate_type e arg in + let%bind ret' = evaluate_type e ret in + ok @@ I.TC_arrow ( arg' , ret' ) + | TC_tuple lst -> + let%bind lst' = bind_map_list (evaluate_type e) lst in + ok @@ I.TC_tuple lst' in return (T_operator (opt)) @@ -496,26 +500,22 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O. in let%bind m' = I.bind_fold_lmap aux (ok I.LMap.empty) m in return (E_record m') (t_record (I.LMap.map get_type_annotation m') ()) - | E_update {record; updates} -> + | E_update {record; update =(l,expr)} -> let%bind record = type_expression' e record in - let aux acc (k, expr) = - let%bind expr' = type_expression' e expr in - ok ((k,expr')::acc) - in - let%bind updates = bind_fold_list aux ([]) updates in + let%bind expr' = type_expression' e expr in let wrapped = get_type_annotation record in - let%bind () = match wrapped.type_value' with - | T_record record -> - let aux (k, e) = - let field_op = I.LMap.find_opt k record in + let%bind tv = + match wrapped.type_value' with + | T_record record -> ( + let field_op = I.LMap.find_opt l record in match field_op with - | None -> failwith @@ Format.asprintf "field %a is not part of record" Stage_common.PP.label k - | Some tv -> O.assert_type_value_eq (tv, get_type_annotation e) - in - bind_iter_list aux updates - | _ -> failwith "Update an expression which is not a record" + | Some tv -> ok (tv) + | None -> failwith @@ Format.asprintf "field %a is not part of record %a" Stage_common.PP.label l O.PP.type_value wrapped + ) + | _ -> failwith "Update an expression which is not a record" in - return (E_record_update (record, updates)) wrapped + let%bind () = O.assert_type_value_eq (tv, get_type_annotation expr') in + return (E_record_update (record, (l,expr'))) wrapped (* Data-structure *) | E_list lst -> let%bind lst' = bind_map_list (type_expression' e) lst in @@ -896,14 +896,11 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result = | E_record_accessor (r, Label s) -> let%bind r' = untype_expression r in return (e_accessor r' [Access_record s]) - | E_record_update (r, updates) -> + | E_record_update (r, (l,e)) -> let%bind r' = untype_expression r in - let aux (Label l,e) = - let%bind e = untype_expression e in - ok (l, e) - in - let%bind updates = bind_map_list aux updates in - return (e_update r' updates) + let%bind e = untype_expression e in + let Label l = l in + return (e_update r' l e) | E_map m -> let%bind m' = bind_map_list (bind_map_pair untype_expression) m in return (e_map m') diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index c59346c8b..8ab5576a0 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -10,5 +10,5 @@ module Solver = Typer_new.Solver (* Both the old typer and the new typer use the type environment = Environment.t let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program -let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression +let type_expression_subst = if use_new_typer then Typer_new.type_expression_subst else Typer_old.type_expression (* the old typer does not have unification variables that would need substitution, so no need to "subst" anything. *) let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression diff --git a/src/passes/4-typer/typer.mli b/src/passes/4-typer/typer.mli index cd11ec423..b7c410383 100644 --- a/src/passes/4-typer/typer.mli +++ b/src/passes/4-typer/typer.mli @@ -12,5 +12,5 @@ module Solver = Typer_new.Solver type environment = Environment.t val type_program : I.program -> (O.program * Solver.state) result -val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result +val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result val untype_expression : O.annotated_expression -> I.expression result diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml index 0cde2e3b5..86c921c70 100644 --- a/src/passes/6-transpiler/transpiler.ml +++ b/src/passes/6-transpiler/transpiler.ml @@ -146,6 +146,11 @@ let rec transpile_type (t:AST.type_value) : type_value result = | T_operator (TC_option o) -> let%bind o' = transpile_type o in ok (T_option o') + | T_operator (TC_arrow (param , result)) -> ( + let%bind param' = transpile_type param in + let%bind result' = transpile_type result in + ok (T_function (param', result')) + ) (* TODO hmm *) | T_sum m -> let node = Append_tree.of_list @@ kv_list_of_cmap m in @@ -173,7 +178,7 @@ let rec transpile_type (t:AST.type_value) : type_value result = ok (Some ann, a)) aux node in ok @@ snd m' - | T_tuple lst -> + | T_operator (TC_tuple lst) -> let node = Append_tree.of_list lst in let aux a b : type_value result = let%bind a = a in @@ -206,11 +211,11 @@ let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [ bind_fold_list aux (ty , []) lr_path in ok lst -let record_access_to_lr : type_value -> type_value AST.label_map -> string -> (type_value * [`Left | `Right]) list result = fun ty tym ind -> +let record_access_to_lr : type_value -> type_value AST.label_map -> label -> (type_value * [`Left | `Right]) list result = fun ty tym ind -> let tys = kv_list_of_lmap tym in let node_tv = Append_tree.of_list tys in let%bind path = - let aux (Label i , _) = i = ind in + let aux (Label i , _) = let Label ind = ind in i = ind in trace_option (corner_case ~loc:__LOC__ "record access leaf") @@ Append_tree.exists_path aux node_tv in let lr_path = List.map (fun b -> if b then `Right else `Left) path in @@ -320,7 +325,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re | E_tuple_accessor (tpl, ind) -> ( let%bind ty' = transpile_type tpl.type_annotation in let%bind ty_lst = - trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@ + trace_strong (corner_case ~loc:__LOC__ "transpiler: E_tuple_accessor: not a tuple") @@ get_t_tuple tpl.type_annotation in let%bind ty'_lst = bind_map_list transpile_type ty_lst in let%bind path = @@ -348,7 +353,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re trace_strong (corner_case ~loc:__LOC__ "record build") @@ Append_tree.fold_ne (transpile_annotated_expression) aux node ) - | E_record_accessor (record, Label property) -> + | E_record_accessor (record, property) -> let%bind ty' = transpile_type (get_type_annotation record) in let%bind ty_lmap = trace_strong (corner_case ~loc:__LOC__ "not a record") @@ @@ -365,23 +370,19 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re let%bind record' = transpile_annotated_expression record in let expr = List.fold_left aux record' path in ok expr - | E_record_update (record, updates) -> + | E_record_update (record, (l,expr)) -> let%bind ty' = transpile_type (get_type_annotation record) in let%bind ty_lmap = trace_strong (corner_case ~loc:__LOC__ "not a record") @@ get_t_record (get_type_annotation record) in let%bind ty'_lmap = AST.bind_map_lmap transpile_type ty_lmap in - let aux (Label l, expr) = - let%bind path = - trace_strong (corner_case ~loc:__LOC__ "record access") @@ - record_access_to_lr ty' ty'_lmap l in - let path' = List.map snd path in - let%bind expr' = transpile_annotated_expression expr in - ok (path',expr') - in - let%bind updates = bind_map_list aux updates in + let%bind path = + trace_strong (corner_case ~loc:__LOC__ "record access") @@ + record_access_to_lr ty' ty'_lmap l in + let path' = List.map snd path in + let%bind expr' = transpile_annotated_expression expr in let%bind record = transpile_annotated_expression record in - return @@ E_update (record, updates) + return @@ E_update (record, (path',expr')) | E_constant (name , lst) -> ( let iterator_generator iterator_name = let lambda_to_iterator_body (f : AST.annotated_expression) (l : AST.lambda) = @@ -509,7 +510,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re match cur with | Access_tuple ind -> ( let%bind ty_lst = - trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@ + trace_strong (corner_case ~loc:__LOC__ "transpiler: E_assign: Access_tuple: not a tuple") @@ AST.Combinators.get_t_tuple prev in let%bind ty'_lst = bind_map_list transpile_type ty_lst in let%bind path = tuple_access_to_lr ty' ty'_lst ind in @@ -521,7 +522,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re trace_strong (corner_case ~loc:__LOC__ "not a record") @@ AST.Combinators.get_t_record prev in let%bind ty'_map = bind_map_lmap transpile_type ty_map in - let%bind path = record_access_to_lr ty' ty'_map prop in + let%bind path = record_access_to_lr ty' ty'_map (Label prop) in let path' = List.map snd path in let%bind prop_in_ty_map = trace_option (Errors.not_found "acessing prop in ty_map [TODO: better error message]") diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml index a548003b0..cc572fa94 100644 --- a/src/passes/6-transpiler/untranspiler.ml +++ b/src/passes/6-transpiler/untranspiler.ml @@ -36,15 +36,6 @@ them. please report this to the developers." in ] in error ~data title content - let unknown_untranspile unknown_type value = - let title () = "untranspiling unknown value" in - let content () = Format.asprintf "can not untranspile %s" unknown_type in - let data = [ - ("unknown_type" , fun () -> unknown_type) ; - ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ; - ] in - error ~data title content - end open Errors @@ -196,6 +187,22 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression ) | TC_contract _ -> fail @@ bad_untranspile "contract" v + | TC_arrow _ -> ( + let%bind n = + trace_strong (wrong_mini_c_value "lambda as string" v) @@ + get_string v in + return (E_literal (Literal_string n)) + ) + | TC_tuple lst -> + let%bind node = match Append_tree.of_list lst with + | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple" + | Full t -> ok t in + let%bind tpl = + trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@ + extract_tuple v node in + let%bind tpl' = bind_list + @@ List.map (fun (x, y) -> untranspile x y) tpl in + return (E_tuple tpl') ) | T_sum m -> let lst = kv_list_of_cmap m in @@ -208,16 +215,6 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression extract_constructor v node in let%bind sub = untranspile v tv in return (E_constructor (Constructor name, sub)) - | T_tuple lst -> - let%bind node = match Append_tree.of_list lst with - | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple" - | Full t -> ok t in - let%bind tpl = - trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@ - extract_tuple v node in - let%bind tpl' = bind_list - @@ List.map (fun (x, y) -> untranspile x y) tpl in - return (E_tuple tpl') | T_record m -> let lst = kv_list_of_lmap m in let%bind node = match Append_tree.of_list lst with diff --git a/src/passes/7-self_mini_c/helpers.ml b/src/passes/7-self_mini_c/helpers.ml index f5638cbe5..6e3a454b1 100644 --- a/src/passes/7-self_mini_c/helpers.ml +++ b/src/passes/7-self_mini_c/helpers.ml @@ -84,13 +84,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini let%bind res = self init' exp in ok res ) - | E_update (r, updates) -> ( + | E_update (r, (_,e)) -> ( let%bind res = self init' r in - let aux prev (_,e) = - let%bind res = self prev e in - ok res - in - let%bind res = bind_fold_list aux res updates in + let%bind res = self res e in ok res ) @@ -158,10 +154,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e -> let%bind exp' = self exp in return @@ E_assignment (s, lrl, exp') ) - | E_update (r, updates) -> ( + | E_update (r, (l,e)) -> ( let%bind r = self r in - let%bind updates = bind_map_list (fun (p,e) -> let%bind e = self e in ok(p,e)) updates in - return @@ E_update(r,updates) + let%bind e = self e in + return @@ E_update(r,(l,e)) ) let map_sub_level_expression : mapper -> expression -> expression result = fun f e -> diff --git a/src/passes/7-self_mini_c/self_mini_c.ml b/src/passes/7-self_mini_c/self_mini_c.ml index da2c66fa6..98bc0315c 100644 --- a/src/passes/7-self_mini_c/self_mini_c.ml +++ b/src/passes/7-self_mini_c/self_mini_c.ml @@ -66,8 +66,8 @@ let rec is_pure : expression -> bool = fun e -> | E_constant (c, args) -> is_pure_constant c && List.for_all is_pure args - | E_update (e, updates) - -> is_pure e && List.for_all (fun (_,e) -> is_pure e) updates + | E_update (r, (_,e)) + -> is_pure r && is_pure e (* I'm not sure about these. Maybe can be tested better? *) | E_application _ @@ -111,8 +111,8 @@ let rec is_assigned : ignore_lambdas:bool -> expression_variable -> expression - match e.content with | E_assignment (x, _, e) -> it x || self e - | E_update (r, updates) -> - List.fold_left (fun prev (_,e) -> prev || self e) (self r) updates + | E_update (r, (_,e)) -> + self r || self e | E_closure { binder; body } -> if ignore_lambdas then false diff --git a/src/passes/7-self_mini_c/subst.ml b/src/passes/7-self_mini_c/subst.ml index ddba8855a..9582c4a6f 100644 --- a/src/passes/7-self_mini_c/subst.ml +++ b/src/passes/7-self_mini_c/subst.ml @@ -94,10 +94,10 @@ let rec replace : expression -> var_name -> var_name -> expression = let v = replace_var v in let e = replace e in return @@ E_assignment (v, path, e) - | E_update (r, updates) -> + | E_update (r, (p,e)) -> let r = replace r in - let updates = List.map (fun (p,e)-> (p, replace e)) updates in - return @@ E_update (r,updates) + let e = replace e in + return @@ E_update (r, (p,e)) | E_while (cond, body) -> let cond = replace cond in let body = replace body in @@ -209,10 +209,10 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e if Var.equal s x then raise Bad_argument ; return @@ E_assignment (s, lrl, exp') ) - | E_update (r, updates) -> ( + | E_update (r, (p,e)) -> ( let r' = self r in - let updates' = List.map (fun (p,e) -> (p, self e)) updates in - return @@ E_update(r',updates') + let e' = self e in + return @@ E_update(r', (p,e')) ) let%expect_test _ = diff --git a/src/passes/8-compiler/compiler_program.ml b/src/passes/8-compiler/compiler_program.ml index 280d93cfd..c1f7cc5b6 100644 --- a/src/passes/8-compiler/compiler_program.ml +++ b/src/passes/8-compiler/compiler_program.ml @@ -402,32 +402,29 @@ and translate_expression (expr:expression) (env:environment) : michelson result i_push_unit ; ] ) - | E_update (record, updates) -> ( + | E_update (record, (path, expr)) -> ( let%bind record' = translate_expression record env in - let insts = [ - i_comment "r_update: start, move the record on top # env"; - record';] in - let aux (init :t list) (update,expr) = - let record_var = Var.fresh () in - let env' = Environment.add (record_var, record.type_value) env in - let%bind expr' = translate_expression expr env' in - let modify_code = - let aux acc step = match step with - | `Left -> seq [dip i_unpair ; acc ; i_pair] - | `Right -> seq [dip i_unpiar ; acc ; i_piar] - in - let init = dip i_drop in - List.fold_right' aux init update + + let record_var = Var.fresh () in + let env' = Environment.add (record_var, record.type_value) env in + let%bind expr' = translate_expression expr env' in + let modify_code = + let aux acc step = match step with + | `Left -> seq [dip i_unpair ; acc ; i_pair] + | `Right -> seq [dip i_unpiar ; acc ; i_piar] in - ok @@ init @ [ - expr'; - i_comment "r_updates : compute rhs # rhs:env"; - modify_code; - i_comment "r_update: modify code # record+rhs : env"; - ] + let init = dip i_drop in + List.fold_right' aux init path in - let%bind insts = bind_fold_list aux insts updates in - return @@ seq insts + return @@ seq [ + i_comment "r_update: start # env"; + record'; + i_comment "r_update: move the record on top # env"; + expr'; + i_comment "r_updates : compute rhs # rhs:env"; + modify_code; + i_comment "r_update: modify code # record+rhs : env"; + ] ) | E_while (expr , block) -> ( diff --git a/src/stages/ast_simplified/PP.ml b/src/stages/ast_simplified/PP.ml index 768d6d12a..92138a014 100644 --- a/src/stages/ast_simplified/PP.ml +++ b/src/stages/ast_simplified/PP.ml @@ -18,7 +18,7 @@ and type_expression ppf (te: type_expression) : unit = te' ppf te.type_expression' let rec expression ppf (e:expression) = match e.expression with - | E_literal l -> literal ppf l + | E_literal l -> fprintf ppf "%a" literal l | E_variable n -> fprintf ppf "%a" name n | E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg | E_constructor (c, ae) -> fprintf ppf "%a(%a)" constructor c expression ae @@ -26,11 +26,11 @@ let rec expression ppf (e:expression) = match e.expression with | E_tuple lst -> fprintf ppf "(%a)" (tuple_sep_d expression) lst | E_accessor (ae, p) -> fprintf ppf "%a.%a" expression ae access_path p | E_record m -> fprintf ppf "{%a}" (lrecord_sep expression (const " , ")) m - | E_update {record; updates} -> fprintf ppf "%a with {%a}" expression record (tuple_sep_d (fun ppf (a,b) -> fprintf ppf "%a = %a" label a expression b)) updates + | E_update {record; update=(path,expr)} -> fprintf ppf "%a with { %a = %a }" expression record Stage_common.PP.label path expression expr | E_map m -> fprintf ppf "[%a]" (list_sep_d assoc_expression) m | E_big_map m -> fprintf ppf "big_map[%a]" (list_sep_d assoc_expression) m | E_list lst -> fprintf ppf "[%a]" (list_sep_d expression) lst - | E_set lst -> fprintf ppf "{%a}" (list_sep_d expression) lst + | E_set lst -> fprintf ppf "{%a}" (list_sep_d expression) lst | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" expression ds expression ind | E_lambda {binder;input_type;output_type;result} -> fprintf ppf "lambda (%a:%a) : %a return %a" diff --git a/src/stages/ast_simplified/combinators.ml b/src/stages/ast_simplified/combinators.ml index a082e2fa9..2a3e0ab33 100644 --- a/src/stages/ast_simplified/combinators.ml +++ b/src/stages/ast_simplified/combinators.ml @@ -36,7 +36,7 @@ let t_key_hash : type_expression = make_t @@ T_constant (TC_key_hash) let t_option o : type_expression = make_t @@ T_operator (TC_option o) let t_list t : type_expression = make_t @@ T_operator (TC_list t) let t_variable n : type_expression = make_t @@ T_variable (Var.of_name n) -let t_tuple lst : type_expression = make_t @@ T_tuple lst +let t_tuple lst : type_expression = make_t @@ T_operator (TC_tuple lst) let t_pair (a , b) : type_expression = t_tuple [a ; b] let t_record_ez lst = let lst = List.map (fun (k, v) -> (Label k, v)) lst in @@ -174,9 +174,10 @@ let e_ez_record ?loc (lst : (string * expr) list) : expression = let e_record ?loc map = let lst = Map.String.to_kv_list map in e_ez_record ?loc lst -let e_update ?loc record updates = - let updates = List.map (fun (x,y) -> (Label x, y)) updates in - location_wrap ?loc @@ E_update {record; updates} + +let e_update ?loc record path expr = + let update = (Label path, expr) in + location_wrap ?loc @@ E_update {record; update} let get_e_accessor = fun t -> match t with @@ -205,7 +206,7 @@ let get_e_list = fun t -> let get_e_tuple = fun t -> match t with | E_tuple lst -> ok lst - | _ -> simple_fail "not a tuple" + | _ -> simple_fail "ast_simplified: get_e_tuple: not a tuple" let extract_pair : expression -> (expression * expression) result = fun e -> match e.expression with diff --git a/src/stages/ast_simplified/combinators.mli b/src/stages/ast_simplified/combinators.mli index 2bc534748..d8349e0a2 100644 --- a/src/stages/ast_simplified/combinators.mli +++ b/src/stages/ast_simplified/combinators.mli @@ -27,8 +27,8 @@ val t_option : type_expression -> type_expression *) val t_list : type_expression -> type_expression val t_variable : string -> type_expression -(* val t_tuple : type_expression list -> type_expression +(* val t_record : te_map -> type_expression *) val t_pair : ( type_expression * type_expression ) -> type_expression @@ -109,7 +109,7 @@ val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expre val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression val e_record : ?loc:Location.t -> expr Map.String.t -> expression -val e_update : ?loc:Location.t -> expression -> (string * expression) list -> expression +val e_update : ?loc:Location.t -> expression -> string -> expression -> expression val e_ez_record : ?loc:Location.t -> ( string * expr ) list -> expression (* diff --git a/src/stages/ast_simplified/misc.ml b/src/stages/ast_simplified/misc.ml index a37e57cf3..bc214863a 100644 --- a/src/stages/ast_simplified/misc.ml +++ b/src/stages/ast_simplified/misc.ml @@ -1,6 +1,8 @@ open Trace open Types +include Stage_common.Misc + module Errors = struct let different_literals_because_different_types name a b () = let title () = "literals have different types: " ^ name in @@ -133,14 +135,14 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result = simple_fail "comparing record with other expression" | E_update ura, E_update urb -> - let%bind lst = - generic_try (simple_error "updates with different number of fields") - (fun () -> List.combine ura.updates urb.updates) in + let _ = + generic_try (simple_error "Updating different record") @@ + fun () -> assert_value_eq (ura.record, urb.record) in let aux ((Label a,expra),(Label b, exprb))= - assert (String.equal a b); + assert (String.equal a b); assert_value_eq (expra,exprb) in - let%bind _all = bind_list @@ List.map aux lst in + let%bind _all = aux (ura.update, urb.update) in ok () | E_update _, _ -> simple_fail "comparing record update with other expression" diff --git a/src/stages/ast_simplified/misc.mli b/src/stages/ast_simplified/misc.mli index 9ef833e55..20813de49 100644 --- a/src/stages/ast_simplified/misc.mli +++ b/src/stages/ast_simplified/misc.mli @@ -1,5 +1,8 @@ open Trace open Types + +include module type of Stage_common.Misc + (* module Errors : sig @@ -15,4 +18,4 @@ val assert_literal_eq : ( literal * literal ) -> unit result val assert_value_eq : ( expression * expression ) -> unit result -val is_value_eq : ( expression * expression ) -> bool \ No newline at end of file +val is_value_eq : ( expression * expression ) -> bool diff --git a/src/stages/ast_simplified/types.ml b/src/stages/ast_simplified/types.ml index 3be7b3fb8..69f564740 100644 --- a/src/stages/ast_simplified/types.ml +++ b/src/stages/ast_simplified/types.ml @@ -67,6 +67,6 @@ and expression = { expression : expression' ; location : Location.t ; } -and update = {record: expr; updates: (label*expr)list} +and update = { record: expr; update: (label *expr) } and matching_expr = (expr,unit) matching diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml index 3fc3c2483..9d412cd53 100644 --- a/src/stages/ast_typed/PP.ml +++ b/src/stages/ast_typed/PP.ml @@ -15,13 +15,12 @@ and type_value ppf (tv:type_value) : unit = let rec annotated_expression ppf (ae:annotated_expression) : unit = match ae.type_annotation.simplified with - | Some _ -> fprintf ppf "@[%a:%a@]" expression ae.expression type_value ae.type_annotation - | _ -> fprintf ppf "@[%a@]" expression ae.expression + | _ -> fprintf ppf "@[%a:%a@]" expression ae.expression type_value ae.type_annotation and lambda ppf l = let ({ binder ; body } : lambda) = l in - fprintf ppf "lambda (%a) -> %a" - name binder + fprintf ppf "(lambda (%a) -> %a)" + name binder annotated_expression body and option_inline ppf inline = @@ -33,14 +32,14 @@ and option_inline ppf inline = and expression ppf (e:expression) : unit = match e with | E_literal l -> Stage_common.PP.literal ppf l - | E_constant (b, lst) -> fprintf ppf "%a(%a)" constant b (list_sep_d annotated_expression) lst - | E_constructor (c, lst) -> fprintf ppf "%a(%a)" constructor c annotated_expression lst - | E_variable a -> fprintf ppf "%a" name a + | E_constant (b, lst) -> fprintf ppf "(e_constant %a(%a))" constant b (list_sep_d annotated_expression) lst + | E_constructor (c, lst) -> fprintf ppf "(e_constructor %a(%a))" constructor c annotated_expression lst + | E_variable a -> fprintf ppf "(e_var %a)" name a | E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg | E_lambda l -> fprintf ppf "%a" lambda l | E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i | E_record_accessor (ae, l) -> fprintf ppf "%a.%a" annotated_expression ae label l - | E_record_update (ae, ups) -> fprintf ppf "%a with record[%a]" annotated_expression ae (lmap_sep annotated_expression (const " , ")) (LMap.of_list ups) + | E_record_update (ae, (path,expr)) -> fprintf ppf "%a with record[%a=%a]" annotated_expression ae Stage_common.PP.label path annotated_expression expr | E_tuple lst -> fprintf ppf "tuple[@; @[%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst | E_record m -> fprintf ppf "record[%a]" (lmap_sep annotated_expression (const " , ")) m | E_map m -> fprintf ppf "map[@; @[%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m @@ -50,7 +49,7 @@ and expression ppf (e:expression) : unit = | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m - | E_sequence (a , b) -> fprintf ppf "%a ; %a" annotated_expression a annotated_expression b + | E_sequence (a , b) -> fprintf ppf "(e_seq %a ; %a)" annotated_expression a annotated_expression b | E_loop (expr , body) -> fprintf ppf "while %a { %a }" annotated_expression expr annotated_expression body | E_assign (name , path , expr) -> fprintf ppf "%a.%a := %a" diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml index 8ebe2b89d..17037787f 100644 --- a/src/stages/ast_typed/combinators.ml +++ b/src/stages/ast_typed/combinators.ml @@ -48,7 +48,7 @@ let t_mutez ?s () : type_value = make_t (T_constant TC_mutez) s let t_timestamp ?s () : type_value = make_t (T_constant TC_timestamp) s let t_unit ?s () : type_value = make_t (T_constant TC_unit) s let t_option o ?s () : type_value = make_t (T_operator (TC_option o)) s -let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s +let t_tuple lst ?s () : type_value = make_t (T_operator (TC_tuple lst)) s let t_variable t ?s () : type_value = make_t (T_variable t) s let t_list t ?s () : type_value = make_t (T_operator (TC_list t)) s let t_set t ?s () : type_value = make_t (T_operator (TC_set t)) s @@ -147,11 +147,11 @@ let get_t_key_hash (t:type_value) : unit result = match t.type_value' with | _ -> fail @@ Errors.not_a_x_type "key_hash" t () let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with - | T_tuple lst -> ok lst + | T_operator (TC_tuple lst) -> ok lst | _ -> fail @@ Errors.not_a_x_type "tuple" t () let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_value' with - | T_tuple lst -> + | T_operator (TC_tuple lst) -> let%bind () = trace_strong (Errors.not_a_x_type "pair (tuple with two elements)" t ()) @@ Assert.assert_list_size lst 2 in @@ -160,6 +160,7 @@ let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_ let get_t_function (t:type_value) : (type_value * type_value) result = match t.type_value' with | T_arrow (a,r) -> ok (a,r) + | T_operator (TC_arrow (a , b)) -> ok (a , b) | _ -> fail @@ Errors.not_a_x_type "function" t () let get_t_sum (t:type_value) : type_value constructor_map result = match t.type_value' with @@ -253,11 +254,11 @@ let ez_e_record (lst : (label * ae) list) : expression = let map = List.fold_left aux LMap.empty lst in e_record map let e_some s : expression = E_constant (C_SOME, [s]) -let e_none : expression = E_constant (C_NONE, []) +let e_none () : expression = E_constant (C_NONE, []) let e_map lst : expression = E_map lst -let e_unit : expression = E_literal (Literal_unit) +let e_unit () : expression = E_literal (Literal_unit) let e_int n : expression = E_literal (Literal_int n) let e_nat n : expression = E_literal (Literal_nat n) let e_mutez n : expression = E_literal (Literal_mutez n) @@ -279,7 +280,7 @@ let e_list lst : expression = E_list lst let e_let_in binder inline rhs result = E_let_in { binder ; rhs ; result; inline } let e_tuple lst : expression = E_tuple lst -let e_a_unit = make_a_e e_unit (t_unit ()) +let e_a_unit = make_a_e (e_unit ()) (t_unit ()) let e_a_int n = make_a_e (e_int n) (t_int ()) let e_a_nat n = make_a_e (e_nat n) (t_nat ()) let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ()) @@ -289,7 +290,7 @@ let e_a_address s = make_a_e (e_address s) (t_address ()) let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ()) let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ()) let e_a_lambda l in_ty out_ty = make_a_e (e_lambda l) (t_function in_ty out_ty ()) -let e_a_none t = make_a_e e_none (t_option t ()) +let e_a_none t = make_a_e (e_none ()) (t_option t ()) let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ()) let e_a_record r = make_a_e (e_record r) (t_record (LMap.map get_type_annotation r) ()) let e_a_application a b = make_a_e (e_application a b) (get_type_annotation b) diff --git a/src/stages/ast_typed/combinators.mli b/src/stages/ast_typed/combinators.mli index f9cd7d93d..4f794deb8 100644 --- a/src/stages/ast_typed/combinators.mli +++ b/src/stages/ast_typed/combinators.mli @@ -111,9 +111,9 @@ val ez_e_record : ( string * annotated_expression ) list -> expression *) val e_some : value -> expression -val e_none : expression +val e_none : unit -> expression val e_map : ( value * value ) list -> expression -val e_unit : expression +val e_unit : unit -> expression val e_int : int -> expression val e_nat : int -> expression val e_mutez : int -> expression diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml index 43d0c8792..f56558b13 100644 --- a/src/stages/ast_typed/misc.ml +++ b/src/stages/ast_typed/misc.ml @@ -1,5 +1,6 @@ open Trace open Types + include Stage_common.Misc module Errors = struct @@ -29,6 +30,21 @@ module Errors = struct ] in error ~data title message () + let different_operator_number_of_arguments opa opb lena lenb () = + let title = (thunk "different number of arguments to type constructors") in + assert (String.equal (type_operator_name opa) (type_operator_name opb)); + let message () = Format.asprintf + "Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)" + (type_operator_name opa) lena lenb in + let data = [ + ("a" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opa) ; + ("b" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opb) ; + ("op" , fun () -> type_operator_name opa) ; + ("len_a" , fun () -> Format.asprintf "%d" lena) ; + ("len_b" , fun () -> Format.asprintf "%d" lenb) ; + ] in + error ~data title message () + let different_size_type name a b () = let title () = name ^ " have different sizes" in let message () = "Expected these two types to be the same, but they're different (both are " ^ name ^ ", but with a different number of arguments)" in @@ -49,8 +65,6 @@ module Errors = struct let _different_size_constants = different_size_type "type constructors" - let different_size_tuples = different_size_type "tuples" - let different_size_sums = different_size_type "sums" let different_size_records = different_size_type "records" @@ -179,7 +193,7 @@ module Free_variables = struct | E_constructor (_ , a) -> self a | E_record m -> unions @@ List.map self @@ LMap.to_list m | E_record_accessor (a, _) -> self a - | E_record_update (r,ups) -> union (self r) @@ unions @@ List.map (fun (_,e) -> self e) ups + | E_record_update (r,(_,e)) -> union (self r) @@ self e | E_tuple_accessor (a, _) -> self a | E_list lst -> unions @@ List.map self lst | E_set lst -> unions @@ List.map self lst @@ -301,13 +315,6 @@ open Errors let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with - | T_tuple ta, T_tuple tb -> ( - let%bind _ = - trace_strong (fun () -> (different_size_tuples a b ())) - @@ Assert.assert_true List.(length ta = length tb) in - bind_list_iter assert_type_value_eq (List.combine ta tb) - ) - | T_tuple _, _ -> fail @@ different_kinds a b | T_constant ca, T_constant cb -> ( trace_strong (different_constants ca cb) @@ Assert.assert_true (ca = cb) @@ -321,10 +328,16 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m | TC_set la, TC_set lb -> ok @@ ([la], [lb]) | TC_map (ka,va), TC_map (kb,vb) | TC_big_map (ka,va), TC_big_map (kb,vb) -> ok @@ ([ka;va] ,[kb;vb]) - | _,_ -> fail @@ different_operators opa opb + | TC_tuple lsta, TC_tuple lstb -> ok @@ (lsta , lstb) + | TC_arrow (froma , toa) , TC_arrow (fromb , tob) -> ok @@ ([froma;toa] , [fromb;tob]) + | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _), + (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _) -> fail @@ different_operators opa opb in - trace (different_types "arguments to type operators" a b) - @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb) + if List.length lsta <> List.length lstb then + fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb) + else + trace (different_types "arguments to type operators" a b) + @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb) ) | T_operator _, _ -> fail @@ different_kinds a b | T_sum sa, T_sum sb -> ( diff --git a/src/stages/ast_typed/misc.mli b/src/stages/ast_typed/misc.mli index 45efb025f..44e3ca324 100644 --- a/src/stages/ast_typed/misc.mli +++ b/src/stages/ast_typed/misc.mli @@ -1,6 +1,8 @@ open Trace open Types +include module type of Stage_common.Misc + val assert_value_eq : ( value * value ) -> unit result val assert_type_value_eq : ( type_value * type_value ) -> unit result @@ -43,7 +45,6 @@ module Errors : sig val different_size_type : name -> type_value -> type_value -> unit -> error val different_props_in_record : string -> string -> unit -> error val different_size_constants : type_value -> type_value -> unit -> error - val different_size_tuples : type_value -> type_value -> unit -> error val different_size_sums : type_value -> type_value -> unit -> error val different_size_records : type_value -> type_value -> unit -> error val different_types : name -> type_value -> type_value -> unit -> error diff --git a/src/stages/ast_typed/misc_smart.ml b/src/stages/ast_typed/misc_smart.ml index d0c087892..556b8d81a 100644 --- a/src/stages/ast_typed/misc_smart.ml +++ b/src/stages/ast_typed/misc_smart.ml @@ -72,14 +72,10 @@ module Captured_variables = struct let%bind lst' = bind_map_list self @@ LMap.to_list m in ok @@ unions lst' | E_record_accessor (a, _) -> self a - | E_record_update (r,ups) -> + | E_record_update (r,(_,e)) -> let%bind r = self r in - let aux (_, e) = - let%bind e = self e in - ok e - in - let%bind lst = bind_map_list aux ups in - ok @@ union r @@ unions lst + let%bind e = self e in + ok @@ union r e | E_tuple_accessor (a, _) -> self a | E_list lst -> let%bind lst' = bind_map_list self lst in diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml index 50d2060ed..cf4957613 100644 --- a/src/stages/ast_typed/types.ml +++ b/src/stages/ast_typed/types.ml @@ -18,7 +18,7 @@ and environment_element_definition = and free_variables = expression_variable list and environment_element = { - type_value : type_value ; + type_value : type_value ; source_environment : full_environment ; definition : environment_element_definition ; } @@ -34,6 +34,12 @@ and annotated_expression = { location : Location.t ; } +(* This seems to be used only for top-level declarations, and + represents the name of the top-level binding, and the expression + assigned to it. -- Suzanne. + + TODO: if this is correct, then we should inline this in + "declaration" or at least move it close to it. *) and named_expression = { name: expression_variable ; annotated_expression: ae ; @@ -41,6 +47,7 @@ and named_expression = { and ae = annotated_expression and type_value' = type_value type_expression' + and type_value = { type_value' : type_value'; simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *) @@ -77,7 +84,7 @@ and 'a expression' = | E_application of (('a) * ('a)) | E_lambda of lambda | E_let_in of let_in - (* Tuple *) + (* Tuple, TODO: remove tuples and use records with integer keys instead *) | E_tuple of ('a) list | E_tuple_accessor of (('a) * int) (* Access n'th tuple's element *) (* Sum *) @@ -85,7 +92,7 @@ and 'a expression' = (* Record *) | E_record of ('a) label_map | E_record_accessor of (('a) * label) - | E_record_update of ('a * (label* 'a) list) + | E_record_update of ('a * (label * 'a)) (* Data Structures *) | E_map of (('a) * ('a)) list | E_big_map of (('a) * ('a)) list diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index 7d42e0c7e..deebe08ee 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -141,7 +141,6 @@ let lmap_sep_d x = lmap_sep x (const " , ") let rec type_expression' : type a . (formatter -> a -> unit) -> formatter -> a type_expression' -> unit = fun f ppf te -> match te with - | T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d f) lst | T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m | T_record m -> fprintf ppf "record[%a]" (lmap_sep_d f ) m | T_arrow (a, b) -> fprintf ppf "%a -> %a" f a f b @@ -178,6 +177,8 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v | TC_contract (c) -> Format.asprintf "Contract (%a)" f c + | TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b + | TC_tuple lst -> Format.asprintf "tuple[%a]" (list_sep_d f) lst in fprintf ppf "(TO_%s)" s diff --git a/src/stages/common/PP.mli b/src/stages/common/PP.mli index b95fd3851..0d6a75434 100644 --- a/src/stages/common/PP.mli +++ b/src/stages/common/PP.mli @@ -13,3 +13,4 @@ val type_expression' : (formatter -> 'a -> unit) -> formatter -> 'a type_express val type_operator : (formatter -> 'a -> unit) -> formatter -> 'a type_operator -> unit val type_constant : formatter -> type_constant -> unit val literal : formatter -> literal -> unit +val list_sep_d : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit diff --git a/src/stages/common/misc.ml b/src/stages/common/misc.ml index 7f38acf62..794a36e7c 100644 --- a/src/stages/common/misc.ml +++ b/src/stages/common/misc.ml @@ -7,7 +7,9 @@ let map_type_operator f = function | TC_list x -> TC_list (f x) | TC_set x -> TC_set (f x) | TC_map (x , y) -> TC_map (f x , f y) - | TC_big_map (x , y)-> TC_big_map (f x , f y) + | TC_big_map (x , y) -> TC_big_map (f x , f y) + | TC_arrow (x , y) -> TC_arrow (f x , f y) + | TC_tuple lst -> TC_tuple (List.map f lst) let bind_map_type_operator f = function TC_contract x -> let%bind x = f x in ok @@ TC_contract x @@ -15,7 +17,9 @@ let bind_map_type_operator f = function | TC_list x -> let%bind x = f x in ok @@ TC_list x | TC_set x -> let%bind x = f x in ok @@ TC_set x | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y) - | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + | TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + | TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y) + | TC_tuple lst -> let%bind lst = bind_map_list f lst in ok @@ TC_tuple lst let type_operator_name = function TC_contract _ -> "TC_contract" @@ -24,6 +28,8 @@ let type_operator_name = function | TC_set _ -> "TC_set" | TC_map _ -> "TC_map" | TC_big_map _ -> "TC_big_map" + | TC_arrow _ -> "TC_arrow" + | TC_tuple _ -> "TC_tuple" let type_expression'_of_string = function | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) @@ -61,6 +67,8 @@ let string_of_type_operator = function | TC_set x -> "TC_set" , [x] | TC_map (x , y) -> "TC_map" , [x ; y] | TC_big_map (x , y) -> "TC_big_map" , [x ; y] + | TC_arrow (x , y) -> "TC_arrow" , [x ; y] + | TC_tuple lst -> "TC_tuple" , lst let string_of_type_constant = function | TC_unit -> "TC_unit", [] @@ -81,5 +89,6 @@ let string_of_type_constant = function let string_of_type_expression' = function | T_operator o -> string_of_type_operator o | T_constant c -> string_of_type_constant c - | T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ -> + | T_sum _|T_record _|T_arrow (_, _)|T_variable _ -> failwith "not a type operator or constant" + diff --git a/src/stages/common/misc.mli b/src/stages/common/misc.mli new file mode 100644 index 000000000..78dfaf17e --- /dev/null +++ b/src/stages/common/misc.mli @@ -0,0 +1,9 @@ +open Types + +val map_type_operator : ('a -> 'b) -> 'a type_operator -> 'b type_operator +val bind_map_type_operator : ('a -> ('b * 'c list, 'd) Pervasives.result) -> 'a type_operator -> ('b type_operator * 'c list, 'd) Pervasives.result +val type_operator_name : 'a type_operator -> string +val type_expression'_of_string : string * 'a list -> ('a type_expression' * 'b list, 'c) Pervasives.result +val string_of_type_operator : 'a type_operator -> string * 'a list +val string_of_type_constant : type_constant -> string * 'a list +val string_of_type_expression' : 'a type_expression' -> string * 'a list diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml index b25eb80a5..70c3bc80a 100644 --- a/src/stages/common/types.ml +++ b/src/stages/common/types.ml @@ -66,7 +66,6 @@ and literal = (* The ast is a tree of node, 'a is the type of the node (type_variable or {type_variable, previous_type}) *) type 'a type_expression' = - | T_tuple of 'a list | T_sum of 'a constructor_map | T_record of 'a label_map | T_arrow of 'a * 'a @@ -96,6 +95,8 @@ and 'a type_operator = | TC_set of 'a | TC_map of 'a * 'a | TC_big_map of 'a * 'a + | TC_arrow of 'a * 'a + | TC_tuple of 'a list type type_base = | Base_unit diff --git a/src/stages/mini_c/PP.ml b/src/stages/mini_c/PP.ml index c012eed48..14fa1846a 100644 --- a/src/stages/mini_c/PP.ml +++ b/src/stages/mini_c/PP.ml @@ -99,8 +99,8 @@ and expression' ppf (e:expression') = match e with fprintf ppf "fold %a on %a with %a do ( %a )" expression collection expression initial Stage_common.PP.name name expression body | E_assignment (r , path , e) -> fprintf ppf "%a.%a := %a" Stage_common.PP.name r (list_sep lr (const ".")) path expression e - | E_update (r, updates) -> - fprintf ppf "%a with {%a}" expression r (list_sep_d (fun ppf (path, e) -> fprintf ppf "%a = %a" (list_sep lr (const ".")) path expression e)) updates + | E_update (r, (path,e)) -> + fprintf ppf "%a with {%a=%a}" expression r (list_sep lr (const ".")) path expression e | E_while (e , b) -> fprintf ppf "while (%a) %a" expression e expression b diff --git a/src/stages/mini_c/misc.ml b/src/stages/mini_c/misc.ml index a30bca8db..caf35c311 100644 --- a/src/stages/mini_c/misc.ml +++ b/src/stages/mini_c/misc.ml @@ -81,7 +81,7 @@ module Free_variables = struct | E_sequence (x, y) -> union (self x) (self y) (* NB different from ast_typed... *) | E_assignment (v, _, e) -> unions [ var_name b v ; self e ] - | E_update (e, updates) -> union (self e) (unions @@ List.map (fun (_,e) -> self e) updates) + | E_update (r, (_,e)) -> union (self r) (self e) | E_while (cond , body) -> union (self cond) (self body) and var_name : bindings -> var_name -> bindings = fun b n -> diff --git a/src/stages/mini_c/types.ml b/src/stages/mini_c/types.ml index ed0b24747..caee68b6c 100644 --- a/src/stages/mini_c/types.ml +++ b/src/stages/mini_c/types.ml @@ -73,7 +73,7 @@ and expression' = | E_let_in of ((var_name * type_value) * inline * expression * expression) | E_sequence of (expression * expression) | E_assignment of (expression_variable * [`Left | `Right] list * expression) - | E_update of (expression * ([`Left | `Right] list * expression) list) + | E_update of (expression * ([`Left | `Right] list * expression)) | E_while of (expression * expression) and expression = { diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index b95c603fc..3321c670f 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -3,120 +3,122 @@ open Core let pair_map = fun f (x , y) -> (f x , f y) module Substitution = struct - module Pattern = struct open Trace module T = Ast_typed (* module TSMap = Trace.TMap(String) *) - type 'a w = 'a -> 'a result + type substs = variable:type_variable -> T.type_value' option (* this string is a type_name or type_variable I think *) + let mk_substs ~v ~expr = (v , expr) + + type 'a w = substs:substs -> 'a -> 'a result let rec rec_yes = true - and s_environment_element_definition ~v ~expr = function + and s_environment_element_definition ~substs = function | T.ED_binder -> ok @@ T.ED_binder | T.ED_declaration (val_, free_variables) -> - let%bind val_ = s_annotated_expression ~v ~expr val_ in - let%bind free_variables = bind_map_list (s_variable ~v ~expr) free_variables in + let%bind val_ = s_annotated_expression ~substs val_ in + let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in ok @@ T.ED_declaration (val_, free_variables) - and s_environment ~v ~expr : T.environment w = fun env -> + and s_environment : T.environment w = fun ~substs env -> bind_map_list (fun (variable, T.{ type_value; source_environment; definition }) -> - let%bind variable = s_variable ~v ~expr variable in - let%bind type_value = s_type_value ~v ~expr type_value in - let%bind source_environment = s_full_environment ~v ~expr source_environment in - let%bind definition = s_environment_element_definition ~v ~expr definition in + let%bind variable = s_variable ~substs variable in + let%bind type_value = s_type_value ~substs type_value in + let%bind source_environment = s_full_environment ~substs source_environment in + let%bind definition = s_environment_element_definition ~substs definition in ok @@ (variable, T.{ type_value; source_environment; definition })) env - and s_type_environment ~v ~expr : T.type_environment w = fun tenv -> + and s_type_environment : T.type_environment w = fun ~substs tenv -> bind_map_list (fun (type_variable , type_value) -> - let%bind type_variable = s_type_variable ~v ~expr type_variable in - let%bind type_value = s_type_value ~v ~expr type_value in + let%bind type_variable = s_type_variable ~substs type_variable in + let%bind type_value = s_type_value ~substs type_value in ok @@ (type_variable , type_value)) tenv - and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) -> - let%bind environment = s_environment ~v ~expr environment in - let%bind type_environment = s_type_environment ~v ~expr type_environment in + and s_small_environment : T.small_environment w = fun ~substs (environment, type_environment) -> + let%bind environment = s_environment ~substs environment in + let%bind type_environment = s_type_environment ~substs type_environment in ok @@ (environment, type_environment) - and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) -> - let%bind a = s_small_environment ~v ~expr a in - let%bind b = bind_map_list (s_small_environment ~v ~expr) b in + and s_full_environment : T.full_environment w = fun ~substs (a , b) -> + let%bind a = s_small_environment ~substs a in + let%bind b = bind_map_list (s_small_environment ~substs) b in ok (a , b) - and s_variable ~v ~expr : T.expression_variable w = fun var -> - let () = ignore (v, expr) in + and s_variable : T.expression_variable w = fun ~substs var -> + let () = ignore @@ substs in ok var - and s_type_variable ~v ~expr : T.type_variable w = fun tvar -> - let _TODO = ignore (v, expr) in + and s_type_variable : T.type_variable w = fun ~substs tvar -> + let _TODO = ignore @@ substs in Printf.printf "TODO: subst: unimplemented case s_type_variable"; ok @@ tvar (* if String.equal tvar v then * expr * else * ok tvar *) - and s_label ~v ~expr : T.label w = fun l -> - let () = ignore (v, expr) in + and s_label : T.label w = fun ~substs l -> + let () = ignore @@ substs in ok l - and s_build_in ~v ~expr : T.constant w = fun b -> - let () = ignore (v, expr) in + and s_build_in : T.constant w = fun ~substs b -> + let () = ignore @@ substs in ok b - and s_constructor ~v ~expr : T.constructor w = fun c -> - let () = ignore (v, expr) in + and s_constructor : T.constructor w = fun ~substs c -> + let () = ignore @@ substs in ok c - and s_type_name_constant ~v ~expr : T.type_constant w = fun type_name -> + and s_type_name_constant : T.type_constant w = fun ~substs type_name -> (* TODO: we don't need to subst anything, right? *) - let () = ignore (v , expr) in + let () = ignore @@ substs in ok @@ type_name - and s_type_value' ~v ~expr : T.type_value' w = function - | T.T_tuple type_value_list -> - let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in - ok @@ T.T_tuple type_value_list + and s_type_value' : T.type_value' w = fun ~substs -> function + | T.T_operator (TC_tuple type_value_list) -> + let%bind type_value_list = bind_map_list (s_type_value ~substs) type_value_list in + ok @@ T.T_operator (TC_tuple type_value_list) | T.T_sum _ -> failwith "TODO: T_sum" | T.T_record _ -> failwith "TODO: T_record" - | T.T_constant (type_name) -> - let%bind type_name = s_type_name_constant ~v ~expr type_name in + | T.T_constant type_name -> + let%bind type_name = s_type_name_constant ~substs type_name in ok @@ T.T_constant (type_name) | T.T_variable variable -> - if Var.equal variable v - then ok @@ expr - else ok @@ T.T_variable variable - | T.T_operator (type_name_and_args) -> - let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *) - let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in + begin + match substs ~variable with + | Some expr -> s_type_value' ~substs expr (* TODO: is it the right thing to recursively examine this? We mustn't go into an infinite loop. *) + | None -> ok @@ T.T_variable variable + end + | T.T_operator type_name_and_args -> + let%bind type_name_and_args = T.Misc.bind_map_type_operator (s_type_value ~substs) type_name_and_args in ok @@ T.T_operator type_name_and_args | T.T_arrow _ -> - let _TODO = (v, expr) in + let _TODO = substs in failwith "TODO: T_function" - and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' -> - match type_expression' with - | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple" - | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum" - | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record" - | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow" - | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable" - | Ast_simplified.T_operator op -> - let%bind op = - Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *) - (s_type_expression ~v ~expr) - op in - ok @@ Ast_simplified.T_operator op - | Ast_simplified.T_constant constant -> - ok @@ Ast_simplified.T_constant constant + and s_type_expression' : _ Ast_simplified.type_expression' w = fun ~substs -> function + | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum" + | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record" + | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow" + | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable" + | Ast_simplified.T_operator op -> + let%bind op = + Ast_simplified.Misc.bind_map_type_operator + (s_type_expression ~substs) + op in + (* TODO: when we have generalized operators, we might need to subst the operator name itself? *) + ok @@ Ast_simplified.T_operator op + | Ast_simplified.T_constant constant -> + ok @@ Ast_simplified.T_constant constant - and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} -> - let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in + and s_type_expression : Ast_simplified.type_expression w = fun ~substs {type_expression'} -> + let%bind type_expression' = s_type_expression' ~substs type_expression' in ok @@ Ast_simplified.{type_expression'} - and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } -> - let%bind type_value' = s_type_value' ~v ~expr type_value' in - let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in + and s_type_value : T.type_value w = fun ~substs { type_value'; simplified } -> + let%bind type_value' = s_type_value' ~substs type_value' in + let%bind simplified = bind_map_option (s_type_expression ~substs) simplified in ok @@ T.{ type_value'; simplified } - and s_literal ~v ~expr : T.literal w = function + and s_literal : T.literal w = fun ~substs -> function | T.Literal_unit -> - let () = ignore (v, expr) in + let () = ignore @@ substs in ok @@ T.Literal_unit | (T.Literal_bool _ as x) | (T.Literal_int _ as x) @@ -132,144 +134,145 @@ module Substitution = struct | (T.Literal_chain_id _ as x) | (T.Literal_operation _ as x) -> ok @@ x - and s_matching_expr ~v ~expr : T.matching_expr w = fun _ -> - let _TODO = v, expr in + and s_matching_expr : T.matching_expr w = fun ~substs _ -> + let _TODO = substs in failwith "TODO: subst: unimplemented case s_matching" - and s_named_type_value ~v ~expr : T.named_type_value w = fun _ -> - let _TODO = v, expr in + and s_named_type_value : T.named_type_value w = fun ~substs _ -> + let _TODO = substs in failwith "TODO: subst: unimplemented case s_named_type_value" - and s_access_path ~v ~expr : T.access_path w = fun _ -> - let _TODO = v, expr in + and s_access_path : T.access_path w = fun ~substs _ -> + let _TODO = substs in failwith "TODO: subst: unimplemented case s_access_path" - and s_expression ~v ~expr : T.expression w = function + and s_expression : T.expression w = fun ~(substs : substs) -> function | T.E_literal x -> - let%bind x = s_literal ~v ~expr x in + let%bind x = s_literal ~substs x in ok @@ T.E_literal x | T.E_constant (var, vals) -> - let%bind var = s_build_in ~v ~expr var in - let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + let%bind var = s_build_in ~substs var in + let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in ok @@ T.E_constant (var, vals) | T.E_variable tv -> - let%bind tv = s_variable ~v ~expr tv in + let%bind tv = s_variable ~substs tv in ok @@ T.E_variable tv | T.E_application (val1 , val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ T.E_application (val1 , val2) | T.E_lambda { binder; body } -> - let%bind binder = s_variable ~v ~expr binder in - let%bind body = s_annotated_expression ~v ~expr body in + let%bind binder = s_variable ~substs binder in + let%bind body = s_annotated_expression ~substs body in ok @@ T.E_lambda { binder; body } | T.E_let_in { binder; rhs; result; inline } -> - let%bind binder = s_variable ~v ~expr binder in - let%bind rhs = s_annotated_expression ~v ~expr rhs in - let%bind result = s_annotated_expression ~v ~expr result in + let%bind binder = s_variable ~substs binder in + let%bind rhs = s_annotated_expression ~substs rhs in + let%bind result = s_annotated_expression ~substs result in ok @@ T.E_let_in { binder; rhs; result; inline } | T.E_tuple vals -> - let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in ok @@ T.E_tuple vals | T.E_tuple_accessor (val_, i) -> - let%bind val_ = s_annotated_expression ~v ~expr val_ in + let%bind val_ = s_annotated_expression ~substs val_ in let i = i in ok @@ T.E_tuple_accessor (val_, i) | T.E_constructor (tvar, val_) -> - let%bind tvar = s_constructor ~v ~expr tvar in - let%bind val_ = s_annotated_expression ~v ~expr val_ in + let%bind tvar = s_constructor ~substs tvar in + let%bind val_ = s_annotated_expression ~substs val_ in ok @@ T.E_constructor (tvar, val_) | T.E_record aemap -> let _TODO = aemap in failwith "TODO: subst in record" (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ -> - * let key = s_type_variable ~v ~expr key in - * let val_ = s_annotated_expression ~v ~expr val_ in + * let key = s_type_variable ~substs key in + * let val_ = s_annotated_expression ~substs val_ in * ok @@ (key , val_)) aemap in * ok @@ T.E_record aemap *) | T.E_record_accessor (val_, l) -> - let%bind val_ = s_annotated_expression ~v ~expr val_ in - let%bind l = s_label ~v ~expr l in + let%bind val_ = s_annotated_expression ~substs val_ in + let l = l in (* Nothing to substitute, this is a label, not a type *) ok @@ T.E_record_accessor (val_, l) - | T.E_record_update (r, ups) -> - let%bind r = s_annotated_expression ~v ~expr r in - let%bind ups = bind_map_list (fun (l,e) -> let%bind e = s_annotated_expression ~v ~expr e in ok (l,e)) ups in - ok @@ T.E_record_update (r,ups) + | T.E_record_update (r, (l, e)) -> + let%bind r = s_annotated_expression ~substs r in + let%bind e = s_annotated_expression ~substs e in + ok @@ T.E_record_update (r, (l, e)) | T.E_map val_val_list -> let%bind val_val_list = bind_map_list (fun (val1 , val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ (val1 , val2) ) val_val_list in ok @@ T.E_map val_val_list | T.E_big_map val_val_list -> let%bind val_val_list = bind_map_list (fun (val1 , val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ (val1 , val2) ) val_val_list in ok @@ T.E_big_map val_val_list | T.E_list vals -> - let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in ok @@ T.E_list vals | T.E_set vals -> - let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in + let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in ok @@ T.E_set vals | T.E_look_up (val1, val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ T.E_look_up (val1 , val2) | T.E_matching (val_ , matching_expr) -> - let%bind val_ = s_annotated_expression ~v ~expr val_ in - let%bind matching = s_matching_expr ~v ~expr matching_expr in + let%bind val_ = s_annotated_expression ~substs val_ in + let%bind matching = s_matching_expr ~substs matching_expr in ok @@ T.E_matching (val_ , matching) | T.E_sequence (val1, val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ T.E_sequence (val1 , val2) | T.E_loop (val1, val2) -> - let%bind val1 = s_annotated_expression ~v ~expr val1 in - let%bind val2 = s_annotated_expression ~v ~expr val2 in + let%bind val1 = s_annotated_expression ~substs val1 in + let%bind val2 = s_annotated_expression ~substs val2 in ok @@ T.E_loop (val1 , val2) | T.E_assign (named_tval, access_path, val_) -> - let%bind named_tval = s_named_type_value ~v ~expr named_tval in - let%bind access_path = s_access_path ~v ~expr access_path in - let%bind val_ = s_annotated_expression ~v ~expr val_ in + let%bind named_tval = s_named_type_value ~substs named_tval in + let%bind access_path = s_access_path ~substs access_path in + let%bind val_ = s_annotated_expression ~substs val_ in ok @@ T.E_assign (named_tval, access_path, val_) - and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } -> - let%bind expression = s_expression ~v ~expr expression in - let%bind type_annotation = s_type_value ~v ~expr type_annotation in - let%bind environment = s_full_environment ~v ~expr environment in + and s_annotated_expression : T.annotated_expression w = fun ~substs { expression; type_annotation; environment; location } -> + let%bind expression = s_expression ~substs expression in + let%bind type_annotation = s_type_value ~substs type_annotation in + let%bind environment = s_full_environment ~substs environment in let location = location in ok T.{ expression; type_annotation; environment; location } - and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } -> - let%bind name = s_variable ~v ~expr name in - let%bind annotated_expression = s_annotated_expression ~v ~expr annotated_expression in + and s_named_expression : T.named_expression w = fun ~substs { name; annotated_expression } -> + let name = name in (* Nothing to substitute, this is a variable name *) + let%bind annotated_expression = s_annotated_expression ~substs annotated_expression in ok T.{ name; annotated_expression } - and s_declaration ~v ~expr : T.declaration w = + and s_declaration : T.declaration w = fun ~substs -> function - Ast_typed.Declaration_constant (e, i, (env1, env2)) -> - let%bind e = s_named_expression ~v ~expr e in - let%bind env1 = s_full_environment ~v ~expr env1 in - let%bind env2 = s_full_environment ~v ~expr env2 in - ok @@ Ast_typed.Declaration_constant (e, i, (env1, env2)) + Ast_typed.Declaration_constant (e, inline, (env1, env2)) -> + let%bind e = s_named_expression ~substs e in + let%bind env1 = s_full_environment ~substs env1 in + let%bind env2 = s_full_environment ~substs env2 in + ok @@ Ast_typed.Declaration_constant (e, inline, (env1, env2)) - and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d -> - Trace.bind_map_location (s_declaration ~v ~expr) d + and s_declaration_wrap : T.declaration Location.wrap w = fun ~substs d -> + Trace.bind_map_location (s_declaration ~substs) d (* Replace the type variable ~v with ~expr everywhere within the program ~p. TODO: issues with scoping/shadowing. *) - and program ~(p : Ast_typed.program) ~(v:type_variable) ~expr : Ast_typed.program Trace.result = - Trace.bind_map_list (s_declaration_wrap ~v ~expr) p + and s_program : Ast_typed.program w = fun ~substs p -> + Trace.bind_map_list (s_declaration_wrap ~substs) p (* Computes `P[v := expr]`. *) - and type_value ~tv ~v ~expr = - let self tv = type_value ~tv ~v ~expr in + and type_value ~tv ~substs = + let self tv = type_value ~tv ~substs in + let (v, expr) = substs in match tv with - | P_variable v' when v' = v -> expr + | P_variable v' when Var.equal v' v -> expr | P_variable _ -> tv | P_constant (x , lst) -> ( let lst' = List.map self lst in @@ -280,7 +283,7 @@ module Substitution = struct P_apply ab' ) | P_forall p -> ( - let aux c = constraint_ ~c ~v ~expr in + let aux c = constraint_ ~c ~substs in let constraints = List.map aux p.constraints in if (p.binder = v) then ( P_forall { p with constraints } @@ -290,31 +293,33 @@ module Substitution = struct ) ) - and constraint_ ~c ~v ~expr = + and constraint_ ~c ~substs = match c with | C_equation ab -> ( - let ab' = pair_map (fun tv -> type_value ~tv ~v ~expr) ab in + let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in C_equation ab' ) | C_typeclass (tvs , tc) -> ( - let tvs' = List.map (fun tv -> type_value ~tv ~v ~expr) tvs in - let tc' = typeclass ~tc ~v ~expr in + let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in + let tc' = typeclass ~tc ~substs in C_typeclass (tvs' , tc') ) | C_access_label (tv , l , v') -> ( - let tv' = type_value ~tv ~v ~expr in + let tv' = type_value ~tv ~substs in C_access_label (tv' , l , v') ) - and typeclass ~tc ~v ~expr = - List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc + and typeclass ~tc ~substs = + List.map (List.map (fun tv -> type_value ~tv ~substs)) tc + + let program = s_program (* Performs beta-reduction at the root of the type *) let eval_beta_root ~(tv : type_value) = match tv with P_apply (P_forall { binder; constraints; body }, arg) -> - let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in - (type_value ~tv:body ~v:binder ~expr:arg , constraints) + let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in + (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:arg) , constraints) | _ -> (tv , []) end diff --git a/src/test/contracts/record.ligo b/src/test/contracts/record.ligo index 0b4921fb3..94b49d9fc 100644 --- a/src/test/contracts/record.ligo +++ b/src/test/contracts/record.ligo @@ -64,5 +64,5 @@ end function modify_inner (const r : double_record) : double_record is block { - r := r with record inner = r.inner with record b = 2048; end; end; + r := r with record inner.b = 2048; end; } with r diff --git a/src/test/contracts/record.mligo b/src/test/contracts/record.mligo index b898c41f1..4863cdf6c 100644 --- a/src/test/contracts/record.mligo +++ b/src/test/contracts/record.mligo @@ -50,4 +50,4 @@ type double_record = { inner : abc; } -let modify_inner (r : double_record) : double_record = {r with inner = {r.inner with b = 2048 }} +let modify_inner (r : double_record) : double_record = {r with inner.b = 2048 } diff --git a/src/test/contracts/record.religo b/src/test/contracts/record.religo index 3c723de34..c82801324 100644 --- a/src/test/contracts/record.religo +++ b/src/test/contracts/record.religo @@ -50,4 +50,4 @@ type double_record = { inner : abc, }; -let modify_inner = (r : double_record) : double_record => {...r,inner : {...r.inner, b : 2048 } }; +let modify_inner = (r : double_record) : double_record => {...r,inner.b : 2048 }; diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index b3a5c5b18..b34ef7554 100644 --- a/src/test/typer_tests.ml +++ b/src/test/typer_tests.ml @@ -12,7 +12,7 @@ let int () : unit result = let open Typer in let e = Environment.full_empty in let state = Typer.Solver.initial_state in - let%bind (post , new_state) = type_expression e state pre in + let%bind (post , new_state) = type_expression_subst e state pre in let () = Typer.Solver.discard_state new_state in let open! Typed in let open Combinators in @@ -27,7 +27,7 @@ module TestExpressions = struct let pre = expr in let open Typer in let open! Typed in - let%bind (post , new_state) = type_expression env state pre in + let%bind (post , new_state) = type_expression_subst env state pre in let () = Typer.Solver.discard_state new_state in let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in ok () @@ -37,7 +37,7 @@ module TestExpressions = struct module E = O let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ()) - let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) + let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) let bool () : unit result = test_expression I.(e_bool true) O.(t_bool ()) let string () : unit result = test_expression I.(e_string "s") O.(t_string ()) let bytes () : unit result = diff --git a/vendors/UnionFind/Partition0.ml b/vendors/UnionFind/Partition0.ml index cd8b26ffc..33616080b 100644 --- a/vendors/UnionFind/Partition0.ml +++ b/vendors/UnionFind/Partition0.ml @@ -38,12 +38,10 @@ module Make (Item: Partition.Item) = (* Printing *) - let print (p: partition) = - let buffer = Buffer.create 80 in + let print ppf p = let print src dst = - let link = - Printf.sprintf "%s -> %s\n" - (Item.to_string src) (Item.to_string dst) - in Buffer.add_string buffer link - in (ItemMap.iter print p; buffer) + Format.fprintf ppf "%s -> %s (%s)\n" + (Item.to_string src) (Item.to_string dst) (Item.to_string (repr src p)) + in ItemMap.iter print p + end