cakeml/compiler/scheme/scheme_astScript.sml at master · CakeML/cakeml · GitHub

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
132
133
134
135
136
137
(*
  AST of Scheme
*)
Theory scheme_ast
Ancestors
  mlstring
Libs
  preamble

Type senv = “:(mlstring |-> num)”
Type loc = “:num”

(* This needs completing: Var, Lit, ... *)
Datatype:
  prim = SAdd | SMul | SMinus | SEqv | CallCC
       | Cons | Car | Cdr | IsNull | IsPair
End

Datatype:
  lit = LitPrim prim | LitNum int | LitBool bool | LitNull
End

Datatype:
  exp = (*Print mlstring
      |*) Apply exp (exp list)
      | Lit lit
      | Cond exp exp exp
      | Ident mlstring
      | Lambda (mlstring list) (mlstring option) exp
      | Begin (exp list) exp
      | Set mlstring exp
      | Letrec ((mlstring # exp) list) exp
      | Letrecstar ((mlstring # exp) list) exp
End

Datatype:
  (*Contexts for small-step operational semantics*)
  cont = ApplyK ((val # val list) option) (exp list)
       | CondK exp exp
       | BeginK (exp list) exp
       | SetK mlstring
       | LetinitK ((mlstring # val) list) mlstring ((mlstring # exp) list) exp
;
  val = Prim prim | SNum int | Wrong string | SBool bool
      | Proc senv (mlstring list) (mlstring option) exp
      (*requires HOL 94eb753a85c5628f4fd0401deb4b7e2972a8eb25*)
      | Throw ((senv # cont) list)
      | PairP loc
      | Null
End

Definition lit_to_val_def:
  lit_to_val (LitPrim p) = Prim p ∧
  lit_to_val (LitNum n) = SNum n ∧
  lit_to_val (LitBool b) = SBool b ∧
  lit_to_val (LitNull) = Null
End

Definition static_scope_def:
  static_scope env (Lit lit) = T ∧

  static_scope env (Cond c t f) = (
  static_scope env c ∧
  static_scope env t ∧
  static_scope env f) ∧

  static_scope env (Apply fn es) = (
  static_scope env fn ∧
  static_scope_list env es) ∧

  static_scope env (Begin es e) = (
  static_scope_list env es ∧
  static_scope env e) ∧

  static_scope env (Lambda xs NONE e) = (
  ALL_DISTINCT xs ∧
  static_scope (env ∪ set xs) e) ∧

  static_scope env (Lambda xs (SOME x) e) = (
  ALL_DISTINCT (x::xs) ∧
  static_scope (env ∪ set (x::xs)) e) ∧

  static_scope env (Letrec bs e) = (
  ALL_DISTINCT (MAP FST bs) ∧
  static_scope_list (env ∪ set (MAP FST bs)) (MAP SND bs) ∧
  static_scope (env ∪ set (MAP FST bs)) e) ∧

  static_scope env (Letrecstar bs e) = (
  ALL_DISTINCT (MAP FST bs) ∧
  static_scope_list (env ∪ set (MAP FST bs)) (MAP SND bs) ∧
  static_scope (env ∪ set (MAP FST bs)) e) ∧

  static_scope env (Ident x) = env x ∧

  static_scope env (Set x e) = (
  env x ∧
  static_scope env e) ∧

  (static_scope_list env [] = T) ∧
  static_scope_list env (e::es) = (static_scope env e ∧ static_scope_list env es)
Termination
  WF_REL_TAC ‘measure (λ x . case x of
    | INL(_,e) => exp_size e
    | INR(_,es) => list_size exp_size es)’
  >> conj_tac
  >> Induct_on ‘bs’
  >> gvs[list_size_def, fetch "-" "exp_size_def"]
  >> PairCases
  >> strip_tac
  >> gvs[list_size_def, fetch "-" "exp_size_def"]
  >> pop_assum $ qspec_then ‘e’ assume_tac
  >> gvs[list_size_def, fetch "-" "exp_size_def"]
End

Theorem static_scope_mono_all:
    (∀ env' e env . env ⊆ env' ∧ static_scope env e ⇒ static_scope env' e) ∧
    (∀ env' es env . env ⊆ env' ∧ static_scope_list env es ⇒ static_scope_list env' es)
Proof
  ho_match_mp_tac static_scope_ind
  >> rpt strip_tac
  >> simp[Once static_scope_def]
  >> gvs[Once static_scope_def]
  >> rpt (last_x_assum $ drule_at_then (Pos last) assume_tac)
  >> simp[]
  >> gvs[SUBSET_DEF, SPECIFICATION]
QED

Theorem static_scope_mono = cj 1 static_scope_mono_all;

Theorem every_static_scope[simp]:
  ∀ env . static_scope_list env = EVERY (static_scope env)
Proof
  gen_tac
  >> irule EQ_EXT
  >> Induct
  >> simp[static_scope_def]
QED