check if Elit is needed

ucsd-progsys · Sep 30, 2015 · fa30bdc · fa30bdc
1 parent 858f020
commit fa30bdc
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 10 deletions.
diff --git a/src/Language/Fixpoint/PrettyPrint.hs b/src/Language/Fixpoint/PrettyPrint.hs
@@ -132,7 +132,7 @@ instance PPrint Expr where
   pprintPrec _ (ESym c)        = pprint c
   pprintPrec _ (ECon c)        = pprint c
   pprintPrec _ (EVar s)        = pprint s
-  pprintPrec _ (ELit s _)      = pprint s
+--   pprintPrec _ (ELit s _)      = pprint s
   pprintPrec _ (EBot)          = text "_|_"
   pprintPrec z (ENeg e)        = parensIf (z > zn) $
                                    text "-" <> pprintPrec (zn+1) e

diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -96,7 +96,7 @@ instance SMTLIB2 Expr where
   smt2 (ESym z)         = smt2 z
   smt2 (ECon c)         = smt2 c
   smt2 (EVar x)         = smt2 x
-  smt2 (ELit x _)       = smt2 x
+--   smt2 (ELit x _)       = smt2 x
   smt2 (EApp f es)      = smt2App f es
   smt2 (ENeg e)         = format "(- {})"         (Only $ smt2 e)
   smt2 (EBin o e1 e2)   = format "({} {} {})"     (smt2 o, smt2 e1, smt2 e2)

diff --git a/src/Language/Fixpoint/Sort.hs b/src/Language/Fixpoint/Sort.hs
@@ -162,7 +162,7 @@ checkExpr f (EBin o e1 e2) = checkOp f e1 o e2
 checkExpr f (EIte p e1 e2) = checkIte f p e1 e2
 checkExpr f (ECst e t)     = checkCst f t e
 checkExpr f (EApp g es)    = checkApp f Nothing g es
-checkExpr f (ELit _ t)     = return t
+-- checkExpr f (ELit _ t)     = return t
 
 -- | Helper for checking symbol occurrences
 

diff --git a/src/Language/Fixpoint/Types.hs b/src/Language/Fixpoint/Types.hs
@@ -66,7 +66,7 @@ module Language.Fixpoint.Types (
   , Constant (..)
   , Bop (..), Brel (..)
   , Expr (..), Pred (..)
-  , eVar
+  , eVar, elit
   , eProp
   , pAnd, pOr, pIte
   , isTautoPred
@@ -224,7 +224,7 @@ exprSymbols :: Expr -> [Symbol]
 exprSymbols = go
   where
     go (EVar x)        = [x]
-    go (ELit x _)      = [val x]
+--     go (ELit x _)      = [val x]
     go (EApp f es)     = val f : concatMap go es
     go (ENeg e)        = go e
     go (EBin _ e1 e2)  = go e1 ++ go e2
@@ -459,7 +459,7 @@ data Bop  = Plus | Minus | Times | Div | Mod
 data Expr = ESym !SymConst
           | ECon !Constant
           | EVar !Symbol
-          | ELit !LocSymbol !Sort
+--           | ELit !LocSymbol !Sort
           | EApp !LocSymbol ![Expr]
           | ENeg !Expr
           | EBin !Bop !Expr !Expr
@@ -468,6 +468,8 @@ data Expr = ESym !SymConst
           | EBot
           deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
+elit l s = ECon $ L (symbolText $ val l) s 
+
 instance Fixpoint Integer where
   toFix = integer
 
@@ -513,7 +515,7 @@ instance Fixpoint Expr where
   toFix (ESym c)       = toFix $ encodeSymConst c
   toFix (ECon c)       = toFix c
   toFix (EVar s)       = toFix s
-  toFix (ELit s _)     = toFix s
+--   toFix (ELit s _)     = toFix s
   toFix (EApp f es)    = toFix f <> parens (toFix es)
   toFix (ENeg e)       = parens $ text "-"  <+> parens (toFix e)
   toFix (EBin o e1 e2) = parens $ toFix e1  <+> toFix o <+> toFix e2
@@ -1343,8 +1345,7 @@ instance NFData Expr where
   rnf (ESym x)        = rnf x
   rnf (ECon x)        = rnf x
   rnf (EVar x)        = rnf x
-  -- rnf (EDat x1 x2)    = rnf x1 `seq` rnf x2
-  rnf (ELit x1 x2)    = rnf x1 `seq` rnf x2
+--   rnf (ELit x1 x2)    = rnf x1 `seq` rnf x2
   rnf (EApp x1 x2)    = rnf x1 `seq` rnf x2
   rnf (ENeg x1)       = rnf x1
   rnf (EBin x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3

diff --git a/src/Language/Fixpoint/Visitor.hs b/src/Language/Fixpoint/Visitor.hs
@@ -137,7 +137,7 @@ visitExpr v = vE
     step _ e@EBot         = return e
     step _ e@(ESym _)     = return e
     step _ e@(ECon _)     = return e
-    step _ e@(ELit _ _)   = return e
+--     step _ e@(ELit _ _)   = return e
     step _ e@(EVar _)     = return e
     step c (EApp f es)    = EApp f     <$> (vE c <$$> es)
     step c (ENeg e)       = ENeg       <$> vE c e