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

This commit is contained in:
Christian Rinderknecht 2020-06-02 22:14:14 +02:00
commit 562f08dabc
25 changed files with 2971 additions and 853 deletions

View File

@ -0,0 +1,31 @@
Components:
* assignments (passive data structure).
Now: just a map from unification vars to types (pb: what about partial types?)
maybe just local assignments (allow only vars as children of pair(α,β))
* constraint propagation: (buch of constraints) → (new constraints * assignments)
* sub-component: constraint selector (worklist / dynamic queries)
* sub-sub component: constraint normalizer: remove dupes and give structure
right now: union-find of unification vars
later: better database-like organisation of knowledge
* sub-sub component: lazy selector (don't re-try all selectors every time)
For now: just re-try everytime
* sub-component: propagation rule
For now: break pair(a, b) = pair(c, d) into a = c, b = d
* generalizer
For now: ?
Workflow:
Start with empty assignments and structured database
Receive a new constraint
For each normalizer:
Use the pre-selector to see if it can be applied
Apply the normalizer, get some new items to insert in the structured database
For each propagator:
Use the selector to query the structured database and see if it can be applied
Apply the propagator, get some new constraints and assignments
Add the new assignments to the data structure.
At some point (when?)
For each generalizer:
Use the generalizer's selector to see if it can be applied
Apply the generalizer to produce a new type, possibly with some ∀s injected

View File

@ -0,0 +1,69 @@
module Map = RedBlackTrees.PolyMap
module UF = UnionFind.Poly2
open Ast_typed.Types
(* Light wrapper for API for grouped_by_variable in the structured
db, to access it modulo unification variable aliases. *)
let get_constraints_related_to : type_variable -> structured_dbs -> constraints =
fun variable dbs ->
let variable , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in
match Map.find_opt variable dbs.grouped_by_variable with
Some l -> l
| None -> {
constructor = [] ;
poly = [] ;
tc = [] ;
}
let add_constraints_related_to : type_variable -> constraints -> structured_dbs -> structured_dbs =
fun variable c dbs ->
(* let (variable_repr , _height) , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in *)
let variable_repr , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in
let grouped_by_variable = Map.update variable_repr (function
None -> Some c
| Some (x : constraints) -> Some {
constructor = c.constructor @ x.constructor ;
poly = c.poly @ x.poly ;
tc = c.tc @ x.tc ;
})
dbs.grouped_by_variable
in
let dbs = { dbs with grouped_by_variable } in
dbs
let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs =
fun variable_a variable_b dbs ->
(* get old representant for variable_a *)
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
let dbs = { dbs with aliases } in
(* get old representant for variable_b *)
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
let dbs = { dbs with aliases } in
(* alias variable_a and variable_b together *)
let aliases = UF.alias variable_a variable_b dbs.aliases in
let dbs = { dbs with aliases } in
(* Replace the two entries in grouped_by_variable by a single one *)
(
let get_constraints ab =
match Map.find_opt ab dbs.grouped_by_variable with
| Some x -> x
| None -> { constructor = [] ; poly = [] ; tc = [] } in
let constraints_a = get_constraints variable_repr_a in
let constraints_b = get_constraints variable_repr_b in
let all_constraints = {
constructor = constraints_a.constructor @ constraints_b.constructor ;
poly = constraints_a.poly @ constraints_b.poly ;
tc = constraints_a.tc @ constraints_b.tc ;
} in
let grouped_by_variable =
Map.add variable_repr_a all_constraints dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
let grouped_by_variable =
Map.remove variable_repr_b dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
dbs
)

View File

@ -0,0 +1,52 @@
(* selector / propagation rule for breaking down composite types
* For now: break pair(a, b) = pair(c, d) into a = c, b = d *)
open Ast_typed.Misc
open Ast_typed.Types
open Solver_types
let selector : (type_constraint_simpl, output_break_ctor) selector =
(* find two rules with the shape x = k(var …) and x = k'(var' …) *)
fun type_constraint_simpl dbs ->
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)
is symmetric *)
let other_cs = (Constraint_databases.get_constraints_related_to c.tv dbs).constructor in
let other_cs = List.filter (fun (o : c_constructor_simpl) -> Var.equal c.tv o.tv) other_cs in
(* TODO double-check the conditions in the propagator, we had a
bug here because the selector was too permissive. *)
let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in
WasSelected cs_pairs
| SC_Alias _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
| SC_Poly _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
| SC_Typeclass _ -> WasNotSelected
let propagator : output_break_ctor propagator =
fun selected dbs ->
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 { 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 (Solver_should_be_generated.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)"
Solver_should_be_generated.debug_pp_c_constructor_simpl a
Solver_should_be_generated.debug_pp_c_constructor_simpl b
(Solver_should_be_generated.compare_simple_c_constant a.c_tag b.c_tag))
else
(* a.tv_list = b.tv_list *)
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 { 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 *)

View File

