1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
open Mo_types
open Type
module Pretty = Type.MakePretty(Type.ElideStampsAndHashes)
let migration_link = "https://internetcomputer.org/docs/motoko/fundamentals/actors/compatibility#explicit-migration-using-a-migration-function"
(* Signature matching *)
let cat = "Compatibility"
(* signature matching with multiple error reporting
c.f. (simpler) Types.match_sig.
*)
let display_typ = Lib.Format.display Pretty.pp_typ
let display_typ_expand = Lib.Format.display Pretty.pp_typ_expand
let error_discard s tf =
Diag.add_msg s
(Diag.error_message Source.no_region "M0169" cat
(Format.asprintf "the stable variable `%s` of the previous version cannot be implicitly discarded. The variable can only be dropped by an explicit migration function, please see %s"
tf.lab
migration_link))
let error_sub s tf1 tf2 explanation =
Diag.add_msg s
(Diag.error_message Source.no_region "M0170" cat
(Format.asprintf "the new type of stable variable `%s` is not compatible with the previous version.\n The previous type%a\n is not a subtype of%a\n because: %s.\n Write an explicit migration function, please see %s."
tf1.lab
display_typ_expand tf1.typ
display_typ_expand tf2.typ
(Pretty.string_of_explanation explanation)
migration_link
))
let error_stable_sub s tf1 tf2 explanation =
Diag.add_msg s
(Diag.error_message Source.no_region "M0216" cat
(Format.asprintf "the new type of stable variable `%s` implicitly drops data of the previous version. \n The previous type%a\n is not a stable subtype of%a because: %s.\n The data can only be dropped by an explicit migration function, please see %s."
tf1.lab
display_typ_expand tf1.typ
display_typ_expand tf2.typ
(Pretty.string_of_explanation explanation)
migration_link))
let error_required s tf =
Diag.add_msg s
(Diag.error_message Source.no_region "M0169" cat
(Format.asprintf "the previous program version does not contain the stable variable %s. The migration function cannot require this variable as input, please see %s."
tf.lab
migration_link))
(*
- Mutability of stable fields can be changed because they are never aliased.
- Stable fields cannot be dropped.
- Lossy promotion to any or dropping record fields is rejected (stricter than subtyping to prevent data loss).
*)
let match_stab_sig sig1 sig2 : unit Diag.result =
let tfs1 = post sig1 in
let tfs2 = pre sig2 in
(* Assume that tfs1 and tfs2 are sorted. *)
let res = Diag.with_message_store (fun s ->
let rec go tfs1 tfs2 = match tfs1, tfs2 with
| [], _ ->
List.iter (fun (required, tf) ->
if required then error_required s tf) tfs2;
Some () (* new fields ok *)
| tf1 :: tfs1', [] ->
(* dropped field rejected, recurse on tfs1' *)
error_discard s tf1;
go tfs1' []
| tf1::tfs1', (is_required, tf2)::tfs2' ->
(match Type.compare_field tf1 tf2 with
| 0 ->
let context = [StableVariable tf2.lab] in
begin
match Type.sub_explained context (as_immut tf1.typ) (as_immut tf2.typ) with
| Incompatible explanation -> error_sub s tf1 tf2 explanation
| Compatible ->
match Type.stable_sub_explained context (as_immut tf1.typ) (as_immut tf2.typ) with
| Incompatible explanation -> error_stable_sub s tf1 tf2 explanation
| Compatible -> ()
end;
go tfs1' tfs2'
| -1 ->
(* dropped field rejected, recurse on tfs1' *)
error_discard s tf1;
go tfs1' tfs2
| _ ->
(if is_required then error_required s tf2);
go tfs1 tfs2' (* new field ok, recurse on tfs2' *)
)
in go tfs1 tfs2)
in
(* cross check with simpler definition *)
match res with
| Ok _ ->
assert (Type.match_stab_sig sig1 sig2);
res
| Error _ ->
assert (not (Type.match_stab_sig sig1 sig2));
res