Nofib patch

Simon Peyton Jones simon.peytonjones at gmail.com
Thu Jan 11 16:53:15 UTC 2024


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 )
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240111/208f7b76/attachment.html>


More information about the ghc-devs mailing list