@ -0,0 +1,53 @@
(* selector / propagation rule for specializing polymorphic types
* For now: (x = forall y, z) and (x = k'(var' ))
* produces the new constraint (z[x |-> k'(var' )])
* where [from |-> to] denotes substitution. *)
module Core = Typesystem.Core
open Ast_typed.Misc
open Ast_typed.Types
open Solver_types
let selector : (type_constraint_simpl, output_specialize1) selector =
(* 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 with
SC_Constructor c ->
(* vice versa *)
let other_cs = (Constraint_databases.get_constraints_related_to c.tv dbs).poly in
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 = (Constraint_databases.get_constraints_related_to p.tv dbs).constructor in
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
let propagator : output_specialize1 propagator =
fun selected dbs ->
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
(* The selector is expected to provide 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 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 = {
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) = Typelang.check_applied @@ Typelang.type_level_eval apply 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 *)

View File

@ -0,0 +1,126 @@
module Core = Typesystem.Core
module Map = RedBlackTrees.PolyMap
open Ast_typed.Misc
open Ast_typed.Types
open Solver_types
(* sub-sub component: constraint normalizer: remove dupes and give structure
* right now: union-find of unification vars
* later: better database-like organisation of knowledge *)
(* Each normalizer returns an updated database (after storing the
incoming constraint) and a list of constraints, used when the
normalizer rewrites the constraints e.g. into simpler ones. *)
(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *)
type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
(** Updates the dbs.all_constraints field when new constraints are
discovered.
This field contains a list of all the constraints, without any form of
grouping or sorting. *)
let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
(** Updates the dbs.grouped_by_variable field when new constraints are
discovered.
This field contains a map from type variables to lists of
constraints that are related to that variable (in other words, the
key appears in the equation).
*)
let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let store_constraint tvars constraints =
let aux dbs (tvar : type_variable) =
Constraint_databases.add_constraints_related_to tvar constraints dbs
in List.fold_left aux dbs tvars
in
let dbs = match new_constraint with
SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []}
| SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]}
| SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []}
| SC_Alias { a; b } -> Constraint_databases.merge_constraints a b dbs
in (dbs , [new_constraint])
(** Stores the first assinment ('a = ctor('b, …)) that is encountered.
Subsequent ('a = ctor('b2, )) with the same 'a are ignored.
TOOD: are we checking somewhere that 'b = 'b2 ? *)
let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
match new_constraint with
| 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
(dbs , [new_constraint])
| _ ->
(dbs , [new_constraint])
(* TODO: at some point there may be uses of named type aliases (type
foo = int; let x : foo = 42). These should be inlined. *)
(** This function converts constraints from type_constraint to
type_constraint_simpl. The former has more possible cases, and the
latter uses a more minimalistic constraint language.
It does not modify the dbs, and only rewrites the constraint
TODO: update the code to show that the dbs are always copied as-is
*)
let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let insert_fresh a b =
let fresh = Core.fresh_type_variable () 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 { 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 , [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) = Typelang.check_applied @@ Typelang.type_level_eval b in
let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in
let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced "normalizer: reduce_type_app") in (* Note: this calls recursively but cant't fall in the same case. *)
(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 { 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, [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=({ 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=({ 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=({ 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=({ 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=({ 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 *)
let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad =
fun new_constraint dbs ->
(fun x -> x)
@@ lift normalizer_grouped_by_variable
@@ lift normalizer_assignments
@@ lift normalizer_all_constraints
@@ lift normalizer_simpl
@@ lift_state_list_monad ~state:dbs ~list:[new_constraint]

View File

@ -1,634 +1,24 @@
open Trace
module Core = Typesystem.Core
module Map = RedBlackTrees.PolyMap
module Set = RedBlackTrees.PolySet
module UF = UnionFind.Poly2
module Wrap = Wrap
open Wrap
open Ast_typed.Misc
(* TODO: remove this, it's not used anymore *)
module TypeVariable =
struct
type t = Core.type_variable
let compare a b = Var.compare a b
let to_string = (fun s -> Format.asprintf "%a" Var.pp s)
end
(*
Components:
* assignments (passive data structure).
Now: just a map from unification vars to types (pb: what about partial types?)
maybe just local assignments (allow only vars as children of pair(α,β))
* constraint propagation: (buch of constraints) (new constraints * assignments)
* sub-component: constraint selector (worklist / dynamic queries)
* sub-sub component: constraint normalizer: remove dupes and give structure
right now: union-find of unification vars
later: better database-like organisation of knowledge
* sub-sub component: lazy selector (don't re-try all selectors every time)
For now: just re-try everytime
* sub-component: propagation rule
For now: break pair(a, b) = pair(c, d) into a = c, b = d
* generalizer
For now: ?
Workflow:
Start with empty assignments and structured database
Receive a new constraint
For each normalizer:
Use the pre-selector to see if it can be applied
Apply the normalizer, get some new items to insert in the structured database
For each propagator:
Use the selector to query the structured database and see if it can be applied
Apply the propagator, get some new constraints and assignments
Add the new assignments to the data structure.
At some point (when?)
For each generalizer:
Use the generalizer's selector to see if it can be applied
Apply the generalizer to produce a new type, possibly with some s injected
*)
open Ast_typed.Types
module UnionFindWrapper = struct
(* Light wrapper for API for grouped_by_variable in the structured
db, to access it modulo unification variable aliases. *)
let get_constraints_related_to : type_variable -> structured_dbs -> constraints =
fun variable dbs ->
let variable , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in
match Map.find_opt variable dbs.grouped_by_variable with
Some l -> l
| None -> {
constructor = [] ;
poly = [] ;
tc = [] ;
}
let add_constraints_related_to : type_variable -> constraints -> structured_dbs -> structured_dbs =
fun variable c dbs ->
(* let (variable_repr , _height) , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in *)
let variable_repr , aliases = UF.get_or_set variable dbs.aliases in
let dbs = { dbs with aliases } in
let grouped_by_variable = Map.update variable_repr (function
None -> Some c
| Some (x : constraints) -> Some {
constructor = c.constructor @ x.constructor ;
poly = c.poly @ x.poly ;
tc = c.tc @ x.tc ;
})
dbs.grouped_by_variable
in
let dbs = { dbs with grouped_by_variable } in
dbs
let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs =
fun variable_a variable_b dbs ->
(* get old representant for variable_a *)
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
let dbs = { dbs with aliases } in
(* get old representant for variable_b *)
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
let dbs = { dbs with aliases } in
(* alias variable_a and variable_b together *)
let aliases = UF.alias variable_a variable_b dbs.aliases in
let dbs = { dbs with aliases } in
(* Replace the two entries in grouped_by_variable by a single one *)
(
let get_constraints ab =
match Map.find_opt ab dbs.grouped_by_variable with
| Some x -> x
| None -> { constructor = [] ; poly = [] ; tc = [] } in
let constraints_a = get_constraints variable_repr_a in
let constraints_b = get_constraints variable_repr_b in
let all_constraints = {
constructor = constraints_a.constructor @ constraints_b.constructor ;
poly = constraints_a.poly @ constraints_b.poly ;
tc = constraints_a.tc @ constraints_b.tc ;
} in
let grouped_by_variable =
Map.add variable_repr_a all_constraints dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
let grouped_by_variable =
Map.remove variable_repr_b dbs.grouped_by_variable in
let dbs = { dbs with grouped_by_variable} in
dbs
)
end
(* sub-sub component: constraint normalizer: remove dupes and give structure
* right now: union-find of unification vars
* later: better database-like organisation of knowledge *)
(* Each normalizer returns an updated database (after storing the
incoming constraint) and a list of constraints, used when the
normalizer rewrites the constraints e.g. into simpler ones. *)
(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *)
type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
(** Updates the dbs.all_constraints field when new constraints are
discovered.
This field contains a list of all the constraints, without any form of
grouping or sorting. *)
let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
(** Updates the dbs.grouped_by_variable field when new constraints are
discovered.
This field contains a map from type variables to lists of
constraints that are related to that variable (in other words, the
key appears in the equation).
*)
let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let store_constraint tvars constraints =
let aux dbs (tvar : type_variable) =
UnionFindWrapper.add_constraints_related_to tvar constraints dbs
in List.fold_left aux dbs tvars
in
let dbs = match new_constraint with
SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []}
| SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]}
| SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []}
| SC_Alias { a; b } -> UnionFindWrapper.merge_constraints a b dbs
in (dbs , [new_constraint])
(** Stores the first assinment ('a = ctor('b, …)) that is encountered.
Subsequent ('a = ctor('b2, )) with the same 'a are ignored.
TOOD: are we checking somewhere that 'b = 'b2 ? *)
let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
match new_constraint with
| 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
(dbs , [new_constraint])
| _ ->
(dbs , [new_constraint])
(** Evaluates a type-leval application. For now, only supports
immediate beta-reduction at the root of the type. *)
let type_level_eval : type_value -> type_value * type_constraint list =
fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
(** Checks that a type-level application has been fully reduced. For
now, only some simple cases like applications of `forall`
<polymorphic types are allowed. *)
let check_applied ((reduced, _new_constraints) as x) =
let () = match reduced with
{ 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
(* TODO: at some point there may be uses of named type aliases (type
foo = int; let x : foo = 42). These should be inlined. *)
(** This function converts constraints from type_constraint to
type_constraint_simpl. The former has more possible cases, and the
latter uses a more minimalistic constraint language.
It does not modify the dbs, and only rewrites the constraint
TODO: update the code to show that the dbs are always copied as-is
*)
let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
fun dbs new_constraint ->
let insert_fresh a b =
let fresh = Core.fresh_type_variable () 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 { 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 , [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
let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced "normalizer: reduce_type_app") in (* Note: this calls recursively but cant't fall in the same case. *)
(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 { 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, [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=({ 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=({ 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=({ 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=({ 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=({ 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 *)
(* Random notes from live discussion. Kept here to include bits as a rationale later on / remind me of the discussion in the short term.
* Feel free to erase if it rots here for too long.
*
* function (zetype, zevalue) { if (typeof(zevalue) != zetype) { ohlàlà; } else { return zevalue; } }
*
* let f = (fun {a : Type} (v : a) -> v)
*
* (forall 'a, 'a -> 'a) ~ (int -> int)
* (forall {a : Type}, forall (v : a), a) ~ (forall (v : int), int)
* ({a : Type} -> (v : a) -> a) ~ ((v : int) -> int)
*
* (@f int)
*
*
* 'c 'c
* 'd -> 'e && 'c ~ d && 'c ~ 'e
* 'c -> 'c ???????????????wtf---->???????????? [ scope of 'c is fun z ]
* 'tid ~ (forall 'c, 'c -> 'c)
* let id = (fun z -> z) in
* let ii = (fun z -> z + 0) : (int -> int) in
*
* 'a 'b ['a ~ 'b] 'a 'b
* 'a 'a 'a 'a 'a
* (forall 'a, 'a -> 'a -> 'a ) 'tid 'tid
*
* 'tid -> 'tid -> 'tid
*
* (forall 'a, 'a -> 'a -> 'a ) (forall 'c1, 'c1 -> 'c1) (int -> int)
* (forall 'c1, 'c1 -> 'c1)~(int -> int)
* ('c1 -> 'c1) ~ (int -> int)
* (fun x y -> if random then x else y) id ii as toto
* id "foo" *)
type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
let lift_state_list_monad ~state ~list = { state ; list }
let lift f =
fun { state ; list } ->
let (new_state , new_lists) = List.fold_map_acc f state list in
{ state = new_state ; list = List.flatten new_lists }
(* TODO: move this to the List module *)
let named_fold_left f ~acc ~lst = List.fold_left (fun acc elt -> f ~acc ~elt) acc lst
module Fun = struct let id x = x end (* in stdlib as of 4.08, we're in 4.07 for now *)
let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad =
fun new_constraint dbs ->
Fun.id
@@ lift normalizer_grouped_by_variable
@@ lift normalizer_assignments
@@ lift normalizer_all_constraints
@@ lift normalizer_simpl
@@ lift_state_list_monad ~state:dbs ~list:[new_constraint]
open Solver_types
(* sub-sub component: lazy selector (don't re-try all selectors every time)
* For now: just re-try everytime *)
type 'old_constraint_type selector_input = 'old_constraint_type (* some info about the constraint just added, so that we know what to look for *)
type 'selector_output selector_outputs =
WasSelected of 'selector_output list
| WasNotSelected
type new_constraints = type_constraint list
type new_assignments = c_constructor_simpl list
type ('old_constraint_type, 'selector_output) selector = 'old_constraint_type selector_input -> structured_dbs -> 'selector_output selector_outputs
type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments
(* selector / propagation rule for breaking down composite types
* 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 x = k(var …) and x = k'(var' …) *)
fun type_constraint_simpl dbs ->
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)
is symmetric *)
let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in
let other_cs = List.filter (fun (o : c_constructor_simpl) -> Var.equal c.tv o.tv) other_cs in
(* TODO double-check the conditions in the propagator, we had a
bug here because the selector was too permissive. *)
let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in
WasSelected cs_pairs
| SC_Alias _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
| SC_Poly _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
| SC_Typeclass _ -> WasNotSelected
(* TODO: move this to a more appropriate place and/or auto-generate it. *)
let compare_simple_c_constant = function
| C_arrow -> (function
(* N/A -> 1 *)
| C_arrow -> 0
| C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_option -> (function
| C_arrow -> 1
| C_option -> 0
| C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_record -> (function
| C_arrow | C_option -> 1
| C_record -> 0
| C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_variant -> (function
| C_arrow | C_option | C_record -> 1
| C_variant -> 0
| C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_map -> (function
| C_arrow | C_option | C_record | C_variant -> 1
| C_map -> 0
| C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_big_map -> (function
| C_arrow | C_option | C_record | C_variant | C_map -> 1
| C_big_map -> 0
| C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_list -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map -> 1
| C_list -> 0
| C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_set -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1
| C_set -> 0
| C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_unit -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
| C_unit -> 0
| C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_string -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
| C_string -> 0
| C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_nat -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string -> 1
| C_nat -> 0
| C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_mutez -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat -> 1
| C_mutez -> 0
| C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_timestamp -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez -> 1
| C_timestamp -> 0
| C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_int -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp -> 1
| C_int -> 0
| C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_address -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
| C_address -> 0
| C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bytes -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
| C_bytes -> 0
| C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key_hash -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
| C_key_hash -> 0
| C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
| C_key -> 0
| C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_signature -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
| C_signature -> 0
| C_operation | C_contract | C_chain_id -> -1)
| C_operation -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
| C_operation -> 0
| C_contract | C_chain_id -> -1)
| C_contract -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
| C_contract -> 0
| C_chain_id -> -1)
| C_chain_id -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
| C_chain_id -> 0
(* N/A -> -1 *)
)
(* Using a pretty-printer from the PP.ml module creates a dependency
loop, so the one that we need temporarily for debugging purposes
has been copied here. *)
let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag ->
let ct = match c_tag with
| T.C_arrow -> "arrow"
| T.C_option -> "option"
| T.C_record -> failwith "record"
| T.C_variant -> failwith "variant"
| T.C_map -> "map"
| T.C_big_map -> "big_map"
| T.C_list -> "list"
| T.C_set -> "set"
| T.C_unit -> "unit"
| T.C_string -> "string"
| T.C_nat -> "nat"
| T.C_mutez -> "mutez"
| T.C_timestamp -> "timestamp"
| T.C_int -> "int"
| T.C_address -> "address"
| T.C_bytes -> "bytes"
| T.C_key_hash -> "key_hash"
| T.C_key -> "key"
| T.C_signature -> "signature"
| T.C_operation -> "operation"
| T.C_contract -> "contract"
| T.C_chain_id -> "chain_id"
in
Format.fprintf ppf "%s" ct
let debug_pp_c_constructor_simpl ppf { tv; c_tag; tv_list } =
Format.fprintf ppf "CTOR %a %a(%a)" Var.pp tv debug_pp_constant c_tag PP_helpers.(list_sep Var.pp (const " , ")) tv_list
let propagator_break_ctor : output_break_ctor propagator =
fun selected dbs ->
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 { 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))
else
(* a.tv_list = b.tv_list *)
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 { 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 *)
(* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-(
We need to return a lazy stream of constraints. *)
let (<?) ca cb =
if ca = 0 then cb () else ca
let rec compare_list f = function
| hd1::tl1 -> (function
[] -> 1
| hd2::tl2 ->
f hd1 hd2 <? fun () ->
compare_list f tl1 tl2)
| [] -> (function [] -> 0 | _::_ -> -1) (* This follows the behaviour of Pervasives.compare for lists of different length *)
let compare_type_variable a b =
Var.compare a b
let compare_label (a:label) (b:label) =
let Label a = a in
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 { 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 () ->
compare_list compare_type_constraint a2 b2 <? fun () ->
compare_type_expression a3 b3
| P_variable _ -> -1
| P_constant _ -> -1
| P_apply _ -> -1)
| P_variable a -> (function
| P_forall _ -> 1
| P_variable b -> compare_type_variable a b
| P_constant _ -> -1
| P_apply _ -> -1)
| P_constant { p_ctor_tag=a1; p_ctor_args=a2 } -> (function
| P_forall _ -> 1
| P_variable _ -> 1
| P_constant { p_ctor_tag=b1; p_ctor_args=b2 } -> compare_simple_c_constant a1 b1 <? fun () -> compare_list compare_type_expression a2 b2
| P_apply _ -> -1)
| P_apply { tf=a1; targ=a2 } -> (function
| P_forall _ -> 1
| P_variable _ -> 1
| P_constant _ -> 1
| P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
and compare_type_constraint = fun { c = ca ; reason = ra } { c = cb ; reason = rb } ->
let c = compare_type_constraint_ ca cb in
if c < 0 then -1
else if c = 0 then String.compare ra rb
else 1
and compare_type_constraint_ = function
| C_equation { aval=a1; bval=a2 } -> (function
| C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
| C_typeclass _ -> -1
| C_access_label _ -> -1)
| C_typeclass { tc_args=a1; typeclass=a2 } -> (function
| C_equation _ -> 1
| C_typeclass { tc_args=b1; typeclass=b2 } -> compare_list compare_type_expression a1 b1 <? fun () -> compare_typeclass a2 b2
| C_access_label _ -> -1)
| C_access_label { c_access_label_tval=a1; accessor=a2; c_access_label_tvar=a3 } -> (function
| C_equation _ -> 1
| C_typeclass _ -> 1
| C_access_label { c_access_label_tval=b1; accessor=b2; c_access_label_tvar=b3 } -> compare_type_expression a1 b1 <? fun () -> compare_label a2 b2 <? fun () -> compare_type_variable a3 b3)
let compare_type_constraint_list = compare_list compare_type_constraint
let compare_p_forall
{ binder = a1; constraints = a2; body = a3 }
{ binder = b1; constraints = b2; body = b3 } =
compare_type_variable a1 b1 <? fun () ->
compare_type_constraint_list a2 b2 <? fun () ->
compare_type_expression a3 b3
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 { 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 } =
compare_c_poly_simpl a1 b1 <? fun () ->
compare_c_constructor_simpl a2 b2
let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_var'=b2 } =
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 (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 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) -> 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) -> 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
let propagator_specialize1 : output_specialize1 propagator =
fun selected dbs ->
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
(* 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 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 = { 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 { 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 =
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
let Set.{ set = already_selected ; duplicates = _ ; added = selected_outputs } = Set.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
@ -637,8 +27,9 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagat
| 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
(* TODO: put the heuristics with their state in a list. *)
let select_and_propagate_break_ctor = select_and_propagate Heuristic_break_ctor.selector Heuristic_break_ctor.propagator
let select_and_propagate_specialize1 = select_and_propagate Heuristic_specialize1.selector Heuristic_specialize1.propagator
(* Takes a constraint, applies all selector+propagator pairs to it.
Keeps track of which constraints have already been selected. *)
@ -671,7 +62,7 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s
match new_constraints with
| [] -> (already_selected, dbs)
| new_constraint :: tl ->
let { state = dbs ; list = modified_constraints } = normalizers new_constraint dbs in
let { state = dbs ; list = modified_constraints } = Normalizer.normalizers new_constraint dbs in
let (already_selected , new_constraints' , dbs) =
List.fold_left
(fun (already_selected , nc , dbs) c ->
@ -686,40 +77,20 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s
(* constraint propagation: (buch of constraints)(new constraints * assignments) *)
(* Below is a draft *)
(* type state = {
* (\* when α-renaming x to y, we put them in the same union-find class *\)
* unification_vars : unionfind ;
*
* (\* assigns a value to the representant in the unionfind *\)
* assignments : type_expression TypeVariableMap.t ;
*
* (\* constraints related to a type variable *\)
* constraints : constraints TypeVariableMap.t ;
* } *)
let initial_state : typer_state = (* {
* unification_vars = UF.empty ;
* constraints = TypeVariableMap.empty ;
* assignments = TypeVariableMap.empty ;
* } *)
{
let initial_state : typer_state = {
structured_dbs =
{
all_constraints = [] ; (* type_constraint_simpl list *)
aliases = UF.empty (fun s -> Format.asprintf "%a" Var.pp s) Var.compare ; (* unionfind *)
assignments = Map.create ~cmp:Var.compare; (* c_constructor_simpl TypeVariableMap.t *)
grouped_by_variable = Map.create ~cmp:Var.compare; (* constraints TypeVariableMap.t *)
cycle_detection_toposort = (); (* unit *)
all_constraints = ([] : type_constraint_simpl list) ;
aliases = UF.empty (fun s -> Format.asprintf "%a" Var.pp s) Var.compare;
assignments = (Map.create ~cmp:Var.compare : (type_variable, c_constructor_simpl) Map.t);
grouped_by_variable = (Map.create ~cmp:Var.compare : (type_variable, constraints) Map.t);
cycle_detection_toposort = ();
} ;
already_selected = {
break_ctor = Set.create ~cmp:compare_output_break_ctor;
specialize1 = Set.create ~cmp:compare_output_specialize1 ;
break_ctor = Set.create ~cmp:Solver_should_be_generated.compare_output_break_ctor;
specialize1 = Set.create ~cmp:Solver_should_be_generated.compare_output_specialize1 ;
}
}
@ -732,23 +103,6 @@ let initial_state : typer_state = (* {
state any further. Suzanne *)
let discard_state (_ : typer_state) = ()
(* let replace_var_in_state = fun (v : type_variable) (state : state) -> *)
(* let aux_tv : type_expression -> _ = function *)
(* | P_forall (w , cs , tval) -> failwith "TODO" *)
(* | P_variable (w) -> *)
(* if w = v then *)
(* (**) *)
(* else *)
(* (**) *)
(* | P_constant (c , args) -> failwith "TODO" *)
(* | P_access_label (tv , label) -> failwith "TODO" in *)
(* let aux_tc tc = *)
(* List.map (fun l -> List.map aux_tv l) tc in *)
(* let aux : type_constraint -> _ = function *)
(* | C_equation (l , r) -> C_equation (aux_tv l , aux_tv r) *)
(* | C_typeclass (l , rs) -> C_typeclass (List.map aux_tv l , aux_tc rs) *)
(* in List.map aux state *)
(* This is the solver *)
let aggregate_constraints : typer_state -> type_constraint list -> typer_state result = fun state newc ->
(* TODO: Iterate over constraints *)
@ -758,12 +112,6 @@ let aggregate_constraints : typer_state -> type_constraint list -> typer_state r
(*let { constraints ; eqv } = state in
ok { constraints = constraints @ newc ; eqv }*)
(* Later on, we'll ensure that all the heuristics register the
existential/unification variables that they create, as well as the
new constraints that they create. We will then check that they only

View File

@ -0,0 +1,214 @@
(* The contents of this file should be auto-generated. *)
open Ast_typed.Types
module T = Ast_typed.Types
let compare_simple_c_constant = function
| C_arrow -> (function
(* N/A -> 1 *)
| C_arrow -> 0
| C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_option -> (function
| C_arrow -> 1
| C_option -> 0
| C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_record -> (function
| C_arrow | C_option -> 1
| C_record -> 0
| C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_variant -> (function
| C_arrow | C_option | C_record -> 1
| C_variant -> 0
| C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_map -> (function
| C_arrow | C_option | C_record | C_variant -> 1
| C_map -> 0
| C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_big_map -> (function
| C_arrow | C_option | C_record | C_variant | C_map -> 1
| C_big_map -> 0
| C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_list -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map -> 1
| C_list -> 0
| C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_set -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1
| C_set -> 0
| C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_unit -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1
| C_unit -> 0
| C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_string -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1
| C_string -> 0
| C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_nat -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string -> 1
| C_nat -> 0
| C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_mutez -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat -> 1
| C_mutez -> 0
| C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_timestamp -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez -> 1
| C_timestamp -> 0
| C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_int -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp -> 1
| C_int -> 0
| C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_address -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1
| C_address -> 0
| C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_bytes -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1
| C_bytes -> 0
| C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key_hash -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1
| C_key_hash -> 0
| C_key | C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_key -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1
| C_key -> 0
| C_signature | C_operation | C_contract | C_chain_id -> -1)
| C_signature -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1
| C_signature -> 0
| C_operation | C_contract | C_chain_id -> -1)
| C_operation -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1
| C_operation -> 0
| C_contract | C_chain_id -> -1)
| C_contract -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1
| C_contract -> 0
| C_chain_id -> -1)
| C_chain_id -> (function
| C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1
| C_chain_id -> 0
(* N/A -> -1 *)
)
let (<?) ca cb =
if ca = 0 then cb () else ca
let rec compare_list f = function
| hd1::tl1 -> (function
[] -> 1
| hd2::tl2 ->
f hd1 hd2 <? fun () ->
compare_list f tl1 tl2)
| [] -> (function [] -> 0 | _::_ -> -1) (* This follows the behaviour of Pervasives.compare for lists of different length *)
let compare_type_variable a b =
Var.compare a b
let compare_label (a:label) (b:label) =
let Label a = a in
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 { 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 () ->
compare_list compare_type_constraint a2 b2 <? fun () ->
compare_type_expression a3 b3
| P_variable _ -> -1
| P_constant _ -> -1
| P_apply _ -> -1)
| P_variable a -> (function
| P_forall _ -> 1
| P_variable b -> compare_type_variable a b
| P_constant _ -> -1
| P_apply _ -> -1)
| P_constant { p_ctor_tag=a1; p_ctor_args=a2 } -> (function
| P_forall _ -> 1
| P_variable _ -> 1
| P_constant { p_ctor_tag=b1; p_ctor_args=b2 } -> compare_simple_c_constant a1 b1 <? fun () -> compare_list compare_type_expression a2 b2
| P_apply _ -> -1)
| P_apply { tf=a1; targ=a2 } -> (function
| P_forall _ -> 1
| P_variable _ -> 1
| P_constant _ -> 1
| P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
and compare_type_constraint = fun { c = ca ; reason = ra } { c = cb ; reason = rb } ->
let c = compare_type_constraint_ ca cb in
if c < 0 then -1
else if c = 0 then String.compare ra rb
else 1
and compare_type_constraint_ = function
| C_equation { aval=a1; bval=a2 } -> (function
| C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
| C_typeclass _ -> -1
| C_access_label _ -> -1)
| C_typeclass { tc_args=a1; typeclass=a2 } -> (function
| C_equation _ -> 1
| C_typeclass { tc_args=b1; typeclass=b2 } -> compare_list compare_type_expression a1 b1 <? fun () -> compare_typeclass a2 b2
| C_access_label _ -> -1)
| C_access_label { c_access_label_tval=a1; accessor=a2; c_access_label_tvar=a3 } -> (function
| C_equation _ -> 1
| C_typeclass _ -> 1
| C_access_label { c_access_label_tval=b1; accessor=b2; c_access_label_tvar=b3 } -> compare_type_expression a1 b1 <? fun () -> compare_label a2 b2 <? fun () -> compare_type_variable a3 b3)
let compare_type_constraint_list = compare_list compare_type_constraint
let compare_p_forall
{ binder = a1; constraints = a2; body = a3 }
{ binder = b1; constraints = b2; body = b3 } =
compare_type_variable a1 b1 <? fun () ->
compare_type_constraint_list a2 b2 <? fun () ->
compare_type_expression a3 b3
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 { 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
(* TODO: use Ast_typed.Compare_generic.output_specialize1 etc. but don't compare the reasons *)
let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var = b2 } =
compare_c_poly_simpl a1 b1 <? fun () ->
compare_c_constructor_simpl a2 b2
let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_var'=b2 } =
compare_c_constructor_simpl a1 b1 <? fun () -> compare_c_constructor_simpl a2 b2
(* Using a pretty-printer from the PP.ml module creates a dependency
loop, so the one that we need temporarily for debugging purposes
has been copied here. *)
let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag ->
let ct = match c_tag with
| T.C_arrow -> "arrow"
| T.C_option -> "option"
| T.C_record -> failwith "record"
| T.C_variant -> failwith "variant"
| T.C_map -> "map"
| T.C_big_map -> "big_map"
| T.C_list -> "list"
| T.C_set -> "set"
| T.C_unit -> "unit"
| T.C_string -> "string"
| T.C_nat -> "nat"
| T.C_mutez -> "mutez"
| T.C_timestamp -> "timestamp"
| T.C_int -> "int"
| T.C_address -> "address"
| T.C_bytes -> "bytes"
| T.C_key_hash -> "key_hash"
| T.C_key -> "key"
| T.C_signature -> "signature"
| T.C_operation -> "operation"
| T.C_contract -> "contract"
| T.C_chain_id -> "chain_id"
in
Format.fprintf ppf "%s" ct
let debug_pp_c_constructor_simpl ppf { tv; c_tag; tv_list } =
Format.fprintf ppf "CTOR %a %a(%a)" Var.pp tv debug_pp_constant c_tag PP_helpers.(list_sep Var.pp (const " , ")) tv_list

View File

@ -0,0 +1,18 @@
open Ast_typed.Types
type 'old_constraint_type selector_input = 'old_constraint_type (* some info about the constraint just added, so that we know what to look for *)
type 'selector_output selector_outputs =
WasSelected of 'selector_output list
| WasNotSelected
type new_constraints = type_constraint list
type new_assignments = c_constructor_simpl list
type ('old_constraint_type, 'selector_output) selector = 'old_constraint_type selector_input -> structured_dbs -> 'selector_output selector_outputs
type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments
(* state+list monad *)
type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
let lift_state_list_monad ~state ~list = { state ; list }
let lift f =
fun { state ; list } ->
let (new_state , new_lists) = List.fold_map_acc f state list in
{ state = new_state ; list = List.flatten new_lists }

View File

@ -0,0 +1,18 @@
(* This file implements the type-level language. For now limited to
type constants, type functions and their application. *)
open Ast_typed.Types
(** Evaluates a type-leval application. For now, only supports
immediate beta-reduction at the root of the type. *)
let type_level_eval : type_value -> type_value * type_constraint list =
fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
(** Checks that a type-level application has been fully reduced. For
now, only some simple cases like applications of `forall`
<polymorphic types are allowed. *)
let check_applied ((reduced, _new_constraints) as x) =
let () = match reduced with
{ 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

View File

@ -416,11 +416,11 @@ and type_lambda e state {
let%bind input_type' = bind_map_option (evaluate_type e) input_type in
let%bind output_type' = bind_map_option (evaluate_type e) output_type in
let fresh : O.type_expression = t_variable (Solver.Wrap.fresh_binder ()) () in
let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in
let e' = Environment.add_ez_binder (binder) fresh e in
let%bind (result , state') = type_expression e' state result in
let wrapped = Solver.Wrap.lambda fresh input_type' output_type' result.type_expression in
let wrapped = 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

@ -2,6 +2,7 @@ module Types = Types
module Environment = Environment
module PP = PP
module PP_generic = PP_generic
module Compare_generic = Compare_generic
module Combinators = struct
include Combinators
end

View File

@ -127,4 +127,3 @@ let fold_map__poly_set : type a state new_a . new_a extra_info__comparable -> (s
ok (state , PolySet.add new_elt s) in
let%bind (state , m) = PolySet.fold_inc aux s ~init:(ok (state, PolySet.create ~cmp:new_compare)) in
ok (state , m)

159
src/test/contracts/id.ligo Normal file
View File

@ -0,0 +1,159 @@
type id is int
type id_details is
record [
owner: address;
controller: address;
profile: bytes;
]
type buy is
record [
profile: bytes;
initial_controller: option(address);
]
type update_owner is
record [
id: id;
new_owner: address;
]
type update_details is
record [
id: id;
new_profile: option(bytes);
new_controller: option(address);
]
type action is
| Buy of buy
| Update_owner of update_owner
| Update_details of update_details
| Skip of unit
(* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. *)
type storage is
record [
identities: big_map (id, id_details);
next_id: int;
name_price: tez;
skip_price: tez;
]
(** Preliminary thoughts on ids:
I very much like the simplicity of http://gurno.com/adam/mne/.
5 three letter words means you have a 15 character identity, not actually more
annoying than an IP address and a lot more memorable than the raw digits. This
can be stored as a single integer which is then translated into the corresponding
series of 5 words.
I in general like the idea of having a 'skip' mechanism, but it does need to cost
something so people don't eat up the address space. 256 ^ 5 means you have a lot
of address space, but if people troll by skipping a lot that could be eaten up.
Should probably do some napkin calculations for how expensive skipping needs to
be to deter people from doing it just to chew up address space.
*)
function buy (const parameter : buy; const storage : storage) : list(operation) * storage is
begin
if amount = storage.name_price
then skip
else failwith("Incorrect amount paid.");
const profile : bytes = parameter.profile;
const initial_controller : option(address) = parameter.initial_controller;
var identities : big_map (id, id_details) := storage.identities;
const new_id : int = storage.next_id;
const controller : address =
case initial_controller of
Some(addr) -> addr
| None -> sender
end;
const new_id_details: id_details =
record [
owner = sender ;
controller = controller ;
profile = profile ;
];
identities[new_id] := new_id_details;
end with ((nil : list(operation)), storage with record [
identities = identities;
next_id = new_id + 1;
])
function update_owner (const parameter : update_owner; const storage : storage) :
list(operation) * storage is
begin
if (amount =/= 0mutez)
then
begin
failwith("Updating owner doesn't cost anything.");
end
else skip;
const id : int = parameter.id;
const new_owner : address = parameter.new_owner;
var identities : big_map (id, id_details) := storage.identities;
const id_details : id_details =
case identities[id] of
Some(id_details) -> id_details
| None -> (failwith("This ID does not exist."): id_details)
end;
if sender = id_details.owner
then skip;
else failwith("You are not the owner of this ID.");
id_details.owner := new_owner;
identities[id] := id_details;
end with ((nil: list(operation)), storage with record [ identities = identities; ])
function update_details (const parameter : update_details; const storage : storage ) :
list(operation) * storage is
begin
if (amount =/= 0mutez)
then failwith("Updating details doesn't cost anything.")
else skip;
const id : int = parameter.id;
const new_profile : option(bytes) = parameter.new_profile;
const new_controller : option(address) = parameter.new_controller;
const identities : big_map (id, id_details) = storage.identities;
const id_details: id_details =
case identities[id] of
Some(id_details) -> id_details
| None -> (failwith("This ID does not exist."): id_details)
end;
if (sender = id_details.controller) or (sender = id_details.owner)
then skip;
else failwith("You are not the owner or controller of this ID.");
const owner: address = id_details.owner;
const profile: bytes =
case new_profile of
None -> (* Default *) id_details.profile
| Some(new_profile) -> new_profile
end;
const controller: address =
case new_controller of
None -> (* Default *) id_details.controller
| Some(new_controller) -> new_controller
end;
id_details.owner := owner;
id_details.controller := controller;
id_details.profile := profile;
identities[id] := id_details;
end with ((nil: list(operation)), storage with record [ identities = identities; ])
(* Let someone skip the next identity so nobody has to take one that's undesirable *)
function skip_ (const p: unit; const storage: storage) : list(operation) * storage is
begin
if amount = storage.skip_price
then skip
else failwith("Incorrect amount paid.");
end with ((nil: list(operation)), storage with record [ next_id = storage.next_id + 1; ])
function main (const action : action; const storage : storage) : list(operation) * storage is
case action of
| Buy(b) -> buy (b, storage)
| Update_owner(uo) -> update_owner (uo, storage)
| Update_details(ud) -> update_details (ud, storage)
| Skip(s) -> skip_ (unit, storage)
end;

View File

@ -6,9 +6,21 @@ type id_details = {
profile: bytes
}
type buy = bytes * address option
type update_owner = id * address
type update_details = id * bytes option * address option
type buy = {
profile: bytes;
initial_controller: address option;
}
type update_owner = {
id: id;
new_owner: address;
}
type update_details = {
id: id;
new_profile: bytes option;
new_controller: address option;
}
type action =
| Buy of buy
@ -19,7 +31,14 @@ type action =
(* The prices kept in storage can be changed by bakers, though they
should only be adjusted down over time, not up. *)
type storage = (id, id_details) big_map * int * (tez * tez)
(* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. *)
type storage = {
identities: (id, id_details) big_map;
next_id: int;
name_price: tez;
skip_price: tez;
}
type return = operation list * storage
@ -38,12 +57,16 @@ a lot that could be eaten up. Should probably do some napkin
calculations for how expensive skipping needs to be to deter people
from doing it just to chew up address space. *)
let buy (parameter, storage: (bytes * address option) * storage) =
let buy (parameter, storage: buy * storage) =
let void: unit =
if Tezos.amount <> storage.2.0
then (failwith "Incorrect amount paid.": unit) in
let profile, initial_controller = parameter in
let identities, new_id, prices = storage in
if amount = storage.name_price
then ()
else (failwith "Incorrect amount paid.": unit)
in
let profile = parameter.profile in
let initial_controller = parameter.initial_controller in
let identities = storage.identities in
let new_id = storage.next_id in
let controller: address =
match initial_controller with
| Some addr -> addr
@ -54,74 +77,84 @@ let buy (parameter, storage: (bytes * address option) * storage) =
profile = profile} in
let updated_identities : (id, id_details) big_map =
Big_map.update new_id (Some new_id_details) identities
in ([]: operation list), (updated_identities, new_id + 1, prices)
in
([]: operation list), {storage with identities = updated_identities;
next_id = new_id + 1;
}
let update_owner (parameter, storage : (id * address) * storage) =
if amount <> 0tez
then (failwith "Updating owner doesn't cost anything.": return)
let update_owner (parameter, storage: update_owner * storage) =
if (amount <> 0mutez)
then (failwith "Updating owner doesn't cost anything.": (operation list) * storage)
else
let id, new_owner = parameter in
let identities, last_id, prices = storage in
let id = parameter.id in
let new_owner = parameter.new_owner in
let identities = storage.identities in
let current_id_details: id_details =
match Big_map.find_opt id identities with
| Some id_details -> id_details
| None -> (failwith "This ID does not exist." : id_details) in
let is_allowed : bool =
if Tezos.sender = current_id_details.owner
then true
else (failwith "You are not the owner of this ID." : bool) in
| None -> (failwith "This ID does not exist.": id_details)
in
let u : unit =
if sender = current_id_details.owner
then ()
else failwith "You are not the owner of this ID."
in
let updated_id_details: id_details = {
owner = new_owner;
controller = current_id_details.controller;
profile = current_id_details.profile} in
let updated_identities =
Big_map.update id (Some updated_id_details) identities
in ([]: operation list), (updated_identities, last_id, prices)
profile = current_id_details.profile;
}
in
let updated_identities = Big_map.update id (Some updated_id_details) identities in
([]: operation list), {storage with identities = updated_identities}
let update_details (parameter, storage: (id * bytes option * address option) * storage) =
if Tezos.amount <> 0tez
then
(failwith "Updating details doesn't cost anything." : return)
let update_details (parameter, storage: update_details * storage) =
if (amount <> 0mutez)
then (failwith "Updating details doesn't cost anything.": (operation list) * storage)
else
let id, new_profile, new_controller = parameter in
let identities, last_id, prices = storage in
let id = parameter.id in
let new_profile = parameter.new_profile in
let new_controller = parameter.new_controller in
let identities = storage.identities in
let current_id_details: id_details =
match Big_map.find_opt id identities with
| Some id_details -> id_details
| None -> (failwith "This ID does not exist.": id_details) in
let is_allowed : bool =
if Tezos.sender = current_id_details.controller
|| Tezos.sender = current_id_details.owner
then true
else
(failwith ("You are not the owner or controller of this ID.")
: bool) in
| None -> (failwith "This ID does not exist.": id_details)
in
let u : unit =
if (sender = current_id_details.controller) || (sender = current_id_details.owner)
then ()
else failwith ("You are not the owner or controller of this ID.")
in
let owner: address = current_id_details.owner in
let profile: bytes =
match new_profile with
| None -> (* Default *) current_id_details.profile
| Some new_profile -> new_profile in
| Some new_profile -> new_profile
in
let controller: address =
match new_controller with
| None -> (* Default *) current_id_details.controller
| Some new_controller -> new_controller in
| Some new_controller -> new_controller
in
let updated_id_details: id_details = {
owner = owner;
controller = controller;
profile = profile} in
profile = profile;
}
in
let updated_identities: (id, id_details) big_map =
Big_map.update id (Some updated_id_details) identities
in ([]: operation list), (updated_identities, last_id, prices)
(* Let someone skip the next identity so nobody has to take one that's
undesirable *)
Big_map.update id (Some updated_id_details) identities in
([]: operation list), {storage with identities = updated_identities}
(* Let someone skip the next identity so nobody has to take one that's undesirable *)
let skip (p,storage: unit * storage) =
let void: unit =
if Tezos.amount <> storage.2.1
then (failwith "Incorrect amount paid." : unit) in
let identities, last_id, prices = storage in
([]: operation list), (identities, last_id + 1, prices)
if amount = storage.skip_price
then ()
else failwith "Incorrect amount paid."
in
([]: operation list), {storage with next_id = storage.next_id + 1}
let main (action, storage : action * storage) : return =
match action with

View File

@ -0,0 +1,167 @@
type id = int
type id_details = {
owner: address,
controller: address,
profile: bytes,
}
type buy = {
profile: bytes,
initial_controller: option(address),
}
type update_owner = {
id: id,
new_owner: address,
}
type update_details = {
id: id,
new_profile: option(bytes),
new_controller: option(address),
}
type action =
| Buy(buy)
| Update_owner(update_owner)
| Update_details(update_details)
| Skip(unit)
/* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. */
type storage = {
identities: big_map (id, id_details),
next_id: int,
name_price: tez,
skip_price: tez,
}
/** Preliminary thoughts on ids:
I very much like the simplicity of http://gurno.com/adam/mne/.
5 three letter words means you have a 15 character identity, not actually more
annoying than an IP address and a lot more memorable than the raw digits. This
can be stored as a single integer which is then translated into the corresponding
series of 5 words.
I in general like the idea of having a 'skip' mechanism, but it does need to cost
something so people don't eat up the address space. 256 ^ 5 means you have a lot
of address space, but if people troll by skipping a lot that could be eaten up.
Should probably do some napkin calculations for how expensive skipping needs to
be to deter people from doing it just to chew up address space.
*/
let buy = ((parameter, storage): (buy, storage)) : (list(operation), storage) => {
let void: unit =
if (amount == storage.name_price) { (); }
else { failwith("Incorrect amount paid."); };
let profile = parameter.profile;
let initial_controller = parameter.initial_controller;
let identities = storage.identities;
let new_id = storage.next_id;
let controller: address =
switch (initial_controller) {
| Some(addr) => addr
| None => sender
};
let new_id_details: id_details = {
owner : sender,
controller : controller,
profile : profile,
};
let updated_identities: big_map (id, id_details) =
Big_map.update(new_id, Some(new_id_details), identities);
(([]: list(operation)), { ...storage,
identities : updated_identities,
next_id : new_id + 1,
});
};
let update_owner = ((parameter, storage): (update_owner, storage)) : (list(operation), storage) => {
let void: unit =
if (amount != 0mutez) {
failwith("Updating owner doesn't cost anything.");
}
else { (); };
let id : int = parameter.id;
let new_owner = parameter.new_owner;
let identities = storage.identities;
let current_id_details: id_details =
switch (Big_map.find_opt(id, identities)) {
| Some(id_details) => id_details
| None => (failwith("This ID does not exist."): id_details)
};
let u: unit =
if (sender == current_id_details.owner) { (); }
else { failwith("You are not the owner of this ID."); };
let updated_id_details: id_details = {
owner : new_owner,
controller : current_id_details.controller,
profile : current_id_details.profile,
};
let updated_identities = Big_map.update(id, (Some updated_id_details), identities);
(([]: list(operation)), { ...storage, identities : updated_identities });
};
let update_details = ((parameter, storage): (update_details, storage)) :
(list(operation), storage) => {
let void : unit =
if (amount != 0mutez) {
failwith("Updating details doesn't cost anything.");
}
else { (); };
let id = parameter.id;
let new_profile = parameter.new_profile;
let new_controller = parameter.new_controller;
let identities = storage.identities;
let current_id_details: id_details =
switch (Big_map.find_opt(id, identities)) {
| Some(id_details) => id_details
| None => (failwith("This ID does not exist."): id_details)
};
let u: unit =
if ((sender != current_id_details.controller) &&
(sender != current_id_details.owner)) {
failwith ("You are not the owner or controller of this ID.")
}
else { (); };
let owner: address = current_id_details.owner;
let profile: bytes =
switch (new_profile) {
| None => /* Default */ current_id_details.profile
| Some(new_profile) => new_profile
};
let controller: address =
switch (new_controller) {
| None => /* Default */ current_id_details.controller
| Some new_controller => new_controller
};
let updated_id_details: id_details = {
owner : owner,
controller : controller,
profile : profile,
};
let updated_identities: big_map (id, id_details) =
Big_map.update(id, (Some updated_id_details), identities);
(([]: list(operation)), { ...storage, identities : updated_identities });
};
/* Let someone skip the next identity so nobody has to take one that's undesirable */
let skip = ((p,storage): (unit, storage)) => {
let void : unit =
if (amount != storage.skip_price) {
failwith("Incorrect amount paid.");
}
else { (); };
(([]: list(operation)), { ...storage, next_id : storage.next_id + 1 });
};
let main = ((action, storage): (action, storage)) : (list(operation), storage) => {
switch (action) {
| Buy(b) => buy((b, storage))
| Update_owner(uo) => update_owner((uo, storage))
| Update_details ud => update_details((ud, storage))
| Skip s => skip(((), storage))
};
};

View File

@ -0,0 +1,243 @@
(*_*
name: ID Contract (CameLIGO)
language: cameligo
compile:
entrypoint: main
dryRun:
entrypoint: main
parameters: |
Buy (
{
profile=0x0501000000026869;
initial_controller=Some(("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address))
}
)
storage: |
{
identities=Big_map.literal[
(1,
{owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869}
);
];
next_id=2;
name_price=0tez;
skip_price=333mutez
}
deploy:
entrypoint: main
storage: |
{
identities=Big_map.literal[
(1,
{owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869}
);
];
next_id=2;
name_price=10tez;
skip_price=333mutez
}
evaluateValue:
entrypoint: ""
evaluateFunction:
entrypoint: buy
parameters: |
{
profile=0x0501000000026869;
initial_controller=Some(("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address))
},
{
identities=Big_map.literal[
(1,
{owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869}
);
];
next_id=2;
name_price=0tez;
skip_price=333mutez
}
*_*)
type id = int
type id_details = {
owner: address;
controller: address;
profile: bytes;
}
type buy = {
profile: bytes;
initial_controller: address option;
}
type update_owner = {
id: id;
new_owner: address;
}
type update_details = {
id: id;
new_profile: bytes option;
new_controller: address option;
}
type action =
| Buy of buy
| Update_owner of update_owner
| Update_details of update_details
| Skip of unit
(* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. *)
type storage = {
identities: (id, id_details) big_map;
next_id: int;
name_price: tez;
skip_price: tez;
}
(** Preliminary thoughts on ids:
I very much like the simplicity of http://gurno.com/adam/mne/
Five three letter words means you have a 15 character identity, not actually more
annoying than an IP address and a lot more memorable than the raw digits. This
can be stored as a single integer which is then translated into the corresponding
series of 5 words.
I, in general like the idea of having a 'skip' mechanism, but it does need to cost
something so people don't eat up the address space. 256 ^ 5 means you have a lot
of address space, but if people troll by skipping a lot that could be eaten up.
Should probably do some napkin calculations for how expensive skipping needs to
be to deter people from doing it just to chew up address space.
*)
let buy (parameter, storage: buy * storage) =
let void: unit =
if amount = storage.name_price
then ()
else (failwith "Incorrect amount paid.": unit)
in
let profile = parameter.profile in
let initial_controller = parameter.initial_controller in
let identities = storage.identities in
let new_id = storage.next_id in
let controller: address =
match initial_controller with
| Some addr -> addr
| None -> sender
in
let new_id_details: id_details = {
owner = sender ;
controller = controller ;
profile = profile ;
}
in
let updated_identities: (id, id_details) big_map =
Big_map.update new_id (Some new_id_details) identities
in
([]: operation list), {identities = updated_identities;
next_id = new_id + 1;
name_price = storage.name_price;
skip_price = storage.skip_price;
}
let update_owner (parameter, storage: update_owner * storage) =
if (amount <> 0mutez)
then (failwith "Updating owner doesn't cost anything.": (operation list) * storage)
else
let id = parameter.id in
let new_owner = parameter.new_owner in
let identities = storage.identities in
let current_id_details: id_details =
match Big_map.find_opt id identities with
| Some id_details -> id_details
| None -> (failwith "This ID does not exist.": id_details)
in
let is_allowed: bool =
if sender = current_id_details.owner
then true
else (failwith "You are not the owner of this ID.": bool)
in
let updated_id_details: id_details = {
owner = new_owner;
controller = current_id_details.controller;
profile = current_id_details.profile;
}
in
let updated_identities = Big_map.update id (Some updated_id_details) identities in
([]: operation list), {identities = updated_identities;
next_id = storage.next_id;
name_price = storage.name_price;
skip_price = storage.skip_price;
}
let update_details (parameter, storage: update_details * storage) =
if (amount <> 0mutez)
then (failwith "Updating details doesn't cost anything.": (operation list) * storage)
else
let id = parameter.id in
let new_profile = parameter.new_profile in
let new_controller = parameter.new_controller in
let identities = storage.identities in
let current_id_details: id_details =
match Big_map.find_opt id identities with
| Some id_details -> id_details
| None -> (failwith "This ID does not exist.": id_details)
in
let is_allowed: bool =
if (sender = current_id_details.controller) || (sender = current_id_details.owner)
then true
else (failwith ("You are not the owner or controller of this ID."): bool)
in
let owner: address = current_id_details.owner in
let profile: bytes =
match new_profile with
| None -> (* Default *) current_id_details.profile
| Some new_profile -> new_profile
in
let controller: address =
match new_controller with
| None -> (* Default *) current_id_details.controller
| Some new_controller -> new_controller
in
let updated_id_details: id_details = {
owner = owner;
controller = controller;
profile = profile;
}
in
let updated_identities: (id, id_details) big_map =
Big_map.update id (Some updated_id_details) identities in
([]: operation list), {identities = updated_identities;
next_id = storage.next_id;
name_price = storage.name_price;
skip_price = storage.skip_price;
}
(* Let someone skip the next identity so nobody has to take one that's undesirable *)
let skip (p,storage: unit * storage) =
let void: unit =
if amount = storage.skip_price
then ()
else (failwith "Incorrect amount paid.": unit)
in
([]: operation list), {identities = storage.identities;
next_id = storage.next_id + 1;
name_price = storage.name_price;
skip_price = storage.skip_price;
}
let main (action, storage: action * storage) : operation list * storage =
match action with
| Buy b -> buy (b, storage)
| Update_owner uo -> update_owner (uo, storage)
| Update_details ud -> update_details (ud, storage)
| Skip s -> skip ((), storage)

View File

@ -0,0 +1,242 @@
(*_*
name: ID Contract (PascaLIGO)
language: pascaligo
compile:
entrypoint: main
dryRun:
entrypoint: main
parameters: |
Buy (
record [
profile=0x0501000000026869;
initial_controller=Some(("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address))
]
)
storage: |
record [
identities=big_map[
1->record
[owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869]
];
next_id=2;
name_price=0tez;
skip_price=50mutez;
]
deploy:
entrypoint: main
storage: |
record [
identities=big_map[
1->record
[owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869]
];
next_id=2;
name_price=0tez;
skip_price=50mutez;
]
evaluateValue:
entrypoint: ""
evaluateFunction:
entrypoint: buy
parameters: |
(
record [
profile=0x0501000000026869;
initial_controller=Some(("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address))
],
record [ identities=big_map[
1->record
[owner=("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address);
controller=("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address);
profile=0x0501000000026869]
];
next_id=2;
name_price=0tez;
skip_price=333mutez;
]
)
*_*)
type id is int
type id_details is
record [
owner: address;
controller: address;
profile: bytes;
]
type buy is
record [
profile: bytes;
initial_controller: option(address);
]
type update_owner is
record [
id: id;
new_owner: address;
]
type update_details is
record [
id: id;
new_profile: option(bytes);
new_controller: option(address);
]
type action is
| Buy of buy
| Update_owner of update_owner
| Update_details of update_details
| Skip of unit
(* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. *)
type storage is
record [
identities: big_map (id, id_details);
next_id: int;
name_price: tez;
skip_price: tez;
]
(** Preliminary thoughts on ids:
I very much like the simplicity of http://gurno.com/adam/mne/.
5 three letter words means you have a 15 character identity, not actually more
annoying than an IP address and a lot more memorable than the raw digits. This
can be stored as a single integer which is then translated into the corresponding
series of 5 words.
I in general like the idea of having a 'skip' mechanism, but it does need to cost
something so people don't eat up the address space. 256 ^ 5 means you have a lot
of address space, but if people troll by skipping a lot that could be eaten up.
Should probably do some napkin calculations for how expensive skipping needs to
be to deter people from doing it just to chew up address space.
*)
function buy (const parameter : buy; const storage : storage) : list(operation) * storage is
begin
if amount = storage.name_price
then skip
else failwith("Incorrect amount paid.");
const profile : bytes = parameter.profile;
const initial_controller : option(address) = parameter.initial_controller;
var identities : big_map (id, id_details) := storage.identities;
const new_id : int = storage.next_id;
const controller : address =
case initial_controller of
Some(addr) -> addr
| None -> sender
end;
const new_id_details: id_details =
record [
owner = sender ;
controller = controller ;
profile = profile ;
];
identities[new_id] := new_id_details;
end with ((nil : list(operation)), record [
identities = identities;
next_id = new_id + 1;
name_price = storage.name_price;
skip_price = storage.skip_price;
])
function update_owner (const parameter : update_owner; const storage : storage) :
list(operation) * storage is
begin
if (amount =/= 0mutez)
then
begin
failwith("Updating owner doesn't cost anything.");
end
else skip;
const id : int = parameter.id;
const new_owner : address = parameter.new_owner;
var identities : big_map (id, id_details) := storage.identities;
const id_details : id_details =
case identities[id] of
Some(id_details) -> id_details
| None -> (failwith("This ID does not exist."): id_details)
end;
var is_allowed : bool := False;
if sender = id_details.owner
then is_allowed := True
else failwith("You are not the owner of this ID.");
id_details.owner := new_owner;
identities[id] := id_details;
end with ((nil: list(operation)), record [
identities = identities;
next_id = storage.next_id;
name_price = storage.name_price;
skip_price = storage.skip_price;
])
function update_details (const parameter : update_details; const storage : storage ) :
list(operation) * storage is
begin
if (amount =/= 0mutez)
then failwith("Updating details doesn't cost anything.")
else skip;
const id : int = parameter.id;
const new_profile : option(bytes) = parameter.new_profile;
const new_controller : option(address) = parameter.new_controller;
const identities : big_map (id, id_details) = storage.identities;
const id_details: id_details =
case identities[id] of
Some(id_details) -> id_details
| None -> (failwith("This ID does not exist."): id_details)
end;
var is_allowed : bool := False;
if (sender = id_details.controller) or (sender = id_details.owner)
then is_allowed := True
else failwith("You are not the owner or controller of this ID.");
const owner: address = id_details.owner;
const profile: bytes =
case new_profile of
None -> (* Default *) id_details.profile
| Some(new_profile) -> new_profile
end;
const controller: address =
case new_controller of
None -> (* Default *) id_details.controller
| Some(new_controller) -> new_controller
end;
id_details.owner := owner;
id_details.controller := controller;
id_details.profile := profile;
identities[id] := id_details;
end with ((nil: list(operation)), record [
identities = identities;
next_id = storage.next_id;
name_price = storage.name_price;
skip_price = storage.skip_price;
])
(* Let someone skip the next identity so nobody has to take one that's undesirable *)
function skip_ (const p: unit; const storage: storage) : list(operation) * storage is
begin
if amount = storage.skip_price
then skip
else failwith("Incorrect amount paid.");
end with ((nil: list(operation)), record [
identities = storage.identities;
next_id = storage.next_id + 1;
name_price = storage.name_price;
skip_price = storage.skip_price;
])
function main (const action : action; const storage : storage) : list(operation) * storage is
case action of
| Buy(b) -> buy (b, storage)
| Update_owner(uo) -> update_owner (uo, storage)
| Update_details(ud) -> update_details (ud, storage)
| Skip(s) -> skip_ (unit, storage)
end;

View File

@ -0,0 +1,248 @@
/* (*_*
name: ID Contract (ReasonLIGO)
language: reasonligo
compile:
entrypoint: main
dryRun:
entrypoint: main
parameters: |
Buy (
{
profile: 0x0501000000026869,
initial_controller: Some(("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address))
}
)
storage: |
{
identities:Big_map.literal([
(1,
{owner:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address),
controller:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address), profile:0x0501000000026869}
)
]),
next_id:2,
name_price:0tez,
skip_price:333mutez
}
deploy:
entrypoint: main
storage: |
{
identities:Big_map.literal([
(1,
{owner:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address), controller:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address), profile:0x0501000000026869}
)
]),
next_id:2,
name_price:10tez,
skip_price:333mutez
}
evaluateValue:
entrypoint: ""
evaluateFunction:
entrypoint: buy
parameters: |
(
{
profile: 0x0501000000026869,
initial_controller: Some(("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address))
},
{
identities:Big_map.literal([
(1,
{owner:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address),
controller:("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address),
profile:0x0501000000026869}
)
]),
next_id:2,
name_price:0tez,
skip_price:333mutez
}
)
*_*) */
type id = int
type id_details = {
owner: address,
controller: address,
profile: bytes,
}
type buy = {
profile: bytes,
initial_controller: option(address),
}
type update_owner = {
id: id,
new_owner: address,
}
type update_details = {
id: id,
new_profile: option(bytes),
new_controller: option(address),
}
type action =
| Buy(buy)
| Update_owner(update_owner)
| Update_details(update_details)
| Skip(unit)
/* The prices kept in storage can be changed by bakers, though they should only be
adjusted down over time, not up. */
type storage = {
identities: big_map (id, id_details),
next_id: int,
name_price: tez,
skip_price: tez,
}
/** Preliminary thoughts on ids:
I very much like the simplicity of http://gurno.com/adam/mne/.
5 three letter words means you have a 15 character identity, not actually more
annoying than an IP address and a lot more memorable than the raw digits. This
can be stored as a single integer which is then translated into the corresponding
series of 5 words.
I in general like the idea of having a 'skip' mechanism, but it does need to cost
something so people don't eat up the address space. 256 ^ 5 means you have a lot
of address space, but if people troll by skipping a lot that could be eaten up.
Should probably do some napkin calculations for how expensive skipping needs to
be to deter people from doing it just to chew up address space.
*/
let buy = ((parameter, storage): (buy, storage)) : (list(operation), storage) => {
let void: unit =
if (amount == storage.name_price) { (); }
else { failwith("Incorrect amount paid."); };
let profile = parameter.profile;
let initial_controller = parameter.initial_controller;
let identities = storage.identities;
let new_id = storage.next_id;
let controller: address =
switch (initial_controller) {
| Some(addr) => addr
| None => sender
};
let new_id_details: id_details = {
owner : sender,
controller : controller,
profile : profile,
};
let updated_identities: big_map (id, id_details) =
Big_map.update(new_id, Some(new_id_details), identities);
(([]: list(operation)), {
identities : updated_identities,
next_id : new_id + 1,
name_price : storage.name_price,
skip_price : storage.skip_price,
});
};
let update_owner = ((parameter, storage): (update_owner, storage)) : (list(operation), storage) => {
let void: unit =
if (amount != 0mutez) {
failwith("Updating owner doesn't cost anything.");
}
else { (); };
let id : int = parameter.id;
let new_owner = parameter.new_owner;
let identities = storage.identities;
let current_id_details: id_details =
switch (Big_map.find_opt(id, identities)) {
| Some(id_details) => id_details
| None => (failwith("This ID does not exist."): id_details)
};
let is_allowed: bool =
if (sender == current_id_details.owner) { true; }
else { (failwith("You are not the owner of this ID."): bool); };
let updated_id_details: id_details = {
owner : new_owner,
controller : current_id_details.controller,
profile : current_id_details.profile,
};
let updated_identities = Big_map.update(id, (Some updated_id_details), identities);
(([]: list(operation)), {
identities : updated_identities,
next_id : storage.next_id,
name_price : storage.name_price,
skip_price : storage.skip_price,
});
};
let update_details = ((parameter, storage): (update_details, storage)) :
(list(operation), storage) => {
let void : unit =
if (amount != 0mutez) {
failwith("Updating details doesn't cost anything.");
}
else { (); };
let id = parameter.id;
let new_profile = parameter.new_profile;
let new_controller = parameter.new_controller;
let identities = storage.identities;
let current_id_details: id_details =
switch (Big_map.find_opt(id, identities)) {
| Some(id_details) => id_details
| None => (failwith("This ID does not exist."): id_details)
};
let is_allowed: bool =
if ((sender != current_id_details.controller) &&
(sender != current_id_details.owner)) {
(failwith ("You are not the owner or controller of this ID."): bool)
}
else { true; };
let owner: address = current_id_details.owner;
let profile: bytes =
switch (new_profile) {
| None => /* Default */ current_id_details.profile
| Some(new_profile) => new_profile
};
let controller: address =
switch (new_controller) {
| None => /* Default */ current_id_details.controller
| Some new_controller => new_controller
};
let updated_id_details: id_details = {
owner : owner,
controller : controller,
profile : profile,
};
let updated_identities: big_map (id, id_details) =
Big_map.update(id, (Some updated_id_details), identities);
(([]: list(operation)), {
identities : updated_identities,
next_id : storage.next_id,
name_price : storage.name_price,
skip_price : storage.skip_price,
});
};
/* Let someone skip the next identity so nobody has to take one that's undesirable */
let skip = ((p,storage): (unit, storage)) => {
let void : unit =
if (amount != storage.skip_price) {
failwith("Incorrect amount paid.");
}
else { (); };
(([]: list(operation)), {
identities : storage.identities,
next_id : storage.next_id + 1,
name_price : storage.name_price,
skip_price : storage.skip_price,
});
};
let main = ((action, storage): (action, storage)) : (list(operation), storage) => {
switch (action) {
| Buy(b) => buy((b, storage))
| Update_owner(uo) => update_owner((uo, storage))
| Update_details ud => update_details((ud, storage))
| Skip s => skip(((), storage))
};
};

View File

@ -40,9 +40,10 @@ let buy_id () =
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1)]) ;
e_int 1;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
@ -54,11 +55,15 @@ let buy_id () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let param = e_pair owner_website (e_some (e_address new_addr)) in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr))) ;
] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options (program, state) "buy"
(e_pair param storage)
@ -73,9 +78,10 @@ let buy_id_sender_addr () =
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1)]) ;
e_int 1;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
@ -87,11 +93,14 @@ let buy_id_sender_addr () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let param = e_pair owner_website (e_typed_none (t_address ())) in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_typed_none (t_address ())))] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options (program, state) "buy"
(e_pair param storage)
@ -107,16 +116,18 @@ let buy_id_wrong_amount () =
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1)]) ;
e_int 1;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~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 param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr)))] in
let%bind () = expect_string_failwith ~options (program, state) "buy"
(e_pair param storage)
"Incorrect amount paid."
@ -144,20 +155,24 @@ let update_details_owner () =
let id_details_2_diff = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)] in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_tuple [e_int 1 ;
e_some details ;
e_some (e_address new_addr)] in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address new_addr))] in
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) new_storage)
@ -185,20 +200,24 @@ let update_details_controller () =
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address owner_addr) ;
("profile", new_website)] in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_tuple [e_int 1 ;
e_some details ;
e_some (e_address owner_addr)] in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) new_storage)
@ -224,15 +243,17 @@ let update_details_nonexistent () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_tuple [e_int 2 ;
e_some details ;
e_some (e_address owner_addr)] in
let param = e_record_ez [("id", e_int 2) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options (program, state) "update_details"
(e_pair param storage)
"This ID does not exist."
@ -257,15 +278,17 @@ let update_details_wrong_addr () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_tuple [e_int 0 ;
e_some details ;
e_some (e_address owner_addr)] in
let param = e_record_ez [("id", e_int 0) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options (program, state) "update_details"
(e_pair param storage)
"You are not the owner or controller of this ID."
@ -291,14 +314,16 @@ let update_details_unchanged () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_tuple [e_int 1 ;
e_typed_none (t_bytes ()) ;
e_typed_none (t_address ())] in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_typed_none (t_bytes ())) ;
("new_controller", e_typed_none (t_address ()))] in
let%bind () = expect_eq ~options (program, state) "update_details"
(e_pair param storage)
(e_pair (e_list []) storage)
@ -326,17 +351,22 @@ let update_owner () =
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)] in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_pair (e_int 1) (e_address owner_addr) in
let param = e_record_ez [("id", e_int 1) ;
("new_owner", e_address owner_addr)] in
let%bind () = expect_eq ~options (program, state) "update_owner"
(e_pair param storage)
(e_pair (e_list []) new_storage)
@ -362,12 +392,15 @@ let update_owner_nonexistent () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_pair (e_int 2) (e_address new_addr) in
let param = e_record_ez [("id", e_int 2);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options (program, state) "update_owner"
(e_pair param storage)
"This ID does not exist."
@ -393,12 +426,15 @@ let update_owner_wrong_addr () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_pair (e_int 0) (e_address new_addr) in
let param = e_record_ez [("id", e_int 0);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options (program, state) "update_owner"
(e_pair param storage)
"You are not the owner of this ID."
@ -422,15 +458,19 @@ let skip () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 3;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 3) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options (program, state) "skip"
(e_pair (e_unit ()) storage)
@ -456,17 +496,19 @@ let skip_wrong_amount () =
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_tuple [(e_big_map [(e_int 0, id_details_1) ;
(e_int 1, id_details_2)]) ;
e_int 2;
e_tuple [e_mutez 1000000 ; e_mutez 1000000]]
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_string_failwith ~options (program, state) "skip"
(e_pair (e_unit ()) storage)
"Incorrect amount paid."
in ok ()
let main = test_suite "ID Layer" [
let main = test_suite "ID Layer (CameLIGO)" [
test "buy" buy_id ;
test "buy (sender addr)" buy_id_sender_addr ;
test "buy (wrong amount)" buy_id_wrong_amount ;

522
src/test/id_tests_p.ml Normal file
View File

@ -0,0 +1,522 @@
open Trace
open Test_helpers
open Ast_imperative
let type_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "pascaligo" (Contract "main") in
ok (typed,state)
let get_program =
let s = ref None in
fun () -> match !s with
| Some s -> ok s
| None -> (
let%bind program = type_file "./contracts/id.ligo" in
s := Some program ;
ok program
)
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 (_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
ok ()
let (first_owner , first_contract) =
let open Proto_alpha_utils.Memory_proto_alpha in
let id = List.nth dummy_environment.identities 0 in
let kt = id.implicit_contract in
Protocol.Alpha_context.Contract.to_b58check kt , kt
let buy_id () =
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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", owner_website)]
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr))) ;
] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", owner_website)]
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_typed_none (t_address ())))] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr)))] in
let%bind () = expect_string_failwith ~options program "buy"
(e_pair param storage)
"Incorrect amount paid."
in ok ()
let update_details_owner () =
let%bind program = 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", owner_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = owner_website in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address new_addr))] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = owner_website in
let id_details_2 = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address owner_addr) ;
("profile", new_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 2) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 0) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_typed_none (t_bytes ())) ;
("new_controller", e_typed_none (t_address ()))] in
let%bind () = expect_eq ~options program "update_details"
(e_pair param storage)
(e_pair (e_list []) storage)
in ok ()
let update_owner () =
let%bind program = 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 1) ;
("new_owner", e_address owner_addr)] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 2);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 0);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 3) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_string_failwith ~options program "skip_"
(e_pair (e_unit ()) storage)
"Incorrect amount paid."
in ok ()
let main = test_suite "ID Layer (PascaLIGO)" [
test "buy" buy_id ;
test "buy (sender addr)" buy_id_sender_addr ;
test "buy (wrong amount)" buy_id_wrong_amount ;
test "update_details (owner)" update_details_owner ;
test "update_details (controller)" update_details_controller ;
test "update_details_nonexistent" update_details_nonexistent ;
test "update_details_wrong_addr" update_details_wrong_addr ;
test "update_details_unchanged" update_details_unchanged ;
test "update_owner" update_owner ;
test "update_owner_nonexistent" update_owner_nonexistent ;
test "update_owner_wrong_addr" update_owner_wrong_addr ;
test "skip" skip ;
test "skip (wrong amount)" skip_wrong_amount ;
]

525
src/test/id_tests_r.ml Normal file
View File

@ -0,0 +1,525 @@
open Trace
open Test_helpers
open Ast_imperative
let retype_file f =
let%bind typed,state = Ligo.Compile.Utils.type_file f "reasonligo" (Contract "main") in
ok (typed,state)
let get_program =
let s = ref None in
fun () -> match !s with
| Some s -> ok s
| None -> (
let%bind program = retype_file "./contracts/id.religo" in
s := Some program ;
ok program
)
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 (_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
ok ()
let (first_owner , first_contract) =
let open Proto_alpha_utils.Memory_proto_alpha in
let id = List.nth dummy_environment.identities 0 in
let kt = id.implicit_contract in
Protocol.Alpha_context.Contract.to_b58check kt , kt
let buy_id () =
let%bind program = 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr))) ;
] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_typed_none (t_address ())))] in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let storage = e_record_ez [("identities", (e_big_map [(e_int 0, id_details_1)])) ;
("next_id", e_int 1) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
in
let param = e_record_ez [("profile", owner_website) ;
("initial_controller", (e_some (e_address new_addr)))] in
let%bind () = expect_string_failwith ~options program "buy"
(e_pair param storage)
"Incorrect amount paid."
in ok ()
let update_details_owner () =
let%bind program = 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address owner_addr) ;
("profile", new_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address new_addr))] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address owner_addr) ;
("profile", new_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 2) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let details = e_bytes_string "ligolang.org" in
let param = e_record_ez [("id", e_int 0) ;
("new_profile", e_some details) ;
("new_controller", e_some (e_address owner_addr))] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 1) ;
("new_profile", e_typed_none (t_bytes ())) ;
("new_controller", e_typed_none (t_address ()))] in
let%bind () = expect_eq ~options program "update_details"
(e_pair param storage)
(e_pair (e_list []) storage)
in ok ()
let update_owner () =
let%bind program = 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let id_details_2_diff = e_record_ez [("owner", e_address owner_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)] in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2_diff)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 1) ;
("new_owner", e_address owner_addr)] in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 2);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.zero)
()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let param = e_record_ez [("id", e_int 0);
("new_owner", e_address new_addr)] in
let%bind () = expect_string_failwith ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.one) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let new_storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 3) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_eq ~options program "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 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) ;
("controller", e_address owner_addr) ;
("profile", owner_website)]
in
let new_addr = first_owner in
let options = Proto_alpha_utils.Memory_proto_alpha.make_options
~sender:first_contract
~amount:(Memory_proto_alpha.Protocol.Alpha_context.Tez.fifty_cents) ()
in
let new_website = e_bytes_string "ligolang.org" in
let id_details_2 = e_record_ez [("owner", e_address new_addr) ;
("controller", e_address new_addr) ;
("profile", new_website)]
in
let storage = e_record_ez [("identities", (e_big_map
[(e_int 0, id_details_1) ;
(e_int 1, id_details_2)])) ;
("next_id", e_int 2) ;
("name_price", e_mutez 1000000) ;
("skip_price", e_mutez 1000000) ; ]
in
let%bind () = expect_string_failwith ~options program "skip"
(e_pair (e_unit ()) storage)
"Incorrect amount paid."
in ok ()
let main = test_suite "ID Layer (ReasonLIGO)" [
test "buy" buy_id ;
test "buy (sender addr)" buy_id_sender_addr ;
test "buy (wrong amount)" buy_id_wrong_amount ;
test "update_details (owner)" update_details_owner ;
test "update_details (controller)" update_details_controller ;
test "update_details_nonexistent" update_details_nonexistent ;
test "update_details_wrong_addr" update_details_wrong_addr ;
test "update_details_unchanged" update_details_unchanged ;
test "update_owner" update_owner ;
test "update_owner_nonexistent" update_owner_nonexistent ;
test "update_owner_wrong_addr" update_owner_wrong_addr ;
test "skip" skip ;
test "skip (wrong amount)" skip_wrong_amount ;
]

