1127668Sbms(*
2127668Sbms * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3127668Sbms *
4127668Sbms * SPDX-License-Identifier: BSD-2-Clause
5127668Sbms *)
6127668Sbms
7127668Sbmschapter Lib
8127668Sbms
9127668Sbmssession Lib (lib) = Word_Lib +
10127668Sbms  sessions
11127668Sbms    "HOL-Library"
12127668Sbms    "HOL-Eisbach"
13127668Sbms  directories
14127668Sbms    "ml-helpers"
15127668Sbms    "subgoal_focus"
16127668Sbms    "Monad_WP"
17127668Sbms    "Monad_WP/wp"
18127668Sbms  theories
19127668Sbms    Lib
20127668Sbms    Apply_Trace_Cmd
21127668Sbms    AddUpdSimps
22127668Sbms    EmptyFailLib
23127668Sbms    List_Lib
24127668Sbms    SubMonadLib
25127668Sbms    Simulation
26190207Srpaulo    MonadEq
27127668Sbms    SimpStrategy
28127668Sbms    Extract_Conjunct
29127668Sbms    GenericLib
30127668Sbms    ProvePart
31127668Sbms    Corres_Adjust_Preconds
32127668Sbms    Requalify
33127668Sbms    Value_Abbreviation
34127668Sbms    Eisbach_Methods
35127668Sbms    HaskellLib_H
36127668Sbms    Eval_Bool
37127668Sbms    Bisim_UL
38127668Sbms    Extend_Locale
39127668Sbms    Solves_Tac
40127668Sbms    Crunch
41127668Sbms    Crunch_Instances_NonDet
42127668Sbms    Crunch_Instances_Trace
43127668Sbms    StateMonad
44127668Sbms    Corres_UL
45127668Sbms    Find_Names
46127668Sbms    LemmaBucket
47127668Sbms    Try_Methods
48127668Sbms    ListLibLemmas
49127668Sbms    Time_Methods_Cmd
50127668Sbms    Apply_Debug
51127668Sbms    MonadicRewrite
52127668Sbms    HaskellLemmaBucket
53127668Sbms    "ml-helpers/MkTermAntiquote"
54127668Sbms    "ml-helpers/TermPatternAntiquote"
55127668Sbms    "ml-helpers/TacticAntiquotation"
56127668Sbms    "ml-helpers/MLUtils"
57127668Sbms    "ml-helpers/TacticTutorial"
58127668Sbms    "ml-helpers/MkTermAntiquote_Tests"
59127668Sbms    "ml-helpers/TacticAntiquotation_Test"
60127668Sbms    "ml-helpers/TermPatternAntiquote_Tests"
61127668Sbms    FP_Eval
62127668Sbms    "subgoal_focus/Subgoal_Methods"
63127668Sbms    Insulin
64127668Sbms    ExtraCorres
65127668Sbms    NICTATools
66127668Sbms    BCorres_UL
67127668Sbms    Qualify
68127668Sbms    LexordList
69127668Sbms    Rule_By_Method
70127668Sbms    Defs
71127668Sbms    AutoLevity_Hooks
72127668Sbms    Distinct_Cmd
73190207Srpaulo    Match_Abbreviation
74190207Srpaulo    ShowTypes
75190207Srpaulo    SpecValid_R
76190207Srpaulo    EquivValid
77190207Srpaulo    SplitRule
78190207Srpaulo    DataMap
79190207Srpaulo    FastMap
80190221Srpaulo    RangeMap
81190207Srpaulo    Corres_Method
82190207Srpaulo    Conjuncts
83190207Srpaulo    DetWPLib
84190221Srpaulo    Guess_ExI
85190207Srpaulo    GenericTag
86127668Sbms    ML_Goal_Test
87127668Sbms
88127668Sbms    (* should really be a separate session, but too entangled atm: *)
89127668Sbms    NonDetMonadLemmaBucket
90146773Ssam    "Monad_WP/WhileLoopRules"
91146773Ssam    "Monad_WP/TraceMonad"
92146773Ssam    "Monad_WP/OptionMonadND"
93146773Ssam    "Monad_WP/OptionMonadWP"
94146773Ssam    "Monad_WP/Strengthen_Demo"
95146773Ssam    "Monad_WP/TraceMonadLemmas"
96146773Ssam    "Monad_WP/wp/WPBang"
97146773Ssam    "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