liquid-fixpoint 0.9.6.3.4 → 0.9.6.3.5

raw patch · 7 files changed

+273/−408 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGES.md +1/−1
• liquid-fixpoint.cabal +1/−2
• src/Language/Fixpoint/Horn/Parse.hs +265/−36
• src/Language/Fixpoint/Horn/SMTParse.hs +0/−362
• src/Language/Fixpoint/Horn/Solve.hs +2/−4
• src/Language/Fixpoint/Solver.hs +2/−1
• src/Language/Fixpoint/Types/Config.hs +2/−2

@@ -2,7 +2,7 @@  ## NEXT -## 0.9.6.3.4 (2026-01-14)+## 0.9.6.3.5 (2026-01-14)  - Implement `--sortedsolution` to keep elaborated sorts in fqout/solution [#821](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/821) - Retire old parser for horn queries [#820](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/820)

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.6.3.4+version:            0.9.6.3.5 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -67,7 +67,6 @@                     Language.Fixpoint.Graph.Types                     Language.Fixpoint.Horn.Info                     Language.Fixpoint.Horn.Parse-                    Language.Fixpoint.Horn.SMTParse                     Language.Fixpoint.Horn.Solve                     Language.Fixpoint.Horn.Transformations                     Language.Fixpoint.Horn.Types

