forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
panScopeScript.sml
114 lines (103 loc) · 4.17 KB
/
panScopeScript.sml
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
(*
Scope checking for Pancake.
*)
open preamble panLangTheory;
val _ = new_theory "panScope";
Datatype:
context = <| vars : varname list ;
funcs : funname list ;
fname : funname |>
End
Definition scope_check_exp_def:
scope_check_exp ctxt (Const c) = NONE ∧
scope_check_exp ctxt (Var vname) =
(if ¬MEM vname ctxt.vars then SOME (vname, ctxt.fname) else NONE) ∧
scope_check_exp ctxt (Label fname) =
(if ¬MEM fname ctxt.funcs then SOME (fname, ctxt.fname) else NONE) ∧
scope_check_exp ctxt (Struct es) =
scope_check_exps ctxt es ∧
scope_check_exp ctxt (Field index e) = scope_check_exp ctxt e ∧
scope_check_exp ctxt (Load shape e) = scope_check_exp ctxt e ∧
scope_check_exp ctxt (LoadByte e) = scope_check_exp ctxt e ∧
scope_check_exp ctxt (Op bop es) = scope_check_exps ctxt es ∧
scope_check_exp ctxt (Panop pop es) = scope_check_exps ctxt es ∧
scope_check_exp ctxt (Cmp cmp e1 e2) =
OPTION_CHOICE
(scope_check_exp ctxt e1)
(scope_check_exp ctxt e2) ∧
scope_check_exp ctxt (Shift sh e n) = scope_check_exp ctxt e ∧
scope_check_exp ctxt BaseAddr = NONE ∧
scope_check_exps ctxt [] = NONE ∧
scope_check_exps ctxt (e::es) =
OPTION_CHOICE (scope_check_exp ctxt e) (scope_check_exps ctxt es)
End
Definition scope_check_prog_def:
scope_check_prog ctxt Skip = NONE ∧
scope_check_prog ctxt (Dec v e p) =
OPTION_CHOICE (scope_check_exp ctxt e)
(scope_check_prog (ctxt with vars := v :: ctxt.vars) p) ∧
scope_check_prog ctxt (Assign v e) =
(if ¬MEM v ctxt.vars
then SOME (v, ctxt.fname)
else scope_check_exp ctxt e) ∧
scope_check_prog ctxt (Store ad v) =
OPTION_CHOICE (scope_check_exp ctxt ad)
(scope_check_exp ctxt v) ∧
scope_check_prog ctxt (StoreByte dest src) =
OPTION_CHOICE (scope_check_exp ctxt dest)
(scope_check_exp ctxt src) ∧
scope_check_prog ctxt (Seq p1 p2) =
OPTION_CHOICE (scope_check_prog ctxt p1)
(scope_check_prog ctxt p2) ∧
scope_check_prog ctxt (If e p1 p2) =
OPTION_CHOICE (scope_check_exp ctxt e)
(OPTION_CHOICE (scope_check_prog ctxt p1)
(scope_check_prog ctxt p2)) ∧
scope_check_prog ctxt (While e p) =
OPTION_CHOICE (scope_check_exp ctxt e)
(scope_check_prog ctxt p) ∧
scope_check_prog ctxt Break = NONE ∧
scope_check_prog ctxt Continue = NONE ∧
scope_check_prog ctxt (TailCall trgt args) =
OPTION_CHOICE
(scope_check_exp ctxt trgt)
(scope_check_exps ctxt args) ∧
scope_check_prog ctxt (RetCall rt hdl trgt args) =
OPTION_CHOICE
(scope_check_exp ctxt trgt)
(OPTION_CHOICE
(scope_check_exps ctxt args)
(if ¬MEM rt ctxt.vars
then SOME (rt, ctxt.fname)
else
case hdl of
NONE => NONE
| SOME (eid, evar, p) =>
if ¬MEM evar ctxt.vars
then SOME (evar, ctxt.fname)
else scope_check_prog (ctxt with vars := evar :: ctxt.vars) p)) ∧
scope_check_prog ctxt (ExtCall fname ptr1 len1 ptr2 len2) =
scope_check_exps ctxt [ptr1;len1;ptr2;len2] ∧
scope_check_prog ctxt (Raise eid excp) = scope_check_exp ctxt excp ∧
scope_check_prog ctxt (Return rt) = scope_check_exp ctxt rt ∧
scope_check_prog ctxt (ShMem mop v e) =
(if ¬MEM v ctxt.vars
then SOME (v, ctxt.fname)
else scope_check_exp ctxt e) ∧
scope_check_prog ctxt Tick = NONE
End
Definition scope_check_funs_def:
scope_check_funs fnames [] = NONE ∧
scope_check_funs fnames ((fname, _, body)::funs) =
let ctxt = <| vars := [] ; funcs := fnames ; fname := fname |> in
OPTION_CHOICE (scope_check_prog ctxt body)
(scope_check_funs fnames funs)
End
(* The scope checker returns NONE to indicate that there is no scope error, and
SOME (name, fname) to indicate that name is not in scope in an expression
within the function fname. The first component name may be the name of a
variable or a function. *)
Definition scope_check_def:
scope_check funs = scope_check_funs (MAP FST funs) funs
End
val _ = export_theory ();