From da7eed00e494aba1da9f51cb92089ca10e2454e7 Mon Sep 17 00:00:00 2001
From: Matthew Pickering <matthewtpickering@gmail.com>
Date: Tue, 16 Jan 2024 17:29:16 +0000
Subject: [PATCH] real/veritas: Rename forall -> vforall
---
real/veritas/Kernel.hs | 32 ++++++++++++++++----------------
real/veritas/Main.hs | 2 +-
real/veritas/Sub_Core3.hs | 6 +++---
real/veritas/Vtslib.hs | 12 ++++++------
4 files changed, 26 insertions(+), 26 deletions(-)
diff --git a/real/veritas/Kernel.hs b/real/veritas/Kernel.hs
index b1c69ef7..64f6bdf0 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
@@ -407,10 +407,10 @@ widen (TM tm1 tm2 sg1) (TH (Binary' Issubtype tm3 tm4 _ _) sg2)
then
TM (add_type tm1 tm4) tm4 sg1
else
- TM_Err "widen: error"
+ TM_Err "widen: error"
widen _ _ = TM_Err "widen: error (2)"
-
+
@@ -515,7 +515,7 @@ get_Sgn_att (SG sg) = get_sgn_att sg
{- Set the attributes of a signature -}
-
+
set_Sgn_att (SG sg) att = (SG (set_sgn_att sg att))
@@ -523,7 +523,7 @@ set_Sgn_att (SG sg) att = (SG (set_sgn_att sg att))
{- Return the internal representation of a signature -}
-
+
internal_Sgn (SG sg) = sg
@@ -548,7 +548,7 @@ symbol_dec (TM tm1 tm2 sg)
-
+
{- declare a new axiom -}
axiom_dec (TM tm (Constant Bool' _ _) sg)
@@ -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
@@ -647,7 +647,7 @@ set_Dec_att (DC dc sg) att
internal_Dec (DC dc sg) = (dc,sg)
-
+
@@ -816,7 +816,7 @@ beta_rw (TH tm sg) i
-{- Eta reduce a subterm of a theorem -}
+{- Eta reduce a subterm of a theorem -}
eta_rw (TH tm sg) i
= case select_trm tm i of
@@ -998,7 +998,7 @@ eq_of_ty _ _ = TH_Err "eq_of_ty error (2)"
from (TM tm1 (Binder Subtype dc tm2 _ _) sg)
= TH (subst_trm dc tm2 tm1) sg
-
+
from _ = TH_Err "from: argument must be term of subtype sort"
@@ -1035,7 +1035,7 @@ weaken (SG sg1) (TH tm sg2)
-
+
set_Thm_att (TH tm sg) iL att
= TH (set_trm_att tm iL att) sg
@@ -1050,7 +1050,7 @@ get_Thm_att (TH tm sg) iL
-
+
{- Restore a theorem from the database -}
restore_Thm s = error "BadTheorem" -- ** exn
@@ -1167,8 +1167,8 @@ write_obj magic_str type_str obj file
| NONE => (write (sgn_dir ^ anon_sgn_name_header ^ name) sgn_rep;
anon_sgn_name_header ^ name)
end
-
-
+
+
val a_chr = fromEnum "a"
and z_chr = fromEnum "z"
and A_chr = fromEnum "A"
@@ -1193,7 +1193,7 @@ write_obj magic_str type_str obj file
(ch = minus_chr) orelse
(ch = underline_chr) orelse
(ch = dot_cht)
- in forall ok_ch (map fromEnum (explode name)) end
+ in vforall ok_ch (map fromEnum (explode name)) end
in (* local *)
@@ -1306,7 +1306,7 @@ typ_of_Thm ( TH tm sg )
shift_Trm i (SG sg1) (TM tm1 tm2 sg2)
= if eq_sgn sg2 sg3
then TM (shift_trm sm i tm1) (shift_trm sm i tm2) sg1
- else TM_Err "shift_Trm: signatures unequal"
+ else TM_Err "shift_Trm: signatures unequal"
where
sg3 = nth_sgn i sg1
sm = get_share_map sg2
diff --git a/real/veritas/Main.hs b/real/veritas/Main.hs
index c0ed8e36..5191a672 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 f6fd733c..82472326 100644
--- a/real/veritas/Sub_Core3.hs
+++ b/real/veritas/Sub_Core3.hs
@@ -6,7 +6,7 @@
*
* Each constructors last argument (of the tuple) is a list of
* information attributes that the parser, unparsers, tactics etc use.
- *
+ *
* Each terms' next to last argument is a list of alternative types the the
* term can have to its natutal type.
*
@@ -246,9 +246,9 @@ eval (Constant T _ _) = True
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 9a6c0fe0..0ec2f1a0 100644
--- a/real/veritas/Vtslib.hs
+++ b/real/veritas/Vtslib.hs
@@ -1,7 +1,7 @@
-module Vtslib( Option(..) , Sum(..) , forall , exists , assoc ,
+module Vtslib( Option(..) , Sum(..) , vforall , exists , assoc ,
haskey , uncurry , curry , for , map' , module Core_datatype )
where
-
+
import Core_datatype
data Option a = NONE | SOME a
@@ -11,12 +11,12 @@ data Sum a b = Inl a | Inr b
{-
(* Apply the predicate p to all the elements of *)
(* a list, and then AND the results together. *)
- N.B. forall & exists rewritten from ML
+ N.B. vforall & exists rewritten from ML
-}
-forall :: ( a -> Bool ) -> [a] -> Bool
+vforall :: ( a -> Bool ) -> [a] -> Bool
-forall p = and . ( map p )
+vforall p = and . ( map p )
@@ -74,7 +74,7 @@ haskey key al
let fun fold e [] = e
| fold e (a::l) = fold (f a e) l
in fold end
-
+
fun foldr f e =
let fun fold [] = e
| fold (a::l) = f a (fold l)
--
GitLab