projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
better error reporting in coreTypeToWeakType; dont use Prelude_error
[coq-hetmet.git]
/
examples
/
RegexMatcher.hs
diff --git
a/examples/RegexMatcher.hs
b/examples/RegexMatcher.hs
index
ca02755
..
a50a10b
100644
(file)
--- a/
examples/RegexMatcher.hs
+++ b/
examples/RegexMatcher.hs
@@
-110,13
+110,12
@@
staged_accept (Times e1 e2) emptyOk k =
staged_accept (Star e) emptyOk' k =
loop emptyOk'
where
staged_accept (Star e) emptyOk' k =
loop emptyOk'
where
- -- loop :: Bool -> <[s -> Bool]>@g
+ -- Note that the type of "loop" is NOT (forall c s. <[s -> Bool]>@c)
+ -- because "k" is free here; this restrictionis analogous to the free
+ -- environment variable in Nanevski's example.
loop emptyOk = if emptyOk
then <[ \s -> ~~k s || ~~(staged_accept e True (loop False)) s ]>
else <[ \s -> ~~(staged_accept e False (loop False)) s ]>
loop emptyOk = if emptyOk
then <[ \s -> ~~k s || ~~(staged_accept e True (loop False)) s ]>
else <[ \s -> ~~(staged_accept e False (loop False)) s ]>
- -- note that loop is not (forall c s. <[s -> Bool]>@c)
- -- because "k" is free in loop; it is analogous to the free
- -- environment variable in Nanevski's example
staged_accept (Const c) emptyOk k =
<[ \s -> if gs_empty s
staged_accept (Const c) emptyOk k =
<[ \s -> if gs_empty s