cakeml/semantics/tokenUtilsScript.sml at master · ncough/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
138
139
open preamble tokensTheory

val _ = new_theory "tokenUtils"
val _ = set_grammar_ancestry ["tokens", "grammar"]

(* ----------------------------------------------------------------------
    Utility functions over tokens; perhaps should just appear in
    TokensTheory
   ---------------------------------------------------------------------- *)

val isInt_def = Define`
  isInt (IntT i) = T ∧
  isInt _ = F
`;
val _ = export_rewrites ["isInt_def"]

val isString_def = Define`
  isString (StringT _) = T ∧
  isString _ = F
`;
val _ = export_rewrites ["isString_def"]

val isAlphaT_def = Define`
  isAlphaT (AlphaT s) = T ∧
  isAlphaT _ = F
`;
val _ = export_rewrites ["isAlphaT_def"]

val isSymbolT_def = Define`isSymbolT (SymbolT s) = T ∧ isSymbolT _ = F`
val _ = export_rewrites ["isSymbolT_def"]

val isAlphaSym_def = Define`
  isAlphaSym (AlphaT _) = T ∧
  isAlphaSym (SymbolT _) = T ∧
  isAlphaSym _ = F
`;
val _ = export_rewrites ["isAlphaSym_def"]

val isTyvarT_def = Define`isTyvarT (TyvarT _) = T ∧ isTyvarT _ = F`
val _ = export_rewrites ["isTyvarT_def"]

val isWhitespaceT_def = Define`
  (isWhitespaceT (WhitespaceT _) ⇔ T) ∧
  (isWhitespaceT _ ⇔ F)
`

val isCharT_def = Define`
  (isCharT (CharT _) ⇔ T) ∧
  (isCharT _ ⇔ F)
`;
val _ = export_rewrites ["isCharT_def"]

val isWordT_def = Define`
  (isWordT (WordT _) ⇔ T) ∧
  (isWordT _ ⇔ F)
`;
val _ = export_rewrites ["isWordT_def"]

val isLongidT_def = Define`
  (isLongidT (LongidT _ _) ⇔ T) ∧
  (isLongidT _ ⇔ F)
`
val _ = export_rewrites ["isLongidT_def"]

val destLongidT_def = Define`
  (destLongidT (LongidT str s) = SOME (str,s)) ∧
  (destLongidT _ = NONE)
`
val _ = export_rewrites ["destLongidT_def"]

val destLongidT_EQ_SOME = Q.store_thm(
  "destLongidT_EQ_SOME[simp]",
  `destLongidT t = SOME strs ⇔ ∃str s. t = LongidT str s ∧ strs = (str, s)`,
  Cases_on `t` >> simp[] >> metis_tac[]);

val destTyvarPT_def = Define`
  (destTyvarPT (Lf (TOK (TyvarT s),_)) = SOME s) ∧
  (destTyvarPT _ = NONE)
`;
val _ = export_rewrites ["destTyvarPT_def"]

val destLf_def = Define`(destLf (Lf (x,_)) = SOME x) ∧ (destLf _ = NONE)`;
val _ = export_rewrites ["destLf_def"]

val destTOK_def = Define`(destTOK (TOK t) = SOME t) ∧ (destTOK _ = NONE)`;
val _ = export_rewrites ["destTOK_def"]

val destAlphaT_def = Define`
  (destAlphaT (AlphaT s) = SOME s) ∧ (destAlphaT _ = NONE)
`;
val _ = export_rewrites ["destAlphaT_def"]

val destAlphaT_EQ_SOME = Q.store_thm(
  "destAlphaT_EQ_SOME[simp]",
  `destAlphaT t = SOME s ⇔ t = AlphaT s`,
  Cases_on `t` >> simp[]);

val destSymbolT_def = Define`
  (destSymbolT (SymbolT s) = SOME s) ∧
  (destSymbolT _ = NONE)
`;
val _ = export_rewrites ["destSymbolT_def"]

val destSymbolT_EQ_SOME = Q.store_thm(
  "destSymbolT_EQ_SOME[simp]",
  `destSymbolT t = SOME s ⇔ t = SymbolT s`,
  Cases_on `t` >> simp[]);

val destIntT_def = Define`
  (destIntT (IntT i) = SOME i) ∧
  (destIntT _ = NONE)
`;
val _ = export_rewrites ["destIntT_def"]

val destCharT_def = Define`
  (destCharT (CharT c) = SOME c) ∧
  (destCharT _ = NONE)
`;
val _ = export_rewrites ["destCharT_def"]

val destStringT_def = Define`
  (destStringT (StringT s) = SOME s) ∧
  (destStringT _ = NONE)
`;
val _ = export_rewrites ["destStringT_def"]

val destWordT_def = Define`
  (destWordT (WordT w) = SOME w) ∧
  (destWordT _ = NONE)
`;
val _ = export_rewrites ["destWordT_def"]

val destFFIT_def = Define`
  (destFFIT (FFIT s) = SOME s) ∧
  (destFFIT _ = NONE)
`;
val _ = export_rewrites ["destFFIT_def"]

val _ = export_theory()