1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7chapter Lib
8
9session Lib (lib) = Word_Lib +
10  sessions
11    "HOL-Library"
12    "HOL-Eisbach"
13  directories
14    "ml-helpers"
15    "subgoal_focus"
16    "Monad_WP"
17    "Monad_WP/wp"
18  theories
19    Lib
20    Apply_Trace_Cmd
21    AddUpdSimps
22    EmptyFailLib
23    List_Lib
24    SubMonadLib
25    Simulation
26    MonadEq
27    SimpStrategy
28    Extract_Conjunct
29    GenericLib
30    ProvePart
31    Corres_Adjust_Preconds
32    Requalify
33    Value_Abbreviation
34    Eisbach_Methods
35    HaskellLib_H
36    Eval_Bool
37    Bisim_UL
38    Extend_Locale
39    Solves_Tac
40    Crunch
41    Crunch_Instances_NonDet
42    Crunch_Instances_Trace
43    StateMonad
44    Corres_UL
45    Find_Names
46    LemmaBucket
47    Try_Methods
48    ListLibLemmas
49    Time_Methods_Cmd
50    Apply_Debug
51    MonadicRewrite
52    HaskellLemmaBucket
53    "ml-helpers/MkTermAntiquote"
54    "ml-helpers/TermPatternAntiquote"
55    "ml-helpers/TacticAntiquotation"
56    "ml-helpers/MLUtils"
57    "ml-helpers/TacticTutorial"
58    "ml-helpers/MkTermAntiquote_Tests"
59    "ml-helpers/TacticAntiquotation_Test"
60    "ml-helpers/TermPatternAntiquote_Tests"
61    FP_Eval
62    "subgoal_focus/Subgoal_Methods"
63    Insulin
64    ExtraCorres
65    NICTATools
66    BCorres_UL
67    Qualify
68    LexordList
69    Rule_By_Method
70    Defs
71    AutoLevity_Hooks
72    Distinct_Cmd
73    Match_Abbreviation
74    ShowTypes
75    SpecValid_R
76    EquivValid
77    SplitRule
78    DataMap
79    FastMap
80    RangeMap
81    Corres_Method
82    Conjuncts
83    DetWPLib
84    Guess_ExI
85    GenericTag
86    ML_Goal_Test
87
88    (* should really be a separate session, but too entangled atm: *)
89    NonDetMonadLemmaBucket
90    "Monad_WP/WhileLoopRules"
91    "Monad_WP/TraceMonad"
92    "Monad_WP/OptionMonadND"
93    "Monad_WP/OptionMonadWP"
94    "Monad_WP/Strengthen_Demo"
95    "Monad_WP/TraceMonadLemmas"
96    "Monad_WP/wp/WPBang"
97    "Monad_WP/wp/WPFix"
98    "Monad_WP/wp/Eisbach_WP"
99    "Monad_WP/wp/WPI"
100    "Monad_WP/wp/WPC"
101    "Monad_WP/wp/WPEx"
102    "Monad_WP/wp/WP_Pre"
103    "Monad_WP/wp/WP"
104    "Monad_WP/Datatype_Schematic"
105    "Monad_WP/WhileLoopRulesCompleteness"
106    "Monad_WP/Strengthen"
107    "Monad_WP/OptionMonad"
108    "Monad_WP/TraceMonadVCG"
109    "Monad_WP/NonDetMonadVCG"
110    "Monad_WP/NonDetMonad"
111    "Monad_WP/NonDetMonadLemmas"
112
113session CLib (lib) in clib = CParser +
114  sessions
115    "HOL-Library"
116    "HOL-Statespace"
117    "HOL-Eisbach"
118    "Simpl-VCG"
119    Lib
120  theories
121    Corres_UL_C
122    CCorresLemmas
123    CCorres_Rewrite
124    Simpl_Rewrite
125    MonadicRewrite_C
126    CTranslationNICTA
127    LemmaBucket_C
128    SIMPL_Lemmas
129    SimplRewrite
130    TypHeapLib
131    BitFieldProofsLib
132    XPres
133
134session CorresK in "CorresK" = Lib +
135  sessions
136    ASpec
137    ExecSpec
138  theories
139    CorresK_Lemmas
140
141session LibTest (lib) in test = Refine +
142  sessions
143    Lib
144    CLib
145    ASpec
146    ExecSpec
147  theories
148    Crunch_Test_NonDet
149    Crunch_Test_Qualified_NonDet
150    Crunch_Test_Qualified_Trace
151    Crunch_Test_Trace
152    WPTutorial
153    Match_Abbreviation_Test
154    Apply_Debug_Test
155    AutoLevity_Test
156    Insulin_Test
157    ShowTypes_Test
158    Time_Methods_Cmd_Test
159    FastMap_Test
160    RangeMap_Test
161    FP_Eval_Tests
162    Trace_Schematic_Insts_Test
163    Local_Method_Tests
164    Qualify_Test
165    Locale_Abbrev_Test
166  (* use virtual memory function as an example, only makes sense on ARM: *)
167  theories [condition = "L4V_ARCH_IS_ARM"]
168    Corres_Test
169
170session SepTactics (lib) in Hoare_Sep_Tactics = Sep_Algebra +
171  theories
172    Hoare_Sep_Tactics
173
174(* bitrotted
175session AutoLevity (lib) = HOL +
176  theories
177    AutoLevity
178    AutoLevity_Run
179    AutoLevity_Theory_Report
180*)
181
182session Concurrency (lib) in concurrency = HOL +
183  sessions
184    Lib
185  directories
186    "examples"
187  theories
188    Atomicity_Lib
189    Triv_Refinement
190    Prefix_Refinement
191    "examples/Peterson_Atomicity"
192    "examples/Plus2_Prefix"
193