@@ -7,36 +7,136 @@   , hPredP   , hQualifierP   , hVarP-  , numericDeclP+  , exprP+  , sortP ) where -import           Language.Fixpoint.Parse+import qualified Language.Fixpoint.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon) import qualified Language.Fixpoint.Types        as F import qualified Language.Fixpoint.Horn.Types   as H import           Text.Megaparsec                hiding (State)-import           Text.Megaparsec.Char           (char)+import           Text.Megaparsec.Char           (space1, string, char) import qualified Data.HashMap.Strict            as M+import qualified Data.Text as T+import qualified Text.Megaparsec.Char.Lexer  as L +type FParser = FP.Parser++fAddNumTyCon :: F.Symbol -> FP.Parser ()+fAddNumTyCon = FP.addNumTyCon++lexeme :: FParser a -> FParser a+lexeme = FP.lexeme' spaces++locLexeme :: FP.Parser a -> FP.Parser (F.Located a)+locLexeme = FP.locLexeme' spaces++-- | Consumes all whitespace, including LH comments.+--+-- Should not be used directly, but primarily via 'lexeme'.+--+-- The only "valid" use case for spaces is in top-level parsing+-- function, to consume initial spaces.+--+spaces :: FParser ()+spaces =+  L.space+    space1+    lineComment+    blockComment++lineComment :: FParser ()+lineComment = L.skipLineComment ";"++blockComment :: FParser ()+blockComment = L.skipBlockComment "/* " "*/"++reserved :: String -> FParser ()+reserved = FP.reserved' spaces++reservedOp :: String -> FParser ()+reservedOp = FP.reservedOp' spaces++sym :: String -> FParser String+sym x = lexeme (string x)++parens :: FParser a -> FParser a+parens = between (sym "(") (sym ")")++stringLiteral :: FParser String+stringLiteral = lexeme FP.stringR <?> "string literal"++symbolP :: FParser F.Symbol+symbolP = lexeme FP.symbolR <?> "identifier"++fIntP :: FParser Int+fIntP = fromInteger <$> natural++natural :: FParser Integer+natural = lexeme FP.naturalR <?> "nat literal"++double :: FParser Double+double = lexeme L.float <?> "float literal"+++locUpperIdP, locSymbolP :: FParser F.LocSymbol+locUpperIdP = locLexeme FP.upperIdR+locSymbolP  = locLexeme FP.symbolR++upperIdP :: FP.Parser F.Symbol+upperIdP = lexeme FP.upperIdR <?> "upperIdP"++lowerIdP :: FP.Parser F.Symbol+lowerIdP = lexeme FP.lowerIdR <?> "upperIdP"++fTyConP :: FParser F.FTycon+fTyConP+  =   (reserved "int"     >> return F.intFTyCon)+  <|> (reserved "Integer" >> return F.intFTyCon)+  <|> (reserved "Int"     >> return F.intFTyCon)+  <|> (reserved "real"    >> return F.realFTyCon)+  <|> (reserved "bool"    >> return F.boolFTyCon)+  <|> (reserved "num"     >> return F.numFTyCon)+  <|> (reserved "Str"     >> return F.strFTyCon)+  <|> (FP.mkFTycon        =<<  locUpperIdP)+++fTrueP :: FP.Parser F.Expr+fTrueP = reserved "true"  >> return F.PTrue++fFalseP :: FP.Parser F.Expr+fFalseP = reserved "false" >> return F.PFalse++fSymconstP :: FP.Parser F.SymConst+fSymconstP =  F.SL . T.pack <$> stringLiteral++-- | Parser for literal numeric constants: floats or integers without sign.+constantP :: FParser F.Constant+constantP =+     try (F.R <$> double)   -- float literal+ <|> F.I <$> natural        -- nat literal+ --------------------------------------------------------------------------------hornP :: Parser H.TagQuery+hornP :: FParser H.TagQuery ------------------------------------------------------------------------------- hornP = do+  spaces   hThings <- many hThingP   pure (mkQuery hThings)  mkQuery :: [HThing a] -> H.Query a mkQuery things = H.Query-  { H.qQuals =            [ q     | HQual q  <- things ]-  , H.qVars  =            [ k     | HVar  k  <- things ]-  , H.qCstr  = H.CAnd     [ c     | HCstr c  <- things ]-  , H.qCon   = M.fromList [ (x,t) | HCon x t <- things ]-  , H.qDis   = M.fromList [ (x,t) | HDis x t <- things ]-  , H.qEqns  =            [ e     | HDef e  <- things ]-  , H.qMats  =            [ m     | HMat m  <- things ]-  , H.qData  =            [ dd    | HDat dd <- things ]-  , H.qOpts  =            [ o     | HOpt o  <- things ]-  , H.qNums  =            [ n     | HNum n  <- things ]-  , H.qDefs  =            []+  { H.qQuals =              [ q     | HQual q  <- things ]+  , H.qVars  =              [ k     | HVar  k  <- things ]+  , H.qCstr  = H.CAnd       [ c     | HCstr c  <- things ]+  , H.qCon   = M.fromList   [ (x,t) | HCon x t <- things ]+  , H.qDis   = M.fromList   [ (x,t) | HDis x t <- things ]+  , H.qEqns  =              [ e     | HDef e   <- things ]+  , H.qDefs  =              [ e     | HDfn e   <- things ]+  , H.qMats  =              [ m     | HMat m   <- things ]+  , H.qData  =              [ dd    | HDat dd  <- things ]+  , H.qOpts  =              [ o     | HOpt o   <- things ]+  , H.qNums  =              [ s     | HNum s   <- things ]   }  -- | A @HThing@ describes the kinds of things we may see, in no particular order@@ -51,14 +151,15 @@   | HCon  F.Symbol F.Sort   | HDis  F.Symbol F.Sort   | HDef  F.Equation+  | HDfn  F.Equation   | HMat  F.Rewrite   | HDat !F.DataDecl   | HOpt !String   | HNum  F.Symbol   deriving (Functor) -hThingP :: Parser (HThing H.Tag)-hThingP  = parens body+hThingP :: FParser (HThing H.Tag)+hThingP  = spaces >> parens body   where     body =  HQual <$> (reserved "qualif"     *> hQualifierP)         <|> HCstr <$> (reserved "constraint" *> hCstrP)@@ -67,52 +168,53 @@         <|> HCon  <$> (reserved "constant"   *> symbolP) <*> sortP         <|> HDis  <$> (reserved "distinct"   *> symbolP) <*> sortP         <|> HDef  <$> (reserved "define"     *> defineP)+        <|> HDfn  <$> (reserved "define_fun" *> defineP)         <|> HMat  <$> (reserved "match"      *> matchP)-        <|> HDat  <$> (reserved "data"       *> dataDeclP)+        <|> HDat  <$> (reserved "datatype"   *> dataDeclP)         <|> HNum  <$> (reserved "numeric"    *> numericDeclP) -numericDeclP :: Parser F.Symbol+numericDeclP :: FParser F.Symbol numericDeclP = do   x <- F.val <$> locUpperIdP-  addNumTyCon x+  fAddNumTyCon x   pure x  --------------------------------------------------------------------------------hCstrP :: Parser (H.Cstr H.Tag)+hCstrP :: FParser (H.Cstr H.Tag) --------------------------------------------------------------------------------hCstrP = parens body+hCstrP =  try (parens body)+      <|> H.Head <$> hPredP                            <*> pure H.NoTag   where     body =  H.CAnd <$> (reserved "and"    *> many hCstrP)-        <|> H.All  <$> (reserved "forall" *> hBindP)      <*> hCstrP-        <|> H.Head <$> (reserved "tag"    *> hPredP)      <*> (H.Tag <$> stringLiteral)-        <|> H.Head <$> hPredP                             <*> pure H.NoTag+        <|> H.All  <$> (reserved "forall" *> hBindP)  <*> hCstrP+        <|> H.Head <$> (reserved "tag"    *> hPredP)  <*> (H.Tag <$> stringLiteral) -hBindP :: Parser (H.Bind H.Tag)+hBindP :: FParser (H.Bind H.Tag) hBindP   = parens $ do   (x, t) <- symSortP   H.Bind x t <$> hPredP <*> pure H.NoTag  --------------------------------------------------------------------------------hPredP :: Parser H.Pred+hPredP :: FParser H.Pred ------------------------------------------------------------------------------- hPredP = parens body   where-    body =  H.Var  <$> kvSymP                           <*> some predP+    body =  H.Var  <$> kvSymP <*> some exprP         <|> H.PAnd <$> (reserved "and" *> some hPredP)-        <|> H.Reft <$> predP+        <|> H.Reft <$> exprP -kvSymP :: Parser F.Symbol+kvSymP :: FParser F.Symbol kvSymP = char '$' *> symbolP  ------------------------------------------------------------------------------- -- | Qualifiers --------------------------------------------------------------------------------hQualifierP :: Parser F.Qualifier+hQualifierP :: FParser F.Qualifier hQualifierP = do   pos    <- getSourcePos   n      <- upperIdP   params <- parens (some symSortP)-  body   <- parens predP+  body   <- exprP   return  $ F.mkQual n (mkParam <$> params) body pos  mkParam :: (F.Symbol, F.Sort) -> F.QualParam@@ -122,12 +224,139 @@ -- | Horn Variables ------------------------------------------------------------------------------- -hVarP :: Parser (H.Var H.Tag)-hVarP = H.HVar <$> kvSymP <*> parens (some (parens sortP)) <*> pure H.NoTag+hVarP :: FParser (H.Var H.Tag)+hVarP = H.HVar <$> kvSymP <*> parens (some sortP) <*> pure H.NoTag  ------------------------------------------------------------------------------- -- | Helpers -------------------------------------------------------------------------------+sPairP :: FParser a -> FParser b -> FParser (a, b)+sPairP aP bP = parens ((,) <$> aP <*> bP) -symSortP :: Parser (F.Symbol, F.Sort)-symSortP = parens ((,) <$> symbolP <*> sortP)+sMany :: FParser a -> FParser [a]+sMany p = parens (many p)+++symSortP :: FParser (F.Symbol, F.Sort)+symSortP = sPairP  symbolP sortP+-- symSortP = fParens ((,) <$> fSymbolP <*> sortP)++dataDeclP :: FParser F.DataDecl+dataDeclP = do+  (tc, n) <- sPairP fTyConP fIntP+  ctors   <- sMany dataCtorP+  pure     $ F.DDecl tc n ctors++dataCtorP :: FParser F.DataCtor+dataCtorP = parens (F.DCtor <$> locSymbolP <*> sMany dataFieldP)++dataFieldP :: FParser F.DataField+dataFieldP = uncurry F.DField <$> sPairP locSymbolP sortP++bindsP :: FParser [(F.Symbol, F.Sort)]+bindsP = sMany bindP++bindP :: FParser (F.Symbol, F.Sort)+bindP = sPairP symbolP sortP++-- | We only support lets with a single binder, but we parse this as a "singleton list"+-- to be forward compatible with multiple binders. Note that the semantics of multiple+-- binders in smtlib is *simulatenous substitution*, so they cannot be desugared to nested+-- lets.+exprBindsP :: FParser (F.Symbol, F.Expr)+exprBindsP = parens exprBindP++exprBindP :: FParser (F.Symbol, F.Expr)+exprBindP = sPairP symbolP exprP++defineP :: FParser F.Equation+defineP = do+  name   <- symbolP+  xts    <- bindsP+  s      <- sortP+  body   <- exprP+  return  $ F.mkEquation name xts body s++matchP :: FParser F.Rewrite+matchP = do+  f    <- symbolP+  d:xs <- parens (some symbolP)+  F.SMeasure f d xs <$> exprP++sortP :: FParser F.Sort+sortP =  (string "@" >> (F.FVar <$> parens fIntP))+     <|> (reserved "Int"  >> return F.FInt)+     <|> (reserved "Real" >> return F.FReal)+     <|> (reserved "Frac" >> return F.FFrac)+     <|> (reserved "num" >> return  F.FNum)+     <|> (F.fAppTC <$> fTyConP <*> pure [])+     <|> (F.FObj . F.symbol <$> lowerIdP)+     <|> try (parens (reserved "func" >> (mkFunc <$> fIntP <*> sMany sortP <*> sortP)))+     <|> try (parens (reserved "list" >> (mkList <$> sortP)))+     <|> parens (F.fAppTC <$> fTyConP <*> many sortP)+     <|> (F.FNatNum <$> natural)++mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort+mkFunc n ss s = F.mkFFunc n (ss ++ [s])++mkList :: F.Sort -> F.Sort+mkList s = F.fAppTC F.listFTyCon [s]++exprP :: FParser F.Expr+exprP+  =   fTrueP+  <|> fFalseP+  <|> (F.ESym <$> fSymconstP)+  <|> (F.ECon <$> constantP)+  <|> (F.EVar <$> symbolP)+  <|> parens pExprP++pExprP :: FParser F.Expr+pExprP+  =   (reserved   "if"     >> (F.EIte   <$> exprP <*> exprP <*> exprP))+  <|> (reserved   "let"    >> (uncurry F.ELet   <$> exprBindsP <*> exprP))+  <|> (reserved   "lit"    >> (mkLit    <$> stringLiteral <*> sortP))+  <|> (reserved   "cast"   >> (F.ECst   <$> exprP <*> sortP))+  <|> (reserved   "not"    >> (F.PNot   <$> exprP))+  <|> (reservedOp "=>"     >> (F.PImp   <$> exprP <*> exprP))+  <|> (reservedOp "<=>"    >> (F.PIff   <$> exprP <*> exprP))+  <|> (reserved   "and"    >> (F.PAnd   <$> many exprP))+  <|> (reserved   "or"     >> (F.POr    <$> many exprP))+  <|> (reserved   "forall" >> (F.PAll   <$> bindsP <*> exprP))+  <|> (reserved   "exists" >> (F.PExist <$> bindsP <*> exprP))+  <|> (reserved   "lam"    >> (F.ELam   <$> bindP <*> exprP))+  <|> (reserved   "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP))+  <|> (reserved   "ETApp"  >> (F.ETApp  <$> exprP <*> sortP))+  <|> (reserved   "ETAbs"  >> (F.ETAbs  <$> exprP <*> symbolP))+  <|> try (F.EBin  <$> bopP <*> exprP <*> exprP)+  <|> try (F.PAtom <$> brelP <*> exprP <*> exprP)+  <|> try (sym "-" >> (F.ENeg <$> exprP))+  <|> (mkApp <$> some exprP)++mkLit :: String -> F.Sort -> F.Expr+mkLit l t = F.ECon (F.L (T.pack l) t)++mkApp :: [F.Expr] -> F.Expr+mkApp (e:es) = F.eApps e es+mkApp _      = error "impossible"++bopP :: FParser F.Bop+bopP+  =  (sym "+"   >> return F.Plus)+ <|> (sym "-"   >> return F.Minus)+ <|> (sym "*"   >> return F.Times)+ <|> (sym "/"   >> return F.Div)+ <|> (reserved "mod" >> return F.Mod)+ <|> (sym "*."  >> return F.RTimes)+ <|> (sym "/."  >> return F.RDiv)++brelP :: FParser F.Brel+brelP+  =  (sym "="  >> return F.Eq)+ <|> (sym "!=" >> return F.Ne)+ <|> (sym "~~" >> return F.Ueq)+ <|> (sym "!~" >> return F.Une)+ <|> (sym ">=" >> return F.Ge)+ <|> (sym ">"  >> return F.Gt)+ <|> (sym "<=" >> return F.Le)+ <|> (sym "<"  >> return F.Lt)

@@ -1,362 +0,0 @@--{-# LANGUAGE DeriveFunctor #-}--module Language.Fixpoint.Horn.SMTParse (-    hornP-  , hCstrP-  , hPredP-  , hQualifierP-  , hVarP-  , exprP-  , sortP-) where--import qualified Language.Fixpoint.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon)-import qualified Language.Fixpoint.Types        as F-import qualified Language.Fixpoint.Horn.Types   as H-import           Text.Megaparsec                hiding (State)-import           Text.Megaparsec.Char           (space1, string, char)-import qualified Data.HashMap.Strict            as M-import qualified Data.Text as T-import qualified Text.Megaparsec.Char.Lexer  as L--type FParser = FP.Parser--fAddNumTyCon :: F.Symbol -> FP.Parser ()-fAddNumTyCon = FP.addNumTyCon--lexeme :: FParser a -> FParser a-lexeme = FP.lexeme' spaces--locLexeme :: FP.Parser a -> FP.Parser (F.Located a)-locLexeme = FP.locLexeme' spaces---- | Consumes all whitespace, including LH comments.------ Should not be used directly, but primarily via 'lexeme'.------ The only "valid" use case for spaces is in top-level parsing--- function, to consume initial spaces.----spaces :: FParser ()-spaces =-  L.space-    space1-    lineComment-    blockComment--lineComment :: FParser ()-lineComment = L.skipLineComment ";"--blockComment :: FParser ()-blockComment = L.skipBlockComment "/* " "*/"--reserved :: String -> FParser ()-reserved = FP.reserved' spaces--reservedOp :: String -> FParser ()-reservedOp = FP.reservedOp' spaces--sym :: String -> FParser String-sym x = lexeme (string x)--parens :: FParser a -> FParser a-parens = between (sym "(") (sym ")")--stringLiteral :: FParser String-stringLiteral = lexeme FP.stringR <?> "string literal"--symbolP :: FParser F.Symbol-symbolP = lexeme FP.symbolR <?> "identifier"--fIntP :: FParser Int-fIntP = fromInteger <$> natural--natural :: FParser Integer-natural = lexeme FP.naturalR <?> "nat literal"--double :: FParser Double-double = lexeme L.float <?> "float literal"---locUpperIdP, locSymbolP :: FParser F.LocSymbol-locUpperIdP = locLexeme FP.upperIdR-locSymbolP  = locLexeme FP.symbolR--upperIdP :: FP.Parser F.Symbol-upperIdP = lexeme FP.upperIdR <?> "upperIdP"--lowerIdP :: FP.Parser F.Symbol-lowerIdP = lexeme FP.lowerIdR <?> "upperIdP"--fTyConP :: FParser F.FTycon-fTyConP-  =   (reserved "int"     >> return F.intFTyCon)-  <|> (reserved "Integer" >> return F.intFTyCon)-  <|> (reserved "Int"     >> return F.intFTyCon)-  <|> (reserved "real"    >> return F.realFTyCon)-  <|> (reserved "bool"    >> return F.boolFTyCon)-  <|> (reserved "num"     >> return F.numFTyCon)-  <|> (reserved "Str"     >> return F.strFTyCon)-  <|> (FP.mkFTycon        =<<  locUpperIdP)---fTrueP :: FP.Parser F.Expr-fTrueP = reserved "true"  >> return F.PTrue--fFalseP :: FP.Parser F.Expr-fFalseP = reserved "false" >> return F.PFalse--fSymconstP :: FP.Parser F.SymConst-fSymconstP =  F.SL . T.pack <$> stringLiteral---- | Parser for literal numeric constants: floats or integers without sign.-constantP :: FParser F.Constant-constantP =-     try (F.R <$> double)   -- float literal- <|> F.I <$> natural        -- nat literal----------------------------------------------------------------------------------hornP :: FParser H.TagQuery---------------------------------------------------------------------------------hornP = do-  spaces-  hThings <- many hThingP-  pure (mkQuery hThings)--mkQuery :: [HThing a] -> H.Query a-mkQuery things = H.Query-  { H.qQuals =              [ q     | HQual q  <- things ]-  , H.qVars  =              [ k     | HVar  k  <- things ]-  , H.qCstr  = H.CAnd       [ c     | HCstr c  <- things ]-  , H.qCon   = M.fromList   [ (x,t) | HCon x t <- things ]-  , H.qDis   = M.fromList   [ (x,t) | HDis x t <- things ]-  , H.qEqns  =              [ e     | HDef e   <- things ]-  , H.qDefs  =              [ e     | HDfn e   <- things ]-  , H.qMats  =              [ m     | HMat m   <- things ]-  , H.qData  =              [ dd    | HDat dd  <- things ]-  , H.qOpts  =              [ o     | HOpt o   <- things ]-  , H.qNums  =              [ s     | HNum s   <- things ]-  }---- | A @HThing@ describes the kinds of things we may see, in no particular order---   in a .smt2 query file.--data HThing a-  = HQual !F.Qualifier-  | HVar  !(H.Var a)-  | HCstr !(H.Cstr a)--  -- for uninterpred functions and ADT constructors-  | HCon  F.Symbol F.Sort-  | HDis  F.Symbol F.Sort-  | HDef  F.Equation-  | HDfn  F.Equation-  | HMat  F.Rewrite-  | HDat !F.DataDecl-  | HOpt !String-  | HNum  F.Symbol-  deriving (Functor)--hThingP :: FParser (HThing H.Tag)-hThingP  = spaces >> parens body-  where-    body =  HQual <$> (reserved "qualif"     *> hQualifierP)-        <|> HCstr <$> (reserved "constraint" *> hCstrP)-        <|> HVar  <$> (reserved "var"        *> hVarP)-        <|> HOpt  <$> (reserved "fixpoint"   *> stringLiteral)-        <|> HCon  <$> (reserved "constant"   *> symbolP) <*> sortP-        <|> HDis  <$> (reserved "distinct"   *> symbolP) <*> sortP-        <|> HDef  <$> (reserved "define"     *> defineP)-        <|> HDfn  <$> (reserved "define_fun" *> defineP)-        <|> HMat  <$> (reserved "match"      *> matchP)-        <|> HDat  <$> (reserved "datatype"   *> dataDeclP)-        <|> HNum  <$> (reserved "numeric"    *> numericDeclP)--numericDeclP :: FParser F.Symbol-numericDeclP = do-  x <- F.val <$> locUpperIdP-  fAddNumTyCon x-  pure x----------------------------------------------------------------------------------hCstrP :: FParser (H.Cstr H.Tag)---------------------------------------------------------------------------------hCstrP =  try (parens body)-      <|> H.Head <$> hPredP                            <*> pure H.NoTag-  where-    body =  H.CAnd <$> (reserved "and"    *> many hCstrP)-        <|> H.All  <$> (reserved "forall" *> hBindP)  <*> hCstrP-        <|> H.Head <$> (reserved "tag"    *> hPredP)  <*> (H.Tag <$> stringLiteral)--hBindP :: FParser (H.Bind H.Tag)-hBindP   = parens $ do-  (x, t) <- symSortP-  H.Bind x t <$> hPredP <*> pure H.NoTag----------------------------------------------------------------------------------hPredP :: FParser H.Pred---------------------------------------------------------------------------------hPredP = parens body-  where-    body =  H.Var  <$> kvSymP <*> some exprP-        <|> H.PAnd <$> (reserved "and" *> some hPredP)-        <|> H.Reft <$> exprP--kvSymP :: FParser F.Symbol-kvSymP = char '$' *> symbolP------------------------------------------------------------------------------------ | Qualifiers---------------------------------------------------------------------------------hQualifierP :: FParser F.Qualifier-hQualifierP = do-  pos    <- getSourcePos-  n      <- upperIdP-  params <- parens (some symSortP)-  body   <- exprP-  return  $ F.mkQual n (mkParam <$> params) body pos--mkParam :: (F.Symbol, F.Sort) -> F.QualParam-mkParam (x, t) = F.QP x F.PatNone t------------------------------------------------------------------------------------ | Horn Variables----------------------------------------------------------------------------------hVarP :: FParser (H.Var H.Tag)-hVarP = H.HVar <$> kvSymP <*> parens (some sortP) <*> pure H.NoTag------------------------------------------------------------------------------------ | Helpers---------------------------------------------------------------------------------sPairP :: FParser a -> FParser b -> FParser (a, b)-sPairP aP bP = parens ((,) <$> aP <*> bP)--sMany :: FParser a -> FParser [a]-sMany p = parens (many p)---symSortP :: FParser (F.Symbol, F.Sort)-symSortP = sPairP  symbolP sortP--- symSortP = fParens ((,) <$> fSymbolP <*> sortP)--dataDeclP :: FParser F.DataDecl-dataDeclP = do-  (tc, n) <- sPairP fTyConP fIntP-  ctors   <- sMany dataCtorP-  pure     $ F.DDecl tc n ctors--dataCtorP :: FParser F.DataCtor-dataCtorP = parens (F.DCtor <$> locSymbolP <*> sMany dataFieldP)--dataFieldP :: FParser F.DataField-dataFieldP = uncurry F.DField <$> sPairP locSymbolP sortP--bindsP :: FParser [(F.Symbol, F.Sort)]-bindsP = sMany bindP--bindP :: FParser (F.Symbol, F.Sort)-bindP = sPairP symbolP sortP---- | We only support lets with a single binder, but we parse this as a "singleton list"--- to be forward compatible with multiple binders. Note that the semantics of multiple--- binders in smtlib is *simulatenous substitution*, so they cannot be desugared to nested--- lets.-exprBindsP :: FParser (F.Symbol, F.Expr)-exprBindsP = parens exprBindP--exprBindP :: FParser (F.Symbol, F.Expr)-exprBindP = sPairP symbolP exprP--defineP :: FParser F.Equation-defineP = do-  name   <- symbolP-  xts    <- bindsP-  s      <- sortP-  body   <- exprP-  return  $ F.mkEquation name xts body s--matchP :: FParser F.Rewrite-matchP = do-  f    <- symbolP-  d:xs <- parens (some symbolP)-  F.SMeasure f d xs <$> exprP--sortP :: FParser F.Sort-sortP =  (string "@" >> (F.FVar <$> parens fIntP))-     <|> (reserved "Int"  >> return F.FInt)-     <|> (reserved "Real" >> return F.FReal)-     <|> (reserved "Frac" >> return F.FFrac)-     <|> (reserved "num" >> return  F.FNum)-     <|> (F.fAppTC <$> fTyConP <*> pure [])-     <|> (F.FObj . F.symbol <$> lowerIdP)-     <|> try (parens (reserved "func" >> (mkFunc <$> fIntP <*> sMany sortP <*> sortP)))-     <|> try (parens (reserved "list" >> (mkList <$> sortP)))-     <|> parens (F.fAppTC <$> fTyConP <*> many sortP)-     <|> (F.FNatNum <$> natural)--mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort-mkFunc n ss s = F.mkFFunc n (ss ++ [s])--mkList :: F.Sort -> F.Sort-mkList s = F.fAppTC F.listFTyCon [s]--exprP :: FParser F.Expr-exprP-  =   fTrueP-  <|> fFalseP-  <|> (F.ESym <$> fSymconstP)-  <|> (F.ECon <$> constantP)-  <|> (F.EVar <$> symbolP)-  <|> parens pExprP--pExprP :: FParser F.Expr-pExprP-  =   (reserved   "if"     >> (F.EIte   <$> exprP <*> exprP <*> exprP))-  <|> (reserved   "let"    >> (uncurry F.ELet   <$> exprBindsP <*> exprP))-  <|> (reserved   "lit"    >> (mkLit    <$> stringLiteral <*> sortP))-  <|> (reserved   "cast"   >> (F.ECst   <$> exprP <*> sortP))-  <|> (reserved   "not"    >> (F.PNot   <$> exprP))-  <|> (reservedOp "=>"     >> (F.PImp   <$> exprP <*> exprP))-  <|> (reservedOp "<=>"    >> (F.PIff   <$> exprP <*> exprP))-  <|> (reserved   "and"    >> (F.PAnd   <$> many exprP))-  <|> (reserved   "or"     >> (F.POr    <$> many exprP))-  <|> (reserved   "forall" >> (F.PAll   <$> bindsP <*> exprP))-  <|> (reserved   "exists" >> (F.PExist <$> bindsP <*> exprP))-  <|> (reserved   "lam"    >> (F.ELam   <$> bindP <*> exprP))-  <|> (reserved   "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP))-  <|> (reserved   "ETApp"  >> (F.ETApp  <$> exprP <*> sortP))-  <|> (reserved   "ETAbs"  >> (F.ETAbs  <$> exprP <*> symbolP))-  <|> try (F.EBin  <$> bopP <*> exprP <*> exprP)-  <|> try (F.PAtom <$> brelP <*> exprP <*> exprP)-  <|> try (sym "-" >> (F.ENeg <$> exprP))-  <|> (mkApp <$> some exprP)--mkLit :: String -> F.Sort -> F.Expr-mkLit l t = F.ECon (F.L (T.pack l) t)--mkApp :: [F.Expr] -> F.Expr-mkApp (e:es) = F.eApps e es-mkApp _      = error "impossible"--bopP :: FParser F.Bop-bopP-  =  (sym "+"   >> return F.Plus)- <|> (sym "-"   >> return F.Minus)- <|> (sym "*"   >> return F.Times)- <|> (sym "/"   >> return F.Div)- <|> (reserved "mod" >> return F.Mod)- <|> (sym "*."  >> return F.RTimes)- <|> (sym "/."  >> return F.RDiv)--brelP :: FParser F.Brel-brelP-  =  (sym "="  >> return F.Eq)- <|> (sym "!=" >> return F.Ne)- <|> (sym "~~" >> return F.Ueq)- <|> (sym "!~" >> return F.Une)- <|> (sym ">=" >> return F.Ge)- <|> (sym ">"  >> return F.Gt)- <|> (sym "<=" >> return F.Le)- <|> (sym "<"  >> return F.Lt)

@@ -17,7 +17,6 @@ import qualified Language.Fixpoint.Horn.Types   as H  import qualified Language.Fixpoint.Horn.Parse   as H-import qualified Language.Fixpoint.Horn.SMTParse   as SH  import qualified Language.Fixpoint.Horn.Transformations as Tx import Text.PrettyPrint.HughesPJ.Compat ( render )@@ -47,13 +46,12 @@  parseQuery :: F.Config -> IO H.TagQuery parseQuery cfg-  | F.stdin cfg = Parse.parseFromStdIn hornP+  | F.stdin cfg = Parse.parseFromStdIn H.hornP   | json        = loadFromJSON file-  | otherwise   = Parse.parseFromFile hornP file+  | otherwise   = Parse.parseFromFile H.hornP file   where     json  = Files.isExtFile Files.Json file     file  = F.srcFile cfg-    hornP = if F.noSmtHorn cfg then H.hornP else SH.hornP  loadFromJSON :: FilePath -> IO H.TagQuery loadFromJSON f = do

@@ -336,6 +336,7 @@       , resNonCutsSolution = HashMap.map (fmap simplifyKVar') (resNonCutsSolution res)       }   where-    simplifyKVar' = unElabSets . unElab . Sol.simplifyKVar HashSet.empty+    simplifyKVar' = unElabSets . unElab' . Sol.simplifyKVar HashSet.empty     sets          = elabSetBag . solverFlags $ cfg     unElabSets    = if sets then unElabFSetBagZ3 else id+    unElab'       = if sortedSolution cfg then id else unElab

@@ -114,9 +114,9 @@   , json                :: Bool        -- ^ Render output in JSON format   , fuel                :: Maybe Int   -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite)   , restOrdering        :: String      -- ^ Term ordering for use in REST-  , noSmtHorn           :: Bool        -- ^ Do not use (new) SMTLIB horn parser   , noStringTheory :: Bool             -- ^ disable interpretation of string theory by SMT   , explicitKvars  :: Bool             -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications"+  , sortedSolution :: Bool             -- ^ leave sorts in the solution   } deriving (Eq,Data,Typeable,Show,Generic)  instance Default Config where@@ -287,8 +287,8 @@   , json                     = False   &= help "Render result in JSON"   , fuel                     = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE"   , restOrdering             = "rpo"   &= help "Ordering Constraint Algebra to use for REST"-  , noSmtHorn                = False &= help "Do not use SMTLIB horn format"   , explicitKvars            = False &= help "Use explicitly declared kvars (horn style) which disables several defensive simplifications"+  , sortedSolution           = False &= help "Leave elaborated sorts in the solution (only for machine consumption)"   }   &= verbosity   &= program "fixpoint"