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

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

  -- * 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)
  , 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
  ) where

import           Control.Applicative         ((<$>), (<*), (*>), (<*>))
import qualified Data.HashMap.Strict         as M
import qualified Data.HashSet                as S
import qualified Data.Text                   as T
import           Text.Parsec
import           Text.Parsec.Expr
import           Text.Parsec.Language
import qualified Text.Parsec.Token           as Token
import           Text.Printf                 (printf)
import           GHC.Generics                (Generic)

import           Data.Char                   (isLower, toUpper)
import           Language.Fixpoint.Bitvector
import           Language.Fixpoint.Errors
import           Language.Fixpoint.Misc      hiding (dcolon)
import           Language.Fixpoint.Smt.Types

import           Language.Fixpoint.Types
import           Language.Fixpoint.Visitor   (foldSort, mapSort)

import           Data.Maybe                  (fromJust, fromMaybe, maybe)

import           Data.Monoid                 (mempty,mconcat)

type Parser = Parsec String Integer

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

languageDef =
  emptyDef { Token.commentStart    = "/* "
           , Token.commentEnd      = " */"
           , Token.commentLine     = "//"
           , Token.identStart      = satisfy (\_ -> False)
           , Token.identLetter     = satisfy (\_ -> 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  :: [Char] -> (String -> Bool) -> Parser Symbol
condIdP chars f
  = do c  <- letter
       cs <- many (satisfy (`elem` chars))
       blanks
       if f (c:cs) then return (symbol $ T.pack $ c:cs) else parserZero

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

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

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
  | isLower (T.head t) = expr cs
  | otherwise          = EVar cs
  where t = symbolText cs
--  <|> try (parens $ condP EIte exprP)

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
  =   try (parens $ sortP)
  <|> try (string "@"    >> varSortP)
  <|> try (string "func" >> funcSortP)
  <|> try (fApp (Left listFTyCon) . single <$> brackets sortP)
  <|> try bvSortP
  <|> try (fApp  <$> (Left <$> fTyConP) <*> sepBy sortP blanks)
  <|> (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)
  <|> (symbolFTycon      <$> locUpperIdP)

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

bvSizeP ss s = do
  parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj"))
  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 Refa
refaP =  try (refa <$> brackets (sepBy predP semi))
     <|> (Refa <$> predP)



refBindP :: Parser Symbol -> Parser Refa -> 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 tP = (,) <$> symbolP <* colon <*> tP

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


mkQual n xts p = Q n ((vv, t) : yts) (subst su p)
  where
    (vv,t):zts = gSorts xts
    yts        = mapFst mkParam <$> zts
    su         = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts

gSorts :: [(a, Sort)] -> [(a, Sort)]
gSorts xts     = [(x, substVars su t) | (x, t) <- xts]
  where
    su         = (`zip` [0..]) . sortNub . concatMap sortVars . map 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


mkParam s      = symbol ('~' `T.cons` toUpper c `T.cons` cs)
  where
    Just (c,cs)= T.uncons $ symbolText s

---------------------------------------------------------------------
-- | 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 <$> many defP

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

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

wfCP :: Parser (WfC ())
wfCP = do reserved "env"
          env <- envP
          reserved "reft"
          r   <- sortedReftP
          return $ wfC env r Nothing ()

subCP :: Parser (SubC ())
subCP = do reserved "env"
           env <- envP
           reserved "grd"
           grd <- predP
           reserved "lhs"
           lhs <- sortedReftP
           reserved "rhs"
           rhs <- sortedReftP
           reserved "id"
           i   <- integer <* spaces
           tag <- tagP
           return $ safeHead "subCP" $ subC env grd 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  =  try (reserved "tag" >> spaces >> (brackets $ sepBy intP semi))
     <|> (return [])

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 = FI cm ws bs gs lts kts qs mempty
  where
    cm     = M.fromList       [(cid c, c)       | Cst c       <- defs]
    ws     =                  [w                | Wfc w       <- defs]
    bs     = bindEnvFromList  [(n, x, r)        | IBind n x r <- defs]
    gs     = fromListSEnv     [(x, RR t mempty) | Con x t     <- defs]
    lts    =                  [(x, t)           | Con x t     <- defs, notFun t]
    kts    = KS $ S.fromList  [k                | Kut k       <- defs]
    qs     =                  [q                | Qul q       <- defs]
    cid    = fromJust . sid
    notFun = not . isFunctionSortedReft . (`RR` trueReft)
---------------------------------------------------------------------
-- | 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' predP

instance Inputable Expr where
  rr' = doParse' exprP

instance Inputable Refa where
  rr' = doParse' refaP

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

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

instance Inputable (FInfo ()) where
  rr' = 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)
-}