removed legacy BoolT and IntT, replaced by classes Boolean and Intege…

…r. Types in L4 files should now also be Boolean / Integer. Renamed UBneg to UBnot
smucclaw · May 28, 2021 · 1549feb · 1549feb
1 parent ec7ee76
commit 1549feb
Show file tree

Hide file tree

Showing 14 changed files with 68 additions and 108 deletions.
diff --git a/l4/mini.l4 b/l4/mini.l4
@@ -8,17 +8,17 @@ IncompatibleWithDignity -> "incompatible with dignity of legal profession"
 # r34_1_a_applies -> "rule 341 applies"
 
 class Business {
-    DetractsFromDignity: Bool         # has lexicon entry
-    IncompatibleWithDignity: Bool     # has lexicon entry
-    DerogatesFromDignity: Bool        # has lexicon entry
-    UnauthorizedSharingFees : Bool    # has lexicon entry
-    DescribedInSectionOne : Bool         # rest parsed from the predicate name
-    Unfair: Bool
-    DescribedInFirstSchedule: Bool
-    Prohibited: Bool
+    DetractsFromDignity: Boolean         # has lexicon entry
+    IncompatibleWithDignity: Boolean     # has lexicon entry
+    DerogatesFromDignity: Boolean        # has lexicon entry
+    UnauthorizedSharingFees : Boolean    # has lexicon entry
+    DescribedInSectionOne : Boolean         # rest parsed from the predicate name
+    Unfair: Boolean
+    DescribedInFirstSchedule: Boolean
+    Prohibited: Boolean
 }
 
-decl r34_1_a_applies: Business -> Bool
+decl r34_1_a_applies: Business -> Boolean
 
 rule <r34_1_a>
 for b: Business

diff --git a/l4/rps.l4 b/l4/rps.l4
@@ -13,16 +13,16 @@ Sign -> "sign_2_N"
 Game -> "game_1_N"
 
 class Sign {
-    beat : Sign -> Bool
+    beat : Sign -> Boolean
 }
 
 class Player {
-    throw : Sign -> Bool
+    throw : Sign -> Boolean
 }
 
 class Game {
-    participate_in : Player -> Bool
-    win : Player -> Bool
+    participate_in : Player -> Boolean
+    win : Player -> Boolean
 }
 
 

diff --git a/src/Error.hs b/src/Error.hs
@@ -50,8 +50,8 @@ printVarName = id
 
 printTp :: Tp -> String
 printTp t = case t of
-  BoolT -> "Bool"
-  IntT -> "Int"
+  ClassT (ClsNm "Boolean") -> "Bool"
+  ClassT (ClsNm "Integer") -> "Integer"
   ClassT cn -> printClassName cn
   FunT t1 t2 -> "(" ++ printTp t1 ++ " -> " ++ printTp t2 ++")"
   TupleT [] -> "()"

diff --git a/src/Exec.hs b/src/Exec.hs
@@ -13,7 +13,7 @@ lift_uarith_op u c = case (u, c) of
 
 lift_ubool_op :: UBoolOp -> Val -> Val
 lift_ubool_op u c = case (u, c) of
-  (UBneg, BoolV b) -> BoolV (not b)
+  (UBnot, BoolV b) -> BoolV (not b)
   _ -> ErrV
 
 lift_unaop_expr :: UnaOp -> Expr Tp -> Expr Tp

diff --git a/src/Parser.y b/src/Parser.y
@@ -153,8 +153,8 @@ Assertion : assert KVMap Expr      { Assertion (tokenRange $1 $3) $2 $3 }
 -- Atomic type
 -- Used to resolve ambigouity of     \x : A -> B -> x
 -- and force the use of parenthesis: \x : (A -> B) -> x
-ATp  : Bool                       { L (getLoc $1) BoolT }
-     | Int                        { L (getLoc $1) IntT }
+ATp  : Bool                       { L (getLoc $1) booleanT }
+     | Int                        { L (getLoc $1) integerT }
      | VAR                        { L (getLoc $1) $ ClassT (ClsNm $ tokenSym $1) }
      | '(' TpsCommaSep ')'        { L (getLoc $2) $ case $2 of [t] -> unLoc t; tcs -> TupleT (map unLoc $ reverse tcs) }
 
