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 )