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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
(*
This module implements the staticity check, needed for modules and imported
files.
The guiding principle is: Static expressions are expressions that can be
compiled to values without evaluation.
There is some mushiness around let-expressions and variables, which do form
some kind of beta-reduction, and can actually cause loops, but are required to
allow re-exporting names in modules.
*)
open Mo_def
open Source
open Syntax
let err m at =
let open Diag in
add_msg m
(error_message
at
"M0014"
"type"
"non-static expression in library, module or migration expression")
let pat_err m at =
let open Diag in
add_msg m
(error_message
at
"M0015"
"type"
"only trivial patterns allowed in static expressions")
let rec exp m e = match e.it with
(* Plain values *)
| (PrimE _ | LitE _ | ActorUrlE _ | FuncE _) -> ()
| (TagE (_, exp1) | OptE exp1) -> exp m exp1
| TupE es -> List.iter (exp m) es
| ArrayE (mut, es) ->
begin
match mut.it with
| Const -> List.iter (exp m) es
| Var -> err m e.at
end
| ObjBlockE (eo, _, _, dfs) ->
Option.iter (exp m) eo; dec_fields m dfs
| ObjE (bases, efs) ->
List.iter (exp m) bases; exp_fields m efs
(* Variable access. Dangerous, due to loops. *)
| (VarE _ | ImportE _) -> ()
(* Projections. These are a form of evaluation. *)
| ProjE (exp1, _)
| DotE (exp1, _) -> exp m exp1
| IdxE (exp1, exp2) -> err m e.at
(* Transparent *)
| AnnotE (exp1, _) | IgnoreE exp1 | DoOptE exp1 -> exp m exp1
| BlockE ds -> List.iter (dec m) ds
(* Clearly non-static *)
| UnE _
| ShowE _
| ToCandidE _
| FromCandidE _
| NotE _
| AssertE _
| LabelE _
| BreakE _
| RetE _
| AsyncE _ (* TBR - Cmp could be static *)
| AwaitE _
| LoopE _
| BinE _
| RelE _
| AssignE _
| CallE _
| AndE _
| OrE _
| WhileE _
| ForE _
| DebugE _
| IfE _
| SwitchE _
| ThrowE _
| TryE _
| BangE _
| ImpliesE _
| OldE _
-> err m e.at
and dec_fields m dfs = List.iter (fun df -> dec m df.it.dec) dfs
and exp_fields m efs = List.iter (fun (ef : exp_field) ->
if ef.it.mut.it = Var then err m ef.at;
exp m ef.it.exp) efs
and dec m d = match d.it with
| TypD _ | ClassD _ -> ()
| ExpD e -> exp m e
| LetD (p, e, fail) -> pat m p; exp m e; Option.iter (exp m) fail
| VarD _ -> err m d.at
and pat m p = match p.it with
| (WildP | VarP _) -> ()
(*
If we allow projections above, then we should allow irrefutable
patterns here.
*)
| TupP ps -> List.iter (pat m) ps
| ObjP fs -> List.iter (pat_field m) fs
(* TODO:
claudio: what about singleton variant patterns? These are irrefutable too.
Andreas suggests simply allowing all patterns: "The worst that can happen is that the program
is immediately terminated, but that doesn't break anything semantically."
*)
(* Everything else is forbidden *)
| _ -> pat_err m p.at
and pat_field m pf = match pf.it with
| ValPF(_, p) -> pat m p
| TypPF(_) -> ()
let prog p =
Diag.with_message_store (fun m -> List.iter (dec m) p.it; Some ())