Merge branch 'dev' of gitlab.com:ligolang/ligo into rinderknecht@pprint

This commit is contained in:
Christian Rinderknecht 2020-05-30 13:50:43 +02:00
commit 3264277310
35 changed files with 384 additions and 1029 deletions

View File

@ -63,12 +63,14 @@ test:
- /^.*-run-dev$/
script:
- nix-build nix -A ligo-coverage
- cat result/share/coverage-all
- cp -Lr --no-preserve=mode,ownership,timestamps result/share/coverage .
artifacts:
paths:
- coverage
webide-e2e:
# Strange race conditions, disable for now
.webide-e2e:
extends: .nix
only:
- merge_requests

View File

@ -133,19 +133,16 @@ in {
echo "Coverage:"
BISECT_ENABLE=yes dune runtest --force
bisect-ppx-report html -o $out/share/coverage/all --title="LIGO overall test coverage"
bisect-ppx-report summary --per-file
bisect-ppx-report summary --per-file > $out/share/coverage-all
echo "Test coverage:"
BISECT_ENABLE=yes dune runtest src/test --force
bisect-ppx-report html -o $out/share/coverage/ligo --title="LIGO test coverage"
bisect-ppx-report summary --per-file
echo "Doc coverage:"
BISECT_ENABLE=yes dune build @doc-test --force
bisect-ppx-report html -o $out/share/coverage/docs --title="LIGO doc coverage"
bisect-ppx-report summary --per-file
echo "CLI test coverage:"
BISECT_ENABLE=yes dune runtest src/bin/expect_tests
bisect-ppx-report html -o $out/share/coverage/cli --title="CLI test coverage"
bisect-ppx-report summary --per-file
'';
installPhase = "true";
});

View File

@ -7,7 +7,7 @@ let bad_contract basename =
let%expect_test _ =
run_ligo_good [ "measure-contract" ; contract "coase.ligo" ; "main" ] ;
[%expect {| 1700 bytes |}] ;
[%expect {| 1668 bytes |}] ;
run_ligo_good [ "measure-contract" ; contract "multisig.ligo" ; "main" ] ;
[%expect {| 995 bytes |}] ;
@ -276,7 +276,7 @@ let%expect_test _ =
DIG 7 ;
DUP ;
DUG 8 ;
NONE (pair (address %card_owner) (nat %card_pattern)) ;
NONE (pair address nat) ;
SWAP ;
UPDATE ;
DIG 2 ;

View File

@ -422,6 +422,56 @@ let rec opt_combine_drops (x : michelson) : michelson =
Prim (l, p, List.map opt_combine_drops args, annot)
| x -> x
(* number of type arguments for (some) prims, where we will strip
annots *)
let prim_type_args : prim -> int option = function
| I_NONE -> Some 1
| I_NIL -> Some 1
| I_EMPTY_SET -> Some 1
| I_EMPTY_MAP -> Some 2
| I_EMPTY_BIG_MAP -> Some 2
| I_LAMBDA -> Some 2
(* _not_ I_CONTRACT! annot is important there *)
(* but could include I_SELF, maybe? *)
| _ -> None
(* returns (List.firstn n xs, List.skipn n xs) as in Coq (OCaml stdlib
does not have those...) *)
let split_at (n : int) (xs : 'a list) : 'a list * 'a list =
let rec aux n acc =
if n <= 0
then acc
else
let (bef, aft) = acc in
match aft with
| [] -> acc
| x :: aft ->
aux (n - 1) (x :: bef, aft) in
let (bef, aft) = aux n ([], xs) in
(List.rev bef, aft)
(* strip annots from type arguments in some instructions *)
let rec opt_strip_annots (x : michelson) : michelson =
match x with
| Seq (l, args) ->
let args = List.map opt_strip_annots args in
Seq (l, args)
| Prim (l, p, args, annot) ->
begin
match prim_type_args p with
| Some n ->
let (type_args, args) = split_at n args in
(* strip annots from type args *)
let type_args = List.map strip_annots type_args in
(* recur into remaining args *)
let args = List.map opt_strip_annots args in
Prim (l, p, type_args @ args, annot)
| None ->
let args = List.map opt_strip_annots args in
Prim (l, p, args, annot)
end
| x -> x
let optimize : michelson -> michelson =
fun x ->
let x = use_lambda_instr x in
@ -436,4 +486,5 @@ let optimize : michelson -> michelson =
] in
let x = iterate_optimizer (sequence_optimizers optimizers) x in
let x = opt_combine_drops x in
let x = opt_strip_annots x in
x

View File

@ -2,7 +2,7 @@ open Ast_typed
open Format
module UF = UnionFind.Poly2
let type_constraint_ : _ -> type_constraint_simpl_ -> unit = fun ppf ->
let type_constraint_ : _ -> type_constraint_simpl -> unit = fun ppf ->
function
|SC_Constructor { tv; c_tag; tv_list=_ } ->
let ct = match c_tag with
@ -34,8 +34,8 @@ let type_constraint_ : _ -> type_constraint_simpl_ -> unit = fun ppf ->
|SC_Poly _ -> fprintf ppf "Poly"
|SC_Typeclass _ -> fprintf ppf "TC"
let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf { reason_simpl ; c_simpl } ->
fprintf ppf "%a (reason: %s)" type_constraint_ c_simpl reason_simpl
let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf c ->
fprintf ppf "%a (reason: %s)" type_constraint_ c (reason_simpl c)
let all_constraints ppf ac =
fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac

View File

@ -159,7 +159,7 @@ 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 dbs = match new_constraint.c_simpl with
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 = []}
@ -173,7 +173,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
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.c_simpl with
match new_constraint with
| SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) ->
let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in
let dbs = {dbs with assignments} in
@ -191,7 +191,7 @@ let type_level_eval : type_value -> type_value * type_constraint list =
<polymorphic types are allowed. *)
let check_applied ((reduced, _new_constraints) as x) =
let () = match reduced with
P_apply _ -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
{ tsrc = _ ; t = P_apply _ } -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
| _ -> ()
in x
@ -210,16 +210,16 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
fun dbs new_constraint ->
let insert_fresh a b =
let fresh = Core.fresh_type_variable () in
let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a "normalizer: simpl") in
let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b "normalizer: simpl") in
let (dbs , cs1) = normalizer_simpl dbs (c_equation { tsrc = "solver: normalizer: simpl 1" ; t = P_variable fresh } a "normalizer: simpl 1") in
let (dbs , cs2) = normalizer_simpl dbs (c_equation { tsrc = "solver: normalizer: simpl 2" ; t = P_variable fresh } b "normalizer: simpl 2") in
(dbs , cs1 @ cs2) in
let split_constant a c_tag args =
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_constant") (List.combine fresh_vars args) in
let fresh_eqns = List.map (fun (v,t) -> c_equation { tsrc = "solver: normalizer: split_constant" ; t = P_variable v } t "normalizer: split_constant") (List.combine fresh_vars args) in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
(dbs , [{c_simpl=SC_Constructor {tv=a;c_tag;tv_list=fresh_vars};reason_simpl="normalizer: split constant"}] @ List.flatten recur) in
let gather_forall a forall = (dbs , [{c_simpl=SC_Poly { tv=a; forall };reason_simpl="normalizer: gather_forall"}]) in
let gather_alias a b = (dbs , [{c_simpl=SC_Alias { a ; b };reason_simpl="normalizer: gather_alias"}]) in
(dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars;reason_constr_simpl=Format.asprintf "normalizer: split constant %a = %a (%a)" Var.pp a Ast_typed.PP_generic.constant_tag c_tag (PP_helpers.list_sep Ast_typed.PP_generic.type_value (fun ppf () -> Format.fprintf ppf ", ")) args}] @ List.flatten recur) in
let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall ; reason_poly_simpl="normalizer: gather_forall"}]) in
let gather_alias a b = (dbs , [SC_Alias { a ; b ; reason_alias_simpl="normalizer: gather_alias"}]) in
let reduce_type_app a b =
let (reduced, new_constraints) = check_applied @@ type_level_eval b in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in
@ -227,27 +227,27 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
(dbs , resimpl @ List.flatten recur) in
let split_typeclass args tc =
let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_typeclass") (List.combine fresh_vars args) in
let fresh_eqns = List.map (fun (v,t) -> c_equation { tsrc = "solver: normalizer: split typeclass" ; t = P_variable v} t "normalizer: split_typeclass") (List.combine fresh_vars args) in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
(dbs, [{c_simpl=SC_Typeclass { tc ; args = fresh_vars };reason_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
(dbs, [SC_Typeclass { tc ; args = fresh_vars ; reason_typeclass_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
match new_constraint.c with
(* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *)
| C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)} -> insert_fresh a b
| C_equation {aval=({ tsrc = _ ; t = P_forall _ } as a); bval=({ tsrc = _ ; t = P_forall _ } as b)} -> insert_fresh a b
(* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *)
| C_equation {aval=(P_forall _ as a); bval=(P_constant _ as b)} -> insert_fresh a b
| C_equation {aval=({ tsrc = _ ; t = P_forall _ } as a); bval=({ tsrc = _ ; t = P_constant _ } as b)} -> insert_fresh a b
(* break down (c(args) = c'(args')) into ('a = c(args) and 'a = c'(args')) *)
| C_equation {aval=(P_constant _ as a); bval=(P_constant _ as b)} -> insert_fresh a b
| C_equation {aval=({ tsrc = _ ; t = P_constant _ } as a); bval=({ tsrc = _ ; t = P_constant _ } as b)} -> insert_fresh a b
(* break down (c(args) = forall 'b, body) into ('a = c(args) and 'a = forall 'b, body) *)
| C_equation {aval=(P_constant _ as a); bval=(P_forall _ as b)} -> insert_fresh a b
| C_equation {aval=(P_forall forall); bval=(P_variable b)} -> gather_forall b forall
| C_equation {aval=P_variable a; bval=P_forall forall} -> gather_forall a forall
| C_equation {aval=P_variable a; bval=P_variable b} -> gather_alias a b
| C_equation {aval=P_variable a; bval=P_constant { p_ctor_tag; p_ctor_args }} -> split_constant a p_ctor_tag p_ctor_args
| C_equation {aval=P_constant {p_ctor_tag; p_ctor_args}; bval=P_variable b} -> split_constant b p_ctor_tag p_ctor_args
| C_equation {aval=({ tsrc = _ ; t = P_constant _ } as a); bval=({ tsrc = _ ; t = P_forall _ } as b)} -> insert_fresh a b
| C_equation {aval={ tsrc = _ ; t = P_forall forall }; bval={ tsrc = _ ; t = P_variable b }} -> gather_forall b forall
| C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_forall forall }} -> gather_forall a forall
| C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_variable b }} -> gather_alias a b
| C_equation {aval={ tsrc = _ ; t = P_variable a }; bval={ tsrc = _ ; t = P_constant { p_ctor_tag; p_ctor_args } }} -> split_constant a p_ctor_tag p_ctor_args
| C_equation {aval={ tsrc = _ ; t = P_constant {p_ctor_tag; p_ctor_args} }; bval={ tsrc = _ ; t = P_variable b }} -> split_constant b p_ctor_tag p_ctor_args
(* Reduce the type-level application, and simplify the resulting constraint + the extra constraints (typeclasses) that appeared at the forall binding site *)
| C_equation {aval=(_ as a); bval=(P_apply _ as b)} -> reduce_type_app a b
| C_equation {aval=(P_apply _ as a); bval=(_ as b)} -> reduce_type_app b a
| C_equation {aval=(_ as a); bval=({ tsrc = _ ; t = P_apply _ } as b)} -> reduce_type_app a b
| C_equation {aval=({ tsrc = _ ; t = P_apply _ } as a); bval=(_ as b)} -> reduce_type_app b a
(* break down (TC(args)) into (TC('a, …) and ('a = arg)) *)
| C_typeclass { tc_args; typeclass } -> split_typeclass tc_args typeclass
| C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO" (* tv, label, result *)
@ -323,9 +323,9 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con
* For now: break pair(a, b) = pair(c, d) into a = c, b = d *)
let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector =
(* find two rules with the shape a = k(var …) and a = k'(var' …) *)
(* find two rules with the shape x = k(var …) and x = k'(var' …) *)
fun type_constraint_simpl dbs ->
match type_constraint_simpl.c_simpl with
match type_constraint_simpl with
SC_Constructor c ->
(* finding other constraints related to the same type variable and
with the same sort of constraint (constructor vs. constructor)
@ -470,10 +470,14 @@ let propagator_break_ctor : output_break_ctor propagator =
let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
let a = selected.a_k_var in
let b = selected.a_k'_var' in
(* The selector is expected to provice two constraints with the shape x = k(var …) and x = k'(var' …) *)
assert (Var.equal (a : c_constructor_simpl).tv (b : c_constructor_simpl).tv);
(* produce constraints: *)
(* a.tv = b.tv *)
let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) "propagator: break_ctor" in
let eq1 = c_equation { tsrc = "solver: propagator: break_ctor a" ; t = P_variable a.tv} { tsrc = "solver: propagator: break_ctor b" ; t = P_variable b.tv} "propagator: break_ctor" in
(* a.c_tag = b.c_tag *)
if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then
failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag))
@ -482,7 +486,7 @@ let propagator_break_ctor : output_break_ctor propagator =
if List.length a.tv_list <> List.length b.tv_list then
failwith "type error: incompatible types, not same length"
else
let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb) "propagator: break_ctor") a.tv_list b.tv_list in
let eqs3 = List.map2 (fun aa bb -> c_equation { tsrc = "solver: propagator: break_ctor aa" ; t = P_variable aa} { tsrc = "solver: propagator: break_ctor bb" ; t = P_variable bb} "propagator: break_ctor") a.tv_list b.tv_list in
let eqs = eq1 :: eqs3 in
(eqs , []) (* no new assignments *)
@ -507,7 +511,12 @@ let compare_label (a:label) (b:label) =
let Label b = b in
String.compare a b
let rec compare_typeclass a b = compare_list (compare_list compare_type_expression) a b
and compare_type_expression = function
and compare_type_expression { tsrc = _ ; t = ta } { tsrc = _ ; t = tb } =
(* Note: this comparison ignores the tsrc, the idea is that types
will often be compared to see if they are the same, regardless of
where the type comes from .*)
compare_type_expression_ ta tb
and compare_type_expression_ = function
| P_forall { binder=a1; constraints=a2; body=a3 } -> (function
| P_forall { binder=b1; constraints=b2; body=b3 } ->
compare_type_variable a1 b1 <? fun () ->
@ -559,7 +568,9 @@ let compare_p_forall
let compare_c_poly_simpl { tv = a1; forall = a2 } { tv = b1; forall = b2 } =
compare_type_variable a1 b1 <? fun () ->
compare_p_forall a2 b2
let compare_c_constructor_simpl { tv=a1; c_tag=a2; tv_list=a3 } { tv=b1; c_tag=b2; tv_list=b3 } =
let compare_c_constructor_simpl { reason_constr_simpl = _ ; tv=a1; c_tag=a2; tv_list=a3 } { reason_constr_simpl = _ ; tv=b1; c_tag=b2; tv_list=b3 } =
(* We do not compare the reasons, as they are only for debugging and
not part of the type *)
compare_type_variable a1 b1 <? fun () -> compare_simple_c_constant a2 b2 <? fun () -> compare_list compare_type_variable a3 b3
let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var = b2 } =
@ -570,21 +581,21 @@ let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_va
compare_c_constructor_simpl a1 b1 <? fun () -> compare_c_constructor_simpl a2 b2
let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector =
(* find two rules with the shape (a = forall b, d) and a = k'(var' …) or vice versa *)
(* find two rules with the shape (x = forall b, d) and x = k'(var' …) or vice versa *)
(* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *)
(* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *)
fun type_constraint_simpl dbs ->
match type_constraint_simpl.c_simpl with
match type_constraint_simpl with
SC_Constructor c ->
(* vice versa *)
let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in
let other_cs = List.filter (fun (x : c_poly_simpl) -> c.tv = x.tv) other_cs in (* TODO: does equality work in OCaml? *)
let other_cs = List.filter (fun (x : c_poly_simpl) -> Var.equal c.tv x.tv) other_cs in
let cs_pairs = List.map (fun x -> { poly = x ; a_k_var = c }) other_cs in
WasSelected cs_pairs
| SC_Alias _ -> WasNotSelected (* TODO: ??? *)
| SC_Poly p ->
let other_cs = (UnionFindWrapper.get_constraints_related_to p.tv dbs).constructor in
let other_cs = List.filter (fun (x : c_constructor_simpl) -> x.tv = p.tv) other_cs in (* TODO: does equality work in OCaml? *)
let other_cs = List.filter (fun (x : c_constructor_simpl) -> Var.equal x.tv p.tv) other_cs in
let cs_pairs = List.map (fun x -> { poly = p ; a_k_var = x }) other_cs in
WasSelected cs_pairs
| SC_Typeclass _ -> WasNotSelected
@ -594,30 +605,30 @@ let propagator_specialize1 : output_specialize1 propagator =
let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
let a = selected.poly in
let b = selected.a_k_var in
let () = if (a.tv <> b.tv) then failwith "internal error" else () in
(* The selector is expected to provice two constraints with the shape (x = forall y, z) and x = k'(var' …) *)
assert (Var.equal (a : c_poly_simpl).tv (b : c_constructor_simpl).tv);
(* produce constraints: *)
(* create a fresh existential variable to instantiate the polymorphic type b *)
(* create a fresh existential variable to instantiate the polymorphic type y *)
let fresh_existential = Core.fresh_type_variable () in
(* Produce the constraint (b.tv = a.body[a.binder |-> fresh_existential])
The substitution is obtained by immediately applying the forall. *)
let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in
let apply = { tsrc = "solver: propagator: specialize1 apply" ; t = P_apply {tf = { tsrc = "solver: propagator: specialize1 tf" ; t = P_forall a.forall }; targ = { tsrc = "solver: propagator: specialize1 targ" ; t = P_variable fresh_existential }} } in
let (reduced, new_constraints) = check_applied @@ type_level_eval apply in
let eq1 = c_equation (P_variable b.tv) reduced "propagator: specialize1" in
let eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in
let eqs = eq1 :: new_constraints in
(eqs, []) (* no new assignments *)
let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
let mem elt set = match RedBlackTrees.PolySet.find_opt elt set with None -> false | Some _ -> true in
fun selector propagator ->
fun already_selected old_type_constraint dbs ->
(* TODO: thread some state to know which selector outputs were already seen *)
match selector old_type_constraint dbs with
WasSelected selected_outputs ->
(* TODO: fold instead. *)
let (already_selected , selected_outputs) = List.fold_left (fun (already_selected, selected_outputs) elt -> if mem elt already_selected then (RedBlackTrees.PolySet.add elt already_selected , elt :: selected_outputs)
else (already_selected , selected_outputs)) (already_selected , selected_outputs) selected_outputs in
let open RedBlackTrees.PolySet in
let { set = already_selected ; duplicates = _ ; added = selected_outputs } = add_list selected_outputs already_selected in
(* Call the propagation rule *)
let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in
let (new_constraints , new_assignments) = List.split new_contraints_and_assignments in

View File

