Skip to content

Commit 65e1919

Browse files
myreenmyreen
authored
Merge pull request #1061 from CakeML/remove-tDefine-paren-matching
2 parents 3605d6f + dfbdb67 commit 65e1919

File tree

82 files changed

+1020
-690
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+1020
-690
lines changed

‎basis/pure/mlintScript.sml

+10-6
Original file line numberDiff line numberDiff line change
@@ -174,28 +174,32 @@ Proof
174174
, EVERY_EL]
175175
QED
176176

177-
val fromChars_unsafe_def = tDefine "fromChars_unsafe" `
177+
Definition fromChars_unsafe_def:
178178
fromChars_unsafe 0 str = 0n ∧ (* Shouldn't happend *)
179179
fromChars_unsafe n str =
180180
if n ≤ padLen_DEC
181181
then fromChars_range_unsafe 0 n str
182182
else let n' = n - padLen_DEC;
183183
front = fromChars_unsafe n' str * maxSmall_DEC;
184184
back = fromChars_range_unsafe n' padLen_DEC str
185-
in front + back`
186-
(wf_rel_tac `measure FST` \\ rw [padLen_DEC_eq]);
185+
in front + back
186+
Termination
187+
wf_rel_tac `measure FST` \\ rw [padLen_DEC_eq]
188+
End
187189
val fromChars_unsafe_ind = theorem"fromChars_unsafe_ind"
188190

189-
val fromChars_def = tDefine "fromChars" `
191+
Definition fromChars_def:
190192
fromChars 0 str = NONE ∧ (* Shouldn't happend *)
191193
fromChars n str =
192194
if n ≤ padLen_DEC
193195
then fromChars_range 0 n str
194196
else let n' = n - padLen_DEC;
195197
front = OPTION_MAP ($* maxSmall_DEC) (fromChars n' str);
196198
back = fromChars_range n' padLen_DEC str
197-
in OPTION_MAP2 $+ front back`
198-
(wf_rel_tac `measure FST` \\ rw [padLen_DEC_eq]);
199+
in OPTION_MAP2 $+ front back
200+
Termination
201+
wf_rel_tac `measure FST` \\ rw [padLen_DEC_eq]
202+
End
199203
val fromChars_ind = theorem"fromChars_ind"
200204

201205
Theorem fromChars_eq_unsafe:

‎basis/pure/mlstringScript.sml

+11-7
Original file line numberDiff line numberDiff line change
@@ -233,12 +233,14 @@ Proof
233233
rw[strcat_thm]
234234
QED
235235

236-
val concatWith_aux_def = tDefine "concatWith_aux"`
236+
Definition concatWith_aux_def:
237237
(concatWith_aux s [] bool = implode []) /\
238238
(concatWith_aux s (h::t) T = strcat h (concatWith_aux s t F)) /\
239-
(concatWith_aux s (h::t) F = strcat s (concatWith_aux s (h::t) T))`
240-
(wf_rel_tac `inv_image ($< LEX $<) (\(s,l,b). (LENGTH l, if b then 0n else 1))` \\
241-
rw[]);
239+
(concatWith_aux s (h::t) F = strcat s (concatWith_aux s (h::t) T))
240+
Termination
241+
wf_rel_tac `inv_image ($< LEX $<) (\(s,l,b). (LENGTH l, if b then 0n else 1))` \\
242+
rw[]
243+
End
242244

243245
Definition concatWith_def:
244246
concatWith s l = concatWith_aux s l T
@@ -296,12 +298,14 @@ Proof
296298
rw [translate_def, translate_aux_thm]
297299
QED
298300

299-
val splitl_aux_def = tDefine"splitl_aux"`
301+
Definition splitl_aux_def:
300302
splitl_aux P s i =
301303
if i < strlen s ∧ P (strsub s i) then
302304
splitl_aux P s (i+1)
303-
else (extract s 0 (SOME i), extract s i NONE)`
304-
(WF_REL_TAC`inv_image $< (λ(x,s,i). strlen s - i)`);
305+
else (extract s 0 (SOME i), extract s i NONE)
306+
Termination
307+
WF_REL_TAC`inv_image $< (λ(x,s,i). strlen s - i)`
308+
End
305309

306310
val splitl_aux_ind = theorem"splitl_aux_ind";
307311

‎basis/pure/mlvectorScript.sml

+5-3
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,14 @@ Definition tabulate_def:
1818
tabulate n f = Vector (GENLIST f n)
1919
End
2020

