move isAligned to HaskellLib
Isabelle2014 doesn't like defs to be less general than the consts declaration.
This commit is contained in:
parent
1af1d2b67b
commit
12b1b0d16f
|
@ -30,7 +30,7 @@ abbreviation(input) bind_drop :: "('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) n
|
||||||
where "bind_drop \<equiv> (\<lambda>x y. bind x (K_bind y))"
|
where "bind_drop \<equiv> (\<lambda>x y. bind x (K_bind y))"
|
||||||
|
|
||||||
lemma bind_drop_test:
|
lemma bind_drop_test:
|
||||||
"foldr (op >>) x (return ()) = sequence_x x"
|
"foldr bind_drop x (return ()) = sequence_x x"
|
||||||
by (rule ext, simp add: sequence_x_def)
|
by (rule ext, simp add: sequence_x_def)
|
||||||
|
|
||||||
(* If the given monad is deterministic, this function converts
|
(* If the given monad is deterministic, this function converts
|
||||||
|
@ -266,6 +266,8 @@ definition
|
||||||
bit_def[simp]:
|
bit_def[simp]:
|
||||||
"bit x \<equiv> shiftL 1 x"
|
"bit x \<equiv> shiftL 1 x"
|
||||||
|
|
||||||
|
definition
|
||||||
|
"isAligned x n \<equiv> x && mask n = 0"
|
||||||
|
|
||||||
class integral = ord +
|
class integral = ord +
|
||||||
fixes fromInteger :: "nat \<Rightarrow> 'a"
|
fixes fromInteger :: "nat \<Rightarrow> 'a"
|
||||||
|
|
|
@ -97,8 +97,5 @@ createFreeSlotRegions :: "unit kernel_init"
|
||||||
consts
|
consts
|
||||||
createEmptyRegions :: "unit kernel_init"
|
createEmptyRegions :: "unit kernel_init"
|
||||||
|
|
||||||
consts
|
|
||||||
isAligned :: "('a :: {minus, one, zero, plus, numeral, HS_bit}) \<Rightarrow> nat \<Rightarrow> bool"
|
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -478,9 +478,6 @@ defs createEmptyRegions_def:
|
||||||
provideRegion $ BootRegion l1magnitude maxBound BREmpty 0
|
provideRegion $ BootRegion l1magnitude maxBound BREmpty 0
|
||||||
od)"
|
od)"
|
||||||
|
|
||||||
defs isAligned_def:
|
|
||||||
"isAligned x n \<equiv> x && mask n = 0"
|
|
||||||
|
|
||||||
|
|
||||||
consts
|
consts
|
||||||
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
||||||
|
|
|
@ -16,6 +16,6 @@ imports
|
||||||
KernelInitMonad_H
|
KernelInitMonad_H
|
||||||
begin
|
begin
|
||||||
|
|
||||||
#INCLUDE_HASKELL SEL4/Kernel/Init.lhs decls_only NOT funArray newKernelState distinct rangesBy InitData doKernelOp runInit
|
#INCLUDE_HASKELL SEL4/Kernel/Init.lhs decls_only NOT isAligned funArray newKernelState distinct rangesBy InitData doKernelOp runInit
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -18,7 +18,7 @@ imports
|
||||||
Config_H
|
Config_H
|
||||||
begin
|
begin
|
||||||
|
|
||||||
#INCLUDE_HASKELL SEL4/Kernel/Init.lhs bodies_only NOT funArray newKernelState distinct rangesBy InitData doKernelOp runInit
|
#INCLUDE_HASKELL SEL4/Kernel/Init.lhs bodies_only NOT isAligned funArray newKernelState distinct rangesBy InitData doKernelOp runInit
|
||||||
|
|
||||||
consts
|
consts
|
||||||
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
Built from git repo at ../../../seL4/haskell by kleing
|
Built from git repo at ../../../seL4/haskell by kleing
|
||||||
|
|
||||||
Generated from changeset:
|
Generated from changeset:
|
||||||
3ffeaac Retire old dft package; resurrect Haskell manual.
|
2261557 Fix IFC6410 build
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue