diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,69 @@ +# CHANGES + +## NEXT + +## 0.9.4.7 + +- Support GHC 9.6 tuples with `--extensionality` [#666](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) [#667](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) + +## 0.9.2.5 + +- Adopt smtlib-backends for interactions with the SMT solvers [#641](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) + +## 0.9.0.2 + +- Simplified the equalities dumped by PLE [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569) [#605](https://github.com/ucsd-progsys/liquid-fixpoint/issues/605) +- Add PLE implementation based on interpreting expressions [#502](https://github.com/ucsd-progsys/liquid-fixpoint/pull/502) + +## 0.8.10.2 + +- Dump equalities discovered by PLE [#491](https://github.com/ucsd-progsys/liquid-fixpoint/pull/491) [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569) +- Dump prettified version of constraints [#473](https://github.com/ucsd-progsys/liquid-fixpoint/pull/473) +- Constraints now indicate the source code location that originated them [#471](https://github.com/ucsd-progsys/liquid-fixpoint/pull/471) +- Add support for term rewriting to PLE [#428](https://github.com/ucsd-progsys/liquid-fixpoint/pull/428) + +## 0.8.6.4 + +- Fix bugs in PLE +- Move to GHC 8.6.4 +- Add `fuel` parameter to debug unfolding in PLE + +## 0.8.0.1 + +- Support for HORN-NNF format clauses, see `tests/horn/{pos,neg}/*.smt2` +- Support for "existential binders", see `tests/pos/ebind-*.fq` for example. + This only works with `--eliminate`. +- Move to GHC 8.4.3 + +## 0.7.0.0 + +- New `eliminate` based solver (see ICFP 2017 paper for algorithm) +- Proof by Logical Evaluation see `tests/proof` +- SMTLIB2 ADTs to make data constructors injective +- Uniformly support polymorphic functions via `apply` and elaborate + +## 0.3.0.0 + +- Make interpreted mul and div the default, when `solver = z3` +- Use `higherorder` flag to allow higher order binders into the environment + +## 0.2.2.0 + +- Added support for theory of Arrays `Map_t`, `Map_select`, `Map_store` + +- Added support for theory of Bitvectors -- see `Language.Fixpoint.Smt.Bitvector` + +- Added support for string literals + +## 0.2.1.0 + +- Pre-compiled binaries of the underlying ocaml solver are now + provided for Linux, Mac OSX, and Windows. + + No more need to install Ocaml! + +## 0.2.0.0 + +- Parsing has been improved to require *much* fewer parentheses. + +- Experimental support for Z3's theory of real numbers with the `--real` flag. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,375 @@ +Liquid Fixpoint +=============== + + +[![Hackage](https://img.shields.io/hackage/v/liquid-fixpoint.svg)](https://hackage.haskell.org/package/liquid-fixpoint) [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquid-fixpoint.svg)](http://packdeps.haskellers.com/feed?needle=liquid-fixpoint) +[![CircleCI](https://circleci.com/gh/ucsd-progsys/liquid-fixpoint.svg?style=svg)](https://circleci.com/gh/ucsd-progsys/liquid-fixpoint) +[![hlint](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/hlint.yml/badge.svg)](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/hlint.yml) +[![cabal](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/cabal.yml/badge.svg)](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/cabal.yml) +[![stack](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/stack.yml/badge.svg)](https://github.com/ucsd-progsys/liquid-fixpoint/actions/workflows/stack.yml) + + +This package implements a Horn-Clause/Logical Implication constraint solver used +for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to: + ++ [Houdini](https://users.soe.ucsc.edu/~cormac/papers/fme01.pdf) ++ [Cartesian predicate abstraction](http://swt.informatik.uni-freiburg.de/berit/papers/boolean-and-cartesian-....pdf) + + +Requirements +------------ + +In addition to the .cabal dependencies you require an SMTLIB2 compatible solver binary: + +- [Z3](https://github.com/Z3Prover/z3) +- [CVC4](https://cvc4.github.io/) +- [MathSat](http://mathsat.fbk.eu/download.html) + +If on Windows, please make sure to place the binary and any associated DLLs somewhere +in your path. + +How To Build and Install +------------------------ + +``` +$ git clone https://github.com/ucsd-progsys/liquid-fixpoint.git +$ cd liquid-fixpoint +$ stack install # alternatively, use `cabal install`. +``` + +Test with + +``` +$ stack test +``` + +Run with + +``` +$ stack exec fixpoint -- tests/pos/adt.fq +``` + +Using SMTLIB-based SMT Solvers +------------------------------ + +You can use one of several SMTLIB2 compliant solvers, by: + + fixpoint --solver=z3 path/to/file.hs + +Currently, we support + + * Z3 + * CVC4 + * MathSat + +"Horn" Format +------------- + +See the examples in `tests/horn/{pos, neg}` eg + +- [sum](tests/horn/pos/ple_sum.smt2) +- [list00](tests/horn/pos/ple_list00.smt2) +- [list03](tests/horn/neg/ple_list03.smt2) + +For how to write VCs "by hand". + +See [this tutorial](https://arxiv.org/abs/2010.07763) +with [accompanying code](https://github.com/ranjitjhala/sprite-lang) +for an example of how to generate Horn queries. + +The main datatypes are described in [src/Language/Fixpoint/Horn/Types.hs](src/Language/Fixpoint/Horn/Types.hs) + + +Configuration Management +------------------------ + +It is very important that the version of Liquid Fixpoint be maintained properly. + +Suppose that the current version of Liquid Haskell is `A.B.C.D`: + ++ After a release to hackage is made, if any of the components `B`, `C`, or `D` are missing, they shall be added and set to `0`. Then the `D` component of Liquid Fixpoint shall be incremented by `1`. The version of Liquid Fixpoint is now `A.B.C.(D + 1)` + ++ The first time a new function or type is exported from Liquid Fixpoint, if any of the components `B`, or `C` are missing, they shall be added and set to `0`. Then the `C` component shall be incremented by `1`, and the `D` component shall stripped. The version of Liquid Fixpoint is now `A.B.(C + 1)` + ++ The first time the signature of an exported function or type is changed, or an exported function or type is removed (this includes functions or types that Liquid Fixpoint re-exports from its own dependencies), if the `B` component is missing, it shall be added and set to `0`. Then the `B` component shall be incremented by `1`, and the `C` and `D` components shall be stripped. The version of Liquid Fixpoint is now `A.(B + 1)` + ++ The `A` component shall be updated at the sole discretion of the project owners. + +It is recommended to use the [Bumper](https://hackage.haskell.org/package/bumper) utility to manage the versioning of Liquid Fixpoint. Bumper will automatically do the correct update to the cabal file. Additionally, it will update any packages that you have the source for that depend on Liquid Fixpoint. + +To update Liquid Fixpoint and Liquid Haskell, first clone Liquid Haskell and Liquid Fixpoint to a common location: + +``` +git clone https://github.com/ucsd-progsys/liquidhaskell.git +git clone https://github.com/ucsd-progsys/liquid-fixpoint.git +``` + +To increment the `D` component of Liquid Fixpoint: + +``` +./path/to/bumper -3 liquid-fixpoint +``` + +This will update the `D` component of Liquid Fixpoint. If necessary, this will update the `Build-Depends` of Liquid Haskell. If the `Build-Depends` was updated, Liquid Haskell's `D` component will be incremented. + +To increment the `C` component of Liquid Fixpoint, and strip the `D` component: + +``` +./path/to/bumper --minor liquid-fixpoint +``` + +As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell. + +To increment the `B` component of Liquid Fixpoint, and strip the `D` and `C` components: + +``` +./path/to/bumper --major liquid-fixpoint +``` + +As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell + +## SMTLIB2 Interface + +There is a new SMTLIB2 interface directly from Haskell: + ++ Language.Fixpoint.SmtLib2 + +See `tests/smt2/{Smt.hs, foo.smt2}` for an example of how to use it. + +### Command Line for SMT2 interface + +You can use the `.smt2` interface from the command-line as follows: + +Use `--stdin` to read files from `stdin` + +``` +$ more tests/horn/pos/test01.smt2 | fixpoint --stdin + +Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. +All Rights Reserved. + +Working 166% [===============================================================] +Safe ( 2 constraints checked) +``` + +Use `-q` to disable all output (banner, progress bar etc.) + +``` +$ more tests/horn/pos/test01.smt2 | fixpoint -q --stdin +``` + +Use `--json` to get the output as a JSON object (rendered to `stdout`) + +``` +$ more tests/horn/pos/abs02-re.smt2 | stack exec -- fixpoint -q --json --stdin +{"contents":{"numIter":3,"numCstr":3,"numChck":3,"numBrkt":3,"numVald":3},"tag":"Safe"} +``` + + +## Options + +`--higherorder` allows higher order binders into the environment + +`--extsolver` runs the **deprecated** external solver. + +`--parts` Partitions an `FInfo` into a `[FInfo]` and emits a bunch of files. So: + + $ fixpoint -n -p path/to/foo.fq + +will now emit files: + + path/to/.liquid/foo.1.fq + path/to/.liquid/foo.2.fq + . . . + path/to/.liquid/foo.k.fq + +and also a dot file with the constraint dependency graph: + + path/to/.liquid/foo.fq.dot + + +## FInfo Invariants + +### Binders + +This is the field + +``` + , bs :: !BindEnv -- ^ Bind |-> (Symbol, SortedReft) +``` + +or in the .fq files as + +``` +bind 1 x : ... +bind 2 y : ... +``` + +* Each `BindId` must be a distinct `Int`, +* Each `BindId` that appears in a constraint + environment i.e. inside _any_ `IBindEnv` + must appear inside the `bs` + +### Environments + +* Each constraint's environment is a set of `BindId` + which must be defined in the `bindInfo`. Furthermore + +* Each constraint should not have _duplicate_ names in its + environment, that is if you have two binders + +``` + bind 1 x : ... + bind 12 x : ... +``` + + Then a single `IBindEnv` should only mention _at most_ + one of `1` or `12`. + +* There is also a "tree-shape" property that its a bit hard + to describe ... TODO + +### LHS + +Each `slhs` of a constraint is a `SortedReft`. + +- Each `SortredReft` is basically a `Reft` -- a logical predicate. + The important bit is that a `KVar` i.e. terms of the formalized + +``` + $k1[x1:=y1][x2:=y2]...[xn:=yn] +``` + + That is represented in the `Expr` type as + +``` + | PKVar !KVar !Subst +``` + + must appear _only_ at the **top-level** that is not under _any_ + other operators, i.e. not as a sub-`Expr` of other expressions. + + +- This is basically a predicate that needs to be "well sorted" + with respect to the `BindId`, intuitively + +``` + x:int, y:int |- x + y : int +``` + + is well sorted. but + +``` + x:int |- x + y : int +``` + + is not, and + +``` + x:int, y: list |- x + y : int +``` + + is not. The exact definition is formalized in `Language.Fixpoint.SortCheck` + + +### RHS + +Similarly each `rhs` of a `SubC` must either be a single `$k[...]` or an plain `$k`-free `Expr`. + +### Global vs. Distinct Literals + +``` + , gLits :: !(SEnv Sort) -- ^ Global Constant symbols + , dLits :: !(SEnv Sort) +``` + +The _global_ literals `gLits` are symbols that +are in scope _everywhere_ i.e. need not be separately +defined in individual environments. These include things like + +- uninterpreted _measure_ functions `len`, `height`, +- uninterpreted _data constructor_ literals `True`, `False` + +Suppose you have an enumerated type like: + +``` +data Day = Sun | Mon | Tue | Wed | ... | Sat +``` + +You can model the above values in fixpoint as: + +``` +constant lit#Sun : Day +constant lit#Mon : Day +constant lit#Tue : Day +constant lit#Wed : Day +``` + +The _distinct_ literals are a subset of the above where we +want to tell the SMT solver that the values are *distinct* +i.e. **not equal** to each other, for example, you can +**additionally** specify this as: + +``` +distinct lit#Sun : Day +distinct lit#Mon : Day +distinct lit#Tue : Day +distinct lit#Wed : Day +``` + +The above two are represented programmatically by generating +suitable `Symbol` values (for the literals see `litSymbol`) +and `Sort` values as `FTC FTycon` and then making an `SEnv` +from the `[(Symbol, Sort)]`. + +### Sorts + +> What's the difference between an FTC and an FObj? + +In early versions of fixpoint, there was support for +three sorts for expressions (`Expr`) that were sent +to the SMT solver: + +1. `int` +2. `bool` +3. "other" + +The `FObj` sort was introduced to represent essentially _all_ +non-int and non-bool values (e.g. tuples, lists, trees, pointers...) + +However, we later realized that it is valuable to keep _more_ +precise information for `Expr`s and so we introduced the `FTC` +(fixpoint type constructor), which lets us represent the above +respectively as: + +- `FTC "String" []` -- in Haskell `String` +- `FTC "Tuple" [FInt, Bool]` -- in Haskell `(Int, Bool)` +- `FTC "List" [FTC "List" [FInt]]` -- in Haskell `[[Int]]` + +> There is a comment that says FObj's are uninterpretted types; +> so probably a type the SMT solver doesn't know about? +> Does that then make FTC types that the SMT solver does +> know about (bools, ints, lists, sets, etc.)? + +The SMT solver knows about `bool`, `int` and `set` (also `bitvector` +and `map`) but _all_ other types are _currently_ represented as plain +`Int` inside the SMT solver. However, we _will be_ changing this +to make use of SMT support for ADTs ... + +To sum up: the `FObj` is there for historical reasons; it has been +subsumed by `FTC` which is what I recomend you use. However `FObj` +is there if you want a simple "unitype" / "any" type for terms +that are not "interpreted". + +## Qualifier Patterns + +```haskell +λ> doParse' (qualParamP sortP) "" "z as (mon . $1) : int" +QP {qpSym = "z", qpPat = PatPrefix "mon" 1, qpSort = FInt} +λ> doParse' (qualParamP sortP) "" "z as ($1 . mon) : int" +QP {qpSym = "z", qpPat = PatSuffix 1 "mon", qpSort = FInt} +λ> doParse' (qualParamP sortP) "" "z as mon : int" +QP {qpSym = "z", qpPat = PatExact "mon", qpSort = FInt} +λ> doParse' (qualParamP sortP) "" "z : int" +QP {qpSym = "z", qpPat = PatNone, qpSort = FInt} +``` diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquid-fixpoint -version: 0.9.2.5 +version: 0.9.4.7 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint @@ -25,13 +25,15 @@ license: BSD-3-Clause license-file: LICENSE build-type: Simple -tested-with: GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4, GHC == 8.10.1, GHC == 8.10.7 +tested-with: GHC == 9.6.3, GHC == 9.4.7, GHC == 9.2.3 extra-source-files: tests/neg/*.fq tests/pos/*.fq unix/Language/Fixpoint/Utils/*.hs win/Language/Fixpoint/Utils/*.hs tests/logs/cur/pin Makefile +extra-doc-files: CHANGES.md + README.md common warnings ghc-options: @@ -156,7 +158,7 @@ , smtlib-backends-process >= 0.3 , stm , store - , vector < 0.13 + , vector < 0.14 , syb , text , transformers @@ -170,6 +172,8 @@ else hs-source-dirs: src-cond/without-z3 + if impl(ghc<9.6) + ghc-options: -Wno-unused-imports if flag(devel) ghc-options: -Werror if !os(windows) diff --git a/src/Language/Fixpoint/Defunctionalize.hs b/src/Language/Fixpoint/Defunctionalize.hs --- a/src/Language/Fixpoint/Defunctionalize.hs +++ b/src/Language/Fixpoint/Defunctionalize.hs @@ -26,6 +26,7 @@ import qualified Data.HashMap.Strict as M import Data.Hashable +import Control.Monad ((>=>)) import Control.Monad.State import Language.Fixpoint.Misc (fM, secondM, mapSnd) import Language.Fixpoint.Solver.Sanitize (symbolEnv) diff --git a/src/Language/Fixpoint/Horn/Info.hs b/src/Language/Fixpoint/Horn/Info.hs --- a/src/Language/Fixpoint/Horn/Info.hs +++ b/src/Language/Fixpoint/Horn/Info.hs @@ -160,10 +160,7 @@ kvEnvWfCs kve = M.fromList [ (F.KV k, kvWfC info) | (k, info) <- M.toList kve ] hvarArg :: H.Var a -> Int -> F.Symbol -hvarArg k i = F.intSymbol (F.suffixSymbol hvarPrefix (H.hvName k)) i - -hvarPrefix :: F.Symbol -hvarPrefix = F.symbol "nnf_arg" +hvarArg k i = F.hvarArgSymbol (H.hvName k) i ------------------------------------------------------------------------------- -- | Automatically scrape qualifiers from all predicates in a constraint diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs --- a/src/Language/Fixpoint/Parse.hs +++ b/src/Language/Fixpoint/Parse.hs @@ -103,6 +103,7 @@ ) where +import Control.Monad (unless, void) import Control.Monad.Combinators.Expr import qualified Data.IntMap.Strict as IM import qualified Data.HashMap.Strict as M diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs --- a/src/Language/Fixpoint/Solver/Extensionality.hs +++ b/src/Language/Fixpoint/Solver/Extensionality.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE FlexibleContexts #-} @@ -201,11 +202,17 @@ where -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?) d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc tupConName)) 2 [ct] +#if MIN_TOOL_VERSION_ghc(9,6,0) + ct = DCtor (dummyLoc (symbol "GHC.Tuple.Prim.(,)")) [ + DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0) + , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1) + ] +#else ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [ DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0) , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$2")) (FVar 1) ] - +#endif setBEnv :: BindEnv a -> Ex a () setBEnv benv = modify (\st -> st{exbenv = benv}) diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs --- a/src/Language/Fixpoint/Solver/Instantiate.hs +++ b/src/Language/Fixpoint/Solver/Instantiate.hs @@ -35,6 +35,7 @@ import qualified Language.Fixpoint.Solver.PLE as PLE (instantiate) import qualified Language.Fixpoint.Solver.Common as Common (toSMT) import Language.Fixpoint.Solver.Common (askSMT) +import Control.Monad ((>=>), foldM, forM, forM_, join) import Control.Monad.State import Data.Bifunctor (second) import qualified Data.Text as T diff --git a/src/Language/Fixpoint/Solver/Interpreter.hs b/src/Language/Fixpoint/Solver/Interpreter.hs --- a/src/Language/Fixpoint/Solver/Interpreter.hs +++ b/src/Language/Fixpoint/Solver/Interpreter.hs @@ -41,6 +41,7 @@ import Language.Fixpoint.Graph.Deps (isTarget) import Language.Fixpoint.Solver.Sanitize (symbolEnv) import Language.Fixpoint.Solver.Simplify +import Control.Monad (foldM) import Control.Monad.State import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -29,6 +29,7 @@ ) where +import Control.Monad (foldM, forM, forM_, when) import Language.Fixpoint.Utils.Progress import qualified Language.Fixpoint.Types.Config as C import Language.Fixpoint.Types.Config (Config) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -52,6 +52,7 @@ import Language.REST.RuntimeTerm as RT import Language.REST.SMT (withZ3, SolverHandle) +import Control.Monad (filterM, foldM, forM_, when) import Control.Monad.State import Control.Monad.Trans.Maybe import Data.Bifunctor (second) diff --git a/src/Language/Fixpoint/Solver/Rewrite.hs b/src/Language/Fixpoint/Solver/Rewrite.hs --- a/src/Language/Fixpoint/Solver/Rewrite.hs +++ b/src/Language/Fixpoint/Solver/Rewrite.hs @@ -21,7 +21,7 @@ , RESTOrdering(..) ) where -import Control.Monad.State (guard) +import Control.Monad (guard) import Control.Monad.Trans.Maybe import Data.Hashable import qualified Data.HashMap.Strict as M diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs --- a/src/Language/Fixpoint/Solver/Solution.hs +++ b/src/Language/Fixpoint/Solver/Solution.hs @@ -216,8 +216,6 @@ qPat = F.qpPat x mono = So.isMono xt - - -- -------------------------------------------------------------------------------- -- candidates :: So.Env -> [(F.Sort, [F.Symbol])] -> F.QualParam -- -> [(So.TVSubst, QPSubst, F.Symbol)] @@ -240,7 +238,7 @@ F.PatNone -> Just NoSub F.PatExact s -> if s == y then Just NoSub else Nothing where - y = F.tidySymbol y' + y = F.unKArgSymbol y' data QPSubst = NoSub | JustSub Int F.Symbol diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs --- a/src/Language/Fixpoint/SortCheck.hs +++ b/src/Language/Fixpoint/SortCheck.hs @@ -70,7 +70,6 @@ -- import Control.DeepSeq import Control.Exception (Exception, catch, try, throwIO) import Control.Monad -import Control.Monad.Except -- (MonadError(..)) import Control.Monad.Reader import qualified Data.HashMap.Strict as M diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs --- a/src/Language/Fixpoint/Types/Names.hs +++ b/src/Language/Fixpoint/Types/Names.hs @@ -60,6 +60,7 @@ , nonSymbol , vvCon , tidySymbol + , unKArgSymbol -- * Widely used prefixes , anfPrefix @@ -73,6 +74,7 @@ , tempSymbol , gradIntSymbol , appendSymbolText + , hvarArgSymbol -- * Wrapping Symbols , litSymbol @@ -478,6 +480,10 @@ gradIntSymbol :: Integer -> Symbol gradIntSymbol = intSymbol gradPrefix +hvarArgSymbol :: Symbol -> Int -> Symbol +hvarArgSymbol s i = intSymbol (suffixSymbol hvarPrefix s) i + + -- | Used to define functions corresponding to binding predicates -- -- The integer is the BindId. @@ -498,14 +504,39 @@ -- ctorPrefix :: Symbol -- ctorPrefix = "mk$" -kArgPrefix, existPrefix :: Symbol -kArgPrefix = "lq_karg$" -existPrefix = "lq_ext$" +kArgPrefix, existPrefix, hvarPrefix :: Symbol +kArgPrefix = "lq_karg$" +existPrefix = "lq_ext$" +hvarPrefix = "nnf_arg$" -------------------------------------------------------------------------- +-- | `unKArgSymbol` is like `tidySymbol` (see comment below) except it +-- (a) *removes* the argument-index, and +-- (b) *preserves* the `nnf_arg` (without replacing it with `$`) +-- For example `unKArgSymbol lq_karg$nnf_arg$##k0##0##k0` ---> `nnf_arg##k0` + +unKArgSymbol :: Symbol -> Symbol +unKArgSymbol = unSuffixSymbol . unSuffixSymbol . unPrefixSymbol kArgPrefix + +-- | 'tidySymbol' is used to prettify the names of parameters of kvars appearing in solutions.(*) +-- For example, if you have a kvar $k0 with two parameters, you may have a solution that looks like +-- 0 < lq_karg$nnf_arg$##k0##0##k0 +-- where we know it is a kvar-arg because of the +-- - `kArgPrefix` (`lq_arg`) +-- - `hvarArgPrefix` (`nnf_arg`) +-- - `k0` the name of the kvar +-- - `0` the parameter index +-- - `k0` again (IDK why?!) +-- all of which are separated by `##` +-- So `tidySymbol` tests if indeed it is a `kArgPrefix`-ed symbol and if so converts +-- `lq_karg$nnf_arg$##k0##0##k0` ----> `$k0##0` + tidySymbol :: Symbol -> Symbol -------------------------------------------------------------------------- -tidySymbol = unSuffixSymbol . unSuffixSymbol . unPrefixSymbol kArgPrefix +tidySymbol s + | s == s' = s + | otherwise = s'' + where + s' = unPrefixSymbol kArgPrefix s + s'' = consSym '$' . unPrefixSymbol symSepName . unSuffixSymbol . unPrefixSymbol hvarPrefix $ s' unPrefixSymbol :: Symbol -> Symbol -> Symbol unPrefixSymbol p s = fromMaybe s (stripPrefix p s)