@@ -180,7 +180,7 @@ Expr : '\\' Pattern ':' ATp '->' Expr  { FunE (tokenRange $1 $6) $2 (unLoc $4) $
      | Expr '||' Expr              { BinOpE (tokenRange $1 $3) (BBool BBor) $1 $3 }
      | Expr '&&' Expr              { BinOpE (tokenRange $1 $3) (BBool BBand) $1 $3 }
      | if Expr then Expr else Expr { IfThenElseE (tokenRange $1 $6) $2 $4 $6 }
-     | not Expr                    { UnaOpE (tokenRange $1 $2) (UBool UBneg) $2 }
+     | not Expr                    { UnaOpE (tokenRange $1 $2) (UBool UBnot) $2 }
      | not derivable VAR           { NotDeriv (tokenRange $1 $3) True (VarE (tokenPos $3) (GlobalVar $ tokenSym $3)) }
      | not derivable not VAR       { NotDeriv (tokenRange $1 $4) False (VarE (tokenPos $4) (GlobalVar $ tokenSym $4)) }
      | not derivable VAR Atom      { NotDeriv (tokenRange $1 $4) True (AppE (tokenRange $3 $4)  (VarE (tokenPos $3) (GlobalVar $ tokenSym $3)) $4) }

diff --git a/src/PrintProg.hs b/src/PrintProg.hs
@@ -24,7 +24,7 @@ printVar (LocalVar vn i) = vn
 
 printUnaOpE :: UnaOp -> String
 printUnaOpE (UArith UAminus) = "-"
-printUnaOpE (UBool UBneg) = "not "
+printUnaOpE (UBool UBnot) = "not "
 
 printBinOpE :: BinOp -> String
 printBinOpE (BArith b1) =

diff --git a/src/RuleTransfo.hs b/src/RuleTransfo.hs
@@ -13,27 +13,19 @@ import Data.List (sortBy)
 -- Logical infrastructure: macros for simplifying formula construction
 ----------------------------------------------------------------------
 
-boolT :: Tp
-boolT = ClassT (ClsNm "Boolean")
 
-trueV :: Expr Tp
-trueV = ValE boolT (BoolV True)
 
-falseV :: Expr Tp
-falseV = ValE boolT (BoolV False)
-
--- TODO: UBneg should be renamed to UBnot
 not :: Expr Tp -> Expr Tp
-not = UnaOpE boolT (UBool UBneg)
+not = UnaOpE booleanT (UBool UBnot)
 
 conj :: Expr Tp -> Expr Tp -> Expr Tp
-conj = BinOpE boolT (BBool BBand)
+conj = BinOpE booleanT (BBool BBand)
 
 disj :: Expr Tp -> Expr Tp -> Expr Tp
-disj = BinOpE boolT (BBool BBor)
+disj = BinOpE booleanT (BBool BBor)
 
 impl :: Expr Tp -> Expr Tp -> Expr Tp
-impl = BinOpE boolT (BBool BBimpl)
+impl = BinOpE booleanT (BBool BBimpl)
 
 conjs :: [Expr Tp] -> Expr Tp
 conjs [] = trueV
@@ -46,7 +38,7 @@ disjs [e] = e
 disjs (e:es) = disj e (disjs es)
 
 eq  :: Expr Tp -> Expr Tp -> Expr Tp
-eq = BinOpE (ClassT (ClsNm "Boolean")) (BCompar BCeq)
+eq = BinOpE booleanT (BCompar BCeq)
 
 ----------------------------------------------------------------------
 -- Logical infrastructure: computing normal forms
@@ -126,7 +118,7 @@ swapQuantif All = Ex
 swapQuantif Ex  = All
 
 prenexUnary :: t -> UBoolOp -> Expr t -> Expr t
-prenexUnary t UBneg (QuantifE tq q vn vt et) = QuantifE tq (swapQuantif q) vn vt (UnaOpE t (UBool UBneg) et)
+prenexUnary t UBnot (QuantifE tq q vn vt et) = QuantifE tq (swapQuantif q) vn vt (UnaOpE t (UBool UBnot) et)
 prenexUnary t u e = UnaOpE t (UBool u) e
 
 prenexBinary :: t -> BBoolOp -> Expr t -> Expr t -> Expr t
@@ -151,7 +143,7 @@ ruleToFormula r = abstract All (varDeclsOfRule r) (impl (precondOfRule r) (postc
 abstract :: Quantif -> [VarDecl Tp] -> Expr Tp -> Expr Tp
 abstract q vds e
   = foldr
-      (\ vd -> QuantifE boolT q (nameOfVarDecl vd) (tpOfVarDecl vd)) e
+      (\ vd -> QuantifE booleanT q (nameOfVarDecl vd) (tpOfVarDecl vd)) e
       vds
 
 -------------------------------------------------------------
@@ -281,7 +273,7 @@ ruleExLInvStep r =
           rmpPostc = zip [ll + 1 .. lvds - 1] [ll .. lvds - 2]
           rmpPrec  = (ll, 0) : zip [0 .. ll - 1] [1 .. ll]
           newPostc = remapExpr rmpPostc postc
-          newPrec = QuantifE boolT Ex (nameOfVarDecl d) (tpOfVarDecl d) (remapExpr rmpPrec prec)
+          newPrec = QuantifE booleanT Ex (nameOfVarDecl d) (tpOfVarDecl d) (remapExpr rmpPrec prec)
       in [r{varDeclsOfRule = reverse (lowers++uppers)}{precondOfRule = newPrec}{postcondOfRule = newPostc}]
     _ -> error "internal error in splitDecls: "
 
@@ -323,7 +315,7 @@ rulesInversion rls =
   let r1 = head rls
       (VarE _ f, args) = appToFunArgs [] (postcondOfRule r1)
       rn = nameOfVar f ++ "Inversion"
-  in Rule boolT rn (varDeclsOfRule r1) (postcondOfRule r1) (disjs (map precondOfRule rls))
+  in Rule booleanT rn (varDeclsOfRule r1) (postcondOfRule r1) (disjs (map precondOfRule rls))
 
 
 -- Adds negated precondition of r1 to r2. Corresponds to:

diff --git a/src/Smt.hs b/src/Smt.hs
@@ -120,7 +120,7 @@ transUArithOp :: UArithOp ->  SExpr -> SExpr
 transUArithOp UAminus = SMT.neg
 
 transUBoolOp :: UBoolOp ->  SExpr -> SExpr
-transUBoolOp UBneg = SMT.not
+transUBoolOp UBnot = SMT.not
 
 transUnaOp :: UnaOp -> SExpr -> SExpr
 transUnaOp (UArith ua) = transUArithOp ua

diff --git a/src/SmtSBV.hs b/src/SmtSBV.hs
@@ -145,7 +145,7 @@ transExprPredicate env (ValE _ _) =
     error "internal error in transExprPredicate: non-boolean value"
 transExprPredicate env (VarE _ (GlobalVar vn)) =
     return (lookupEnvSBool env vn)
-transExprPredicate env (UnaOpE _ (UBool UBneg) e) =
+transExprPredicate env (UnaOpE _ (UBool UBnot) e) =
     do re <- transExprPredicate env e
        return (sNot re)
        {-
@@ -226,7 +226,7 @@ transExprSBool env (ValE _ (BoolV b)) = if b then sTrue else sFalse
 transExprSBool env (ValE _ _) =
     error "internal error in transExprPredicate: non-boolean value"
 transExprSBool env (VarE _ (GlobalVar vn)) = lookupEnvSBool env vn
-transExprSBool env (UnaOpE _ (UBool UBneg) e) = sNot (transExprSBool env e)
+transExprSBool env (UnaOpE _ (UBool UBnot) e) = sNot (transExprSBool env e)
 transExprSBool env _ = error "in transExprSBool"
 
 --transToPredicateSingle:: Provable a => VarDecl t -> Expr t -> a
@@ -307,7 +307,7 @@ transUArithOpDyn :: UArithOp ->  SVal -> SVal
 transUArithOpDyn UAminus = svUNeg
 
 transUBoolOpDyn :: UBoolOp ->  SVal -> SVal
-transUBoolOpDyn UBneg = svNot
+transUBoolOpDyn UBnot = svNot
 
 transUnaOpDyn :: UnaOp -> SVal -> SVal
 transUnaOpDyn (UArith ua) = transUArithOpDyn ua

diff --git a/src/Syntax.hs b/src/Syntax.hs
@@ -84,15 +84,22 @@ data ErrorCause
 -- TODO: also types have to be annotated with position information
 -- for the parser to do the right job
 data Tp
-  = BoolT
-  | IntT
-  | ClassT ClassName
+  = ClassT ClassName
   | FunT {funTp :: Tp, argTp :: Tp}
   | TupleT [Tp]
   | ErrT ErrorCause
   | OkT                    -- fake type appearing in constructs (classes, rules etc.) that do not have a genuine type
   deriving (Eq, Ord, Show, Read, Data, Typeable)
 
+
+booleanT :: Tp
+booleanT = ClassT (ClsNm "Boolean")
+integerT :: Tp
+integerT = ClassT (ClsNm "Integer")
+stringT :: Tp
+stringT = ClassT (ClsNm "String")
+
+
 data VarDecl t = VarDecl {annotOfVarDecl ::t
                          , nameOfVarDecl :: VarName
                          , tpOfVarDecl :: Tp }
@@ -110,7 +117,6 @@ instance HasLoc t => HasLoc (Mapping t) where
 data FieldDecl t = FieldDecl {annotOfFieldDecl ::t
                              , nameOfFieldDecl :: FieldName
                              , tpOfFieldDecl ::  Tp }
-                            -- FieldAttribs
   deriving (Eq, Ord, Show, Read, Functor, Data, Typeable)
 instance HasLoc t => HasLoc (FieldDecl t) where
   getLoc = getLoc . annotOfFieldDecl
@@ -180,6 +186,11 @@ data Val
     | ErrV
   deriving (Eq, Ord, Show, Read, Data, Typeable)
 
+trueV :: Expr Tp
+trueV = ValE booleanT (BoolV True)
+falseV :: Expr Tp
+falseV = ValE booleanT (BoolV False)
+
 data Var
       -- global variable only known by its name
     = GlobalVar { nameOfVar :: VarName }
@@ -193,7 +204,7 @@ data UArithOp = UAminus
   deriving (Eq, Ord, Show, Read, Data, Typeable)
 
 -- unary boolean operators
-data UBoolOp = UBneg
+data UBoolOp = UBnot
   deriving (Eq, Ord, Show, Read, Data, Typeable)
 
 -- unary operators (union of the above)
@@ -281,42 +292,9 @@ childExprs x = case x of
 allSubExprs :: Expr t -> [Expr t]
 allSubExprs e = e : concatMap allSubExprs (childExprs e)
 
-{-
-annotOfExpr :: Expr t -> t
-annotOfExpr x = case x of
-  ValE        t _       -> t
-  VarE        t _       -> t
-  UnaOpE      t _ _     -> t
-  BinOpE      t _ _ _   -> t
-  IfThenElseE t _ _ _   -> t
-  AppE        t _ _     -> t
-  FunE        t _ _ _   -> t
-  QuantifE    t _ _ _ _ -> t
-  FldAccE     t _ _     -> t
-  TupleE      t _       -> t
-  CastE       t _ _     -> t
-  ListE       t _ _     -> t
-  NotDeriv    t _ _     -> t
--}
 
 updAnnotOfExpr :: (a -> a) -> Expr a -> Expr a
 updAnnotOfExpr f e = e {annotOfExpr = f (annotOfExpr e)}
-{-
-updAnnotOfExpr f x = case x of
-  ValE        t a       -> ValE (f t) a
-  VarE        t a       -> VarE (f t) a
-  UnaOpE      t a b     -> UnaOpE (f t) a b
-  BinOpE      t a b c   -> BinOpE (f t) a b c
-  IfThenElseE t a b c   -> IfThenElseE (f t) a b c
-  AppE        t a b     -> AppE (f t) a b
-  FunE        t a b c   -> FunE (f t) a b c
-  QuantifE    t a b c d -> QuantifE (f t) a b c d
-  FldAccE     t a b     -> FldAccE (f t) a b
-  TupleE      t a       -> TupleE (f t) a
-  CastE       t a b     -> CastE (f t) a b
-  ListE       t a b     -> ListE (f t) a b
-  NotDeriv    t a b     -> NotDeriv (f t) a b
--}
 
 instance HasLoc t => HasLoc (Expr t) where
   getLoc e = getLoc (annotOfExpr e)

diff --git a/src/ToDA2.hs b/src/ToDA2.hs
@@ -56,7 +56,7 @@ instance (Show t) => DSYaml (DSBlock t) where
 --                               , fieldsOfClassDef = [ FieldDecl { annotOfFieldDecl = _
 --                                                                , nameOfFieldDecl = FldNm "beat"
 --                                                                , tpOfFieldDecl = FunT
---                                                                    ( ClassT ( ClsNm "Sign" ) ) BoolT }]} }
+--                                                                    ( ClassT ( ClsNm "Sign" ) ) booleanT}]} }
 --
 -- ClassDecl { annotOfClassDecl = _
 --           , nameOfClassDecl = ClsNm "Player"
@@ -65,7 +65,7 @@ instance (Show t) => DSYaml (DSBlock t) where
 --                                                            , ClsNm "Object" ]
 --                                       , fieldsOfClassDef = [ FieldDecl { annotOfFieldDecl = _ 
 --                                                                        , nameOfFieldDecl = FldNm "throw"
---                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Sign" ) ) BoolT } ] } }
+--                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Sign" ) ) booleanT } ] } }
 
 -- ClassDecl { annotOfClassDecl = _
 --           , nameOfClassDecl = ClsNm "Game"
@@ -74,11 +74,11 @@ instance (Show t) => DSYaml (DSBlock t) where
 --                                                            , ClsNm "Object" ]
 --                                       , fieldsOfClassDef = [ FieldDecl { annotOfFieldDecl = _
 --                                                                        , nameOfFieldDecl = FldNm "participate_in"
---                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Player" ) ) BoolT
+--                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Player" ) ) booleanT
 --                                                                        }
 --                                                            , FieldDecl { annotOfFieldDecl = _
 --                                                                        , nameOfFieldDecl = FldNm "win"
---                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Player" ) ) BoolT
+--                                                                        , tpOfFieldDecl = FunT ( ClassT ( ClsNm "Player" ) ) booleanT
 --                                                                        }
 --                                                            ] } } ]
 
