Friends
I have forgotten the workflow for adding a patch to nofib.
The patch is below. (Trivial). Could someone apply it (and update GHC
head to use it). Or tell me how to do it. Or both!
Thanks
Simon
This patch makes 'veritas' stop using 'forall' as a function name.
Reason: 'forall' is now a keyword
diff --git a/real/veritas/Kernel.hs b/real/veritas/Kernel.hs
index b1c69ef..2c491a7 100644
--- a/real/veritas/Kernel.hs
+++ b/real/veritas/Kernel.hs
@@ -384,7 +384,7 @@ constructor (SG sg) i j k
{- Datatype elimination -}
recurse tmL (TM (tm@(Binder Pi (Symbol_dec tm1 _) _ _ _)) _ sg)
- = if forall ok (zip tmL tyL)
+ = if vforall ok (zip tmL tyL)
then
TM (Recurse (map fst tmL) tm [] []) tm sg
else
@@ -570,7 +570,7 @@ def (TM tm1 tm2 sg)
make_data tmLL (TH tm sg)
- = if forall (forall (wf_param sg1)) tmLL
+ = if vforall (vforall (wf_param sg1)) tmLL
then
if exists (eq_trm tm) non_empty_thms
then
diff --git a/real/veritas/Main.hs b/real/veritas/Main.hs
index c0ed8e3..5191a67 100644
--- a/real/veritas/Main.hs
+++ b/real/veritas/Main.hs
@@ -107,7 +107,7 @@ goto_next tr@(TreeSt t _ _)
incomplete_tree (Tree _ tl (SOME _) _ _ ) = False
-incomplete_tree (Tree _ tl NONE _ _ ) = forall is_complete tl
+incomplete_tree (Tree _ tl NONE _ _ ) = vforall is_complete tl
diff --git a/real/veritas/Sub_Core3.hs b/real/veritas/Sub_Core3.hs
index f6fd733..12c2987 100644
--- a/real/veritas/Sub_Core3.hs
+++ b/real/veritas/Sub_Core3.hs
@@ -248,7 +248,7 @@ eval (Constant F _ _) = False
--eval (Constant _ _ _) = error "EvalError" -- ** exn
eval (Binder Forall dc tm _ _)
- = eval_quant forall dc tm
+ = eval_quant vforall dc tm
eval (Binder Exists dc tm _ _)
= eval_quant exists dc tm
diff --git a/real/veritas/Vtslib.hs b/real/veritas/Vtslib.hs
index 9a6c0fe..9ae06ab 100644
--- a/real/veritas/Vtslib.hs
+++ b/real/veritas/Vtslib.hs
@@ -1,4 +1,4 @@
-module Vtslib( Option(..) , Sum(..) , forall , exists , assoc ,
+module Vtslib( Option(..) , Sum(..) , vforall , exists , assoc ,
haskey , uncurry , curry , for , map' , module Core_datatype )
where
@@ -14,9 +14,9 @@ data Sum a b = Inl a | Inr b
N.B. forall & exists rewritten from ML
-}
-forall :: ( a -> Bool ) -> [a] -> Bool
+vforall :: ( a -> Bool ) -> [a] -> Bool
-forall p = and . ( map p )
+vforall p = and . ( map p )
