{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE PatternGuards             #-}

module Language.Fixpoint.Parse (

  -- * Top Level Class for Parseable Values
    Inputable (..)

  -- * Top Level Class for Parseable Values
  , Parser

  -- * Lexer to add new tokens
  , lexer

  -- * Some Important keyword and parsers
  , reserved, reservedOp
  , parens  , brackets, angles, braces
  , semi    , comma
  , colon   , dcolon
  , whiteSpace
  , blanks
  , pairP

  -- * Parsing basic entities

  --   fTyConP  -- Type constructors
  , lowerIdP    -- Lower-case identifiers
  , upperIdP    -- Upper-case identifiers
  , symbolP     -- Arbitrary Symbols
  , constantP   -- (Integer) Constants
  , integer     -- Integer
  , bindP       -- Binder (lowerIdP <* colon)
  , sortP       -- Sort
  , mkQual      -- constructing qualifiers

  -- * Parsing recursive entities
  , exprP       -- Expressions
  , predP       -- Refinement Predicates
  , funAppP     -- Function Applications
  , qualifierP  -- Qualifiers
  , refaP       -- Refa
  , refP        -- (Sorted) Refinements
  , refDefP     -- (Sorted) Refinements with default binder
  , refBindP    -- (Sorted) Refinements with configurable sub-parsers
  , bvSortP     -- Bit-Vector Sort

  -- * Some Combinators
  , condIdP     -- condIdP  :: [Char] -> (Text -> Bool) -> Parser Text

  -- * Add a Location to a parsed value
  , locParserP
  , locLowerIdP
  , locUpperIdP

  -- * Getting a Fresh Integer while parsing
  , freshIntP

  -- * Parsing Function
  , doParse'
  , parseFromFile
  , remainderP

  -- * Utilities
  , isSmall
  ) where

import Debug.Trace (trace)

import qualified Data.HashMap.Strict         as M
import qualified Data.HashSet                as S
import qualified Data.Text                   as T
import           Data.Maybe                  (fromJust)
import           Text.Parsec
import           Text.Parsec.Expr
import           Text.Parsec.Language        (emptyDef)
import qualified Text.Parsec.Token           as Token
import           Text.Printf                 (printf)
import           GHC.Generics                (Generic)

import           Data.Char                   (isLower)
import           Language.Fixpoint.Smt.Bitvector
import           Language.Fixpoint.Types.Errors
import           Language.Fixpoint.Misc      (sortNub, thd3)
import           Language.Fixpoint.Smt.Types
import           Language.Fixpoint.Types.Names     (headSym)
import           Language.Fixpoint.Types.Visitor   (foldSort, mapSort)
import           Language.Fixpoint.Types

type Parser = Parsec String Integer

--------------------------------------------------------------------

languageDef =
  emptyDef { Token.commentStart    = "/* "
           , Token.commentEnd      = " */"
           , Token.commentLine     = "//"
           , Token.identStart      = satisfy (const False)
           , Token.identLetter     = satisfy (const False)
           , Token.reservedNames   = [ "SAT"
                                     , "UNSAT"
                                     , "true"
                                     , "false"
                                     , "mod"
                                     , "data"
                                     , "Bexp"
                                     , "forall"
                                     , "exists"
                                     , "assume"
                                     , "measure"
                                     , "module"
                                     , "spec"
                                     , "where"
                                     , "True"
                                     , "Int"
                                     , "import"
                                     , "_|_"
                                     , "|"
                                     , "if", "then", "else"
                                     ]
           , Token.reservedOpNames = [ "+", "-", "*", "/", "\\", ":"
                                     , "<", ">", "<=", ">=", "=", "!=" , "/="
                                     , "mod", "and", "or"
                                  --, "is"
                                     , "&&", "||"
                                     , "~", "=>", "==>", "<=>"
                                     , "->"
                                     , ":="
                                     , "&", "^", "<<", ">>", "--"
                                     , "?", "Bexp" -- , "'"
                                     ]
           }

lexer         = Token.makeTokenParser languageDef
reserved      = Token.reserved      lexer
reservedOp    = Token.reservedOp    lexer
parens        = Token.parens        lexer
brackets      = Token.brackets      lexer
angles        = Token.angles        lexer
semi          = Token.semi          lexer
colon         = Token.colon         lexer
comma         = Token.comma         lexer
whiteSpace    = Token.whiteSpace    lexer
stringLiteral = Token.stringLiteral lexer
braces        = Token.braces        lexer
double        = Token.float         lexer
-- integer       = Token.integer       lexer

-- identifier = Token.identifier lexer


blanks  = many (satisfy (`elem` [' ', '\t']))

integer = posInteger

--  try (char '-' >> (negate <$> posInteger))
--       <|> posInteger

posInteger = toI <$> (many1 digit <* spaces)
  where
    toI :: String -> Integer
    toI = read

----------------------------------------------------------------
------------------------- Expressions --------------------------
----------------------------------------------------------------

locParserP :: Parser a -> Parser (Located a)
locParserP p = do l1 <- getPosition
                  x  <- p
                  l2 <- getPosition
                  return $ Loc l1 l2 x


-- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing
-- whitespace, in order to avoid some parsers spanning multiple lines..
condIdP  :: S.HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP chars f
  = do c  <- letter <|> char '_'
       cs <- many (satisfy (`S.member` chars))
       blanks
       if f (c:cs) then return (symbol $ c:cs) else parserZero

upperIdP :: Parser Symbol
upperIdP = condIdP symChars (not . isSmall . head)

lowerIdP :: Parser Symbol
lowerIdP = condIdP symChars (isSmall . head)

isSmall :: Char -> Bool
isSmall c = isLower c || c == '_'

symCharsP :: Parser Symbol
symCharsP = condIdP symChars (`notElem` keyWordSyms)

locLowerIdP = locParserP lowerIdP
locUpperIdP = locParserP upperIdP

symbolP :: Parser Symbol
symbolP = symbol <$> symCharsP

constantP :: Parser Constant
constantP =  try (R <$> double)
         <|> I <$> integer

symconstP :: Parser SymConst
symconstP = SL . T.pack <$> stringLiteral

expr0P :: Parser Expr
expr0P
  =  (fastIfP EIte exprP)
 <|> (ESym <$> symconstP)
 <|> (ECon <$> constantP)
 <|> (reserved "_|_" >> return EBot)
 <|> try (parens  exprP)
 <|> try (parens  exprCastP)
 <|> (charsExpr <$> symCharsP)

charsExpr cs
  | isSmall (headSym cs) = expr cs
  | otherwise            = EVar cs

fastIfP f bodyP
  = do reserved "if"
       p <- predP
       reserved "then"
       b1 <- bodyP
       reserved "else"
       b2 <- bodyP
       return $ f p b1 b2

qmIfP f bodyP
  = parens $ do
      p  <- predP
      reserved "?"
      b1 <- bodyP
      colon
      b2 <- bodyP
      return $ f p b1 b2


expr1P :: Parser Expr
expr1P
  =  try funAppP
 <|> expr0P

exprP :: Parser Expr
exprP = buildExpressionParser bops expr1P

funAppP            =  (try litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
  where
    exprFunSpacesP = EApp <$> funSymbolP <*> sepBy1 expr0P blanks
    exprFunCommasP = EApp <$> funSymbolP <*> parens        (sepBy exprP comma)
    exprFunSemisP  = EApp <$> funSymbolP <*> parenBrackets (sepBy exprP semi)
    funSymbolP     = locParserP symbolP


-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
litP = do reserved "lit"
          l <- stringLiteral
          t <- sortP
          return $ ECon $ L (T.pack l) t

parenBrackets  = parens . brackets

bops = [ [ Prefix (reservedOp "-"   >> return ENeg)]
       , [ Infix  (reservedOp "*"   >> return (EBin Times)) AssocLeft
         , Infix  (reservedOp "/"   >> return (EBin Div  )) AssocLeft
         ]
       , [ Infix  (reservedOp "-"   >> return (EBin Minus)) AssocLeft
         , Infix  (reservedOp "+"   >> return (EBin Plus )) AssocLeft
         ]
       , [ Infix  (reservedOp "mod"  >> return (EBin Mod  )) AssocLeft]
       ]

eMinus     = EBin Minus (expr (0 :: Integer))
-- eCons x xs = EApp (dummyLoc consName) [x, xs]
-- eNil       = EVar nilName

exprCastP
  = do e  <- exprP
       (try dcolon) <|> colon
       so <- sortP
       return $ ECst e so

dcolon = string "::" <* spaces

varSortP  = FVar  <$> parens intP
funcSortP = parens $ FFunc <$> intP <* comma <*> sortsP

sortsP = brackets $ sepBy sortP semi

sortP    :: Parser Sort
sortP    = sortP' (sepBy sortArgP blanks)

sortArgP :: Parser Sort
sortArgP = sortP' (return [])

sortFunP :: Parser Sort
sortFunP
   =  try (string "@" >> varSortP)
  <|> (fTyconSort <$> fTyConP)

sortP' :: Parser [Sort] -> Parser Sort
sortP' appArgsP
   =  try (parens sortP)
  <|> try (string "func" >> funcSortP)
  <|> try (fAppTC listFTyCon . single <$> brackets sortP)
  <|> try bvSortP
  <|> try (fAppTC <$> fTyConP <*> appArgsP)
  <|> try (fApp   <$> tvarP   <*> appArgsP)

single x = [x]

tvarP :: Parser Sort
tvarP
   =  try (string "@" >> varSortP)
  <|> (FObj . symbol <$> lowerIdP)


fTyConP :: Parser FTycon
fTyConP
  =   (reserved "int"     >> return intFTyCon)
  <|> (reserved "Integer" >> return intFTyCon)
  <|> (reserved "Int"     >> return intFTyCon)
  <|> (reserved "int"     >> return intFTyCon)
  <|> (reserved "real"    >> return realFTyCon)
  <|> (reserved "bool"    >> return boolFTyCon)
  <|> (reserved "num"     >> return numFTyCon)
  <|> (symbolFTycon      <$> locUpperIdP)

bvSortP
  = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)

bvSizeP ss s = do
  parens (reserved "BitVec" >> reserved ss)
  return s

keyWordSyms = ["if", "then", "else", "mod"]

---------------------------------------------------------------------
-------------------------- Predicates -------------------------------
---------------------------------------------------------------------


pred0P :: Parser Pred
pred0P =  trueP
      <|> falseP
      <|> try kvarPredP
      <|> try (fastIfP pIte predP)
      <|> try predrP
      <|> try (parens predP)
      <|> try (PBexp <$> (reserved "?" *> exprP))
      <|> try (PBexp <$> funAppP)
      <|> try (reservedOp "&&" >> PAnd <$> predsP)
      <|> try (reservedOp "||" >> POr  <$> predsP)

-- qmP    = reserved "?" <|> reserved "Bexp"

trueP, falseP :: Parser Pred
trueP  = reserved "true"  >> return PTrue
falseP = reserved "false" >> return PFalse

kvarPredP :: Parser Pred
kvarPredP = PKVar <$> kvarP <*> substP

kvarP :: Parser KVar
kvarP = KV <$> (char '$' *> symbolP <* spaces)

substP :: Parser Subst
substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP)
  where
    aP = reserved ":="