21-
val toList_aux_def = tDefine "toList_aux"`
21+
Definition toList_aux_def:
2222
toList_aux vec n =
2323
if length(vec) <= n
2424
then []
25-
else sub vec n::toList_aux vec (n + 1)`
26-
(wf_rel_tac `measure (\(vec, n). length(vec) - n)`)
25+
else sub vec n::toList_aux vec (n + 1)
26+
Termination
27+
wf_rel_tac `measure (\(vec, n). length(vec) - n)`
28+
End
2729

2830
val toList_aux_ind = theorem"toList_aux_ind";
2931

‎candle/overloading/ml_kernel/ml_hol_kernel_funsProgScript.sml

+6-4
Original file line numberDiff line numberDiff line change
@@ -307,7 +307,7 @@ val res = translate concl_def;
307307

308308
val _ = ml_prog_update open_local_block;
309309

310-
val type_compare_def = tDefine "type_compare" `
310+
Definition type_compare_def:
311311
(type_compare t1 t2 =
312312
case (t1,t2) of
313313
| (Tyvar x1,Tyvar x2) => mlstring$compare x1 x2
@@ -325,10 +325,12 @@ val type_compare_def = tDefine "type_compare" `
325325
| (t1::ts1,t2::ts2) =>
326326
(case type_compare t1 t2 of
327327
| Equal => type_list_compare ts1 ts2
328-
| other => other))`
329-
(WF_REL_TAC `measure (\x. case x of
328+
| other => other))
329+
Termination
330+
WF_REL_TAC `measure (\x. case x of
330331
INR (x,_) => type1_size x
331-
| INL (x,_) => type_size x)`)
332+
| INL (x,_) => type_size x)`
333+
End
332334

333335
val type_cmp_thm = Q.prove(
334336
`(type_cmp = type_compare) /\

‎candle/overloading/monadic/holKernelScript.sml

+18-12
Original file line numberDiff line numberDiff line change
@@ -247,15 +247,17 @@ End
247247
| (Tyvar v as tv) -> [tv]
248248
*)
249249

250-
val _ = tDefine "tyvars" `
250+
Definition tyvars_def:
251251
tyvars x =
252252
dtcase x of (Tyapp _ args) => itlist union (MAP tyvars args) []
253-
| (Tyvar tv) => [tv]`
254-
(WF_REL_TAC `measure (type_size)` THEN Induct_on `args`
253+
| (Tyvar tv) => [tv]
254+
Termination
255+
WF_REL_TAC `measure (type_size)` THEN Induct_on `args`
255256
THEN FULL_SIMP_TAC (srw_ss()) [type_size_def]
256257
THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN RES_TAC
257258
THEN REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN REPEAT STRIP_TAC
258-
THEN DECIDE_TAC);
259+
THEN DECIDE_TAC
260+
End
259261

