liquidhaskell-0.1: Language/Haskell/Liquid/Parse.hs
{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances, UndecidableInstances, TypeSynonymInstances, TupleSections #-}
module Language.Haskell.Liquid.Parse
(hsSpecificationP, lhsSpecificationP, specSpecificationP)
where
import Control.Monad
import Text.Parsec
import Text.Parsec.Error (newErrorMessage, errorPos, Message (..))
import Text.Parsec.Pos (newPos)
import qualified Text.Parsec.Token as Token
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Control.Applicative ((<$>), (<*), (<*>))
import Data.Char (toLower, isLower, isSpace, isAlpha)
import Data.List (partition)
import Data.Monoid (mempty)
import GHC (mkModuleName, ModuleName)
import Text.PrettyPrint.HughesPJ (text)
import Language.Preprocessor.Unlit (unlit)
import Language.Fixpoint.Types
import Language.Haskell.Liquid.GhcMisc
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.RefType
import qualified Language.Haskell.Liquid.Measure as Measure
import Language.Fixpoint.Names (listConName, propConName, tupConName)
import Language.Fixpoint.Misc hiding (dcolon, dot)
import Language.Fixpoint.Parse
----------------------------------------------------------------------------
-- Top Level Parsing API ---------------------------------------------------
----------------------------------------------------------------------------
-------------------------------------------------------------------------------
hsSpecificationP :: SourceName -> String -> Either Error (ModName, Measure.BareSpec)
-------------------------------------------------------------------------------
hsSpecificationP = parseWithError $ do
S name <- try (lookAhead $ skipMany (commentP >> spaces)
>> reserved "module" >> symbolP)
<|> return (S "Main")
liftM (mkSpec (ModName SrcImport $ mkModuleName name)) $ specWraps specP
-------------------------------------------------------------------------------
lhsSpecificationP :: SourceName -> String -> Either Error (ModName, Measure.BareSpec)
-------------------------------------------------------------------------------
lhsSpecificationP sn s = hsSpecificationP sn $ unlit sn s
commentP = simpleComment (string "{-") (string "-}")
<|> simpleComment (string "--") newlineP
<|> simpleComment (string "\\") newlineP
<|> simpleComment (string "#") newlineP
simpleComment open close = open >> manyTill anyChar (try close)
newlineP = try (string "\r\n") <|> string "\n" <|> string "\r"
-- | Used to parse .spec files
--------------------------------------------------------------------------
specSpecificationP :: SourceName -> String -> Either Error (ModName, Measure.BareSpec)
--------------------------------------------------------------------------
specSpecificationP = parseWithError specificationP
specificationP :: Parser (ModName, Measure.BareSpec)
specificationP
= do reserved "module"
reserved "spec"
S name <- symbolP
reserved "where"
xs <- grabs (specP <* whiteSpace)
return $ mkSpec (ModName SpecImport $ mkModuleName name) xs
---------------------------------------------------------------------------
parseWithError :: Parser a -> SourceName -> String -> Either Error a
---------------------------------------------------------------------------
parseWithError parser f s
= case runParser (remainderP (whiteSpace >> parser)) 0 f s of
Left e -> Left $ parseErrorError f e
Right (r, "") -> Right $ r
Right (_, rem) -> Left $ parseErrorError f $ remParseError f s rem
---------------------------------------------------------------------------
parseErrorError :: SourceName -> ParseError -> Error
---------------------------------------------------------------------------
parseErrorError f e = ErrParse p msg e
where
p = sourcePosSrcSpan $ errorPos e
msg = text $ "Error Parsing Specification from: " ++ f
---------------------------------------------------------------------------
remParseError :: SourceName -> String -> String -> ParseError
---------------------------------------------------------------------------
remParseError f s r = newErrorMessage msg $ newPos f line col
where
msg = Message "Leftover while parsing"
(line, col) = remLineCol s r
remLineCol :: String -> String -> (Int, Int)
remLineCol src rem = (line, col)
where
line = 1 + srcLine - remLine
srcLine = length srcLines
remLine = length remLines
col = srcCol - remCol
srcCol = length $ srcLines !! (line - 1)
remCol = length $ remLines !! 0
srcLines = lines $ src
remLines = lines $ rem
----------------------------------------------------------------------------------
-- Lexer Tokens ------------------------------------------------------------------
----------------------------------------------------------------------------------
dot = Token.dot lexer
braces = Token.braces lexer
angles = Token.angles lexer
stringLiteral = Token.stringLiteral lexer
----------------------------------------------------------------------------------
-- BareTypes ---------------------------------------------------------------------
----------------------------------------------------------------------------------
-- | The top-level parser for "bare" refinement types. If refinements are
-- not supplied, then the default "top" refinement is used.
bareTypeP :: Parser BareType
bareTypeP
= try bareFunP
<|> bareAllP
<|> bareAllExprP
<|> bareExistsP
<|> bareAtomP
bareArgP
= bareAtomP
<|> parens bareTypeP
bareAtomP
= refP bbaseP
<|> try (dummyP (bbaseP <* spaces))
bbaseP :: Parser (Reft -> BareType)
bbaseP
= liftM2 bLst (brackets bareTypeP) predicatesP
<|> liftM2 bTup (parens $ sepBy bareTypeP comma) predicatesP
<|> try (liftM2 bAppTy lowerIdP bareTyArgP)
<|> try (liftM2 bRVar lowerIdP monoPredicateP)
<|> liftM3 bCon upperIdP predicatesP (sepBy bareTyArgP blanks)
bbaseNoAppP :: Parser (Reft -> BareType)
bbaseNoAppP
= liftM2 bLst (brackets bareTypeP) predicatesP
<|> liftM2 bTup (parens $ sepBy bareTypeP comma) predicatesP
<|> try (liftM3 bCon upperIdP predicatesP (return []))
<|> liftM2 bRVar lowerIdP monoPredicateP
bareTyArgP
= try (braces $ liftM RExprArg exprP)
<|> try bareAtomNoAppP
<|> try (parens bareTypeP)
bareAtomNoAppP
= refP bbaseNoAppP
<|> try (dummyP (bbaseNoAppP <* spaces))
bareAllExprP
= do reserved "forall"
zs <- brackets $ sepBy1 exBindP comma
dot
t <- bareTypeP
return $ foldr (uncurry RAllE) t zs
bareExistsP
= do reserved "exists"
zs <- brackets $ sepBy1 exBindP comma
dot
t <- bareTypeP
return $ foldr (uncurry REx) t zs
exBindP
= xyP binderP colon bareTypeP
bareAllP
= do reserved "forall"
as <- many tyVarIdP -- sepBy1 tyVarIdP comma
ps <- predVarDefsP
dot
t <- bareTypeP
return $ foldr RAllT (foldr RAllP t ps) as
tyVarIdP :: Parser String
tyVarIdP = condIdP alphanums (isLower . head)
where alphanums = ['a'..'z'] ++ ['0'..'9']
predVarDefsP
= try (angles $ sepBy1 predVarDefP comma)
<|> return []
predVarDefP
= liftM3 bPVar predVarIdP dcolon predVarTypeP
predVarIdP
= stringSymbol <$> tyVarIdP
bPVar p _ xts = PV p τ τxs
where (_, τ) = safeLast "bPVar last" xts
τxs = [ (τ, x, EVar x) | (x, τ) <- init xts ]
predVarTypeP :: Parser [(Symbol, BSort)]
predVarTypeP = do t <- bareTypeP
let (xs, ts, t') = bkArrow $ thd3 $ bkUniv $ t
if isPropBareType t'
then return $ zip xs (toRSort <$> ts)
else parserFail $ "Predicate Variable with non-Prop output sort: " ++ showpp t
xyP lP sepP rP
= liftM3 (\x _ y -> (x, y)) lP (spaces >> sepP) rP
data ArrowSym = ArrowFun | ArrowPred
arrowP
= (reserved "->" >> return ArrowFun)
<|> (reserved "=>" >> return ArrowPred)
positionNameP = dummyNamePos <$> getPosition
dummyNamePos pos = "dummy." ++ name ++ ['.'] ++ line ++ ['.'] ++ col
where
name = san <$> sourceName pos
line = show $ sourceLine pos
col = show $ sourceColumn pos
san '/' = '.'
san c = toLower c
bareFunP
= do b <- try bindP <|> dummyBindP
t1 <- bareArgP
a <- arrowP
t2 <- bareTypeP
return $ bareArrow b t1 a t2
dummyBindP
= tempSymbol "db" <$> freshIntP
-- = stringSymbol <$> positionNameP
bbindP = lowerIdP <* dcolon
bindP = liftM stringSymbol (lowerIdP <* colon)
bareArrow b t1 ArrowFun t2
= rFun b t1 t2
bareArrow _ t1 ArrowPred t2
= foldr (rFun dummySymbol) t2 (getClasses t1)
isPropBareType (RApp tc [] _ _) = tc == propConName
isPropBareType _ = False
getClasses (RApp tc ts _ _)
| isTuple tc
= getClass `fmap` ts
getClasses t
= [getClass t]
getClass (RApp c ts _ _)
= RCls c ts
getClass t
= errorstar $ "Cannot convert " ++ (show t) ++ " to Class"
dummyP :: Monad m => m (Reft -> b) -> m b
dummyP fm
= fm `ap` return dummyReft
refP :: Parser (Reft -> a) -> Parser a
refP kindP
= braces $ do
v <- symbolP
colon
t <- kindP
reserved "|"
ras <- refasP
return $ t (Reft (v, ras))
symsP
= do reserved "\\"
ss <- sepBy symbolP spaces
reserved "->"
return $ (, dummyRSort) <$> ss
<|> return []
refasP :: Parser [Refa]
refasP = (try (brackets $ sepBy (RConc <$> predP) semi))
<|> liftM ((:[]) . RConc) predP
predicatesP
= try (angles $ sepBy1 predicate1P comma)
<|> return []
predicate1P
= try (liftM2 RPoly symsP (refP bbaseP))
<|> liftM (RMono [] . predUReft) monoPredicate1P
<|> (braces $ liftM2 bRPoly symsP' refasP)
where
symsP' = do ss <- symsP
fs <- mapM refreshSym (fst <$> ss)
return $ zip ss fs
refreshSym s = liftM (intSymbol (symbolString s)) freshIntP
monoPredicateP
= try (angles monoPredicate1P)
<|> return mempty
monoPredicate1P
= try (reserved "True" >> return mempty)
<|> try (liftM pdVar (parens predVarUseP))
<|> liftM pdVar predVarUseP
predVarUseP
= do p <- predVarIdP
xs <- sepBy exprP spaces
return $ PV p dummyTyId [ (dummyTyId, dummySymbol, x) | x <- xs ]
------------------------------------------------------------------------
----------------------- Wrapped Constructors ---------------------------
------------------------------------------------------------------------
bRPoly [] _ = errorstar "Parse.bRPoly empty list"
bRPoly syms' expr = RPoly ss $ bRVar dummyName top r
where (ss, (v, _)) = (init syms, last syms)
syms = [(y, s) | ((_, s), y) <- syms']
su = mkSubst [(x, EVar y) | ((x, _), y) <- syms']
r = su `subst` Reft(v, expr)
bRVar α p r = RVar α (U r p)
bLst t rs r = RApp listConName [t] rs (reftUReft r)
bTup [t] _ r | isTauto r = t
| otherwise = t `strengthen` (reftUReft r)
bTup ts rs r = RApp tupConName ts rs (reftUReft r)
bCon b [RMono _ r1] [] r = RApp b [] [] (r1 `meet` (reftUReft r))
bCon b rs ts r = RApp b ts rs (reftUReft r)
bAppTy v t r = RAppTy (RVar v top) t (reftUReft r)
reftUReft = (`U` mempty)
predUReft = (U dummyReft)
dummyReft = top
dummyTyId = ""
dummyRSort = ROth "dummy"
------------------------------------------------------------------
--------------------------- Measures -----------------------------
------------------------------------------------------------------
data Pspec ty ctor
= Meas (Measure.Measure ty ctor)
| Assm (LocSymbol, ty)
| Assms ([LocSymbol], ty)
| Impt Symbol
| DDecl DataDecl
| Incl FilePath
| Invt (Located ty)
| Alias (RTAlias String BareType)
| PAlias (RTAlias Symbol Pred)
| Embed (Located String, FTycon)
| Qualif Qualifier
| Decr (LocSymbol, [Int])
| LVars LocSymbol
| Lazy Symbol
| Pragma (Located String)
-- mkSpec :: String -> [Pspec ty LocSymbol] -> Measure.Spec ty LocSymbol
mkSpec name xs = (name,)
$ Measure.qualifySpec (getModString name)
$ Measure.Spec
{ Measure.measures = [m | Meas m <- xs]
, Measure.sigs = [a | Assm a <- xs]
++ [(y, t) | Assms (ys, t) <- xs, y <- ys]
, Measure.invariants = [t | Invt t <- xs]
, Measure.imports = [i | Impt i <- xs]
, Measure.dataDecls = [d | DDecl d <- xs]
, Measure.includes = [q | Incl q <- xs]
, Measure.aliases = [a | Alias a <- xs]
, Measure.paliases = [p | PAlias p <- xs]
, Measure.embeds = M.fromList [e | Embed e <- xs]
, Measure.qualifiers = [q | Qualif q <- xs]
, Measure.decr = [d | Decr d <- xs]
, Measure.lvars = [d | LVars d <- xs]
, Measure.lazy = S.fromList [s | Lazy s <- xs]
, Measure.pragmas = [s | Pragma s <- xs]
}
specP :: Parser (Pspec BareType Symbol)
specP
= try (reserved "assume" >> liftM Assm tyBindP )
<|> (reserved "assert" >> liftM Assm tyBindP )
<|> (reserved "measure" >> liftM Meas measureP )
<|> (reserved "import" >> liftM Impt symbolP )
<|> (reserved "data" >> liftM DDecl dataDeclP )
<|> (reserved "include" >> liftM Incl filePathP )
<|> (reserved "invariant" >> liftM Invt invariantP)
<|> (reserved "type" >> liftM Alias aliasP )
<|> (reserved "predicate" >> liftM PAlias paliasP )
<|> (reserved "embed" >> liftM Embed embedP )
<|> (reserved "qualif" >> liftM Qualif qualifierP)
<|> (reserved "Decrease" >> liftM Decr decreaseP )
<|> (reserved "LAZYVAR" >> liftM LVars lazyVarP )
<|> (reserved "Strict" >> liftM Lazy lazyP )
<|> (reserved "Lazy" >> liftM Lazy lazyP )
<|> (reserved "LIQUID" >> liftM Pragma pragmaP )
<|> ({- DEFAULT -} liftM Assms tyBindsP )
pragmaP :: Parser (Located String)
pragmaP = locParserP $ stringLiteral
lazyP :: Parser Symbol
lazyP = binderP
lazyVarP :: Parser LocSymbol
lazyVarP = locParserP binderP
decreaseP :: Parser (LocSymbol, [Int])
decreaseP = mapSnd f <$> liftM2 (,) (locParserP binderP) (spaces >> (many integer))
where f = ((\n -> fromInteger n - 1) <$>)
filePathP :: Parser FilePath
filePathP = angles $ many1 pathCharP
where
pathCharP = choice $ char <$> pathChars
pathChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['.', '/']
tyBindsP :: Parser ([LocSymbol], BareType)
tyBindsP = xyP (sepBy (locParserP binderP) comma) dcolon genBareTypeP
tyBindP :: Parser (LocSymbol, BareType)
tyBindP = xyP (locParserP binderP) dcolon genBareTypeP
locParserP :: Parser a -> Parser (Located a)
locParserP p = liftM2 Loc getPosition p
invariantP = locParserP genBareTypeP
genBareTypeP
= bareTypeP -- liftM generalize bareTypeP
embedP
= xyP (locParserP upperIdP) (reserved "as") fTyConP
aliasP = rtAliasP id bareTypeP
paliasP = rtAliasP stringSymbol predP
rtAliasP f bodyP
= do pos <- getPosition
name <- upperIdP
spaces
args <- sepBy aliasIdP spaces
whiteSpace >> reservedOp "=" >> whiteSpace
body <- bodyP
let (tArgs, vArgs) = partition (isLower . head) args
return $ RTA name (f <$> tArgs) (f <$> vArgs) body pos
aliasIdP :: Parser String
aliasIdP = condIdP (['A' .. 'Z'] ++ ['a'..'z'] ++ ['0'..'9']) (isAlpha . head)
measureP :: Parser (Measure.Measure BareType Symbol)
measureP
= do (x, ty) <- tyBindP
whiteSpace
eqns <- grabs $ measureDefP $ (rawBodyP <|> tyBodyP ty)
return $ Measure.mkM x ty eqns
rawBodyP
= braces $ do
v <- symbolP
reserved "|"
p <- predP
return $ Measure.R v p
-- tyBodyP :: BareType -> Parser Measure.Body
tyBodyP ty
= case outTy ty of
Just bt | isPropBareType bt -> Measure.P <$> predP
_ -> Measure.E <$> exprP
where outTy (RAllT _ t) = outTy t
outTy (RAllP _ t) = outTy t
outTy (RFun _ _ t _) = Just t
outTy _ = Nothing
binderP :: Parser Symbol
binderP = try $ stringSymbol <$> idP badc
<|> pwr <$> parens (idP bad)
where
idP p = many1 (satisfy (not . p))
badc c = (c == ':') || (c == ',') || bad c
bad c = isSpace c || c `elem` "(,)"
pwr s = stringSymbol $ "(" ++ s ++ ")"
grabs p = try (liftM2 (:) p (grabs p))
<|> return []
measureDefP :: Parser Measure.Body -> Parser (Measure.Def Symbol)
measureDefP bodyP
= do mname <- locParserP symbolP
(c, xs) <- {- ORIGINAL parens $ -} measurePatP
whiteSpace >> reservedOp "=" >> whiteSpace
body <- bodyP
whiteSpace
let xs' = (stringSymbol . val) <$> xs
return $ Measure.Def mname (stringSymbol c) xs' body
-- ORIGINAL
-- measurePatP :: Parser (String, [LocString])
-- measurePatP
-- = try (liftM2 (,) upperIdP (sepBy locLowerIdP whiteSpace))
-- <|> try (liftM3 (\x c y -> (c, [x,y])) locLowerIdP colon locLowerIdP)
-- <|> (brackets whiteSpace >> return ("[]",[]))
measurePatP :: Parser (String, [LocString])
measurePatP
= try tupPatP
<|> try (parens conPatP)
<|> try (parens consPatP)
<|> (parens nilPatP)
tupPatP = mkTupPat <$> (parens $ sepBy locLowerIdP comma)
conPatP = (,) <$> dataConNameP <*> sepBy locLowerIdP whiteSpace
consPatP = mkConsPat <$> locLowerIdP <*> colon <*> locLowerIdP
nilPatP = mkNilPat <$> brackets whiteSpace
mkTupPat zs = (tupDataCon (length zs), zs)
mkNilPat _ = ("[]", [] )
mkConsPat x c y = (":" , [x, y])
tupDataCon n = "(" ++ replicate (n - 1) ',' ++ ")"
locLowerIdP = locParserP lowerIdP
{- len (Cons x1 x2 ...) = e -}
-------------------------------------------------------------------------------
--------------------------------- Predicates ----------------------------------
-------------------------------------------------------------------------------
dataConFieldsP
= (braces $ sepBy predTypeDDP comma)
<|> (sepBy (parens predTypeDDP) spaces)
predTypeDDP
= liftM2 (,) bbindP bareTypeP
dataConP
= do x <- dataConNameP
spaces
xts <- dataConFieldsP
return (x, xts)
-- dataConNameP = symbolString <$> binderP -- upperIdP
dataConNameP
= try upperIdP
<|> pwr <$> parens (idP bad)
where
idP p = many1 (satisfy (not . p))
bad c = isSpace c || c `elem` "(,)"
pwr s = "(" ++ s ++ ")"
dataSizeP
= (brackets $ (Just . mkFun) <$> lowerIdP)
<|> return Nothing
where mkFun s = \x -> EApp (stringSymbol s) [EVar x]
dataDeclP
= do pos <- getPosition
x <- upperIdP
spaces
fsize <- dataSizeP
spaces
ts <- sepBy tyVarIdP spaces
ps <- predVarDefsP
whiteSpace >> reservedOp "=" >> whiteSpace
dcs <- sepBy dataConP (reserved "|")
whiteSpace
-- spaces
-- reservedOp "--"
return $ D x ts ps dcs pos fsize
---------------------------------------------------------------------
------------ Interacting with Fixpoint ------------------------------
---------------------------------------------------------------------
grabUpto p
= try (lookAhead p >>= return . Just)
<|> try (eof >> return Nothing)
<|> (anyChar >> grabUpto p)
betweenMany leftP rightP p
= do z <- grabUpto leftP
case z of
Just _ -> liftM2 (:) (between leftP rightP p) (betweenMany leftP rightP p)
Nothing -> return []
-- specWrap = between (string "{-@" >> spaces) (spaces >> string "@-}")
specWraps = betweenMany (string "{-@" >> spaces) (spaces >> string "@-}")
----------------------------------------------------------------------------------------
------------------------ Bundling Parsers into a Typeclass -----------------------------
----------------------------------------------------------------------------------------
instance Inputable BareType where
rr' = doParse' bareTypeP
instance Inputable (Measure.Measure BareType Symbol) where
rr' = doParse' measureP
{-
---------------------------------------------------------------
--------------------------- Testing ---------------------------
---------------------------------------------------------------
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)
-}