@ -420,8 +420,7 @@ and type_lambda e state {
let e' = Environment.add_ez_binder (binder) fresh e in
let%bind (result , state') = type_expression e' state result in
let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' result.type_expression in
ok (({binder;result}:O.lambda),state',wrapped)
and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =

View File

@ -44,7 +44,7 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
| T_arrow {type1;type2} ->
p_constant C_arrow (List.map type_expression_to_type_value [ type1 ; type2 ])
| T_variable (type_name) -> P_variable type_name
| T_variable (type_name) -> { tsrc = "wrap: from source code maybe?" ; t = P_variable type_name }
| T_constant (type_name) ->
let csttag = T.(match type_name with
| TC_unit -> C_unit
@ -89,7 +89,7 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
p_constant C_record (List.map type_expression_to_type_value_copypasted tlist)
| T_arrow {type1;type2} ->
p_constant C_arrow (List.map type_expression_to_type_value_copypasted [ type1 ; type2 ])
| T_variable type_name -> P_variable (type_name) (* eird stuff*)
| T_variable type_name -> { tsrc = "wrap: from source code maybe?" ; t = P_variable type_name }
| T_constant (type_name) ->
let csttag = T.(match type_name with
| TC_unit -> C_unit
@ -121,12 +121,12 @@ let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr ->
let pattern = type_expression_to_type_value expr in
let type_name = Core.fresh_type_variable () in
[{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: variable" }] , type_name
[{ c = C_equation { aval = { tsrc = "wrap: variable: whole" ; t = P_variable type_name } ; bval = pattern } ; reason = "wrap: variable" }] , type_name
let literal : T.type_expression -> (constraints * T.type_variable) = fun t ->
let pattern = type_expression_to_type_value t in
let type_name = Core.fresh_type_variable () in
[{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: literal" }] , type_name
[{ c = C_equation { aval = { tsrc = "wrap: literal: whole" ; t = P_variable type_name } ; bval = pattern } ; reason = "wrap: literal" }] , type_name
(*
let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@ -144,7 +144,7 @@ let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys
let patterns = List.map type_expression_to_type_value tys in
let pattern = p_constant C_record patterns in
let type_name = Core.fresh_type_variable () in
[{ c = C_equation { aval = P_variable type_name ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
[{ c = C_equation { aval = { tsrc = "wrap: tuple: whole" ; t = P_variable type_name } ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
(* let t_tuple = ('label:int, 'v) … -> record ('label : 'v)*)
(* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *)
@ -184,25 +184,25 @@ let constructor
let sum = type_expression_to_type_value sum in
let whole_expr = Core.fresh_type_variable () in
[
c_equation (P_variable whole_expr) sum "wrap: constructor: whole" ;
c_equation { tsrc = "wrap: constructor: whole" ; t = P_variable whole_expr } sum "wrap: constructor: whole" ;
c_equation t_arg c_arg "wrap: construcotr: arg" ;
] , whole_expr
let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields ->
let record_type = type_expression_to_type_value (T.t_record fields ()) in
let whole_expr = Core.fresh_type_variable () in
[c_equation (P_variable whole_expr) record_type "wrap: record: whole"] , whole_expr
[c_equation { tsrc = "wrap: record: whole" ; t = P_variable whole_expr } record_type "wrap: record: whole"] , whole_expr
let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
fun ctor element_tys ->
let elttype = T.P_variable (Core.fresh_type_variable ()) in
let elttype = T.{ tsrc = "wrap: collection: p_variable" ; t = P_variable (Core.fresh_type_variable ()) } in
let aux elt =
let elt' = type_expression_to_type_value elt
in c_equation elttype elt' "wrap: collection: elt" in
let equations = List.map aux element_tys in
let whole_expr = Core.fresh_type_variable () in
[
c_equation (P_variable whole_expr) (p_constant ctor [elttype]) "wrap: collection: whole" ;
c_equation { tsrc = "wrap: collection: whole" ; t = P_variable whole_expr} (p_constant ctor [elttype]) "wrap: collection: whole" ;
] @ equations , whole_expr
let list = collection T.C_list
@ -210,8 +210,8 @@ let set = collection T.C_set
let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
let k_type = T.P_variable (Core.fresh_type_variable ()) in
let v_type = T.P_variable (Core.fresh_type_variable ()) in
let k_type = T.{ tsrc = "wrap: map: k" ; t = P_variable (Core.fresh_type_variable ()) } in
let v_type = T.{ tsrc = "wrap: map: v" ; t = P_variable (Core.fresh_type_variable ()) } in
let aux_k (k , _v) =
let k' = type_expression_to_type_value k in
c_equation k_type k' "wrap: map: key" in
@ -222,13 +222,13 @@ let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_
let equations_v = List.map aux_v kv_tys in
let whole_expr = Core.fresh_type_variable () in
[
c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
c_equation ({ tsrc = "wrap: map: whole" ; t = P_variable whole_expr }) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
] @ equations_k @ equations_v , whole_expr
let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
fun kv_tys ->
let k_type = T.P_variable (Core.fresh_type_variable ()) in
let v_type = T.P_variable (Core.fresh_type_variable ()) in
let k_type = T.{ tsrc = "wrap: big_map: k" ; t = P_variable (Core.fresh_type_variable ()) } in
let v_type = T.{ tsrc = "wrap: big_map: v" ; t = P_variable (Core.fresh_type_variable ()) } in
let aux_k (k , _v) =
let k' = type_expression_to_type_value k in
c_equation k_type k' "wrap: big_map: key" in
@ -241,7 +241,7 @@ let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.t
[
(* TODO: this doesn't tag big_maps uniquely (i.e. if two
big_map have the same type, they can be swapped. *)
c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
c_equation ({ tsrc = "wrap: big_map: whole" ; t = P_variable whole_expr}) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
] @ equations_k @ equations_v , whole_expr
let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -250,7 +250,7 @@ let application : T.type_expression -> T.type_expression -> (constraints * T.typ
let f' = type_expression_to_type_value f in
let arg' = type_expression_to_type_value arg in
[
c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) "wrap: application: f" ;
c_equation f' (p_constant C_arrow [arg' ; { tsrc = "wrap: application: whole" ; t = P_variable whole_expr }]) "wrap: application: f" ;
] , whole_expr
let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -258,10 +258,10 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va
let ds' = type_expression_to_type_value ds in
let ind' = type_expression_to_type_value ind in
let whole_expr = Core.fresh_type_variable () in
let v = Core.fresh_type_variable () in
let v = T.{ tsrc = "wrap: look_up: ds" ; t = P_variable (Core.fresh_type_variable ()) } in
[
c_equation ds' (p_constant C_map [ind' ; P_variable v]) "wrap: look_up: map" ;
c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) "wrap: look_up: whole" ;
c_equation ds' (p_constant C_map [ind' ; v]) "wrap: look_up: map" ;
c_equation ({ tsrc = "wrap: look_up: whole" ; t = P_variable whole_expr }) (p_constant C_option [v]) "wrap: look_up: whole" ;
] , whole_expr
let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -271,7 +271,7 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v
let whole_expr = Core.fresh_type_variable () in
[
c_equation a' (p_constant C_unit []) "wrap: sequence: first" ;
c_equation b' (P_variable whole_expr) "wrap: sequence: second (whole)" ;
c_equation b' ({ tsrc = "wrap: sequence: whole" ; t = P_variable whole_expr}) "wrap: sequence: second (whole)" ;
] , whole_expr
let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -280,9 +280,9 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
let body' = type_expression_to_type_value body in
let whole_expr = Core.fresh_type_variable () in
[
c_equation expr' (P_variable Stage_common.Constant.t_bool) "wrap: loop: expr" ;
c_equation expr' ({ tsrc = "built-in type" ; t = P_variable Stage_common.Constant.t_bool }) "wrap: loop: expr" ;
c_equation body' (p_constant C_unit []) "wrap: loop: body" ;
c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: loop: whole (unit)" ;
c_equation (p_constant C_unit []) ({ tsrc = "wrap: loop: whole" ; t = P_variable whole_expr}) "wrap: loop: whole (unit)" ;
] , whole_expr
let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) =
@ -294,7 +294,7 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression
| Some annot -> [c_equation rhs' (type_expression_to_type_value annot) "wrap: let_in: rhs"] in
let whole_expr = Core.fresh_type_variable () in
[
c_equation result' (P_variable whole_expr) "wrap: let_in: result (whole)" ;
c_equation result' { tsrc = "wrap: let_in: whole" ; t = P_variable whole_expr } "wrap: let_in: result (whole)" ;
] @ rhs_tv_opt', whole_expr
let recursive : T.type_expression -> (constraints * T.type_variable) =
@ -302,7 +302,7 @@ let recursive : T.type_expression -> (constraints * T.type_variable) =
let fun_type = type_expression_to_type_value fun_type in
let whole_expr = Core.fresh_type_variable () in
[
c_equation fun_type (P_variable whole_expr) "wrap: recursive: fun_type (whole)" ;
c_equation fun_type ({ tsrc = "wrap: recursive: whole" ; t = P_variable whole_expr }) "wrap: recursive: fun_type (whole)" ;
], whole_expr
let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -312,7 +312,7 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var
let whole_expr = Core.fresh_type_variable () in
[
c_equation v' e' "wrap: assign: var type must eq rhs type" ;
c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: assign: unit (whole)" ;
c_equation { tsrc = "wrap: assign: whole" ; t = P_variable whole_expr } (p_constant C_unit []) "wrap: assign: unit (whole)" ;
] , whole_expr
let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@ -322,14 +322,14 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type
let whole_expr = Core.fresh_type_variable () in
[
c_equation e' annot' "wrap: annotation: expr type must eq annot" ;
c_equation e' (P_variable whole_expr) "wrap: annotation: whole" ;
c_equation e' { tsrc = "wrap: annotation: whole" ; t = P_variable whole_expr } "wrap: annotation: whole" ;
] , whole_expr
let matching : T.type_expression list -> (constraints * T.type_variable) =
fun es ->
let whole_expr = Core.fresh_type_variable () in
let type_expressions = (List.map type_expression_to_type_value es) in
let cs = List.map (fun e -> c_equation (P_variable whole_expr) e "wrap: matching: case (whole)") type_expressions
let cs = List.map (fun e -> c_equation { tsrc = "wrap: matching: case" ; t = P_variable whole_expr } e "wrap: matching: case (whole)") type_expressions
in cs, whole_expr
let fresh_binder () =
@ -339,24 +339,26 @@ let lambda
: T.type_expression ->
T.type_expression option ->
T.type_expression option ->
T.type_expression ->
(constraints * T.type_variable) =
fun fresh arg body ->
fun fresh arg output result ->
let whole_expr = Core.fresh_type_variable () in
let unification_arg = Core.fresh_type_variable () in
let unification_body = Core.fresh_type_variable () in
let unification_arg = T.{ tsrc = "wrap: lambda: arg" ; t = P_variable (Core.fresh_type_variable ()) } in
let unification_output = T.{ tsrc = "wrap: lambda: whole" ; t = P_variable (Core.fresh_type_variable ()) } in
let result' = type_expression_to_type_value result in
let arg' = match arg with
None -> []
| Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
let body' = match body with
| Some arg -> [c_equation unification_arg (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
let output' = match output with
None -> []
| Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body) "wrap: lambda: body annot"]
| Some output -> [c_equation unification_output (type_expression_to_type_value output) "wrap: lambda: output annot"]
in [
c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) "wrap: lambda: arg" ;
c_equation (P_variable whole_expr)
(p_constant C_arrow ([P_variable unification_arg ;
P_variable unification_body]))
c_equation unification_output result' "wrap: lambda: result" ;
c_equation (type_expression_to_type_value fresh) unification_arg "wrap: lambda: arg" ;
c_equation ({ tsrc = "wrap: lambda: whole" ; t = P_variable whole_expr })
(p_constant C_arrow ([unification_arg ; unification_output]))
"wrap: lambda: arrow (whole)"
] @ arg' @ body' , whole_expr
] @ arg' @ output' , whole_expr
(* This is pretty much a wrapper for an n-ary function. *)
let constant : O.type_value -> T.type_expression list -> (constraints * T.type_variable) =
@ -365,5 +367,5 @@ let constant : O.type_value -> T.type_expression list -> (constraints * T.type_v
let args' = List.map type_expression_to_type_value args in
let args_tuple = p_constant C_record args' in
[
c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) "wrap: constant: as declared for built-in"
c_equation f (p_constant C_arrow ([args_tuple ; { tsrc = "wrap: lambda: whole" ; t = P_variable whole_expr }])) "wrap: constant: as declared for built-in"
] , whole_expr

View File

@ -434,17 +434,17 @@ module Typer = struct
module Operators_types = struct
open Typesystem.Shorthands
let tc_subarg a b c = tc [a;b;c] [ (*TODO…*) ]
let tc_sizearg a = tc [a] [ [int] ]
let tc_packable a = tc [a] [ [int] ; [string] ; [bool] (*TODO…*) ]
let tc_timargs a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
let tc_edivargs a b c = tc [a;b;c] [ (*TODO…*) ]
let tc_divargs a b c = tc [a;b;c] [ (*TODO…*) ]
let tc_modargs a b c = tc [a;b;c] [ (*TODO…*) ]
let tc_addargs a b c = tc [a;b;c] [ (*TODO…*) ]
let tc_comparable a = tc [a] [ [nat] ; [int] ; [mutez] ; [timestamp] ]
let tc_concatable a = tc [a] [ [string] ; [bytes] ]
let tc_storable a = tc [a] [ [string] ; [bytes] ; (*Humm .. TODO ?*) ]
let tc_subarg a b c = tc "arguments for (-)" [a;b;c] [ (*TODO…*) ]
let tc_sizearg a = tc "arguments for size" [a] [ [int] ]
let tc_packable a = tc "packable" [a] [ [int] ; [string] ; [bool] (*TODO…*) ]
let tc_timargs a b c = tc "arguments for ( * )" [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
let tc_edivargs a b c = tc "arguments for ediv" [a;b;c] [ (*TODO…*) ]
let tc_divargs a b c = tc "arguments for div" [a;b;c] [ (*TODO…*) ]
let tc_modargs a b c = tc "arguments for mod" [a;b;c] [ (*TODO…*) ]
let tc_addargs a b c = tc "arguments for (+)" [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ]
let tc_comparable a = tc "comparable" [a] [ [nat] ; [int] ; [mutez] ; [timestamp] ]
let tc_concatable a = tc "concatenable" [a] [ [string] ; [bytes] ]
let tc_storable a = tc "storable" [a] [ [string] ; [bytes] ; (*Humm .. TODO ?*) ]
let t_none = forall "a" @@ fun a -> option a

View File

@ -3,6 +3,5 @@ include Types
(* include Misc *)
include Combinators
module Types = Types
module Misc = Misc
module PP=PP
module Combinators = Combinators

View File

@ -1,353 +0,0 @@
open Trace
open Types
open Stage_common.Helpers
module Errors = struct
let different_literals_because_different_types name a b () =
let title () = "literals have different types: " ^ name in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
let different_literals name a b () =
let title () = name ^ " are different" in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
let error_uncomparable_literals name a b () =
let title () = name ^ " are not comparable" in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
end
open Errors
let assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
| Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
| Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
| Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
| Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
| Literal_mutez a, Literal_mutez b when a = b -> ok ()
| Literal_mutez _, Literal_mutez _ -> fail @@ different_literals "different tezs" a b
| Literal_mutez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
| Literal_string a, Literal_string b when a = b -> ok ()
| Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
| Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
| Literal_bytes a, Literal_bytes b when a = b -> ok ()
| Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytess" a b
| Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
| Literal_void, Literal_void -> ok ()
| Literal_void, _ -> fail @@ different_literals_because_different_types "void vs non-void" a b
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
| Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
| Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
| Literal_signature a, Literal_signature b when a = b -> ok ()
| Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
| Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
| Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
| Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
| Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
| Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
| Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
| Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b
let rec assert_value_eq (a, b: (expression * expression )) : unit result =
Format.printf "in assert_value_eq %a %a\n%!" PP.expression a PP.expression b;
let error_content () =
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
in
trace (fun () -> error (thunk "not equal") error_content ()) @@
match (a.expression_content , b.expression_content) with
| E_literal a , E_literal b ->
assert_literal_eq (a, b)
| E_literal _ , _ ->
simple_fail "comparing a literal with not a literal"
| E_constant (ca) , E_constant (cb) when ca.cons_name = cb.cons_name -> (
let%bind lst =
generic_try (simple_error "constants with different number of elements")
(fun () -> List.combine ca.arguments cb.arguments) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_constant _ , E_constant _ ->
simple_fail "different constants"
| E_constant _ , _ ->
let error_content () =
Format.asprintf "%a vs %a"
PP.expression a
PP.expression b
in
fail @@ (fun () -> error (thunk "comparing constant with other expression") error_content ())
| E_constructor (ca), E_constructor (cb) when ca.constructor = cb.constructor -> (
let%bind _eq = assert_value_eq (ca.element, cb.element) in
ok ()
)
| E_constructor _, E_constructor _ ->
simple_fail "different constructors"
| E_constructor _, _ ->
simple_fail "comparing constructor with other expression"
| E_record sma, E_record smb -> (
let aux _ a b =
match a, b with
| Some a, Some b -> Some (assert_value_eq (a, b))
| _ -> Some (simple_fail "different record keys")
in
let%bind _all = bind_lmap @@ LMap.merge aux sma smb in
ok ()
)
| E_record _, _ ->
simple_fail "comparing record with other expression"
| E_record_update ura, E_record_update urb ->
let _ =
generic_try (simple_error "Updating different record") @@
fun () -> assert_value_eq (ura.record, urb.record) in
let aux (Label a,Label b) =
assert (String.equal a b)
in
let () = aux (ura.path, urb.path) in
let%bind () = assert_value_eq (ura.update,urb.update) in
ok ()
| E_record_update _, _ ->
simple_fail "comparing record update with other expression"
| E_tuple lsta, E_tuple lstb -> (
let%bind lst =
generic_try (simple_error "tuples with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_tuple _, _ ->
simple_fail "comparing tuple with other expression"
| E_tuple_update uta, E_tuple_update utb ->
let _ =
generic_try (simple_error "Updating different tuple") @@
fun () -> assert_value_eq (uta.tuple, utb.tuple) in
let () = assert (uta.path == utb.path) in
let%bind () = assert_value_eq (uta.update,utb.update) in
ok ()
| E_tuple_update _, _ ->
simple_fail "comparing tuple update with other expression"
| (E_map lsta, E_map lstb | E_big_map lsta, E_big_map lstb) -> (
let%bind lst = generic_try (simple_error "maps of different lengths")
(fun () ->
let lsta' = List.sort compare lsta in
let lstb' = List.sort compare lstb in
List.combine lsta' lstb') in
let aux = fun ((ka, va), (kb, vb)) ->
let%bind _ = assert_value_eq (ka, kb) in
let%bind _ = assert_value_eq (va, vb) in
ok () in
let%bind _all = bind_map_list aux lst in
ok ()
)
| (E_map _ | E_big_map _), _ ->
simple_fail "comparing map with other expression"
| E_list lsta, E_list lstb -> (
let%bind lst =
generic_try (simple_error "list of different lengths")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_list _, _ ->
simple_fail "comparing list with other expression"
| E_set lsta, E_set lstb -> (
let lsta' = List.sort (compare) lsta in
let lstb' = List.sort (compare) lstb in
let%bind lst =
generic_try (simple_error "set of different lengths")
(fun () -> List.combine lsta' lstb') in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_set _, _ ->
simple_fail "comparing set with other expression"
| (E_ascription a , _b') -> assert_value_eq (a.anno_expr , b)
| (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
| (E_variable _, _) | (E_lambda _, _)
| (E_application _, _) | (E_let_in _, _)
| (E_recursive _,_)
| (E_record_accessor _, _) | (E_tuple_accessor _, _)
| (E_look_up _, _)
| (E_matching _, _) | (E_cond _, _)
| (E_sequence _, _) | (E_skip, _)
| (E_assign _, _)
| (E_for _, _) | (E_for_each _, _)
| (E_while _, _) -> simple_fail "comparing not a value"
let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)
(* module Rename = struct
* open Trace
*
* module Type = struct
* (\* Type renaming, not needed. Yet. *\)
* end
*
* module Value = struct
* type renaming = string * (string * access_path) (\* src -> dst *\)
* type renamings = renaming list
* let filter (r:renamings) (s:string) : renamings =
* List.filter (fun (x, _) -> not (x = s)) r
* let filters (r:renamings) (ss:string list) : renamings =
* List.filter (fun (x, _) -> not (List.mem x ss)) r
*
* let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
* match i with
* | I_assignment ({name;annotated_expression = e} as a) -> (
* match List.assoc_opt name r with
* | None ->
* let%bind annotated_expression = rename_annotated_expression (filter r name) e in
* ok (I_assignment {a with annotated_expression})
* | Some (name', lst) -> (
* let%bind annotated_expression = rename_annotated_expression r e in
* match lst with
* | [] -> ok (I_assignment {name = name' ; annotated_expression})
* | lst ->
* let (hds, tl) =
* let open List in
* let r = rev lst in
* rev @@ tl r, hd r
* in
* let%bind tl' = match tl with
* | Access_record n -> ok n
* | Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
* ok (I_record_patch (name', hds, [tl', annotated_expression]))
* )
* )
* | I_skip -> ok I_skip
* | I_fail e ->
* let%bind e' = rename_annotated_expression r e in
* ok (I_fail e')
* | I_loop (cond, body) ->
* let%bind cond' = rename_annotated_expression r cond in
* let%bind body' = rename_block r body in
* ok (I_loop (cond', body'))
* | I_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_block r m in
* ok (I_matching (ae', m'))
* | I_record_patch (v, path, lst) ->
* let aux (x, y) =
* let%bind y' = rename_annotated_expression (filter r v) y in
* ok (x, y') in
* let%bind lst' = bind_map_list aux lst in
* match List.assoc_opt v r with
* | None -> (
* ok (I_record_patch (v, path, lst'))
* )
* | Some (v', path') -> (
* ok (I_record_patch (v', path' @ path, lst'))
* )
* and rename_block (r:renamings) (bl:block) : block result =
* bind_map_list (rename_instruction r) bl
*
* and rename_matching : type a . (renamings -> a -> a result) -> renamings -> a matching -> a matching result =
* fun f r m ->
* match m with
* | Match_bool { match_true = mt ; match_false = mf } ->
* let%bind match_true = f r mt in
* let%bind match_false = f r mf in
* ok (Match_bool {match_true ; match_false})
* | Match_option { match_none = mn ; match_some = (some, ms) } ->
* let%bind match_none = f r mn in
* let%bind ms' = f (filter r some) ms in
* ok (Match_option {match_none ; match_some = (some, ms')})
* | Match_list { match_nil = mn ; match_cons = (hd, tl, mc) } ->
* let%bind match_nil = f r mn in
* let%bind mc' = f (filters r [hd;tl]) mc in
* ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
* | Match_tuple (lst, body) ->
* let%bind body' = f (filters r lst) body in
* ok (Match_tuple (lst, body'))
*
* and rename_matching_instruction = fun x -> rename_matching rename_block x
*
* and rename_matching_expr = fun x -> rename_matching rename_expression x
*
* and rename_annotated_expression (r:renamings) (ae:annotated_expression) : annotated_expression result =
* let%bind expression = rename_expression r ae.expression in
* ok {ae with expression}
*
* and rename_expression : renamings -> expression -> expression result = fun r e ->
* match e with
* | E_literal _ as l -> ok l
* | E_constant (name, lst) ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_constant (name, lst'))
* | E_constructor (name, ae) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_constructor (name, ae'))
* | E_variable v -> (
* match List.assoc_opt v r with
* | None -> ok (E_variable v)
* | Some (name, path) -> ok (E_accessor (ae (E_variable (name)), path))
* )
* | E_lambda ({binder;body;result} as l) ->
* let r' = filter r binder in
* let%bind body = rename_block r' body in
* let%bind result = rename_annotated_expression r' result in
* ok (E_lambda {l with body ; result})
* | E_application (f, arg) ->
* let%bind f' = rename_annotated_expression r f in
* let%bind arg' = rename_annotated_expression r arg in
* ok (E_application (f', arg'))
* | E_tuple lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_tuple lst')
* | E_accessor (ae, p) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_accessor (ae', p))
* | E_record sm ->
* let%bind sm' = bind_smap
* @@ SMap.map (rename_annotated_expression r) sm in
* ok (E_record sm')
* | E_map m ->
* let%bind m' = bind_map_list
* (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
* ok (E_map m')
* | E_list lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_list lst')
* | E_look_up m ->
* let%bind m' = bind_map_pair (rename_annotated_expression r) m in
* ok (E_look_up m')
* | E_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_annotated_expression r m in
* ok (E_matching (ae', m'))
* end
* end *)

View File

@ -1,20 +0,0 @@
open Trace
open Types
(*
module Errors : sig
val different_literals_because_different_types : name -> literal -> literal -> unit -> error
val different_literals : name -> literal -> literal -> unit -> error
val error_uncomparable_literals : name -> literal -> literal -> unit -> error
end
val assert_literal_eq : ( literal * literal ) -> unit result
*)
val assert_value_eq : ( expression * expression ) -> unit result
val is_value_eq : ( expression * expression ) -> bool

View File

@ -3,6 +3,5 @@ include Types
(* include Misc *)
include Combinators
module Types = Types
module Misc = Misc
module PP=PP
module Combinators = Combinators

View File

@ -1,350 +0,0 @@
open Trace
open Types
open Stage_common.Helpers
module Errors = struct
let different_literals_because_different_types name a b () =
let title () = "literals have different types: " ^ name in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
let different_literals name a b () =
let title () = name ^ " are different" in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
let error_uncomparable_literals name a b () =
let title () = name ^ " are not comparable" in
let message () = "" in
let data = [
("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
("b" , fun () -> Format.asprintf "%a" PP.literal b )
] in
error ~data title message ()
end
open Errors
let assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with
| Literal_int a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
| Literal_nat a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
| Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
| Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
| Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
| Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
| Literal_mutez a, Literal_mutez b when a = b -> ok ()
| Literal_mutez _, Literal_mutez _ -> fail @@ different_literals "different tezs" a b
| Literal_mutez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
| Literal_string a, Literal_string b when a = b -> ok ()
| Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
| Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
| Literal_bytes a, Literal_bytes b when a = b -> ok ()
| Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytess" a b
| Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
| Literal_void, Literal_void -> ok ()
| Literal_void, _ -> fail @@ different_literals_because_different_types "void vs non-void" a b
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
| Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
| Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
| Literal_signature a, Literal_signature b when a = b -> ok ()
| Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
| Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
| Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
| Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
| Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
| Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
| Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
| Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b
let rec assert_value_eq (a, b: (expression * expression )) : unit result =
Format.printf "in assert_value_eq %a %a\n%!" PP.expression a PP.expression b;
let error_content () =
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
in
trace (fun () -> error (thunk "not equal") error_content ()) @@
match (a.expression_content , b.expression_content) with
| E_literal a , E_literal b ->
assert_literal_eq (a, b)
| E_literal _ , _ ->
simple_fail "comparing a literal with not a literal"
| E_constant (ca) , E_constant (cb) when ca.cons_name = cb.cons_name -> (
let%bind lst =
generic_try (simple_error "constants with different number of elements")
(fun () -> List.combine ca.arguments cb.arguments) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_constant _ , E_constant _ ->
simple_fail "different constants"
| E_constant _ , _ ->
let error_content () =
Format.asprintf "%a vs %a"
PP.expression a
PP.expression b
in
fail @@ (fun () -> error (thunk "comparing constant with other expression") error_content ())
| E_constructor (ca), E_constructor (cb) when ca.constructor = cb.constructor -> (
let%bind _eq = assert_value_eq (ca.element, cb.element) in
ok ()
)
| E_constructor _, E_constructor _ ->
simple_fail "different constructors"
| E_constructor _, _ ->
simple_fail "comparing constructor with other expression"
| E_record sma, E_record smb -> (
let aux _ a b =
match a, b with
| Some a, Some b -> Some (assert_value_eq (a, b))
| _ -> Some (simple_fail "different record keys")
in
let%bind _all = bind_lmap @@ LMap.merge aux sma smb in
ok ()
)
| E_record _, _ ->
simple_fail "comparing record with other expression"
| E_record_update ura, E_record_update urb ->
let _ =
generic_try (simple_error "Updating different record") @@
fun () -> assert_value_eq (ura.record, urb.record) in
let aux (Label a,Label b) =
assert (String.equal a b)
in
let () = aux (ura.path, urb.path) in
let%bind () = assert_value_eq (ura.update,urb.update) in
ok ()
| E_record_update _, _ ->
simple_fail "comparing record update with other expression"
| E_tuple lsta, E_tuple lstb -> (
let%bind lst =
generic_try (simple_error "tuples with different number of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| E_tuple _, _ ->
simple_fail "comparing tuple with other expression"
| E_tuple_update uta, E_tuple_update utb ->
let _ =
generic_try (simple_error "Updating different tuple") @@
fun () -> assert_value_eq (uta.tuple, utb.tuple) in
let () = assert (uta.path == utb.path) in
let%bind () = assert_value_eq (uta.update,utb.update) in
ok ()
| E_tuple_update _, _ ->
simple_fail "comparing tuple update with other expression"
| (E_map lsta, E_map lstb | E_big_map lsta, E_big_map lstb) -> (
let%bind lst = generic_try (simple_error "maps of different lengths")
(fun () ->
let lsta' = List.sort compare lsta in
let lstb' = List.sort compare lstb in
List.combine lsta' lstb') in
let aux = fun ((ka, va), (kb, vb)) ->
let%bind _ = assert_value_eq (ka, kb) in
let%bind _ = assert_value_eq (va, vb) in
ok () in
let%bind _all = bind_map_list aux lst in
ok ()
)
| (E_map _ | E_big_map _), _ ->
simple_fail "comparing map with other expression"
| E_list lsta, E_list lstb -> (
let%bind lst =
generic_try (simple_error "list of different lengths")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_list _, _ ->
simple_fail "comparing list with other expression"
| E_set lsta, E_set lstb -> (
let lsta' = List.sort (compare) lsta in
let lstb' = List.sort (compare) lstb in
let%bind lst =
generic_try (simple_error "set of different lengths")
(fun () -> List.combine lsta' lstb') in
let%bind _all = bind_map_list assert_value_eq lst in
ok ()
)
| E_set _, _ ->
simple_fail "comparing set with other expression"
| (E_ascription a , _b') -> assert_value_eq (a.anno_expr , b)
| (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
| (E_variable _, _) | (E_lambda _, _)
| (E_application _, _) | (E_let_in _, _)
| (E_recursive _,_)
| (E_record_accessor _, _) | (E_tuple_accessor _, _)
| (E_look_up _, _)
| (E_matching _, _) | (E_cond _, _)
| (E_sequence _, _) | (E_skip, _) -> simple_fail "comparing not a value"
let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)
(* module Rename = struct
* open Trace
*
* module Type = struct
* (\* Type renaming, not needed. Yet. *\)
* end
*
* module Value = struct
* type renaming = string * (string * access_path) (\* src -> dst *\)
* type renamings = renaming list
* let filter (r:renamings) (s:string) : renamings =
* List.filter (fun (x, _) -> not (x = s)) r
* let filters (r:renamings) (ss:string list) : renamings =
* List.filter (fun (x, _) -> not (List.mem x ss)) r
*
* let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
* match i with
* | I_assignment ({name;annotated_expression = e} as a) -> (
* match List.assoc_opt name r with
* | None ->
* let%bind annotated_expression = rename_annotated_expression (filter r name) e in
* ok (I_assignment {a with annotated_expression})
* | Some (name', lst) -> (
* let%bind annotated_expression = rename_annotated_expression r e in
* match lst with
* | [] -> ok (I_assignment {name = name' ; annotated_expression})
* | lst ->
* let (hds, tl) =
* let open List in
* let r = rev lst in
* rev @@ tl r, hd r
* in
* let%bind tl' = match tl with
* | Access_record n -> ok n
* | Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
* ok (I_record_patch (name', hds, [tl', annotated_expression]))
* )
* )
* | I_skip -> ok I_skip
* | I_fail e ->
* let%bind e' = rename_annotated_expression r e in
* ok (I_fail e')
* | I_loop (cond, body) ->
* let%bind cond' = rename_annotated_expression r cond in
* let%bind body' = rename_block r body in
* ok (I_loop (cond', body'))
* | I_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_block r m in
* ok (I_matching (ae', m'))
* | I_record_patch (v, path, lst) ->
* let aux (x, y) =
* let%bind y' = rename_annotated_expression (filter r v) y in
* ok (x, y') in
* let%bind lst' = bind_map_list aux lst in
* match List.assoc_opt v r with
* | None -> (
* ok (I_record_patch (v, path, lst'))
* )
* | Some (v', path') -> (
* ok (I_record_patch (v', path' @ path, lst'))
* )
* and rename_block (r:renamings) (bl:block) : block result =
* bind_map_list (rename_instruction r) bl
*
* and rename_matching : type a . (renamings -> a -> a result) -> renamings -> a matching -> a matching result =
* fun f r m ->
* match m with
* | Match_bool { match_true = mt ; match_false = mf } ->
* let%bind match_true = f r mt in
* let%bind match_false = f r mf in
* ok (Match_bool {match_true ; match_false})
* | Match_option { match_none = mn ; match_some = (some, ms) } ->
* let%bind match_none = f r mn in
* let%bind ms' = f (filter r some) ms in
* ok (Match_option {match_none ; match_some = (some, ms')})
* | Match_list { match_nil = mn ; match_cons = (hd, tl, mc) } ->
* let%bind match_nil = f r mn in
* let%bind mc' = f (filters r [hd;tl]) mc in
* ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
* | Match_tuple (lst, body) ->
* let%bind body' = f (filters r lst) body in
* ok (Match_tuple (lst, body'))
*
* and rename_matching_instruction = fun x -> rename_matching rename_block x
*
* and rename_matching_expr = fun x -> rename_matching rename_expression x
*
* and rename_annotated_expression (r:renamings) (ae:annotated_expression) : annotated_expression result =
* let%bind expression = rename_expression r ae.expression in
* ok {ae with expression}
*
* and rename_expression : renamings -> expression -> expression result = fun r e ->
* match e with
* | E_literal _ as l -> ok l
* | E_constant (name, lst) ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_constant (name, lst'))
* | E_constructor (name, ae) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_constructor (name, ae'))
* | E_variable v -> (
* match List.assoc_opt v r with
* | None -> ok (E_variable v)
* | Some (name, path) -> ok (E_accessor (ae (E_variable (name)), path))
* )
* | E_lambda ({binder;body;result} as l) ->
* let r' = filter r binder in
* let%bind body = rename_block r' body in
* let%bind result = rename_annotated_expression r' result in
* ok (E_lambda {l with body ; result})
* | E_application (f, arg) ->
* let%bind f' = rename_annotated_expression r f in
* let%bind arg' = rename_annotated_expression r arg in
* ok (E_application (f', arg'))
* | E_tuple lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_tuple lst')
* | E_accessor (ae, p) ->
* let%bind ae' = rename_annotated_expression r ae in
* ok (E_accessor (ae', p))
* | E_record sm ->
* let%bind sm' = bind_smap
* @@ SMap.map (rename_annotated_expression r) sm in
* ok (E_record sm')
* | E_map m ->
* let%bind m' = bind_map_list
* (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
* ok (E_map m')
* | E_list lst ->
* let%bind lst' = bind_map_list (rename_annotated_expression r) lst in
* ok (E_list lst')
* | E_look_up m ->
* let%bind m' = bind_map_pair (rename_annotated_expression r) m in
* ok (E_look_up m')
* | E_matching (ae, m) ->
* let%bind ae' = rename_annotated_expression r ae in
* let%bind m' = rename_matching rename_annotated_expression r m in
* ok (E_matching (ae', m'))
* end
* end *)

View File

@ -1,20 +0,0 @@
open Trace
open Types
(*
module Errors : sig
val different_literals_because_different_types : name -> literal -> literal -> unit -> error
val different_literals : name -> literal -> literal -> unit -> error
val error_uncomparable_literals : name -> literal -> literal -> unit -> error
end
val assert_literal_eq : ( literal * literal ) -> unit result
*)
val assert_value_eq : ( expression * expression ) -> unit result
val is_value_eq : ( expression * expression ) -> bool

View File

@ -463,11 +463,15 @@ type constant_tag =
| C_chain_id (* * *)
(* TODO: rename to type_expression or something similar (it includes variables, and unevaluated functions + applications *)
type type_value =
type type_value_ =
| P_forall of p_forall
| P_variable of type_variable
| P_constant of p_constant
| P_apply of p_apply
and type_value = {
tsrc : string;
t : type_value_ ;
}
and p_apply = {
tf : type_value ;
@ -556,6 +560,7 @@ and constraints = {
}
and type_variable_list = type_variable list
and c_constructor_simpl = {
reason_constr_simpl : string ;
tv : type_variable;
c_tag : constant_tag;
tv_list : type_variable_list;
@ -569,24 +574,23 @@ and c_equation_e = {
bex : type_expression ;
}
and c_typeclass_simpl = {
reason_typeclass_simpl : string ;
tc : typeclass ;
args : type_variable_list ;
}
and c_poly_simpl = {
reason_poly_simpl : string ;
tv : type_variable ;
forall : p_forall ;
}
and type_constraint_simpl = {
reason_simpl : string ;
c_simpl : type_constraint_simpl_ ;
}
and type_constraint_simpl_ =
and type_constraint_simpl =
| SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *)
| SC_Alias of c_alias (* α = β *)
| SC_Poly of c_poly_simpl (* α = forall β, δ where δ can be a more complex type *)
| SC_Typeclass of c_typeclass_simpl (* TC(α, …) *)
and c_alias = {
reason_alias_simpl : string ;
a : type_variable ;
b : type_variable ;
}

View File

@ -527,10 +527,19 @@ let equal_variables a b : bool =
| E_variable a, E_variable b -> Var.equal a b
| _, _ -> false
let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) =
P_constant {
let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) = {
tsrc = "misc.ml/p_constant" ;
t = P_constant {
p_ctor_tag : constant_tag ;
p_ctor_args : p_ctor_args ;
}
}
let c_equation aval bval reason = { c = C_equation { aval ; bval }; reason }
let reason_simpl : type_constraint_simpl -> string = function
| SC_Constructor { reason_constr_simpl=reason; _ }
| SC_Alias { reason_alias_simpl=reason; _ }
| SC_Poly { reason_poly_simpl=reason; _ }
| SC_Typeclass { reason_typeclass_simpl=reason; _ }
-> reason

View File

@ -73,3 +73,5 @@ val get_entry : program -> string -> expression result
val p_constant : constant_tag -> p_ctor_args -> type_value
val c_equation : type_value -> type_value -> string -> type_constraint
val reason_simpl : type_constraint_simpl -> string

View File

@ -29,7 +29,6 @@ module Substitution = struct
ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env
and s_type_environment : T.type_environment w = fun ~substs tenv ->
bind_map_list (fun T.{type_variable ; type_} ->
let%bind type_variable = s_type_variable ~substs type_variable in
let%bind type_ = s_type_expression ~substs type_ in
ok @@ T.{type_variable ; type_}) tenv
and s_environment : T.environment w = fun ~substs T.{expression_environment ; type_environment} ->
@ -45,14 +44,6 @@ module Substitution = struct
let () = ignore @@ substs in
ok var
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 : T.label w = fun ~substs l ->
let () = ignore @@ substs in
ok l
@ -71,7 +62,12 @@ module Substitution = struct
ok @@ type_name
and s_type_content : T.type_content w = fun ~substs -> function
| T.T_sum _ -> failwith "TODO: T_sum"
| T.T_sum s ->
let aux T.{ ctor_type; michelson_annotation ; ctor_decl_pos } =
let%bind ctor_type = s_type_expression ~substs ctor_type in
ok @@ T.{ ctor_type; michelson_annotation; ctor_decl_pos } in
let%bind s = Ast_typed.Helpers.bind_map_cmap aux s in
ok @@ T.T_sum s
| T.T_record _ -> failwith "TODO: T_record"
| T.T_constant type_name ->
let%bind type_name = s_type_name_constant ~substs type_name in
@ -223,24 +219,24 @@ module Substitution = struct
and type_value ~tv ~substs =
let self tv = type_value ~tv ~substs in
let (v, expr) = substs in
match (tv : type_value) with
match (tv : type_value).t with
| P_variable v' when Var.equal v' v -> expr
| P_variable _ -> tv
| P_constant {p_ctor_tag=x ; p_ctor_args=lst} -> (
let lst' = List.map self lst in
P_constant {p_ctor_tag=x ; p_ctor_args=lst'}
{ tsrc = "?TODO1?" ; t = P_constant {p_ctor_tag=x ; p_ctor_args=lst'} }
)
| P_apply { tf; targ } -> (
P_apply { tf = self tf ; targ = self targ }
{ tsrc = "?TODO2?" ; t = P_apply { tf = self tf ; targ = self targ } }
)
| P_forall p -> (
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 }
{ tsrc = "?TODO3?" ; t = P_forall { p with constraints } }
) else (
let body = self p.body in
P_forall { p with constraints ; body }
{ tsrc = "?TODO4?" ; t = P_forall { p with constraints ; body } }
)
)
@ -270,9 +266,10 @@ module Substitution = struct
(* Performs beta-reduction at the root of the type *)
let eval_beta_root ~(tv : type_value) =
match tv with
P_apply {tf = P_forall { binder; constraints; body }; targ} ->
match tv.t with
P_apply {tf = { tsrc = _ ; t = P_forall { binder; constraints; body } }; targ} ->
let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:targ)) constraints in
(* TODO: indicate in the result's tsrc that it was obtained via beta-reduction of the original type *)
(type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:targ) , constraints)
| _ -> (tv , [])
end

View File

@ -2,19 +2,24 @@ open Ast_typed.Types
open Core
open Ast_typed.Misc
let tc type_vars allowed_list : type_constraint =
{ c = C_typeclass {tc_args = type_vars ; typeclass = allowed_list} ; reason = "shorthands: typeclass" }
let tc description type_vars allowed_list : type_constraint = {
c = C_typeclass {tc_args = type_vars ;typeclass = allowed_list} ;
reason = "typeclass for operator: " ^ description
}
let forall binder f =
let () = ignore binder in
let freshvar = fresh_type_variable () in
P_forall { binder = freshvar ; constraints = [] ; body = f (P_variable freshvar) }
let body = f { tsrc = "shorthands.ml/forall" ; t = P_variable freshvar } in
{ tsrc = "shorthands.ml/forall" ;
t = P_forall { binder = freshvar ; constraints = [] ; body } }
let forall_tc binder f =
let () = ignore binder in
let freshvar = fresh_type_variable () in
let (tc, ty) = f (P_variable freshvar) in
P_forall { binder = freshvar ; constraints = tc ; body = ty }
let (tc, ty) = f { tsrc = "shorthands.ml/forall_tc" ; t = P_variable freshvar } in
{ tsrc = "shorthands.ml/forall_tc" ;
t = P_forall { binder = freshvar ; constraints = tc ; body = ty } }
(* chained forall *)
let forall2 a b f =
@ -55,7 +60,7 @@ let map k v = p_constant C_map [k; v]
let unit = p_constant C_unit []
let list t = p_constant C_list [t]
let set t = p_constant C_set [t]
let bool = P_variable Stage_common.Constant.t_bool
let bool = { tsrc = "built-in type" ; t = P_variable Stage_common.Constant.t_bool }
let string = p_constant C_string []
let nat = p_constant C_nat []
let mutez = p_constant C_mutez []

View File

@ -13,13 +13,13 @@ let get_program =
| Some s -> ok s
| None -> (
let%bind (program , state) = type_file "./contracts/coase.ligo" in
let () = Typer.Solver.discard_state state in
s := Some program ;
ok program
s := Some (program , state) ;
ok (program , state)
)
let compile_main () =
let%bind typed_prg = get_program () in
let%bind (typed_prg, state) = get_program () in
let () = Typer.Solver.discard_state state in
let%bind mini_c_prg = Ligo.Compile.Of_typed.compile typed_prg in
let%bind michelson_prg = Ligo.Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg "main" in
let%bind (_contract: Tezos_utils.Michelson.michelson) =

View File

@ -50,7 +50,7 @@ let empty_message = e_lambda (Var.of_name "arguments")
let commit () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
let%bind lock_time = mk_time "2000-01-02T00:10:11Z" in
let test_hash_raw = sha_256_hash (Bytes.of_string "hello world") in
@ -79,12 +79,12 @@ let commit () =
~sender:first_contract
()
in
expect_eq ~options program "commit"
expect_eq ~options (program, state) "commit"
(e_pair salted_hash init_storage) (e_pair empty_op_list post_storage)
(* Test that the contract fails if we haven't committed before revealing the answer *)
let reveal_no_commit () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
("message", empty_message)]
@ -95,13 +95,13 @@ let reveal_no_commit () =
("salted_hash", (t_bytes ()))])
in
let init_storage = storage test_hash true pre_commits in
expect_string_failwith program "reveal"
expect_string_failwith (program, state) "reveal"
(e_pair reveal init_storage)
"You have not made a commitment to hash against yet."
(* Test that the contract fails if our commit isn't 24 hours old yet *)
let reveal_young_commit () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
("message", empty_message)]
@ -128,13 +128,13 @@ let reveal_young_commit () =
~sender:first_contract
()
in
expect_string_failwith ~options program "reveal"
expect_string_failwith ~options (program, state) "reveal"
(e_pair reveal init_storage)
"It has not been 24 hours since your commit yet."
(* Test that the contract fails if our reveal doesn't meet our commitment *)
let reveal_breaks_commit () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
("message", empty_message)]
@ -160,13 +160,13 @@ let reveal_breaks_commit () =
~sender:first_contract
()
in
expect_string_failwith ~options program "reveal"
expect_string_failwith ~options (program, state) "reveal"
(e_pair reveal init_storage)
"This reveal does not match your commitment."
(* Test that the contract fails if we reveal the wrong bytes for the stored hash *)
let reveal_wrong_commit () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello");
("message", empty_message)]
@ -192,13 +192,13 @@ let reveal_wrong_commit () =
~sender:first_contract
()
in
expect_string_failwith ~options program "reveal"
expect_string_failwith ~options (program, state) "reveal"
(e_pair reveal init_storage)
"Your commitment did not match the storage hash."
(* Test that the contract fails if we try to reuse it after unused flag changed *)
let reveal_no_reuse () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello");
("message", empty_message)]
@ -224,13 +224,13 @@ let reveal_no_reuse () =
~sender:first_contract
()
in
expect_string_failwith ~options program "reveal"
expect_string_failwith ~options (program, state) "reveal"
(e_pair reveal init_storage)
"This contract has already been used."
(* Test that the contract executes successfully with valid commit-reveal *)
let reveal () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let empty_message = empty_message in
let reveal = e_record_ez [("hashable", e_bytes_string "hello world");
("message", empty_message)]
@ -257,7 +257,7 @@ let reveal () =
~sender:first_contract
()
in
expect_eq ~options program "reveal"
expect_eq ~options (program, state) "reveal"
(e_pair reveal init_storage) (e_pair empty_op_list post_storage)
let main = test_suite "Hashlock" [

View File

@ -33,7 +33,7 @@ let (first_owner , first_contract) =
Protocol.Alpha_context.Contract.to_b58check kt , kt
let buy_id () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -60,13 +60,13 @@ let buy_id () =
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let%bind () = expect_eq ~options program "buy"
let%bind () = expect_eq ~options (program, state) "buy"
(e_pair param storage)
(e_pair (e_list []) new_storage)
in ok ()
let buy_id_sender_addr () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -93,14 +93,14 @@ let buy_id_sender_addr () =
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let%bind () = expect_eq ~options program "buy"
let%bind () = expect_eq ~options (program, state) "buy"
(e_pair param storage)
(e_pair (e_list []) new_storage)
in ok ()
(* Test that contract fails if we attempt to buy an ID for the wrong amount *)
let buy_id_wrong_amount () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -117,13 +117,13 @@ let buy_id_wrong_amount () =
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
in
let param = e_pair owner_website (e_some (e_address new_addr)) in
let%bind () = expect_string_failwith ~options program "buy"
let%bind () = expect_string_failwith ~options (program, state) "buy"
(e_pair param storage)
"Incorrect amount paid."
in ok ()
let update_details_owner () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -158,13 +158,13 @@ let update_details_owner () =
let param = e_tuple [e_int 1 ;
e_some details ;
e_some (e_address new_addr)] in
let%bind () = expect_eq ~options program "update_details"
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) new_storage)
in ok ()
let update_details_controller () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -199,14 +199,14 @@ let update_details_controller () =
let param = e_tuple [e_int 1 ;
e_some details ;
e_some (e_address owner_addr)] in
let%bind () = expect_eq ~options program "update_details"
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) new_storage)
in ok ()
(* Test that contract fails when we attempt to update details of nonexistent ID *)
let update_details_nonexistent () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -233,14 +233,14 @@ let update_details_nonexistent () =
let param = e_tuple [e_int 2 ;
e_some details ;
e_some (e_address owner_addr)] in
let%bind () = expect_string_failwith ~options program "update_details"
let%bind () = expect_string_failwith ~options (program, state) "update_details"
(e_pair param storage)
"This ID does not exist."
in ok ()
(* Test that contract fails when we attempt to update details from wrong addr *)
let update_details_wrong_addr () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -266,14 +266,14 @@ let update_details_wrong_addr () =
let param = e_tuple [e_int 0 ;
e_some details ;
e_some (e_address owner_addr)] in
let%bind () = expect_string_failwith ~options program "update_details"
let%bind () = expect_string_failwith ~options (program, state) "update_details"
(e_pair param storage)
"You are not the owner or controller of this ID."
in ok ()
(* Test that giving none on both profile and controller address is a no-op *)
let update_details_unchanged () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -299,13 +299,13 @@ let update_details_unchanged () =
let param = e_tuple [e_int 1 ;
e_typed_none (t_bytes ()) ;
e_typed_none (t_address ())] in
let%bind () = expect_eq ~options program "update_details"
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) storage)
in ok ()
let update_owner () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -337,14 +337,14 @@ let update_owner () =
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let param = e_pair (e_int 1) (e_address owner_addr) in
let%bind () = expect_eq ~options program "update_owner"
let%bind () = expect_eq ~options (program, state) "update_owner"
(e_pair param storage)
(e_pair (e_list []) new_storage)
in ok ()
(* Test that contract fails when we attempt to update owner of nonexistent ID *)
let update_owner_nonexistent () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -368,14 +368,14 @@ let update_owner_nonexistent () =
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let param = e_pair (e_int 2) (e_address new_addr) in
let%bind () = expect_string_failwith ~options program "update_owner"
let%bind () = expect_string_failwith ~options (program, state) "update_owner"
(e_pair param storage)
"This ID does not exist."
in ok ()
(* Test that contract fails when we attempt to update owner from non-owner addr *)
let update_owner_wrong_addr () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -399,13 +399,13 @@ let update_owner_wrong_addr () =
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let param = e_pair (e_int 0) (e_address new_addr) in
let%bind () = expect_string_failwith ~options program "update_owner"
let%bind () = expect_string_failwith ~options (program, state) "update_owner"
(e_pair param storage)
"You are not the owner of this ID."
in ok ()
let skip () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -432,14 +432,14 @@ let skip () =
e_int 3;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let%bind () = expect_eq ~options program "skip"
let%bind () = expect_eq ~options (program, state) "skip"
(e_pair (e_unit ()) storage)
(e_pair (e_list []) new_storage)
in ok ()
(* Test that contract fails if we try to skip without paying the right amount *)
let skip_wrong_amount () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let owner_addr = addr 5 in
let owner_website = e_bytes_string "ligolang.org" in
let id_details_1 = e_record_ez [("owner", e_address owner_addr) ;
@ -461,7 +461,7 @@ let skip_wrong_amount () =
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
in
let%bind () = expect_string_failwith ~options program "skip"
let%bind () = expect_string_failwith ~options (program, state) "skip"
(e_pair (e_unit ()) storage)
"Incorrect amount paid."
in ok ()

View File

@ -4,17 +4,11 @@ open Test_helpers
open Ast_imperative.Combinators
let retype_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "reasonligo" Env in
let () = Typer.Solver.discard_state state in
ok typed
Ligo.Compile.Utils.type_file f "reasonligo" Env
let mtype_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "cameligo" Env in
let () = Typer.Solver.discard_state state in
ok typed
Ligo.Compile.Utils.type_file f "cameligo" Env
let type_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "pascaligo" Env in
let () = Typer.Solver.discard_state state in
ok typed
Ligo.Compile.Utils.type_file f "pascaligo" Env
let type_alias () : unit result =
let%bind program = type_file "./contracts/type-alias.ligo" in

View File

@ -76,39 +76,39 @@ let params counter msg keys is_validl f s =
(* Provide one valid signature when the threshold is two of two keys *)
let not_enough_1_of_2 f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let exp_failwith = "Not enough signatures passed the check" in
let keys = gen_keys () in
let%bind test_params = params 0 empty_message [keys] [true] f s in
let%bind () = expect_string_failwith
program "main" (e_pair test_params (init_storage 2 0 [keys;gen_keys()])) exp_failwith in
(program, state) "main" (e_pair test_params (init_storage 2 0 [keys;gen_keys()])) exp_failwith in
ok ()
let unmatching_counter f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let exp_failwith = "Counters does not match" in
let keys = gen_keys () in
let%bind test_params = params 1 empty_message [keys] [true] f s in
let%bind () = expect_string_failwith
program "main" (e_pair test_params (init_storage 1 0 [keys])) exp_failwith in
(program, state) "main" (e_pair test_params (init_storage 1 0 [keys])) exp_failwith in
ok ()
(* Provide one invalid signature (correct key but incorrect signature)
when the threshold is one of one key *)
let invalid_1_of_1 f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let exp_failwith = "Invalid signature" in
let keys = [gen_keys ()] in
let%bind test_params = params 0 empty_message keys [false] f s in
let%bind () = expect_string_failwith
program "main" (e_pair test_params (init_storage 1 0 keys)) exp_failwith in
(program, state) "main" (e_pair test_params (init_storage 1 0 keys)) exp_failwith in
ok ()
(* Provide one valid signature when the threshold is one of one key *)
let valid_1_of_1 f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let keys = gen_keys () in
let%bind () = expect_eq_n_trace_aux [0;1;2] program "main"
let%bind () = expect_eq_n_trace_aux [0;1;2] (program, state) "main"
(fun n ->
let%bind params = params n empty_message [keys] [true] f s in
ok @@ e_pair params (init_storage 1 n [keys])
@ -120,10 +120,10 @@ let valid_1_of_1 f s () =
(* Provive two valid signatures when the threshold is two of three keys *)
let valid_2_of_3 f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let param_keys = [gen_keys (); gen_keys ()] in
let st_keys = param_keys @ [gen_keys ()] in
let%bind () = expect_eq_n_trace_aux [0;1;2] program "main"
let%bind () = expect_eq_n_trace_aux [0;1;2] (program, state) "main"
(fun n ->
let%bind params = params n empty_message param_keys [true;true] f s in
ok @@ e_pair params (init_storage 2 n st_keys)
@ -135,7 +135,7 @@ let valid_2_of_3 f s () =
(* Provide one invalid signature and two valid signatures when the threshold is two of three keys *)
let invalid_3_of_3 f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let valid_keys = [gen_keys() ; gen_keys()] in
let invalid_key = gen_keys () in
let param_keys = valid_keys @ [invalid_key] in
@ -143,18 +143,18 @@ let invalid_3_of_3 f s () =
let%bind test_params = params 0 empty_message param_keys [false;true;true] f s in
let exp_failwith = "Invalid signature" in
let%bind () = expect_string_failwith
program "main" (e_pair test_params (init_storage 2 0 st_keys)) exp_failwith in
(program, state) "main" (e_pair test_params (init_storage 2 0 st_keys)) exp_failwith in
ok ()
(* Provide two valid signatures when the threshold is three of three keys *)
let not_enough_2_of_3 f s () =
let%bind program,_ = get_program f s() in
let%bind (program , state) = get_program f s() in
let valid_keys = [gen_keys() ; gen_keys()] in
let st_keys = gen_keys () :: valid_keys in
let%bind test_params = params 0 empty_message (valid_keys) [true;true] f s in
let exp_failwith = "Not enough signatures passed the check" in
let%bind () = expect_string_failwith
program "main" (e_pair test_params (init_storage 3 0 st_keys)) exp_failwith in
(program, state) "main" (e_pair test_params (init_storage 3 0 st_keys)) exp_failwith in
ok ()
let main = test_suite "Multisig" [

View File

@ -65,7 +65,7 @@ let storage {state_hash ; threshold ; max_proposal ; max_msg_size ; id_counter_l
(* sender not stored in the authorized set *)
let wrong_addr () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage {
threshold = 1 ; max_proposal = 1 ; max_msg_size = 1 ; state_hash = Bytes.empty ;
id_counter_list = [1,0 ; 2,0] ;
@ -75,13 +75,13 @@ let wrong_addr () =
let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let%bind () =
let exp_failwith = "Unauthorized address" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair (send_param empty_message) init_storage) exp_failwith in
ok ()
(* send a message which exceed the size limit *)
let message_size_exceeded () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage {
threshold = 1 ; max_proposal = 1 ; max_msg_size = 1 ; state_hash = Bytes.empty ;
id_counter_list = [1,0] ;
@ -91,13 +91,13 @@ let message_size_exceeded () =
let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let%bind () =
let exp_failwith = "Message size exceed maximum limit" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair (send_param empty_message) init_storage) exp_failwith in
ok ()
(* sender has already has reached maximum number of proposal *)
let maximum_number_of_proposal () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload1 = pack_payload program (send_param empty_message) in
let bytes1 = e_bytes_raw packed_payload1 in
let init_storage = storage {
@ -109,13 +109,13 @@ let maximum_number_of_proposal () =
let options = Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let%bind () =
let exp_failwith = "Maximum number of proposal reached" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair (send_param empty_message2) init_storage) exp_failwith in
ok ()
(* sender message is already stored in the message store *)
let send_already_accounted () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let init_storage = storage {
@ -126,12 +126,12 @@ let send_already_accounted () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair (send_param empty_message) init_storage) (e_pair empty_op_list init_storage)
(* sender message isn't stored in the message store *)
let send_never_accounted () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let init_storage' = {
@ -147,12 +147,12 @@ let send_never_accounted () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair (send_param empty_message) init_storage) (e_pair empty_op_list final_storage)
(* sender withdraw message is already binded to one address in the message store *)
let withdraw_already_accounted_one () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let param = withdraw_param in
@ -168,12 +168,12 @@ let withdraw_already_accounted_one () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list final_storage)
(* sender withdraw message is already binded to two addresses in the message store *)
let withdraw_already_accounted_two () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let param = withdraw_param in
@ -189,12 +189,12 @@ let withdraw_already_accounted_two () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list final_storage)
(* triggers the threshold and check that all the participants get their counters decremented *)
let counters_reset () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let param = send_param empty_message in
@ -212,12 +212,12 @@ let counters_reset () =
let options =
let sender = contract 3 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list final_storage)
(* sender withdraw message was never accounted *)
let withdraw_never_accounted () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let param = withdraw_param in
let init_storage = storage {
threshold = 2 ; max_proposal = 1 ; max_msg_size = 1 ; state_hash = Bytes.empty ;
@ -227,12 +227,12 @@ let withdraw_never_accounted () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list init_storage)
(* successful storing in the message store *)
let succeeded_storing () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind packed_payload = pack_payload program empty_message in
let bytes = e_bytes_raw packed_payload in
let init_storage th = {
@ -243,7 +243,7 @@ let succeeded_storing () =
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let%bind () = expect_eq_n_trace_aux ~options [1;2] program "main"
let%bind () = expect_eq_n_trace_aux ~options [1;2] (program, state) "main"
(fun th ->
let init_storage = storage (init_storage th) in
ok @@ e_pair (send_param empty_message) init_storage

View File

@ -45,36 +45,36 @@ let empty_message = e_lambda (Var.of_name "arguments")
let pledge () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let storage = e_address oracle_addr in
let parameter = e_unit () in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:oracle_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
expect_eq ~options program "donate"
expect_eq ~options (program, state) "donate"
(e_pair parameter storage)
(e_pair (e_list []) storage)
let distribute () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let storage = e_address oracle_addr in
let parameter = empty_message in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:oracle_contract ()
in
expect_eq ~options program "distribute"
expect_eq ~options (program, state) "distribute"
(e_pair parameter storage)
(e_pair (e_list []) storage)
let distribute_unauthorized () =
let%bind program, _ = get_program () in
let%bind (program , state) = get_program () in
let storage = e_address oracle_addr in
let parameter = empty_message in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:stranger_contract ()
in
expect_string_failwith ~options program "distribute"
expect_string_failwith ~options (program, state) "distribute"
(e_pair parameter storage)
"You're not the oracle for this distribution."

View File

@ -39,45 +39,45 @@ let entry_pass_message = e_constructor "Pass_message"
@@ empty_message
let change_addr_success () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage 1 in
let param = entry_change_addr 2 in
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list (storage 2))
let change_addr_fail () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage 1 in
let param = entry_change_addr 2 in
let options =
let sender = contract 3 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let exp_failwith = "Unauthorized sender" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair param init_storage) exp_failwith
let pass_message_success () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage 1 in
let param = entry_pass_message in
let options =
let sender = contract 1 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair param init_storage) (e_pair empty_op_list init_storage)
let pass_message_fail () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let init_storage = storage 1 in
let param = entry_pass_message in
let options =
let sender = contract 2 in
Proto_alpha_utils.Memory_proto_alpha.make_options ~sender () in
let exp_failwith = "Unauthorized sender" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair param init_storage) exp_failwith
let main = test_suite "Replaceable ID" [

View File

@ -86,11 +86,10 @@ let sha_256_hash pl =
open Ast_imperative.Combinators
let typed_program_with_imperative_input_to_michelson
(program: Ast_typed.program) (entry_point: string)
((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string)
(input: Ast_imperative.expression) : Compiler.compiled_expression result =
Printexc.record_backtrace true;
let env = Ast_typed.program_environment Environment.default program in
let state = Typer.Solver.initial_state in
let%bind sugar = Compile.Of_imperative.compile_expression input in
let%bind core = Compile.Of_sugar.compile_expression sugar in
let%bind app = Compile.Of_core.apply entry_point core in
@ -100,9 +99,9 @@ let typed_program_with_imperative_input_to_michelson
Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied
let run_typed_program_with_imperative_input ?options
(program: Ast_typed.program) (entry_point: string)
((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string)
(input: Ast_imperative.expression) : Ast_core.expression result =
let%bind michelson_program = typed_program_with_imperative_input_to_michelson program entry_point input in
let%bind michelson_program = typed_program_with_imperative_input_to_michelson (program , state) entry_point input in
let%bind michelson_output = Ligo.Run.Of_michelson.run_no_failwith ?options michelson_program.expr michelson_program.expr_ty in
Uncompile.uncompile_typed_program_entry_function_result program entry_point michelson_output
@ -160,7 +159,7 @@ let expect_eq_core ?options program entry_point input expected =
Ast_core.Misc.assert_value_eq (expected,result) in
expect ?options program entry_point input expecter
let expect_evaluate program entry_point expecter =
let expect_evaluate (program, _state) entry_point expecter =
let error =
let title () = "expect evaluate" in
let content () = Format.asprintf "Entry_point: %s" entry_point in
@ -173,11 +172,11 @@ let expect_evaluate program entry_point expecter =
let%bind res_simpl = Uncompile.uncompile_typed_program_entry_expression_result program entry_point res_michelson in
expecter res_simpl
let expect_eq_evaluate program entry_point expected =
let expect_eq_evaluate ((program , state) : Ast_typed.program * Ast_typed.typer_state) entry_point expected =
let%bind expected = expression_to_core expected in
let expecter = fun result ->
Ast_core.Misc.assert_value_eq (expected , result) in
expect_evaluate program entry_point expecter
expect_evaluate (program, state) entry_point expecter
let expect_n_aux ?options lst program entry_point make_input make_expecter =
let aux n =

View File

@ -43,21 +43,21 @@ let storage st interval execute =
("execute", execute)]
let early_call () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
let%bind lock_time = mk_time "2000-01-01T10:10:10Z" in
let init_storage = storage lock_time 86400 empty_message in
let options =
Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
let exp_failwith = "You have to wait before you can execute this contract again." in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair (e_unit ()) init_storage) exp_failwith
let fake_uncompiled_empty_message = e_string "[lambda of type: (lambda unit (list operation)) ]"
(* Test that when we use the contract the next use time advances by correct interval *)
let interval_advance () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind predecessor_timestamp = mk_time "2000-01-01T10:10:10Z" in
let%bind lock_time = mk_time "2000-01-01T00:10:10Z" in
let init_storage = storage lock_time 86400 empty_message in
@ -66,7 +66,7 @@ let interval_advance () =
let new_storage_fake = storage new_timestamp 86400 fake_uncompiled_empty_message in
let options =
Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair (e_unit ()) init_storage) (e_pair empty_op_list new_storage_fake)
let main = test_suite "Time Lock Repeating" [

View File

@ -41,24 +41,24 @@ let to_sec t = Tezos_utils.Time.Protocol.to_seconds t
let storage st = e_timestamp (Int64.to_int @@ to_sec st)
let early_call () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind predecessor_timestamp = mk_time "2000-01-01T00:10:10Z" in
let%bind lock_time = mk_time "2000-01-01T10:10:10Z" in
let init_storage = storage lock_time in
let options =
Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
let exp_failwith = "Contract is still time locked" in
expect_string_failwith ~options program "main"
expect_string_failwith ~options (program, state) "main"
(e_pair (call empty_message) init_storage) exp_failwith
let call_on_time () =
let%bind program,_ = get_program () in
let%bind (program , state) = get_program () in
let%bind predecessor_timestamp = mk_time "2000-01-01T10:10:10Z" in
let%bind lock_time = mk_time "2000-01-01T00:10:10Z" in
let init_storage = storage lock_time in
let options =
Proto_alpha_utils.Memory_proto_alpha.make_options ~predecessor_timestamp () in
expect_eq ~options program "main"
expect_eq ~options (program, state) "main"
(e_pair (call empty_message) init_storage) (e_pair empty_op_list init_storage)
let main = test_suite "Time lock" [

View File

@ -49,7 +49,7 @@ let sender = e_address @@ sender
let external_contract = e_annotation (e_constant C_IMPLICIT_ACCOUNT [e_key_hash external_contract]) (t_contract (t_nat ()))
let transfer f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair sender from_, e_nat 100)]);
@ -64,10 +64,10 @@ let transfer f s () =
let input = e_pair parameter storage in
let expected = e_pair (e_typed_list [] (t_operation ())) new_storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_eq program ~options "transfer" input expected
expect_eq (program, state) ~options "transfer" input expected
let transfer_not_e_allowance f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair sender from_, e_nat 0)]);
@ -76,11 +76,11 @@ let transfer_not_e_allowance f s () =
let parameter = e_record_ez [("address_from", from_);("address_to",to_); ("value",e_nat 10)] in
let input = e_pair parameter storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_string_failwith ~options program "transfer" input
expect_string_failwith ~options (program, state) "transfer" input
"Not Enough Allowance"
let transfer_not_e_balance f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 0); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair sender from_, e_nat 100)]);
@ -89,11 +89,11 @@ let transfer_not_e_balance f s () =
let parameter = e_record_ez [("address_from", from_);("address_to",to_); ("value",e_nat 10)] in
let input = e_pair parameter storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_string_failwith ~options program "transfer" input
expect_string_failwith ~options (program, state) "transfer" input
"Not Enough Balance"
let approve f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair from_ sender, e_nat 0)]);
@ -108,10 +108,10 @@ let approve f s () =
let input = e_pair parameter storage in
let expected = e_pair (e_typed_list [] (t_operation ())) new_storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_eq program ~options "approve" input expected
expect_eq (program, state) ~options "approve" input expected
let approve_unsafe f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@ -120,11 +120,11 @@ let approve_unsafe f s () =
let parameter = e_record_ez [("spender", from_);("value",e_nat 100)] in
let input = e_pair parameter storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_string_failwith ~options program "approve" input
expect_string_failwith ~options (program, state) "approve" input
"Unsafe Allowance Change"
let get_allowance f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@ -134,10 +134,10 @@ let get_allowance f s () =
let input = e_pair parameter storage in
let expected = e_pair (e_typed_list [] (t_operation ())) storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_eq program ~options "getAllowance" input expected
expect_eq (program, state) ~options "getAllowance" input expected
let get_balance f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@ -147,10 +147,10 @@ let get_balance f s () =
let input = e_pair parameter storage in
let expected = e_pair (e_typed_list [] (t_operation ())) storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_eq program ~options "getBalance" input expected
expect_eq (program, state) ~options "getBalance" input expected
let get_total_supply f s () =
let%bind program,_ = get_program f s () in
let%bind (program , state) = get_program f s () in
let storage = e_record_ez [
("tokens", e_big_map [(sender, e_nat 100); (from_, e_nat 100); (to_, e_nat 100)]);
("allowances", e_big_map [(e_pair from_ sender, e_nat 100)]);
@ -160,7 +160,7 @@ let get_total_supply f s () =
let input = e_pair parameter storage in
let expected = e_pair (e_typed_list [] (t_operation ())) storage in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options () in
expect_eq program ~options "getTotalSupply" input expected
expect_eq (program, state) ~options "getTotalSupply" input expected
let main = test_suite "tzip-12" [
test "transfer" (transfer file_FA12 "pascaligo");

View File

@ -2,8 +2,7 @@ open Trace
open Test_helpers
let type_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "cameligo" (Contract "main") in
ok @@ (typed,state)
Ligo.Compile.Utils.type_file f "cameligo" (Contract "main")
let get_program =
let s = ref None in
@ -36,10 +35,10 @@ let reset title start_time finish_time =
let yea = e_constructor "Vote" (e_constructor "Yea" (e_unit ()))
let init_vote () =
let%bind (program , _) = get_program () in
let%bind (program , state) = get_program () in
let%bind result =
Test_helpers.run_typed_program_with_imperative_input
program "main" (e_pair yea (init_storage "basic")) in
(program, state) "main" (e_pair yea (init_storage "basic")) in
let%bind (_, storage) = Ast_core.extract_pair result in
let%bind storage' = Ast_core.extract_record storage in
(* let votes = List.assoc (Label "voters") storage' in

View File

@ -23,6 +23,17 @@ let find elt set =
let find_opt elt set = RB.find_opt ~cmp:set.cmp elt set.tree
let mem elt set = match RB.find_opt ~cmp:set.cmp elt set.tree with None -> false | Some _ -> true
type 'a added = {set : 'a set; duplicates : 'a list; added : 'a list}
let add_list elts set =
let aux = fun {set ; duplicates ; added} elt ->
if mem elt set
then {set; duplicates = elt :: duplicates ; added}
else {set = add elt set; duplicates; added = elt :: added} in
List.fold_left aux {set; duplicates=[]; added = []} elts
let elements set = RB.elements set.tree
let iter f set = RB.iter f set.tree

View File

@ -46,10 +46,28 @@ val find : 'elt -> 'elt t -> 'elt
val find_opt : 'elt -> 'elt t -> 'elt option
(* The value of the call [mem elt set] is [true] if there exists an
element [y] of set [set] such that [cmp y elt = true], where [cmp]
is the comparison function of [set] (see [create]). If [elt] is not
in [set], then [false] is returned instead. *)
val mem : 'elt -> 'elt t -> bool
(* The value of the call [element set] is the list of elements of the
set [set] in increasing order (with respect to the total comparison
function used to create the set). *)
(* The value of the call [add_list element_list set] is a record of
type ['a added]. The elements from the [element_list] are added to
the [set] starting from the head of the list. The elements which
are already part of the [set] at the point at which they are added
are gathered in the [duplicates] list (and the [set] is not updated
for these elements, i.e. it keeps the pre-existing version of the
element). The elements which are not already members of the set are
added to the [set], and gathered in the [added] list. *)
type 'a added = {set : 'a set; duplicates : 'a list; added : 'a list}
val add_list : 'a list -> 'a set -> 'a added
val elements : 'elt t -> 'elt list
(* The side-effect of evaluating the call [iter f set] is the