@@ -111,11 +111,11 @@ fieldDeclToBlock (FieldDecl _ (FldNm fldnm) fieldtype) =
           }
 
 eitherTp :: String -> a -> Tp -> Either String a
-eitherTp x1 x2 tp = if elem tp [BoolT, IntT] then Right x2 else Left x1
+eitherTp x1 x2 tp = if elem tp [booleanT, integerT] then Right x2 else Left x1
 
 showFTname :: Tp -> Maybe String 
 showFTname tp = case tp of 
-  (FunT x BoolT)        -> showFTname x
+  (FunT x (ClassT (ClsNm "Boolean")))        -> showFTname x
   (ClassT (ClsNm name)) -> Just $ lowercase name
   _                     -> Nothing
 
@@ -141,6 +141,6 @@ instance DSYaml (Program Tp) where
 
 instance DSYaml Tp where
   showDS tp = case tp of
-    BoolT         -> "Boolean"
-    IntT          -> "Number"
+    (ClassT (ClsNm "Boolean")) -> "Boolean"
+    (ClassT (ClsNm "Integer")) -> "Number"
     _             -> "Unsupported Type"
diff --git a/src/ToGF/NormalizeSyntax.hs b/src/ToGF/NormalizeSyntax.hs
@@ -45,7 +45,7 @@ normalizeQuantifGF r = r { varDeclsOfRule = [],
     wrapInExistential [] e = e
     wrapInExistential (VarDecl ann nm tp:xs) e = wrapInExistential xs (QuantifE ann Ex nm tp e)
 negateExpr :: Expr t -> Expr t
-negateExpr e = UnaOpE (annotOfExpr e) (UBool UBneg) e
+negateExpr e = UnaOpE (annotOfExpr e) (UBool UBnot) e
 
 extractName :: Expr t -> String
 extractName (ValE t v) = "someVal"