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

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)

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

  -- * 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           Control.Monad
import qualified Data.HashMap.Strict         as M
import qualified Data.HashSet                as S
import           Data.Text                   (Text)
import qualified Data.Text                   as T
import           Text.Parsec
import           Text.Parsec.Expr
import           Text.Parsec.Language
import           Text.Parsec.Pos
import           Text.Parsec.String          hiding (Parser, parseFromFile)
import qualified Text.Parsec.Token           as Token
import           Text.Printf                 (printf)

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

import           Data.Maybe                  (fromJust, maybe)

import           Data.Monoid                 (mempty)

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 = liftM2 Loc getPosition p

-- 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)

locLowerIdP = locParserP lowerIdP
locUpperIdP = locParserP upperIdP

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

constantP :: Parser Constant
constantP = try (liftM R double) <|> liftM 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


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

exprP :: Parser Expr
exprP = buildExpressionParser bops expr1P

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


-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
litP = do reserved "lit"
          l <- stringLiteral
          s <- try (bvSortP "Size32" S32) <|> bvSortP "Size64" S64
          return $ ECon $ L (T.pack l) (mkSort s)
  where
    bvSortP ss s = do parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj"))
                      return s


-- ORIG exprP :: Parser Expr
-- ORIG exprP =  expr2P <|> lexprP
--
-- ORIG lexprP :: Parser Expr
-- ORIG lexprP
-- ORIG   =  try (parens exprP)
-- ORIG  <|> try (parens exprCastP)
-- ORIG  <|> try (parens $ condP EIte exprP)
-- ORIG  <|> try exprFunP
-- ORIG  <|> try (liftM (EVar . stringSymbol) upperIdP)
-- ORIG  <|> liftM expr symbolP
-- ORIG  <|> liftM ECon constantP
-- ORIG  <|> liftM ESym symconstP
-- ORIG  <|> (reserved "_|_" >> return EBot)
-- ORIG
-- ORIG exprFunP           =  (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
-- ORIG   where
-- ORIG     exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces)
-- ORIG     exprFunCommasP = liftM2 EApp funSymbolP (parens        $ sepBy exprP comma)
-- ORIG     exprFunSemisP  = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
-- ORIG     funSymbolP     = locParserP symbolP -- liftM stringSymbol lowerIdP

parenBrackets  = parens . brackets

-- ORIG expr2P = buildExpressionParser bops lexprP

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))


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

dcolon = string "::" <* spaces

sortP
  =   try (string "Integer" >>  return FInt)
  <|> try (string "Int"     >>  return FInt)
  <|> try (string "int"     >>  return FInt)
  <|> try (FObj . symbol <$> lowerIdP)
  <|> (fApp <$> (Left <$> fTyConP) <*> many sortP)

symCharsP   = condIdP symChars (`notElem` keyWordSyms)

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

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

trueP  = reserved "true"  >> return PTrue
falseP = reserved "false" >> return PFalse

pred0P :: Parser Pred
pred0P =  trueP
      <|> falseP
      <|> try (fastIfP pIte predP)
      <|> try predrP
      <|> try (parens predP)
      <|> try (liftM PBexp funAppP)
      <|> try (reservedOp "&&" >> liftM PAnd predsP)
      <|> try (reservedOp "||" >> liftM POr  predsP)

predP  :: Parser Pred
predP  = buildExpressionParser lops pred0P


predsP = brackets $ sepBy predP semi

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

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))

condP f bodyP
   =   try (condIteP f bodyP)
   <|> (condQmP f bodyP)

condI = condIteP EIte


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

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

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

fTyConP
  =   (reserved "int"  >> return intFTyCon)
  <|> (reserved "bool" >> return boolFTyCon)
  <|> (reserved "real" >> return realFTyCon)
  <|> (symbolFTycon   <$> locUpperIdP)

refasP :: Parser [Refa]
refasP  =  (try (brackets $ sepBy (RConc <$> predP) semi))
       <|> liftM ((:[]) . RConc) predP

refBindP :: Parser Symbol -> Parser [Refa] -> Parser (Reft -> a) -> Parser a
refBindP bp rp kindP
  = braces $ do
      vv  <- bp
      t   <- kindP
      reserved "|"
      ras <- rp <* spaces
      return $ t (Reft (vv, ras))

bindP       = liftM symbol (lowerIdP <* colon)
optBindP vv = try bindP <|> return vv

refP       = refBindP bindP refasP
refDefP vv = refBindP (optBindP vv)

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

-- qualifierP = mkQual <$> upperIdP <*> parens $ sepBy1 sortBindP comma <*> predP

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

sortBindP  = (,) <$> symbolP <* colon <*> sortP

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

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

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

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 "qualifier"   >> qualifierP)
    <|> Kut   <$> (reserved "cut"         >> symbolP)
    <|> 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 ()

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
  where
    cm     = M.fromList       [(cid c, c)       | Cst c       <- defs]
    ws     =                  [w                | Wfc w       <- defs]
    bs     = rawBindEnv       [(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  <- symbolP
       reserved ":="
       ps <- brackets $ sepBy predSolP semi
       return (k, simplify $ PAnd ps)

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

solutionFileP
  = liftM2 (,) (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' refasP

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)
-}