View File

@ -11,6 +11,8 @@ let () =
Coase_tests.main ;
Vote_tests.main ;
Id_tests.main ;
Id_tests_p.main ;
Id_tests_r.main ;
Multisig_tests.main ;
Multisig_v2_tests.main ;
Replaceable_id_tests.main ;

View File

@ -4,12 +4,6 @@ const join = require('path').join;
const fs = require('fs');
const YAML = require('yamljs');
const CURATED_EXAMPLES = [
'cameligo/arithmetic-contract.ligo',
'pascaligo/arithmetic-contract.ligo',
'reasonligo/arithmetic-contract.ligo'
];
function urlFriendlyHash(content) {
const hash = createHash('md5');
hash.update(content);
@ -109,6 +103,15 @@ async function main() {
// const EXAMPLES_GLOB = '**/*.ligo';
// const files = await findFiles(EXAMPLES_GLOB, EXAMPLES_DIR);
const CURATED_EXAMPLES = [
'pascaligo/arithmetic-contract.ligo',
'cameligo/arithmetic-contract.ligo',
'reasonligo/arithmetic-contract.ligo',
'pascaligo/id.ligo',
'cameligo/id.mligo',
'reasonligo/id.religo',
];
const EXAMPLES_DEST_DIR = join(process.cwd(), 'build', 'static', 'examples');
fs.mkdirSync(EXAMPLES_DEST_DIR, { recursive: true });

View File

@ -33,9 +33,12 @@ export const DEFAULT_STATE: ExamplesState = {
if (process.env.NODE_ENV === 'development') {
DEFAULT_STATE.list = [
{ id: 'MzkMQ1oiVHJqbcfUuVFKTw', name: 'CameLIGO Contract' },
{ id: 'FEb62HL7onjg1424eUsGSg', name: 'PascaLIGO Contract' },
{ id: 'JPhSOehj_2MFwRIlml0ymQ', name: 'ReasonLIGO Contract' }
{ id: 'MzkMQ1oiVHJqbcfUuVFKTw', name: 'Increment Example CameLIGO ' },
{ id: 'FEb62HL7onjg1424eUsGSg', name: 'Increment Example PascaLIGO' },
{ id: 'JPhSOehj_2MFwRIlml0ymQ', name: 'Increment Example ReasonLIGO' },
{ id: 'ehDv-Xaf70mQoiPhQDTAUQ', name: 'ID Example CameLIGO' },
{ id: 'CpnK7TFuUjJiQTT8KiiGyQ', name: 'ID Example ReasonLIGO' },
{ id: 'yP-THvmURsaqHxpwCravWg', name: 'ID Example PascaLIGO' },
];
}

View File

@ -24,7 +24,7 @@ describe('Share', () => {
await responseCallback;
const actualShareLink = await page.evaluate(getInputValue, 'share-link');
const expectedShareLink = `${API_HOST}/p/WxKPBq9-mkZ_kq4cMHXfCQ`;
const expectedShareLink = `${API_HOST}/p/2GnQR0cUYeO7feAw71SJYQ`
expect(actualShareLink).toEqual(expectedShareLink);
done();