predP  :: Parser Pred
predP  = buildExpressionParser lops pred0P


predsP = brackets $ sepBy predP semi


lops = [ [Prefix (reservedOp "~"    >> return PNot)]
       , [Prefix (reservedOp "not " >> return PNot)]
       , [Infix  (reservedOp "&&"   >> return (\x y -> PAnd [x,y])) AssocRight]
       , [Infix  (reservedOp "||"   >> return (\x y -> POr  [x,y])) AssocRight]
       , [Infix  (reservedOp "=>"   >> return PImp) AssocRight]
       , [Infix  (reservedOp "==>"  >> return PImp) AssocRight]
       , [Infix  (reservedOp "<=>"  >> return PIff) AssocRight]]

predrP = do e1    <- exprP
            r     <- brelP
            e2    <- exprP
            return $ r e1 e2

brelP ::  Parser (Expr -> Expr -> Pred)
brelP =  (reservedOp "==" >> return (PAtom Eq))
     <|> (reservedOp "="  >> return (PAtom Eq))
     <|> (reservedOp "~~" >> return (PAtom Ueq))
     <|> (reservedOp "!=" >> return (PAtom Ne))
     <|> (reservedOp "/=" >> return (PAtom Ne))
     <|> (reservedOp "!~" >> return (PAtom Une))
     <|> (reservedOp "<"  >> return (PAtom Lt))
     <|> (reservedOp "<=" >> return (PAtom Le))
     <|> (reservedOp ">"  >> return (PAtom Gt))
     <|> (reservedOp ">=" >> return (PAtom Ge))