260262
(*
261263
let rec type_subst i ty =
@@ -274,18 +276,20 @@ Definition rev_assocd_def:
274276
| ((x,y)::l) => if y = a then x else rev_assocd a l d
275277
End
276278

277-
val _ = tDefine "type_subst" `
279+
Definition type_subst_def:
278280
type_subst i ty =
279281
dtcase ty of
280282
Tyapp tycon args =>
281283
let args' = MAP (type_subst i) args in
282284
if args' = args then ty else Tyapp tycon args'
283-
| _ => rev_assocd ty i ty`
284-
(WF_REL_TAC `measure (type_size o SND)` THEN Induct_on `args`
285+
| _ => rev_assocd ty i ty
286+
Termination
287+
WF_REL_TAC `measure (type_size o SND)` THEN Induct_on `args`
285288
THEN FULL_SIMP_TAC (srw_ss()) [type_size_def]
286289
THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN RES_TAC
287290
THEN REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN REPEAT STRIP_TAC
288-
THEN DECIDE_TAC);
291+
THEN DECIDE_TAC
292+
End
289293

290294
(*
291295
let bool_ty = mk_type("bool",[]);;
@@ -716,7 +720,7 @@ val ZERO_LT_term_size = Q.prove(
716720
`!t. 0 < my_term_size t`,
717721
Cases THEN EVAL_TAC THEN DECIDE_TAC);
718722

719-
val inst_aux_def = tDefine "inst_aux" `
723+
Definition inst_aux_def:
720724
(inst_aux (env:(term # term) list) tyin tm) =
721725
dtcase tm of
722726
Var n ty => let ty' = type_subst tyin ty in
@@ -745,12 +749,14 @@ val inst_aux_def = tDefine "inst_aux" `
745749
t' <- inst_aux ((Var v1 ty,Var v1 ty')::env) tyin
746750
(vsubst_aux [(Var v1 ty,y)] t) ;
747751
return (Abs y' t') od)
748-
od`
749-
(WF_REL_TAC `measure (\(env,tyin,tm). my_term_size tm)`
752+
od
753+
Termination
754+
WF_REL_TAC `measure (\(env,tyin,tm). my_term_size tm)`
750755
THEN SIMP_TAC (srw_ss()) [my_term_size_def]
751756
THEN REPEAT STRIP_TAC
752757
THEN FULL_SIMP_TAC std_ss [my_term_size_vsubst_aux]
753-
THEN DECIDE_TAC)
758+
THEN DECIDE_TAC
759+
End
754760

755761
Definition inst_def:
756762
inst tyin tm = if tyin = [] then return tm else inst_aux [] tyin tm

‎candle/overloading/semantics/holModelConservativityScript.sml

+7-5
Original file line numberDiff line numberDiff line change
@@ -1924,8 +1924,7 @@ val one_one_conext = EVAL ``conexts_of_upd(EL 3 (mk_infinity_ctxt ARB))`` |> con
19241924

19251925
(* construction of the model extension basing on the independent fragment *)
19261926

1927-
val type_interpretation_ext_of_def =
1928-
tDefine "type_interpretation_ext_of0" `
1927+
Definition type_interpretation_ext_of0_def:
19291928
(type_interpretation_ext_of0
19301929
^mem ind upd ctxt Δ (Γ :mlstring # type -> 'U) ty =
19311930
if ~terminating(subst_clos (dependency (upd::ctxt))) then
@@ -2070,8 +2069,9 @@ val type_interpretation_ext_of_def =
20702069
sigma'
20712070
trm0
20722071
| NONE => One (* cannot happen *)
2073-
)`
2074-
(
2072+
)
2073+
Termination
2074+
20752075
wf_rel_tac `subst_clos_term_ext_rel`
20762076
>- (
20772077
rw[wellorderTheory.WF_IND,subst_clos_term_ext_rel_def,WF_TC_EQN] >>
@@ -2602,11 +2602,13 @@ val type_interpretation_ext_of_def =
26022602
fs[extends_init_def]
26032603
)
26042604
)
2605-
)
2605+
2606+
End
26062607

26072608
Overload type_interpretation_ext_of = ``type_interpretation_ext_of0 ^mem``
26082609
Overload term_interpretation_ext_of = ``term_interpretation_ext_of0 ^mem``
26092610

2611+
val type_interpretation_ext_of_def = type_interpretation_ext_of0_def;
26102612
val type_interpretation_ext_of_ind = fetch "-" "type_interpretation_ext_of0_ind";
26112613

26122614
(* symbols from the independent fragment keeps their earlier interpretation *)

‎candle/overloading/semantics/holSemanticsScript.sml

+5-4
Original file line numberDiff line numberDiff line change
@@ -75,14 +75,15 @@ Definition terms_of_frag_def:
7575
/\ set(allTypes t) ⊆ tys /\ welltyped t}
7676
End
7777

78-
val TYPE_SUBSTf_def = tDefine "TYPE_SUBSTf" `
78+
Definition TYPE_SUBSTf_def:
7979
(TYPE_SUBSTf i (Tyvar v) = i v) ∧
8080
(TYPE_SUBSTf i (Tyapp v tys) =
8181
Tyapp v (MAP (λa. TYPE_SUBSTf i a) tys))
82-
`
83-
(WF_REL_TAC(`measure (type_size o SND)`) >> simp[] >>
82+
Termination
83+
WF_REL_TAC(`measure (type_size o SND)`) >> simp[] >>
8484
gen_tac >> Induct >> simp[type_size_def] >> rw[] >>
85-
simp[] >> res_tac >> simp[]);
85+
simp[] >> res_tac >> simp[]
86+
End
8687

8788
val _ = export_rewrites["TYPE_SUBSTf_def"]
8889

‎candle/standard/ml_kernel/ml_hol_kernel_funsProgScript.sml

+6-4
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ val res = translate concl_def;
262262

263263
val _ = ml_prog_update open_local_block;
264264

265-
val type_compare_def = tDefine "type_compare" `
265+
Definition type_compare_def:
266266
(type_compare t1 t2 =
267267
case (t1,t2) of
268268
| (Tyvar x1,Tyvar x2) => mlstring$compare x1 x2
@@ -280,10 +280,12 @@ val type_compare_def = tDefine "type_compare" `
280280
| (t1::ts1,t2::ts2) =>
281281
(case type_compare t1 t2 of
282282
| Equal => type_list_compare ts1 ts2
283-
| other => other))`
284-
(WF_REL_TAC `measure (\x. case x of
283+
| other => other))
284+
Termination
285+
WF_REL_TAC `measure (\x. case x of
285286
INR (x,_) => type1_size x
286-
| INL (x,_) => type_size x)`)
287+
| INL (x,_) => type_size x)`
288+
End
287289

288290
val type_cmp_thm = Q.prove(
289291
`(type_cmp = type_compare) /\

‎candle/standard/monadic/holKernelScript.sml

+18-12
Original file line numberDiff line numberDiff line change
@@ -245,15 +245,17 @@ End
245245
| (Tyvar v as tv) -> [tv]
246246
*)
247247

248-
val _ = tDefine "tyvars" `
248+
Definition tyvars_def:
249249
tyvars x =
250250
dtcase x of (Tyapp _ args) => itlist union (MAP tyvars args) []
251-
| (Tyvar tv) => [tv]`
252-
(WF_REL_TAC `measure (type_size)` THEN Induct_on `args`
251+
| (Tyvar tv) => [tv]
252+
Termination
253+
WF_REL_TAC `measure (type_size)` THEN Induct_on `args`
253254
THEN FULL_SIMP_TAC (srw_ss()) [type_size_def]
254255
THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN RES_TAC
255256
THEN REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN REPEAT STRIP_TAC
256-
THEN DECIDE_TAC);
257+
THEN DECIDE_TAC
258+
End
257259

258260
(*
259261
let rec type_subst i ty =
@@ -272,18 +274,20 @@ Definition rev_assocd_def:
272274
| ((x,y)::l) => if y = a then x else rev_assocd a l d
273275
End
274276

275-
val _ = tDefine "type_subst" `
277+
Definition type_subst_def:
276278
type_subst i ty =
277279
dtcase ty of
278280
Tyapp tycon args =>
279281
let args' = MAP (type_subst i) args in
280282
if args' = args then ty else Tyapp tycon args'
281-
| _ => rev_assocd ty i ty`
282-
(WF_REL_TAC `measure (type_size o SND)` THEN Induct_on `args`
283+
| _ => rev_assocd ty i ty
284+
Termination
285+
WF_REL_TAC `measure (type_size o SND)` THEN Induct_on `args`
283286
THEN FULL_SIMP_TAC (srw_ss()) [type_size_def]
284287
THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN RES_TAC
285288
THEN REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN REPEAT STRIP_TAC
286-
THEN DECIDE_TAC);
289+
THEN DECIDE_TAC
290+
End
287291

288292
(*
289293
let bool_ty = mk_type("bool",[]);;
@@ -714,7 +718,7 @@ val ZERO_LT_term_size = Q.prove(
714718
`!t. 0 < my_term_size t`,
715719
Cases THEN EVAL_TAC THEN DECIDE_TAC);
716720

717-
val inst_aux_def = tDefine "inst_aux" `
721+
Definition inst_aux_def:
718722
(inst_aux (env:(term # term) list) tyin tm) =
719723
dtcase tm of
720724
Var n ty => let ty' = type_subst tyin ty in
@@ -743,12 +747,14 @@ val inst_aux_def = tDefine "inst_aux" `
743747
t' <- inst_aux ((Var v1 ty,Var v1 ty')::env) tyin
744748
(vsubst_aux [(Var v1 ty,y)] t) ;
745749
return (Abs y' t') od)
746-
od`
747-
(WF_REL_TAC `measure (\(env,tyin,tm). my_term_size tm)`
750+
od
751+
Termination
752+
WF_REL_TAC `measure (\(env,tyin,tm). my_term_size tm)`
748753
THEN SIMP_TAC (srw_ss()) [my_term_size_def]
749754
THEN REPEAT STRIP_TAC
750755
THEN FULL_SIMP_TAC std_ss [my_term_size_vsubst_aux]
751-
THEN DECIDE_TAC)
756+
THEN DECIDE_TAC
757+
End
752758

753759
Definition inst_def:
754760
inst tyin tm = if tyin = [] then return tm else inst_aux [] tyin tm

‎candle/standard/semantics/holSemanticsScript.sml

+5-3
Original file line numberDiff line numberDiff line change
@@ -49,11 +49,13 @@ Overload is_type_valuation = ``is_type_valuation0 ^mem``
4949

5050
(* Semantics of types. Simply applies the valuation and assignment. *)
5151

52-
val typesem_def = tDefine "typesem"`
52+
Definition typesem_def:
5353
(typesem δ (τ:'U tyval) (Tyvar s) = τ s) ∧
5454
(typesem δ τ (Tyapp name args) =
55-
(δ name) (MAP (typesem δ τ) args))`
56-
(type_rec_tac "SND o SND")
55+
(δ name) (MAP (typesem δ τ) args))
56+
Termination
57+
type_rec_tac "SND o SND"
58+
End
5759

5860
(* A term assignment is a map from a constant name and a list of values for the
5961
free type variables to a value for the constant. The assignment is with

0 commit comments

Comments
 (0)