Skip to content

Commit a395c9c

Browse files
dnezamdnezam
committed
Use Theory syntax
1 parent 0a3f866 commit a395c9c

File tree

169 files changed

+1187
-1734
lines changed

Some content is hidden

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

169 files changed

+1187
-1734
lines changed

‎compiler/backend/languages/env_cexpScript.sml‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
(*
22
Compiler expressions for stateLang
33
*)
4-
open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
5-
open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
6-
pure_expTheory pure_semanticsTheory arithmeticTheory mlstringTheory
7-
pred_setTheory;
8-
9-
val _ = new_theory "env_cexp";
10-
11-
val _ = set_grammar_ancestry ["pure_exp","mlstring"];
4+
Theory env_cexp
5+
Ancestors
6+
string option sum pair list alist
7+
pure_semantics arithmetic pred_set
8+
pure_exp mlstring
9+
Libs
10+
BasicProvers dep_rewrite
1211

1312
val _ = numLib.prefer_num();
1413

@@ -99,5 +98,3 @@ Definition dest_Lam_def:
9998
dest_Lam (Lam v x) = SOME (v,x) ∧
10099
dest_Lam _ = NONE
101100
End
102-
103-
val _ = export_theory();

‎compiler/backend/languages/properties/env_cexp_lemmasScript.sml‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
1-
open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
2-
open arithmeticTheory listTheory stringTheory alistTheory
3-
optionTheory pairTheory pred_setTheory finite_mapTheory
4-
envLangTheory;
5-
open pure_miscTheory env_cexpTheory ;
6-
7-
val _ = new_theory "env_cexp_lemmas";
1+
Theory env_cexp_lemmas
2+
Ancestors
3+
arithmetic list string alist option pair pred_set finite_map
4+
envLang pure_misc env_cexp
5+
Libs
6+
BasicProvers dep_rewrite
87

98
val freevars_def = envLangTheory.freevars_def;
109
val Lams_def = envLangTheory.Lams_def;
@@ -107,4 +106,3 @@ Proof
107106
QED
108107
*)
109108

110-
val _ = export_theory();

‎compiler/backend/languages/properties/pure_cexp_lemmasScript.sml‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11

2-
open HolKernel Parse boolLib bossLib term_tactic BasicProvers dep_rewrite;
3-
open arithmeticTheory listTheory stringTheory alistTheory
4-
optionTheory pairTheory pred_setTheory finite_mapTheory;
5-
open pure_miscTheory pure_cexpTheory pureLangTheory
6-
pure_expTheory pure_exp_lemmasTheory;
7-
8-
val _ = new_theory "pure_cexp_lemmas";
2+
Theory pure_cexp_lemmas
3+
Ancestors
4+
arithmetic list string alist option pair pred_set finite_map
5+
pure_misc pure_cexp pureLang pure_exp pure_exp_lemmas
6+
Libs
7+
term_tactic BasicProvers dep_rewrite
98

109
Theorem silly_cong_lemma[local]:
1110
((∀a b. MEM (a,b) l2 ⇒ P a b) ⇔ (∀p. MEM p l2 ⇒ P (FST p) (SND p))) ∧
@@ -471,4 +470,3 @@ Proof
471470
QED
472471

473472

474-
val _ = export_theory();

‎compiler/backend/languages/pure_cexpScript.sml‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,13 @@
11
(*
22
This file defines expressions for pure_lang as the compiler sees them.
33
*)
4-
open HolKernel Parse boolLib bossLib term_tactic;
5-
open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
6-
optionTheory pairTheory ltreeTheory llistTheory bagTheory dep_rewrite
7-
BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory;
8-
open pure_expTheory;
9-
10-
local open mlstringTheory in end
11-
12-
val _ = new_theory "pure_cexp";
4+
Theory pure_cexp
5+
Ancestors
6+
fixedPoint arithmetic list string alist option pair ltree llist
7+
bag pred_set relation rich_list finite_map pure_exp
8+
mlstring[qualified]
9+
Libs
10+
term_tactic dep_rewrite BasicProvers
1311

1412
Datatype:
1513
cop = Cons mlstring (* datatype constructor *)
@@ -456,4 +454,3 @@ Proof
456454
gvs[AllCaseEqs(), SF ETA_ss]
457455
QED
458456