----------------------------------------------------------------------------------
------------------------------------ BareTypes -----------------------------------
----------------------------------------------------------------------------------

refaP :: Parser Pred
refaP =  try (pAnd <$> brackets (sepBy predP semi))
     <|> predP



refBindP :: Parser Symbol -> Parser Pred -> Parser (Reft -> a) -> Parser a
refBindP bp rp kindP
  = braces $ do
      x  <- bp
      t  <- kindP
      reserved "|"
      ra <- rp <* spaces
      return $ t (Reft (x, ra))

-- bindP      = symbol    <$> (lowerIdP <* colon)
bindP      = symbolP <* colon
optBindP x = try bindP <|> return x

refP       = refBindP bindP refaP
refDefP x  = refBindP (optBindP x)

---------------------------------------------------------------------
-- | Parsing Qualifiers ---------------------------------------------
---------------------------------------------------------------------

qualifierP tP = do
  pos    <- getPosition
  n      <- upperIdP
  params <- parens $ sepBy1 (sortBindP tP) comma
  _      <- colon
  body   <- predP
  return  $ mkQual n params body pos

sortBindP = pairP symbolP colon

pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP xP sepP yP = (,) <$> xP <* sepP <*> yP

mkQual :: Symbol -> [(Symbol, Sort)] -> Pred -> SourcePos -> Qualifier
mkQual n xts p = Q n ((v, t) : yts) (subst su p)
  where
    (v, t):zts = gSorts xts
    -- yts        = first mkParam <$> zts
    yts        = zts
    su         = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts

-- mkParam :: Symbol -> Symbol
-- mkParam s       = unsafeTextSymbol ('~' `T.cons` toUpper c `T.cons` cs)
--  where
--    Just (c,cs) = T.uncons $ symbolSafeText s

gSorts :: [(a, Sort)] -> [(a, Sort)]
gSorts xts     = [(x, substVars su t) | (x, t) <- xts]
  where
    su         = (`zip` [0..]) . sortNub . concatMap (sortVars . snd) $ xts

substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars su = mapSort tx
  where
    tx (FObj x)
      | Just i <- lookup x su = FVar i
    tx t                      = t

sortVars :: Sort -> [Symbol]
sortVars = foldSort go []
  where
    go b (FObj x) = x : b
    go b _        = b


---------------------------------------------------------------------
-- | Parsing Constraints (.fq files) --------------------------------
---------------------------------------------------------------------

-- Entities in Query File
data Def a
  = Srt Sort
  | Axm Pred
  | Cst (SubC a)
  | Wfc (WfC a)
  | Con Symbol Sort
  | Qul Qualifier
  | Kut KVar
  | IBind Int Symbol SortedReft
  deriving (Show, Generic)
  --  Sol of solbind
  --  Dep of FixConstraint.dep

fInfoP :: Parser (FInfo ())
fInfoP = defsFInfo <$> {-# SCC "many-defP" #-} many defP

defP :: Parser (Def ())
defP =  Srt   <$> (reserved "sort"       >> colon >> sortP)
    <|> Axm   <$> (reserved "axiom"      >> colon >> predP)
    <|> Cst   <$> (reserved "constraint" >> colon >> {-# SCC "subCP" #-} subCP)
    <|> Wfc   <$> (reserved "wf"         >> colon >> {-# SCC "wfCP"  #-} wfCP)
    <|> Con   <$> (reserved "constant"   >> symbolP) <*> (colon >> sortP)
    <|> Qul   <$> (reserved "qualif"     >> qualifierP sortP)
    <|> Kut   <$> (reserved "cut"        >> kvarP)
    <|> IBind <$> (reserved "bind"       >> intP) <*> symbolP <*> (colon >> {-# SCC "sortedReftP" #-} sortedReftP)

sortedReftP :: Parser SortedReft
sortedReftP = refP (RR <$> (sortP <* spaces))

wfCP :: Parser (WfC ())
wfCP = do reserved "env"
          env <- envP
          reserved "reft"
          r   <- sortedReftP
          let [w] = wfC env r ()
          return w

subCP :: Parser (SubC ())
subCP = do pos <- getPosition
           reserved "env"
           env <- envP
           reserved "lhs"
           lhs <- sortedReftP
           reserved "rhs"
           rhs <- sortedReftP
           reserved "id"
           i   <- integer <* spaces
           tag <- tagP
           pos' <- getPosition
           return $ subC' env lhs rhs i tag pos pos'

subC' env lhs rhs i tag l l'
  = case cs of
      [c] -> c
      _   -> die $ err (SS l l') $ printf "RHS without single conjunct at %s \n" (show l')
    where
       cs = subC env lhs rhs (Just i) tag ()

-- idVV :: Integer -> SortedReft -> SortedReft
-- idVV i sr = sr {sr_reft = ri }
--   where
--     ri    = shiftVV r vvi
--     r     = sr_reft sr
--     vvi   = vv $ Just i


tagP  :: Parser [Int]
tagP  = reserved "tag" >> spaces >> (brackets $ sepBy intP semi)

envP  :: Parser IBindEnv
envP  = do binds <- brackets $ sepBy (intP <* spaces) semi
           return $ insertsIBindEnv binds emptyIBindEnv

intP :: Parser Int
intP = fromInteger <$> integer

defsFInfo :: [Def a] -> FInfo a
defsFInfo defs = {-# SCC "defsFI" #-} FI cm ws bs lts kts qs mempty mempty
  where
    cm     = M.fromList       [(cid c, c)       | Cst c       <- defs]
    ws     = M.fromList       [(thd3 $ wrft w, w) | Wfc w     <- defs]
    bs     = bindEnvFromList  [(n, x, r)        | IBind n x r <- defs]
    lts    = fromListSEnv     [(x, t)           | Con x t     <- defs]
    kts    = KS $ S.fromList  [k                | Kut k       <- defs]
    qs     =                  [q                | Qul q       <- defs]
    cid    = fromJust . sid
    -- msg    = show $ "#Lits = " ++ (show $ length consts)

---------------------------------------------------------------------
-- | Interacting with Fixpoint --------------------------------------
---------------------------------------------------------------------

fixResultP :: Parser a -> Parser (FixResult a)
fixResultP pp
  =  (reserved "SAT"   >> return Safe)
 <|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma))
 <|> (reserved "CRASH" >> crashP pp)

crashP pp
  = do i   <- pp
       msg <- many anyChar
       return $ Crash [i] msg

predSolP
  = parens $ (predP  <* (comma >> iQualP))


iQualP
  = upperIdP >> (parens $ sepBy symbolP comma)

solution1P
  = do reserved "solution:"
       k  <- kvP
       reserved ":="
       ps <- brackets $ sepBy predSolP semi
       return (k, simplify $ PAnd ps)
    where
      kvP = try kvarP <|> (KV <$> symbolP)

solutionP :: Parser (M.HashMap KVar Pred)
solutionP
  = M.fromList <$> sepBy solution1P whiteSpace

solutionFileP
  = (,) <$> fixResultP integer <*> solutionP

------------------------------------------------------------------------

remainderP p
  = do res <- p
       str <- getInput
       pos <- getPosition
       return (res, str, pos)

doParse' parser f s
  = case runParser (remainderP (whiteSpace >> parser)) 0 f s of
      Left e            -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f
      Right (r, "", _)  -> r
      Right (_, rem, l) -> die $ err (SS l l)
                               $ printf "doParse has leftover when parsing: %s\nfrom file %s\n" rem f

errorSpan e = SS l l where l = errorPos e

parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile p f = doParse' p f <$> readFile f

freshIntP :: Parser Integer
freshIntP = do n <- getState
               updateState (+ 1)
               return n

---------------------------------------------------------------------
-- Standalone SMTLIB2 commands --------------------------------------
---------------------------------------------------------------------

commandsP = sepBy commandP semi

commandP
  =  (reserved "var"      >> cmdVarP)
 <|> (reserved "push"     >> return Push)
 <|> (reserved "pop"      >> return Pop)
 <|> (reserved "check"    >> return CheckSat)
 <|> (reserved "assert"   >> (Assert Nothing <$> predP))
 <|> (reserved "distinct" >> (Distinct <$> (brackets $ sepBy exprP comma)))

cmdVarP
  = do x <- bindP
       t <- sortP
       return $ Declare x [] t


---------------------------------------------------------------------
-- Bundling Parsers into a Typeclass --------------------------------
---------------------------------------------------------------------

class Inputable a where
  rr  :: String -> a
  rr' :: String -> String -> a
  rr' _ = rr
  rr    = rr' ""

instance Inputable Symbol where
  rr' = doParse' symbolP

instance Inputable Constant where
  rr' = doParse' constantP

instance Inputable Pred where
  rr' = doParse' refaP

instance Inputable Expr where
  rr' = doParse' exprP

instance Inputable (FixResult Integer) where
  rr' = doParse' $ fixResultP integer

instance Inputable (FixResult Integer, FixSolution) where
  rr' = doParse' solutionFileP

instance Inputable (FInfo ()) where
  rr' = {-# SCC "fInfoP" #-} doParse' fInfoP

instance Inputable Command where
  rr' = doParse' commandP

instance Inputable [Command] where
  rr' = doParse' commandsP

{-
---------------------------------------------------------------
--------------------------- Testing ---------------------------
---------------------------------------------------------------

-- A few tricky predicates for parsing
-- myTest1 = "((((v >= 56320) && (v <= 57343)) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o ((i - o) - 1)))) && (((numchars a o (i - (o -1))) >= 0) && (((i - o) - 1) >= 0)))) && ((not (((v >= 56320) && (v <= 57343)))) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o (i - o)))) && ((numchars a o (i - o)) >= 0))))"
--
-- myTest2 = "len x = len y - 1"
-- myTest3 = "len x y z = len a b c - 1"
-- myTest4 = "len x y z = len a b (c - 1)"
-- myTest5 = "x >= -1"
-- myTest6 = "(bLength v) = if n > 0 then n else 0"
-- myTest7 = "(bLength v) = (if n > 0 then n else 0)"
-- myTest8 = "(bLength v) = (n > 0 ? n : 0)"


sa  = "0"
sb  = "x"
sc  = "(x0 + y0 + z0) "
sd  = "(x+ y * 1)"
se  = "_|_ "
sf  = "(1 + x + _|_)"
sg  = "f(x,y,z)"
sh  = "(f((x+1), (y * a * b - 1), _|_))"
si  = "(2 + f((x+1), (y * a * b - 1), _|_))"

s0  = "true"
s1  = "false"
s2  = "v > 0"
s3  = "(0 < v && v < 100)"
s4  = "(x < v && v < y+10 && v < z)"
s6  = "[(v > 0)]"
s6' = "x"
s7' = "(x <=> y)"
s8' = "(x <=> a = b)"
s9' = "(x <=> (a <= b && b < c))"

s7  = "{ v: Int | [(v > 0)] }"
s8  = "x:{ v: Int | v > 0 } -> {v : Int | v >= x}"
s9  = "v = x+y"
s10 = "{v: Int | v = x + y}"

s11 = "x:{v:Int | true } -> {v:Int | true }"
s12 = "y : {v:Int | true } -> {v:Int | v = x }"
s13 = "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
s14 = "x:{v:a  | true} -> y:{v:b | true } -> {v:a | (x < v && v < y) }"
s15 = "x:Int -> Bool"
s16 = "x:Int -> y:Int -> {v:Int | v = x + y}"
s17 = "a"
s18 = "x:a -> Bool"
s20 = "forall a . x:Int -> Bool"

s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }"

r0  = (rr s0) :: Pred
r0' = (rr s0) :: [Refa]
r1  = (rr s1) :: [Refa]


e1, e2  :: Expr
e1  = rr "(k_1 + k_2)"
e2  = rr "k_1"

o1, o2, o3 :: FixResult Integer
o1  = rr "SAT "
o2  = rr "UNSAT [1, 2, 9,10]"
o3  = rr "UNSAT []"

-- sol1 = doParse solution1P "solution: k_5 := [0 <= VV_int]"
-- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]"

b0, b1, b2, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13 :: BareType
b0  = rr "Int"
b1  = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
b2  = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x - y}"
b4  = rr "forall a . x : a -> Bool"
b5  = rr "Int -> Int -> Int"
b6  = rr "(Int -> Int) -> Int"
b7  = rr "({v: Int | v > 10} -> Int) -> Int"
b8  = rr "(x:Int -> {v: Int | v > x}) -> {v: Int | v > 10}"
b9  = rr "x:Int -> {v: Int | v > x} -> {v: Int | v > 10}"
b10 = rr "[Int]"
b11 = rr "x:[Int] -> {v: Int | v > 10}"
b12 = rr "[Int] -> String"
b13 = rr "x:(Int, [Bool]) -> [(String, String)]"

-- b3 :: BareType
-- b3  = rr "x:Int -> y:Int -> {v:Bool | ((v is True) <=> x = y)}"

m1 = ["len :: [a] -> Int", "len (Nil) = 0", "len (Cons x xs) = 1 + len(xs)"]
m2 = ["tog :: LL a -> Int", "tog (Nil) = 100", "tog (Cons y ys) = 200"]

me1, me2 :: Measure.Measure BareType Symbol
me1 = (rr $ intercalate "\n" m1)
me2 = (rr $ intercalate "\n" m2)
-}
