adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib/design: enable more Haskell-like list comprehension syntax 

Accept "[f x | x \leftarrow t]" in addition to "[f x . x \leftarrow t]",
because the former is what naturally comes out of the Haskell translator, and
the regexps that would be necessary in the Haskell translator for this are
distasteful.

JIRA-VER 927
This commit is contained in:
Gerwin Klein 2018-07-29 09:58:49 +02:00
parent 24fbac1e67
commit 53fde5e5ff
2 changed files with 6 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/HaskellLib_H.thy
View File

@ -549,4 +549,9 @@ definition
abbreviation
"null == List.null"
syntax (input)
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ | __")
lemma "[(x,1) . x \<leftarrow> [0..10]] = [(x,1) | x \<leftarrow> [0..10]]" by (rule refl)
end

11
spec/design/skel/X64/ArchRetype_H.thy
View File

@ -20,16 +20,7 @@ begin
context Arch begin global_naming X64_H
(* FIXME haskell-translator: VER-927 *)
defs setIOPortMask_def:
"setIOPortMask f l val \<equiv> (do
ports \<leftarrow> gets (x64KSAllocatedIOPorts \<circ> ksArchState);
ports' \<leftarrow> return $ ports aLU [(i,val). i \<leftarrow> [f .e. l]];
modify (\<lambda> s. s \<lparr>
ksArchState := (ksArchState s) \<lparr> x64KSAllocatedIOPorts := ports' \<rparr>\<rparr>)
od)"
#INCLUDE_HASKELL SEL4/Object/ObjectType/X64.lhs CONTEXT X64_H Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H NOT setIOPortMask bodies_only
#INCLUDE_HASKELL SEL4/Object/ObjectType/X64.lhs CONTEXT X64_H Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H NOT bodies_only
#INCLUDE_HASKELL SEL4/API/Invocation/X64.lhs CONTEXT X64_H bodies_only
end (* context X64 *)