459-
val _ = export_theory();

‎compiler/backend/languages/relations/pure_inline_rel_altScript.sml‎

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,16 @@
11
(*
22
Relation describing inlining and proof that it fits bidir from pure_pres
33
*)
4-
open HolKernel Parse boolLib bossLib term_tactic;
5-
open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
6-
optionTheory pairTheory ltreeTheory llistTheory bagTheory dep_rewrite
7-
BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory
8-
combinTheory;
9-
open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
10-
pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory
11-
pure_alpha_equivTheory pure_miscTheory pure_congruenceTheory
12-
pure_letrec_seqTheory pure_demandTheory pure_barendregtTheory
13-
pure_presTheory pure_pres_lemmasTheory;
14-
15-
val _ = new_theory "pure_inline_rel_alt";
4+
Theory pure_inline_rel_alt
5+
Ancestors
6+
fixedPoint arithmetic list string alist option pair ltree llist
7+
bag pred_set relation rich_list finite_map combin pure_exp
8+
pure_value pure_eval pure_eval_lemmas pure_exp_lemmas
9+
pure_limit pure_exp_rel pure_alpha_equiv pure_misc
10+
pure_congruence pure_letrec_seq pure_demand pure_barendregt
11+
pure_pres pure_pres_lemmas
12+
Libs
13+
term_tactic dep_rewrite BasicProvers
1614

1715
val _ = Parse.hide "bind_ok";
1816

@@ -1930,4 +1928,3 @@ QED
19301928
19311929
*)
19321930

1933-
val _ = export_theory();

‎compiler/backend/languages/relations/pure_presScript.sml‎

Lines changed: 12 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2,27 +2,24 @@
22
This theory defines a syntactic relation that preserves both semantics
33
and typing.
44
*)
5-
open HolKernel Parse boolLib bossLib term_tactic;
6-
open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
7-
optionTheory pairTheory ltreeTheory llistTheory bagTheory dep_rewrite
8-
BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory
9-
combinTheory;
10-
open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
11-
pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory
12-
pure_alpha_equivTheory pure_miscTheory pure_congruenceTheory
13-
pure_letrecProofTheory pure_demandTheory pure_letrec_delargTheory
14-
pure_cexpTheory pure_cexp_lemmasTheory pureLangTheory
15-
pure_freshenTheory pure_freshenProofTheory
16-
pure_tcexpTheory pure_tcexp_lemmasTheory
17-
pure_typingTheory pure_typingPropsTheory;
5+
Theory pure_pres
6+
Ancestors
7+
fixedPoint arithmetic list string alist option pair ltree llist
8+
bag pred_set relation rich_list finite_map combin pure_exp
9+
pure_value pure_eval pure_eval_lemmas pure_exp_lemmas
10+
pure_limit pure_exp_rel pure_alpha_equiv pure_misc
11+
pure_congruence pure_letrecProof pure_demand pure_letrec_delarg
12+
pure_cexp pure_cexp_lemmas pureLang pure_freshen
13+
pure_freshenProof pure_tcexp pure_tcexp_lemmas pure_typing
14+
pure_typingProps
15+
Libs
16+
term_tactic dep_rewrite BasicProvers
1817

1918
val exp_of_def = pureLangTheory.exp_of_def;
2019
val rows_of_def = pureLangTheory.rows_of_def;
2120
val lets_for_def = pureLangTheory.lets_for_def;
2221
val freevars_exp_of = pure_cexp_lemmasTheory.freevars_exp_of
2322

24-
val _ = new_theory "pure_pres";
25-
2623
(*----------------------------------------------------------------------------*
2724
Definition of syntactic relation
2825
*----------------------------------------------------------------------------*)
@@ -1250,4 +1247,3 @@ QED
12501247

12511248
(**********)
12521249

1253-
val _ = export_theory ();

‎compiler/backend/languages/relations/pure_pres_lemmasScript.sml‎

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,16 @@
11
(*
22
Proves lemmas that follow from the definitions in pure_presTheory
33
*)
4-
open HolKernel Parse boolLib bossLib term_tactic;
5-
open fixedPointTheory arithmeticTheory listTheory stringTheory alistTheory
6-
optionTheory pairTheory ltreeTheory llistTheory bagTheory dep_rewrite
7-
BasicProvers pred_setTheory relationTheory rich_listTheory finite_mapTheory
8-
combinTheory;
9-
open pure_expTheory pure_valueTheory pure_evalTheory pure_eval_lemmasTheory
10-
pure_exp_lemmasTheory pure_limitTheory pure_exp_relTheory
11-
pure_alpha_equivTheory pure_miscTheory pure_congruenceTheory
12-
pure_demandTheory pure_letrec_delargTheory
13-
pure_cexpTheory pure_cexp_lemmasTheory pureLangTheory pure_presTheory;
14-
15-
val _ = new_theory "pure_pres_lemmas";
4+
Theory pure_pres_lemmas
5+
Ancestors
6+
fixedPoint arithmetic list string alist option pair ltree llist
7+
bag pred_set relation rich_list finite_map combin pure_exp
8+
pure_value pure_eval pure_eval_lemmas pure_exp_lemmas
9+
pure_limit pure_exp_rel pure_alpha_equiv pure_misc
10+
pure_congruence pure_demand pure_letrec_delarg pure_cexp
11+
pure_cexp_lemmas pureLang pure_pres
12+
Libs
13+
term_tactic dep_rewrite BasicProvers
1614

1715
Theorem bidir_letrec_eta:
1816
MEM (f,Lam a vs x) l ∧ ALL_DISTINCT (MAP FST l) ∧ vs ≠ [] ∧
@@ -160,4 +158,3 @@ Proof
160158
\\ irule bidir_App_Lam \\ fs []
161159
QED
162160

163-
val _ = export_theory ();

‎compiler/backend/languages/semantics/envLangScript.sml‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@
88
99
See [thunkLangScript.sml] for the thunkLang semantics.
1010
*)
11+
Theory envLang
12+
Ancestors
13+
string option sum pair list alist pure_exp thunkLang_primitives
14+
pure_misc mlstring env_cexp
15+
Libs
16+
term_tactic monadsyntax
1117

12-
open HolKernel Parse boolLib bossLib term_tactic monadsyntax;
13-
open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
14-
pure_expTheory thunkLang_primitivesTheory
15-
pure_miscTheory mlstringTheory env_cexpTheory;
16-
17-
val _ = new_theory "envLang";
1818

1919
val _ = numLib.prefer_num();
2020

@@ -519,4 +519,3 @@ Termination
519519
WF_REL_TAC ‘measure cexp_size’
520520
End
521521

522-
val _ = export_theory ();

‎compiler/backend/languages/semantics/env_semanticsScript.sml‎

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,13 @@
11
(*
22
Observable semantics for envLang.
33
*)
4-
open HolKernel Parse boolLib bossLib BasicProvers;
5-
open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
6-
pure_semanticsTheory pure_configTheory
7-
thunkLang_primitivesTheory envLangTheory itreeTheory;
8-
9-
val _ = new_theory "env_semantics";
10-
11-
val _ = set_grammar_ancestry ["envLang", "itree"];
12-
4+
Theory env_semantics
5+
Ancestors
6+
string option sum pair list alist pure_semantics
7+
pure_config thunkLang_primitives
8+
envLang itree
9+
Libs
10+
BasicProvers
1311

1412
(******************** Datatypes and helpers ********************)
1513

@@ -293,5 +291,3 @@ Proof
293291
QED
294292

295293
(****************************************)
296-
297-
val _ = export_theory();

‎compiler/backend/languages/semantics/pureLangScript.sml‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
(*
22
Conversion of ``:cexp`` from pure_cexpTheory to ``:exp``
33
*)
4-
open HolKernel Parse boolLib bossLib;
5-
open pairTheory listTheory pred_setTheory combinTheory pure_expTheory pure_cexpTheory;
6-
7-
val _ = new_theory "pureLang";
4+
Theory pureLang
5+
Ancestors
6+
pair list pred_set combin pure_exp pure_cexp
87

98
Overload True[local] = “Prim (Cons "True") []”;
109
Overload False[local] = “Prim (Cons "False") []”;
@@ -229,4 +228,3 @@ Proof
229228
\\ Cases_on ‘x’ \\ gvs [dest_App_def,exp_of_def,SF ETA_ss,Apps_append]
230229
QED
231230

232-
val _ = export_theory();

0 commit comments

Comments
 (0)