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

Merge branch 'bugfix-typer-11' into 'dev'

Browse Source 
Bugfixes for new typer, volume 11

See merge request ligolang/ligo!640
This commit is contained in:
Suzanne Dupéron 2020-05-29 19:37:50 +00:00
commit 6cab827f17
25 changed files with 327 additions and 277 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/passes/8-typer-new/PP.ml
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

117
src/passes/8-typer-new/solver.ml
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,37 +605,37 @@ 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
(* 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
(* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
(already_selected , List.flatten new_constraints , List.flatten new_assignments)
| WasNotSelected ->
(already_selected, [] , [])
let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
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 ->
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
(* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
(already_selected , List.flatten new_constraints , List.flatten new_assignments)
| WasNotSelected ->
(already_selected, [] , [])
let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1

3
src/passes/8-typer-new/typer.ml
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 =

80
src/passes/8-typer-new/wrap.ml
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

22
src/passes/operators/operators.ml
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

16
src/stages/4-ast_typed/ast.ml
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 ;
}

13
src/stages/4-ast_typed/misc.ml
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

2
src/stages/4-ast_typed/misc.mli
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

31
src/stages/typesystem/misc.ml
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

17
src/stages/typesystem/shorthands.ml
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 []

12
src/test/coase_tests.ml
View File

@ -13,15 +13,15 @@ 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 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 (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) =
(* fails if the given entry point is not a valid contract *)
Ligo.Compile.Of_michelson.build_contract michelson_prg in

28
src/test/hash_lock_tests.ml
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" [

52
src/test/id_tests.ml
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 ()

12
src/test/integration_tests.ml
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

28
src/test/multisig_tests.ml
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" [

40
src/test/multisig_v2_tests.ml
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

12
src/test/pledge_tests.ml
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."

16
src/test/replaceable_id_tests.ml
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" [

13
src/test/test_helpers.ml
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 =

8
src/test/time_lock_repeat_tests.ml
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" [

8
src/test/time_lock_tests.ml
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" [

32
src/test/tzip12_tests.ml
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");

7
src/test/vote_tests.ml
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

11
vendors/Red-Black_Trees/PolySet.ml vendored
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

18
vendors/Red-Black_Trees/PolySet.mli vendored
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