liquid-fixpoint 0.6.0.1 → 0.7.0.1

raw patch · 112 files changed

+3294/−11186 lines, 112 filesdep +parallel-iodep +stmdep +tasty-ant-xmldep ~basedep ~containersdep ~mtlnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: parallel-io, stm, tasty-ant-xml

Dependency ranges changed: base, containers, mtl, tasty-hunit, transformers

API changes (from Hackage documentation)

Files

• .ghci +0/−1
• .git +0/−1
• .gitignore +0/−30
• .travis.yml +0/−51
• CHANGES.md +0/−29
• Makefile +0/−59
• README.md +0/−303
• TODO.md +0/−37
• bin/Fixpoint.hs +0/−1
• default.nix +0/−32
• liquid-fixpoint.cabal +16/−7
• scripts/travis +0/−137
• shell.nix +0/−17
• src/Language/Fixpoint/Defunctionalize.hs +70/−51
• src/Language/Fixpoint/Graph/Deps.hs +7/−7
• src/Language/Fixpoint/Graph/Partition.hs +31/−32
• src/Language/Fixpoint/Graph/Reducible.hs +3/−3
• src/Language/Fixpoint/Misc.hs +68/−5
• src/Language/Fixpoint/Parse.hs +80/−21
• src/Language/Fixpoint/Smt/Interface.hs +157/−26
• src/Language/Fixpoint/Smt/Serialize.hs +152/−114
• src/Language/Fixpoint/Smt/Theories.hs +206/−105
• src/Language/Fixpoint/Smt/Types.hs +20/−34
• src/Language/Fixpoint/Solver.hs +18/−13
• src/Language/Fixpoint/Solver/GradualSolution.hs +6/−305
• src/Language/Fixpoint/Solver/GradualSolve.hs +0/−319
• src/Language/Fixpoint/Solver/Instantiate.hs +144/−105
• src/Language/Fixpoint/Solver/Monad.hs +20/−61
• src/Language/Fixpoint/Solver/Sanitize.hs +26/−12
• src/Language/Fixpoint/Solver/Solution.hs +18/−15
• src/Language/Fixpoint/Solver/Solve.hs +194/−23
• src/Language/Fixpoint/SortCheck.hs +303/−252
• src/Language/Fixpoint/Types.hs +1/−0
• src/Language/Fixpoint/Types/Config.hs +2/−0
• src/Language/Fixpoint/Types/Constraints.hs +154/−53
• src/Language/Fixpoint/Types/Environments.hs +3/−0
• src/Language/Fixpoint/Types/Errors.hs +15/−1
• src/Language/Fixpoint/Types/Graduals.hs +258/−0
• src/Language/Fixpoint/Types/Names.hs +60/−9
• src/Language/Fixpoint/Types/PrettyPrint.hs +17/−0
• src/Language/Fixpoint/Types/Refinements.hs +54/−16
• src/Language/Fixpoint/Types/Solutions.hs +21/−18
• src/Language/Fixpoint/Types/Sorts.hs +116/−17
• src/Language/Fixpoint/Types/Spans.hs +4/−0
• src/Language/Fixpoint/Types/Substitutions.hs +2/−2
• src/Language/Fixpoint/Types/Theories.hs +275/−0
• src/Language/Fixpoint/Types/Triggers.hs +7/−0
• src/Language/Fixpoint/Types/Utils.hs +4/−4
• src/Language/Fixpoint/Types/Visitor.hs +91/−57
• stack.yaml +0/−12
• tests/crash/num00.fq +0/−29
• tests/crash/sort00.fq +0/−12
• tests/crash/sort01.fq +0/−13
• tests/cut/test00-tx.fq +0/−12
• tests/cut/test00.fq +0/−28
• tests/cut/test00a-tx.fq +0/−43
• tests/cut/test00a.fq +0/−29
• tests/cut/test1-tx.fq +0/−43
• tests/cut/test1.fq +0/−29
• tests/cut/test2-tx.fq +0/−112
• tests/cut/test2.fq +0/−51
• tests/elim/div00.fq +0/−23
• tests/elim/elim00.fq +0/−1494
• tests/elim/kvparam00.fq +0/−20
• tests/elim/len00.fq +0/−23
• tests/elim/test00-tx.fq +0/−12
• tests/elim/test00.fq +0/−26
• tests/elim/test00a.fq +0/−28
• tests/elim/test1.fq +0/−29
• tests/elim/test2.fq +0/−53
• tests/elim/tuple00.fq +0/−114
• tests/elim/tuple01.fq +0/−137
• tests/minimize/two-cores.fq +0/−30
• tests/neg/NonLinear.hs.fq +0/−91
• tests/neg/adt0.fq +19/−0
• tests/neg/adt1.fq +31/−0
• tests/neg/adt2.fq +18/−0
• tests/neg/adt3.fq +18/−0
• tests/neg/adt_bin_0.fq +30/−0
• tests/neg/adt_even_0.fq +33/−0
• tests/neg/hex00.fq +9/−0
• tests/neg/lit00.fq +18/−0
• tests/neg/test00.hs.fq +0/−286
• tests/pos/LogicCurry1.hs.fq +0/−245
• tests/pos/adt.fq +43/−0
• tests/pos/adt_bin_0.fq +27/−0
• tests/pos/adt_bin_lam.fq +16/−0
• tests/pos/adt_curry.fq +14/−0
• tests/pos/adt_dep_0.fq +16/−0
• tests/pos/adt_dep_1.fq +16/−0
• tests/pos/adt_even_0.fq +33/−0
• tests/pos/adt_list_0.fq +15/−0
• tests/pos/adt_list_1.fq +16/−0
• tests/pos/adt_list_2.fq +14/−0
• tests/pos/adt_list_nested.fq +15/−0
• tests/pos/adt_qual.fq +25/−0
• tests/pos/hex.ts.fq +0/−342
• tests/pos/hex00.fq +9/−0
• tests/pos/listqual.hs.fq +0/−577
• tests/pos/lit00.fq +18/−0
• tests/pos/poly_inst.fq +11/−0
• tests/pos/real00.fq +9/−0
• tests/pos/test00.hs.fq +0/−1021
• tests/pos/test000.hs.fq +0/−489
• tests/smt2/Smt.hs +0/−28
• tests/test.hs +156/−5
• tests/testParser.hs +41/−5
• tests/todo/MergeSort.fq +0/−3234
• tests/todo/baz.fq +0/−22
• tests/todo/poly.fq +0/−14
• tests/todo/wl01.fq +0/−39
• unix/Language/Fixpoint/Utils/Progress.hs +1/−1

@@ -1,1 +0,0 @@-:set -isrc

@@ -1,1 +0,0 @@-gitdir: ../.git/modules/liquid-fixpoint

@@ -1,30 +0,0 @@-.depend-*.cmi-*.cmo-*.cmx-*.o-/dist*-.liquid-/.vagrant/-/.stack-work/-/build.sh-/external/fixpoint/config.make-/external/fixpoint/fixpoint.native-/external/fixpoint/misc-/external/fixpoint/smtZ3.ml-/external/ocamlgraph/META-/external/ocamlgraph/Makefile-/external/ocamlgraph/config.status-/external/ocamlgraph/graph.a-/external/ocamlgraph/graph.cma-/external/ocamlgraph/graph.cmxa-/external/ocamlgraph/src/dot_lexer.ml-/external/ocamlgraph/src/dot_parser.ml-/external/ocamlgraph/src/dot_parser.mli-/external/ocamlgraph/src/dot_parser.output-/external/ocamlgraph/src/gml.ml-/external/ocamlgraph/src/version.ml-/tests/neg/.liquid/-/tests/pos/.liquid/-/external/ocamlgraph/config.log-/TAGS

@@ -1,51 +0,0 @@-language: c-sudo: false--# Only build master, develop, and PRs-branches:-  only:-  - master-  - develop-  - parser-az--matrix:-  include:-    - env: SMT="z3" CABAL=1.22 GHC=7.10.3-      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,],sources: [hvr-ghc]}}-    - env: SMT="z3" CABAL=1.24 GHC=8.0.1-      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,],sources: [hvr-ghc]}}-    - env: SMT="z3" CABAL=1.24 GHC=8.0.2-      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.2,],sources: [hvr-ghc]}}-    - env: CABALVER=head GHCVER=head-      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}--  allow_failures:-   - env: CABALVER=head GHCVER=head--cache:-  directories:-  - $HOME/.cabal-  - $HOME/.ghc--before_install:- - export PATH="$HOME/.cabal/bin:/opt/ghc/$GHC/bin:/opt/cabal/$CABAL/bin:$PATH"- - scripts/travis clean_cache "$SMT"--install:- - scripts/travis install_cabal_deps- - scripts/travis install_smt "$SMT"--script:- - scripts/travis do_build && scripts/travis do_test "$SMT"- - scripts/travis clean_cache "$SMT"--after_failure:- - scripts/travis dump_fail_logs--notifications:-  slack:-    rooms:-      secure: VT1SqW+4WQKb2PXgObQ/rNdQN8pFK5LaFacxB0fEvRZ2FSbM3qp1NGgii7WHlQdr598+L5qYhkpy1B8ssgNeR7iMmYP4GV/fhCoMd8nTQHLSrTMH8iQgT0D7SnuKdk5FQq1IXWtHjUzXtTIhnkfwOJF/xYf6BMMrO0sCta5JZgg=-    on_success: change-    on_failure: always-    on_start: never

@@ -1,29 +0,0 @@-# CHANGES--## NEXT--## 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.

@@ -1,59 +0,0 @@--OPTS="-W -O2 -XStandaloneDeriving"-PROFOPTS="-O2 -rtsopts -prof -auto-all -caf-all -XStandaloneDeriving -XDeriveDataTypeable"--CABAL=cabal-CABALI=$(CABAL) install --ghc-options=$(OPTS)-CABALP=$(CABAL) install --ghc-options=$(OPTS) -p--DEPS=unix-compat transformers mtl filemanip text parsec ghc-paths deepseq comonad contravariant semigroupoids semigroups bifunctors hscolour ansi-terminal hashable unordered-containers--TASTY=./dist/build/test/test--all:-	$(CABAL) install --ghc-options=$(OPTS)--force:-	$(CABAL) install --force-reinstalls --ghc-options=$(OPTS)--rebuild: ocaml-	make--igoto:-	$(CABAL) configure --ghc-options=$(OPTS)--goto:-	$(CABAL) build --ghc-options=$(OPTS)-	cp dist/build/liquid/liquid ~/.cabal/bin/--prof:-	$(CABAL) install --enable-executable-profiling --enable-library-profiling --ghc-options=$(PROFOPTS)--clean:-	cabal clean--docs:-	$(CABAL) haddock --executables --internal --hoogle --hyperlink-source #--html-location=http://goto.ucsd.edu/~rjhala/llvm-haskell/---deps:-	$(CABALI) $(DEPS)--pdeps:-	$(CABALP) $(DEPS)--lint:-	hlint --colour --report .--tags:-	hasktags -c src/-	hasktags -e src/-	hasktags -x -c src/--test:-	cabal configure -fdevel --enable-tests --disable-library-profiling -O2-	cabal build-	cabal exec $(TASTY)--test710:-	$(TASTY)

@@ -1,303 +0,0 @@-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) [![Build Status](https://img.shields.io/travis/ucsd-progsys/liquid-fixpoint/master.svg)](https://travis-ci.org/ucsd-progsys/liquid-fixpoint)-===============---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](http://z3.codeplex.com)-- [CVC4](http://cvc4.cs.nyu.edu)-- [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---------------------------Simply do:--    git clone https://github.com/ucsd-progsys/liquid-fixpoint.git-    cd liquid-fixpoint-    stack install--or (`cabal` instead of `stack` if you prefer.)---Using SMTLIB-based SMT Solvers---------------------------------You can use one of several SMTLIB2 compliant solvers, by:--    fixpoint --smtsolver=z3 path/to/file.hs--Currently, we support--    * Z3-    * CVC4-    * MathSat----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.--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".-

@@ -1,37 +0,0 @@-# TODO--## Proper Encoding of DataTypes--```-(declare-datatypes (T) ((LL lnil (lcons (lhd T) (ltl LL)))))-(declare-fun l1 () (LL Int))-(declare-fun l2 () (LL Int))-(declare-fun l3 () (LL Int))-(declare-fun x  () Int)-(declare-fun zzz () Int)--(assert (not (= l1 (as lnil (LL Int)))))-(assert (not (= l2 (as lnil (LL Int)))))--(assert (= (lhd l1) (lhd l2)))-(assert (not (= l1 l2)))-(assert (= l3 (lcons x l2)))-(assert (> x 100))-(check-sat)--(get-model)---(declare-fun xs () (LL Int))-(declare-fun ys () (LL Int))-(declare-fun y  () Int)--(assert (= xs (as lnil (LL Int))))-(assert (= ys (lcons y ys)))-(assert (= xs ys))-(check-sat)---;; (assert (= (ltl l1) (ltl l2)))-;; (check-sat)-```

@@ -8,4 +8,3 @@   writeLoud $  "Options: " ++ show cfg   e <- solveFQ cfg   exitWith e-

@@ -1,32 +0,0 @@-{ fetchgitLocal }:-{ mkDerivation, ansi-terminal, array, ascii-progress, async-, attoparsec, base, bifunctors, binary, boxes, bytestring, cereal-, cmdargs, containers, deepseq, directory, filemanip, filepath-, ghc-prim, hashable, intern, located-base, mtl, parallel, parsec, pretty-, process, stdenv, syb, tasty, tasty-hunit, tasty-rerun, text-, text-format, transformers, unordered-containers, z3-, dotgen, fgl, fgl-visualize-}:-mkDerivation {-  pname = "liquid-fixpoint";-  version = "9.9.9.9";-  src = fetchgitLocal ./.;-  isLibrary = true;-  isExecutable = true;-  libraryHaskellDepends = [-    ansi-terminal array ascii-progress async attoparsec base bifunctors-    binary boxes bytestring cereal cmdargs containers deepseq directory-    filemanip filepath ghc-prim hashable intern located-base mtl parallel parsec-    pretty process syb text text-format transformers-    unordered-containers-    dotgen fgl fgl-visualize-  ];-  executableHaskellDepends = [ base ];-  testHaskellDepends = [-    base directory filepath process tasty tasty-hunit tasty-rerun text-  ];-  testSystemDepends = [ z3 ];-  homepage = "https://github.com/ucsd-progsys/liquid-fixpoint";-  description = "Predicate Abstraction-based Horn-Clause/Implication Constraint Solver";-  license = stdenv.lib.licenses.bsd3;-}

@@ -1,5 +1,5 @@ name:                liquid-fixpoint-version:             0.6.0.1+version:             0.7.0.1 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego. synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage:            https://github.com/ucsd-progsys/liquid-fixpoint@@ -51,7 +51,7 @@   if flag(devel)     ghc-options: -Werror   hs-source-dirs: bin-  Build-Depends: base >= 4.8 && < 5+  Build-Depends: base >=4.8.1.0 && <5                , liquid-fixpoint  Library@@ -59,12 +59,12 @@   ghc-options:     -W -fno-warn-missing-methods   if flag(devel)     ghc-options:   -Werror-  ghc-prof-options: -fprof-auto   hs-source-dirs:  src   Exposed-Modules: Language.Fixpoint.Types.Names,                    Language.Fixpoint.Types.Errors,                    Language.Fixpoint.Types.Config,                    Language.Fixpoint.Types.Visitor,+                   Language.Fixpoint.Types.Theories,                    Language.Fixpoint.Types.PrettyPrint,                    Language.Fixpoint.Types.Spans,                    Language.Fixpoint.Types.Sorts,@@ -75,6 +75,7 @@                    Language.Fixpoint.Types.Triggers,                    Language.Fixpoint.Types.Solutions,                    Language.Fixpoint.Types.Utils,+                   Language.Fixpoint.Types.Graduals,                    Language.Fixpoint.Types,                    Language.Fixpoint.Graph.Types,                    Language.Fixpoint.Graph.Reducible,@@ -106,10 +107,9 @@                    Language.Fixpoint.Solver.Instantiate,                    Language.Fixpoint.Solver.Sanitize,                    Language.Fixpoint.Utils.Statistics,-                   Language.Fixpoint.Solver.GradualSolve,                    Language.Fixpoint.Solver.Solve -  Build-Depends: base >= 4.8 && < 5+  Build-Depends: base >=4.8.1.0 && <5                , array                , async                , attoparsec@@ -143,6 +143,7 @@                , fgl-visualize                , dotgen                , time+               , parallel-io    if impl(ghc >= 7.10.2)     Build-Depends: located-base@@ -160,13 +161,19 @@   if flag(devel)     ghc-options:    -Werror   main-is:          test.hs-  build-depends:    base,+  build-depends:    base >= 4.8 && < 5,                     directory,                     filepath,                     process,+                    stm >= 2.4,+                    containers >= 0.5,+                    mtl >= 2.1,+                    transformers >= 0.3,                     tasty >= 0.10,                     tasty-hunit,                     tasty-rerun >= 1.1,+                    tasty-ant-xml,+                    tasty-hunit >= 0.9,                     text  test-suite testparser@@ -177,12 +184,14 @@   if flag(devel)     ghc-options:    -Werror   main-is:          testParser.hs-  build-depends:    base,+  build-depends:    base >= 4.8 && < 5,                     directory,                     filepath,                     tasty >= 0.10,                     tasty-hunit,                     tasty-rerun >= 1.1,+                    tasty-ant-xml,+                    tasty-hunit >= 0.9,                     text   if flag(devel)     hs-source-dirs:   tests src

@@ -1,137 +0,0 @@-#!/bin/bash--set -eu-set -o pipefail--## Helper Functions--function loud {-  echo "$ $@"-  $@-}--# Source: https://github.com/travis-ci/travis-build/blob/fc4ae8a2ffa1f2b3a2f62533bbc4f8a9be19a8ae/lib/travis/build/script/templates/header.sh#L104-L123-RED="\033[31;1m"-GREEN="\033[32;1m"-RESET="\033[0m"-function travis_retry {-  local result=0-  local count=1-  while [ $count -le 3 ]; do-    [ $result -ne 0 ] && {-      echo -e "\n${RED}The command \"$@\" failed. Retrying, $count of 3.${RESET}\n" >&2-    }-    set +e-    "$@"-    result=$?-    set -e-    [ $result -eq 0 ] && break-    count=$(($count + 1))-    sleep 1-  done--  [ $count -eq 4 ] && {-    echo "\n${RED}The command \"$@\" failed 3 times.${RESET}\n" >&2-  }--  return $result-}--function prevent_timeout {-  local cmd="$@"--  $cmd &-  local cmd_pid=$!--  poke_stdout &-  local poke_pid=$!--  wait $cmd_pid-  exit_code=$?--  kill $poke_pid-  (wait $poke_pid 2>/dev/null) || true--  return $exit_code-}--function poke_stdout {-  # Print an invisible character every minute-  while true; do-    echo -ne "\xE2\x80\x8B"-    sleep 60-  done-}--function pastebin {-  curl -s -F 'clbin=<-' https://clbin.com-}--## Testing Stages--function clean_cache {-  local smt="$1"--  loud ghc-pkg unregister liquid-fixpoint --force || true-  loud rm "$HOME/.cabal/bin/$smt" || true-}--function install_smt {-  local smt="$1"--  mkdir -p "$HOME/.cabal/bin"-  loud curl "http://goto.ucsd.edu/~gridaphobe/$smt" -o "$HOME/.cabal/bin/$smt"-  loud chmod a+x "$HOME/.cabal/bin/$smt"-}--function install_cabal_deps {-  if ! _install_cabal_deps; then-    echo " ==> Cabal install failed. Clearing dependency cache and retrying."-    loud rm -rf "$HOME/.cabal"-    loud rm -rf "$HOME/.ghc"-    _install_cabal_deps-  fi-}--function _install_cabal_deps {-  loud travis_retry cabal update || return 1-  loud travis_retry cabal install --only-dependencies --enable-tests || return 1-}--function do_build {-  loud cabal configure -fbuild-external --enable-tests -v2-  loud prevent_timeout cabal build -j2-  loud cabal haddock-}--function do_test {-  loud prevent_timeout ./dist/build/test/test-}--function dump_fail_logs {-  find . -type f -wholename '*/.liquid/*' -name '*.log' -print0 | while IFS= read -r -d $'\0' file; do-    echo "${file}:"-    echo "    $(pastebin < "${file}")"-  done-}--function test_source_pkg {-  loud cabal sdist--  local src_tgz="dist/$(cabal info . | awk '{print $2 ".tar.gz";exit}')"--  if [ -f "$src_tgz" ]; then-    loud prevent_timeout cabal install -j4 "$src_tgz"-  else-    echo "expected '$src_tgz' not found"-    return 1-  fi-}--## Run Test Stage--stage="$1"-shift--$stage "$@"-

@@ -1,17 +0,0 @@-{ nixpkgs ? import <nixpkgs> {}, compiler ? "default" }:--let--  inherit (nixpkgs) pkgs;--  f = import ./default.nix { inherit (pkgs) fetchgitLocal; };--  haskellPackages = if compiler == "default"-                       then pkgs.haskellPackages-                       else pkgs.haskell.packages.${compiler};--  drv = haskellPackages.callPackage f { inherit (pkgs) z3; };--in--  if pkgs.lib.inNixShell then drv.env else drv

@@ -5,6 +5,7 @@ {-# LANGUAGE PatternGuards        #-} {-# LANGUAGE OverloadedStrings    #-} + -------------------------------------------------------------------------------- -- | `defunctionalize` traverses the query to: --      1. "normalize" lambda terms by renaming binders,@@ -18,7 +19,12 @@ --   `EApp` and `ELam` to determine the lambdas and redexes. -------------------------------------------------------------------------------- -module Language.Fixpoint.Defunctionalize (defunctionalize, Defunc(..), defuncAny, makeLamArg) where+module Language.Fixpoint.Defunctionalize+  ( defunctionalize+  , Defunc(..)+  , defuncAny+  , defuncAxioms+  ) where  import qualified Data.HashMap.Strict as M import           Data.Hashable@@ -37,13 +43,18 @@ defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a defunctionalize cfg si = evalState (defunc si) (makeInitDFState cfg si) -defuncAny :: Defunc a => Config -> SEnv Sort -> a -> a +defuncAny :: Defunc a => Config -> SymEnv -> a -> a defuncAny cfg env e = evalState (defunc e) (makeDFState cfg env emptyIBindEnv) +defuncAxioms :: (Defunc a) => Config -> SymEnv -> a -> (a, [Triggered Expr])+defuncAxioms cfg env z = flip evalState (makeDFState cfg env emptyIBindEnv) $ do+  z' <- defunc z+  as <- map noTrigger <$> makeAxioms+  return (z', as) ------------------------------------------------------------------------------------ | Expressions defunctionalization ----------------------------------------------------------------------------------------------------------------------------+---------------------------------------------------------------------------------------------+-- | Expressions defunctionalization --------------------------------------------------------+--------------------------------------------------------------------------------------------- txExpr :: Expr -> DF Expr txExpr e = do   hoFlag <- gets dfHO@@ -56,7 +67,7 @@          >=> mapMExpr (fM normalizeLams)  reBind :: Expr -> DF Expr-reBind (ELam (x, s) e) = (\y -> ELam (y, s) (subst1 e (x, EVar y))) <$> freshSym s+reBind (ELam (x, s) e) = ((\y -> ELam (y, s) (subst1 e (x, EVar y))) <$> freshSym s) reBind e               = return e  maxLamArg :: Int@@ -64,20 +75,19 @@  -- NIKI TODO: allow non integer lambda arguments -- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort]-makeLamArg :: Sort -> Int -> Symbol-makeLamArg _ = intArgName+-- makeLamArg :: Sort -> Int -> Symbol+-- makeLamArg _ = intArgName  --------------------------------------------------------------------------------- makeAxioms :: DF [Expr] makeAxioms = do   alphEqs <- concatMap makeAlphaAxioms <$> getLams-  betaEqs <- concatMap makeBetaAxioms  <$> getRedexes+  betaEqs <- concatMap makeBetaAxioms  <$> ({- tracepp "getRedexes" <$> -} getRedexes)   env     <- gets dfEnv   return   $ filter (validAxiom env) (alphEqs ++ betaEqs) -validAxiom :: SEnv Sort -> Expr -> Bool-validAxiom env = isJust . checkSortExpr env+validAxiom :: SymEnv -> Expr -> Bool+validAxiom env = isJust . checkSortExpr (seSort env)  -------------------------------------------------------------------------------- -- | Alpha Equivalence ---------------------------------------------------------@@ -106,9 +116,10 @@ normalize :: Expr -> Expr normalize = snd . go   where-    go (ELam (y, sy) e) = let (i', e') = go e-                              y'      = makeLamArg sy i'-                          in (i'+1, ELam (y', sy) (e' `subst1` (y, EVar y')))+    go (ELam (y, sy) e) = (i + 1, shiftLam i y sy e') where (i, e') = go e+                              -- y'       = lamArgSymbol i'  -- SHIFTLAM+                          -- in  -- ELam (y', sy) (e' `subst1` (y, EVar y')))+     go (EApp e e2)       |  (ELam (x, _) bd) <- unECst e                         = let (i1, e1') = go bd@@ -124,6 +135,12 @@     unECst (ECst e _) = unECst e     unECst e          = e +shiftLam :: Int -> Symbol -> Sort -> Expr -> Expr+shiftLam i x t e = ELam (x_i, t) (e `subst1` (x, x_i_t))+  where+    x_i          = lamArgSymbol i+    x_i_t        = ECst (EVar x_i) t+ -- normalize lambda arguments [TODO: example]  normalizeLams :: Expr -> Expr@@ -132,9 +149,10 @@ normalizeLamsFromTo :: Int -> Expr -> (Int, Expr) normalizeLamsFromTo i   = go   where-    go (ELam (y, sy) e) = let (i', e') = go e-                              y'      = makeLamArg sy i'-                          in (i' + 1, ELam (y', sy) (e' `subst1` (y, EVar y')))+    go (ELam (y, sy) e) = (i + 1, shiftLam i y sy e') where (i, e') = go e+                          -- let (i', e') = go e+                          --    y'       = lamArgSymbol i'  -- SHIFTLAM+                          -- in (i' + 1, ELam (y', sy) (e' `subst1` (y, EVar y')))     go (EApp e1 e2)     = let (i1, e1') = go e1                               (i2, e2') = go e2                           in (max i1 i2, EApp e1' e2')@@ -170,18 +188,10 @@ splitPAll acc (PAll xs e) = splitPAll (acc ++ xs) e splitPAll acc e           = (acc, e) --- NOPROP instantiate :: [(Symbol, Sort)] -> [[(Symbol, (Symbol,Sort))]]--- NOPROP instantiate []     = [[]]--- NOPROP instantiate xs     = L.foldl' (\acc x -> combine (instOne x) acc) [] xs-  -- NOPROP where-    -- NOPROP instOne (x, s) = [(x, (makeLamArg s i, s)) | i <- [1..maxLamArg]]-    -- NOPROP combine xs []  = [[x] | x <- xs]-    -- NOPROP combine xs acc = concat [(x:) <$> acc | x <- xs]--instantiate    :: [(Symbol, Sort)] -> [[(Symbol, (Symbol,Sort))]]-instantiate     = choices . map inst1+instantiate     :: [(Symbol, Sort)] -> [[(Symbol, (Symbol, Sort))]]+instantiate      = choices . map inst1   where-    inst1 (x,s) = [(x, (makeLamArg s i, s)) | i <- [1..maxLamArg]]+    inst1 (x, s) = [(x, (lamArgSymbol i, s)) | i <- [1..maxLamArg]]  choices :: [[a]] -> [[a]] choices []       = [[]]@@ -202,7 +212,7 @@     gLits' <- defunc $ gLits fi     dLits' <- defunc $ dLits fi     bs'    <- defunc $ bs    fi-    ass'   <- defunc $ asserts fi +    ass'   <- defunc $ asserts fi     -- NOPROP quals' <- defunc $ quals fi     axioms <- makeAxioms     return $ fi { cm      = cm'@@ -211,11 +221,11 @@                 , dLits   = dLits'                 , bs      = bs'                 -- NOPROP , quals   = quals'-                , asserts = (noTrigger <$> axioms) ++ ass' +                , asserts = (noTrigger <$> axioms) ++ ass'                 }  instance (Defunc a) => Defunc (Triggered a) where-  defunc (TR t e) = TR t <$> defunc e +  defunc (TR t e) = TR t <$> defunc e  instance Defunc (SimpC a) where   defunc sc = do crhs' <- defunc $ _crhs sc@@ -276,8 +286,8 @@ type DF    = State DFST  data DFST = DFST-  { dfFresh   :: !Int-  , dfEnv   :: !(SEnv Sort)+  { dfFresh :: !Int+  , dfEnv   :: !SymEnv   , dfBEnv  :: !IBindEnv   , dfLam   :: !Bool        -- ^ normalize lams   , dfExt   :: !Bool        -- ^ enable extensionality axioms@@ -291,14 +301,13 @@   , dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders   } --makeDFState :: Config -> SEnv Sort -> IBindEnv -> DFST-makeDFState cfg senv ibind = DFST+makeDFState :: Config -> SymEnv -> IBindEnv -> DFST+makeDFState cfg env ibind = DFST   { dfFresh = 0-  , dfEnv   = senv +  , dfEnv   = env   , dfBEnv  = ibind   , dfLam   = True-  , dfExt   = False +  , dfExt   = False   , dfAEq   = alphaEquivalence cfg   , dfBEq   = betaEquivalence  cfg   , dfNorm  = normalForm       cfg@@ -310,12 +319,11 @@   , dfBinds = mempty   } - makeInitDFState :: Config -> SInfo a -> DFST-makeInitDFState cfg si -  = makeDFState cfg -         (symbolEnv cfg si) -         (mconcat ((senv <$> M.elems (cm si)) ++ (wenv <$> M.elems (ws si))))+makeInitDFState cfg si+  = makeDFState cfg+      (symbolEnv cfg si)+      (mconcat ((senv <$> M.elems (cm si)) ++ (wenv <$> M.elems (ws si))))  -------------------------------------------------------------------------------- -- | Low level monad manipulation ----------------------------------------------@@ -331,18 +339,29 @@ logLam e = whenM (gets dfAEq) (putLam e) >> return e  logRedex :: Expr -> DF Expr-logRedex e = whenM (gets dfBEq) (putRedex e) >> return e+logRedex e = do+  whenM (gets dfBEq) $+    when ({- tracepp ("isRedex:" ++ showpp e) $ -} isRedex e)+      (modify $ \s -> s { dfRedex = ({- tracepp "putRedex" -} e) : dfRedex s })+  return e +  -- (putRedex (tracepp "isRedex" e)) >> return e+ putLam :: Expr -> DF () putLam e@(ELam {}) = modify $ \s -> s { dfLams = e : dfLams s} putLam _           = return () -putRedex :: Expr -> DF ()-putRedex e@(EApp f _)-  | ELam _ _ <- stripCasts f-  = modify $ \s -> s { dfRedex = e : dfRedex s }-putRedex _-  = return ()+isRedex :: Expr -> Bool+isRedex (EApp f _)+  | ELam _ _ <- stripCasts f = True+isRedex _                    = False+++-- putRedex :: Expr -> DF ()+-- putRedex e@(EApp f _) = case stripCasts f of+                          -- ELam _ _ -> modify $ \s -> s { dfRedex = (tracepp "putRedex" e) : dfRedex s }+                          -- e'       -> return  $ tracepp ("SKIP-Redex" ++ showpp e') ()+-- putRedex _            = return ()   -- | getLams and getRedexes return the (previously seen) lambdas and redexes,

@@ -222,7 +222,7 @@ -------------------------------------------------------------------------------- -- | Eliminated Dependencies ---------------------------------------------------------------------------------elimDeps :: F.SInfo a -> [CEdge] -> S.HashSet F.KVar -> CDeps+elimDeps :: (F.TaggedC c a) => F.GInfo c a -> [CEdge] -> S.HashSet F.KVar -> CDeps elimDeps si es nonKutVs = graphDeps si es'   where     es'                 = graphElim es nonKutVs@@ -437,7 +437,7 @@   ----------------------------------------------------------------------------graphDeps :: F.SInfo a -> [CEdge] -> CDeps+graphDeps :: F.TaggedC c a => F.GInfo c a -> [CEdge] -> CDeps --------------------------------------------------------------------------- graphDeps fi cs = CDs { cSucc   = gSucc cg                       , cPrev   = cPrevM@@ -472,15 +472,15 @@     iWrites  = group [ (i, k) | (Cstr i, KVar k) <- es ]     kReads   = group [ (k, j) | (KVar k, Cstr j) <- es ] -rankF :: CMap (F.SimpC a) -> CMap Int -> CMap Int -> F.SubcId -> Rank+rankF ::  F.TaggedC c a => CMap (c a) -> CMap Int -> CMap Int -> F.SubcId -> Rank rankF cm outR inR = \i -> Rank (outScc i) (inScc i) (tag i)   where     outScc        = lookupCMap outR     inScc         = lookupCMap inR-    tag           = F._ctag . lookupCMap cm+    tag           = F.stag . lookupCMap cm  ----------------------------------------------------------------------------inRanks :: F.SInfo a -> [DepEdge] -> CMap Int -> CMap Int+inRanks ::  F.TaggedC c a => F.GInfo c a -> [DepEdge] -> CMap Int -> CMap Int --------------------------------------------------------------------------- inRanks fi es outR   | ks == mempty      = outR@@ -496,7 +496,7 @@     isKutWrite        = any (`F.ksMember` ks) . kvWriteBy cm  ---------------------------------------------------------------------------------graphStatistics :: Config -> F.SInfo a -> IO ()+graphStatistics :: F.TaggedC c a => Config -> F.GInfo c a -> IO () -------------------------------------------------------------------------------- graphStatistics cfg si = when (elimStats cfg) $ do   -- writeGraph f  (kvGraph si)@@ -525,7 +525,7 @@     , ("KVars NonLin"     , pprint stSetKVNonLin)     ] -graphStats :: Config -> F.SInfo a -> Stats+graphStats :: F.TaggedC c a => Config -> F.GInfo c a -> Stats graphStats cfg si = Stats {     stNumKVCuts   = S.size $ F.tracepp "CUTS:" (depCuts d)   , stNumKVNonLin = S.size  nlks

@@ -51,12 +51,12 @@ -- | Constraint Partition Container -------------------------------------------- -------------------------------------------------------------------------------- -data CPart a = CPart { pws :: !(M.HashMap F.KVar (F.WfC a))-                     , pcm :: !(M.HashMap Integer (F.SubC a))-                     }--instance Monoid (CPart a) where-   mempty = CPart mempty mempty+data CPart c a = CPart { pws :: !(M.HashMap F.KVar (F.WfC a))+                       , pcm :: !(M.HashMap Integer (c a))+                       }+  +instance Monoid (CPart c a) where+   mempty      = CPart mempty mempty    mappend l r = CPart { pws = pws l `mappend` pws r                        , pcm = pcm l `mappend` pcm r                        }@@ -79,7 +79,7 @@                  , mcMaxPartSize = maxPartSize c                  } -partition :: (F.Fixpoint a) => Config -> F.FInfo a -> IO (F.Result (Integer, a))+partition :: (F.Fixpoint a, F.Fixpoint (c a), F.TaggedC c a) => Config -> F.GInfo c a -> IO (F.Result (Integer, a)) partition cfg fi   = do dumpPartitions cfg fis        -- writeGraph      f   g@@ -93,7 +93,8 @@ --   produce the maximum possible number of partitions. Or a MultiCore Info --   to control the partitioning -------------------------------------------------------------------------------partition' :: Maybe MCInfo -> F.FInfo a -> [F.FInfo a]+partition' :: (F.TaggedC c a) +           => Maybe MCInfo -> F.GInfo c a -> [F.GInfo c a] ------------------------------------------------------------------------------ partition' mn fi  = case mn of    Nothing -> fis mkPartition id@@ -105,10 +106,10 @@  -- | Partition an FInfo into a specific number of partitions of roughly equal -- amounts of work-partitionN :: MCInfo    -- ^ describes thresholds and partiton amounts-           -> F.FInfo a   -- ^ The originial FInfo-           -> [CPart a] -- ^ A list of the smallest possible CParts-           -> [F.FInfo a] -- ^ At most N partitions of at least thresh work+partitionN :: MCInfo        -- ^ describes thresholds and partiton amounts+           -> F.GInfo c a   -- ^ The originial FInfo+           -> [CPart c a]   -- ^ A list of the smallest possible CParts+           -> [F.GInfo c a] -- ^ At most N partitions of at least thresh work partitionN mi fi cp    | cpartSize (finfoToCpart fi) <= minThresh = [fi]    | otherwise = map (cpartToFinfo fi) $ toNParts sortedParts@@ -140,23 +141,21 @@  -- | Return the "size" of a CPart. Used to determine if it's -- substantial enough to be worth parallelizing.-cpartSize :: CPart a -> Int+cpartSize :: CPart c a -> Int cpartSize c = (M.size . pcm) c + (length . pws) c  -- | Convert a CPart to an FInfo-cpartToFinfo :: F.FInfo a -> CPart a -> F.FInfo a-cpartToFinfo fi p = fi { F.cm = pcm p-                       , F.ws = pws p-                       }+cpartToFinfo :: F.GInfo c a -> CPart c a -> F.GInfo c a+cpartToFinfo fi p = fi {F.ws = pws p, F.cm = pcm p}   -- | Convert an FInfo to a CPart-finfoToCpart :: F.FInfo a -> CPart a+finfoToCpart :: F.GInfo c a -> CPart c a finfoToCpart fi = CPart { pcm = F.cm fi                         , pws = F.ws fi                         }  --------------------------------------------------------------------------------------dumpPartitions :: (F.Fixpoint a) => Config -> [F.FInfo a] -> IO ()+dumpPartitions :: (F.Fixpoint (c a), F.Fixpoint a) => Config -> [F.GInfo c a] -> IO () ------------------------------------------------------------------------------------- dumpPartitions cfg fis =   forM_ (zip [0..] fis) $ \(i, fi) ->@@ -165,16 +164,16 @@  -- | Type alias for a function to construct a partition. mkPartition and --   mkPartition' are the two primary functions that conform to this interface-type PartitionCtor a b = F.FInfo a-                       -> M.HashMap Int [(Integer, F.SubC a)]+type PartitionCtor c a b = F.GInfo c a+                       -> M.HashMap Int [(Integer, c a)]                        -> M.HashMap Int [(F.KVar, F.WfC a)]                        -> Int                        -> b -- ^ typically a F.FInfo a or F.CPart a -partitionByConstraints :: PartitionCtor a b -- ^ mkPartition or mkPartition'-                          -> F.FInfo a-                          -> KVComps-                          -> ListNE b -- ^ [F.FInfo a] or [F.CPart a]+partitionByConstraints :: PartitionCtor c a b -- ^ mkPartition or mkPartition'+                       -> F.GInfo c a+                       -> KVComps+                       -> ListNE b          -- ^ [F.FInfo a] or [F.CPart a] partitionByConstraints f fi kvss = f fi icM iwM <$> js   where     js   = fst <$> jkvs                                -- groups@@ -189,21 +188,21 @@     kM   = M.fromList [ (k, i) | (KVar k, i) <- kvI ]     cM   = M.fromList [ (c, i) | (Cstr c, i) <- kvI ] -mkPartition :: F.GInfo F.SubC a+mkPartition :: F.GInfo c a             -> M.HashMap Int [(Integer, c a)]             -> M.HashMap Int [(F.KVar, F.WfC a)]             -> Int             -> F.GInfo c a mkPartition fi icM iwM j-  = fi { F.cm       = M.fromList $ M.lookupDefault [] j icM-       , F.ws       = M.fromList $ M.lookupDefault [] j iwM-       }+  = fi{ F.cm       = M.fromList $ M.lookupDefault [] j icM+      , F.ws       = M.fromList $ M.lookupDefault [] j iwM+      } -mkPartition' :: F.FInfo a1-             -> M.HashMap Int [(Integer, F.SubC a)]+mkPartition' :: F.GInfo c a+             -> M.HashMap Int [(Integer, c a)]              -> M.HashMap Int [(F.KVar, F.WfC a)]              -> Int-             -> CPart a+             -> CPart c a mkPartition' _ icM iwM j   = CPart { pcm       = M.fromList $ M.lookupDefault [] j icM           , pws       = M.fromList $ M.lookupDefault [] j iwM

@@ -16,7 +16,7 @@   ---------------------------------------------------------------------------------isReducible :: F.SInfo a -> Bool+isReducible :: (F.TaggedC c a) => F.GInfo c a -> Bool -------------------------------------------------------------------------------- isReducible fi = all (isReducibleWithStart g) vs   where@@ -32,7 +32,7 @@   -convertToGraph :: F.SInfo a -> Gr Int ()+convertToGraph :: (F.TaggedC c a) => F.GInfo c a -> Gr Int () convertToGraph fi = mkGraph vs es   where     subCs        = M.elems (F.cm fi)@@ -57,6 +57,6 @@   where     (Just xs) = lookup u t -subcEdges' :: (F.KVar -> Node) -> F.BindEnv -> F.SimpC a -> [(Node, Node)]+subcEdges' :: (F.TaggedC c a) => (F.KVar -> Node) -> F.BindEnv -> c a -> [(Node, Node)] subcEdges' kvI be c = [(kvI k1, kvI k2) | k1 <- V.envKVars be c                                         , k2 <- V.kvars $ F.crhs c]

@@ -5,6 +5,7 @@ {-# LANGUAGE TupleSections             #-} {-# LANGUAGE ConstraintKinds           #-} {-# LANGUAGE TypeOperators             #-}+{-# LANGUAGE BangPatterns              #-} {-# LANGUAGE ImplicitParams            #-} -- ignore hlint  module Language.Fixpoint.Misc where@@ -14,7 +15,7 @@ import           Data.Hashable -- import           Data.IORef import           Control.Arrow                    (second)-import           Control.Monad                    (when, forM_)+import           Control.Monad                    (when, forM_, filterM) import qualified Data.HashMap.Strict              as M import qualified Data.List                        as L import           Data.Tuple                       (swap)@@ -35,6 +36,7 @@ import           System.Exit                      (ExitCode) import           Control.Concurrent.Async + #ifdef MIN_VERSION_located_base import Prelude hiding (error, undefined) import GHC.Err.Located@@ -199,6 +201,9 @@ allMap :: (Eq k, Hashable k) => (v -> Bool) -> M.HashMap k v -> Bool allMap p = L.foldl' (\a v -> a && p v) True +hashNub :: (Eq k, Hashable k) => [k] -> [k]+hashNub = M.keys . M.fromList . fmap (, ())+ sortNub :: (Ord a) => [a] -> [a] sortNub = nubOrd . L.sort   where@@ -207,6 +212,8 @@       | otherwise = x : nubOrd t     nubOrd xs     = xs +duplicates :: (Eq k, Hashable k) => [k] -> [k]+duplicates xs = [ x | (x, n) <- count xs, 1 < n ]  #ifdef MIN_VERSION_located_base safeZip :: (?callStack :: CallStack) => String -> [a] -> [b] -> [(a,b)]@@ -240,14 +247,21 @@ safeInit   :: (?callStack :: CallStack) => String -> ListNE a -> [a] safeUncons :: (?callStack :: CallStack) => String -> ListNE a -> (a, [a]) safeUnsnoc :: (?callStack :: CallStack) => String -> ListNE a -> ([a], a)+safeFromList :: (?callStack :: CallStack, Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v #else safeHead   :: String -> ListNE a -> a safeLast   :: String -> ListNE a -> a safeInit   :: String -> ListNE a -> [a] safeUncons :: String -> ListNE a -> (a, [a]) safeUnsnoc :: String -> ListNE a -> ([a], a)+safeFromList :: (Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v #endif +safeFromList msg kvs = applyNonNull (M.fromList kvs) err (dups kvs)+  where+    dups             = duplicates . fmap fst+    err              = errorstar . wrap "safeFromList with duplicates" msg . show+    wrap m1 m2 s     = m1 ++ " " ++ s ++ " " ++ m2  safeHead _   (x:_) = x safeHead msg _     = errorstar $ "safeHead with empty list " ++ msg@@ -292,6 +306,13 @@ singleton :: a -> [a] singleton x = [x] +pair :: a -> a -> [a]+pair x1 x2 = [x1, x2]++triple :: a -> a -> a -> [a]+triple x1 x2 x3 = [x1, x2, x3]++ fM :: (Monad m) => (a -> b) -> a -> m b fM f = return . f @@ -315,7 +336,26 @@     (g,f,_)         = G.graphFromEdges . eF $ x     vss             = T.flatten <$> G.components g +topoSortWith :: (Ord v) => (a -> (v, [v])) -> [a] -> [a]+topoSortWith vF xs = fst3 . f <$> G.topSort g+  where+    (g, f, _)      = G.graphFromEdges es+    es             = [ (x, ux, vxs) | x <- xs, let (ux, vxs) = vF x ] +-- >>> λ> exTopo+-- >>> [1,2,4,6,5,3]+exTopo  :: [Int]+exTopo  = topoSortWith f [1,2,3,4,5,6]+  where+    f 1 = (1, [2, 3])+    f 2 = (2, [3, 4])+    f 3 = (3, []    )+    f 4 = (4, [5, 6])+    f 5 = (5, []    )+    f 6 = (6, [3]   )+    f n = (n, []    )++ type EqHash a = (Eq a, Ord a, Hashable a)  -- >>> coalesce [[1], [2,1], [5], [5, 6], [5, 7], [9, 6], [10], [10,100]]@@ -347,7 +387,30 @@  {-@ allCombinations :: xss:[[a]] -> [{v:[a]| len v == len xss}] @-} allCombinations :: [[a]] -> [[a]]-allCombinations []          = [[]]-allCombinations [[]]        = [[]]-allCombinations ([]:_)     = []-allCombinations ((x:xs):ys) = ((x:) <$> allCombinations ys) ++ allCombinations (xs:ys)+allCombinations xs = assert (and . map (((length xs) == ) . length)) $ go xs+  where+   go []          = [[]]+   go [[]]        = []+   go ([]:_)      = []+   go ((x:xs):ys) = ((x:) <$> go ys) ++ go (xs:ys)++   assert b x = if b x then x else errorstar "allCombinations: assertion violation"++powerset :: [a] -> [[a]]+powerset xs = filterM (const [False, True]) xs+++(<$$>) ::  (Monad m) => (a -> m b) -> [a] -> m [b]+_ <$$> []           = return []+f <$$> [x1]         = singleton <$> f x1+f <$$> [x1, x2]     = pair      <$> f x1 <*> f x2+f <$$> [x1, x2, x3] = triple    <$> f x1 <*> f x2 <*> f x3+f <$$> xs           = revMapM f ({- trace msg -} xs)+  where+    _msg            = "<$$> on " ++ show (length xs)++revMapM  :: (Monad m) => (a -> m b) -> [a] -> m [b]+revMapM f          = go []+  where+    go !acc []     = return (reverse acc)+    go !acc (x:xs) = do {!y <- f x; go (y:acc) xs}

@@ -76,6 +76,10 @@    -- * For testing   , expr0P+  , dataFieldP+  , dataCtorP+  , dataDeclP+   ) where  import qualified Data.HashMap.Strict         as M@@ -244,15 +248,15 @@  -- | Integer integer :: Parser Integer-integer = posInteger+integer = (Token.natural lexer <* spaces) --posInteger  --  try (char '-' >> (negate <$> posInteger)) --       <|> posInteger-posInteger :: Parser Integer-posInteger = toI <$> (many1 digit <* spaces)-  where-    toI :: String -> Integer-    toI = read+-- posInteger :: Parser Integer+-- posInteger = toI <$> (many1 digit <* spaces)+--  where+--    toI :: String -> Integer+--    toI = read  ---------------------------------------------------------------- ------------------------- Expressions --------------------------@@ -303,9 +307,10 @@ isSmall :: Char -> Bool isSmall c = isLower c || c == '_' -locLowerIdP, locUpperIdP :: Parser LocSymbol+locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol locLowerIdP = locParserP lowerIdP locUpperIdP = locParserP upperIdP+locSymbolP  = locParserP symbolP  -- | Arbitrary Symbols symbolP :: Parser Symbol@@ -316,6 +321,7 @@ constantP =  try (R <$> double)          <|> I <$> integer + symconstP :: Parser SymConst symconstP = SL . T.pack <$> stringLiteral @@ -516,7 +522,7 @@   =   (reserved "int"     >> return intFTyCon)   <|> (reserved "Integer" >> return intFTyCon)   <|> (reserved "Int"     >> return intFTyCon)-  <|> (reserved "int"     >> return intFTyCon) -- TODO:AZ duplicate?+  -- <|> (reserved "int"     >> return intFTyCon) -- TODO:AZ duplicate?   <|> (reserved "real"    >> return realFTyCon)   <|> (reserved "bool"    >> return boolFTyCon)   <|> (reserved "num"     >> return numFTyCon)@@ -550,10 +556,10 @@       <|> (reservedOp "&&" >> pGAnds <$> predsP)       <|> (reservedOp "||" >> POr  <$> predsP) -makeUniquePGrad :: Parser Expr +makeUniquePGrad :: Parser Expr makeUniquePGrad   = do uniquePos <- getPosition-       return $ PGrad (KV $ symbol $ show uniquePos) mempty mempty+       return $ PGrad (KV $ symbol $ show uniquePos) mempty (srcGradInfo uniquePos) mempty  -- qmP    = reserved "?" <|> reserved "Bexp" @@ -641,10 +647,25 @@ refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a refDefP x  = refBindP (optBindP x) ------------------------------------------------------------------------- | Parsing Qualifiers -------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Parsing Data Declarations -------------------------------------------------+-------------------------------------------------------------------------------- +dataFieldP :: Parser DataField+dataFieldP = DField <$> locSymbolP <* colon <*> sortP++dataCtorP :: Parser DataCtor+dataCtorP  = DCtor <$> locSymbolP+                   <*> braces (sepBy dataFieldP comma)++dataDeclP :: Parser DataDecl+dataDeclP  = DDecl <$> fTyConP <*> intP <* (reservedOp "=")+                   <*> brackets (many (reservedOp "|" *> dataCtorP))++--------------------------------------------------------------------------------+-- | Parsing Qualifiers --------------------------------------------------------+--------------------------------------------------------------------------------+ -- | Qualifiers qualifierP :: Parser Sort -> Parser Qualifier qualifierP tP = do@@ -665,7 +686,18 @@ --  where --    Just (c,cs) = T.uncons $ symbolSafeText s +---------------------------------------------------------------------+-- | Axioms for Symbolic Evaluation ---------------------------------+--------------------------------------------------------------------- +defineP :: Parser Equation+defineP = Equ <$> symbolP <*> many symbolP <*> (reserved "=" >> exprP)++matchP :: Parser Rewrite+matchP = SMeasure <$> symbolP <*> symbolP <*> many symbolP <*> (reserved "=" >> exprP)++pairsP :: Parser a -> Parser b -> Parser [(a, b)]+pairsP aP bP = brackets $ sepBy1 (pairP aP (reserved ":") bP) semi --------------------------------------------------------------------- -- | Parsing Constraints (.fq files) -------------------------------- ---------------------------------------------------------------------@@ -683,6 +715,12 @@   | Pack !KVar !Int   | IBind !Int !Symbol !SortedReft   | Opt !String+  | Def !Equation+  | Mat !Rewrite+  | Fuel ![(Int,Int)]+  | Expand ![(Int,Bool)]+  | Syms !Int+  | Adt  !DataDecl   deriving (Show, Generic)   --  Sol of solbind   --  Dep of FixConstraint.dep@@ -704,9 +742,18 @@     <|> Pack  <$> (reserved "pack"       >> kvarP)   <*> (colon >> intP)     <|> Qul   <$> (reserved "qualif"     >> qualifierP sortP)     <|> Kut   <$> (reserved "cut"        >> kvarP)-    <|> IBind <$> (reserved "bind"       >> intP) <*> symbolP <*> (colon >> {-# SCC "sortedReftP" #-} sortedReftP)-    <|> Opt   <$> (reserved "fixpoint"   >> stringLiteral)+    <|> IBind <$> (reserved "bind"       >> intP)+              <*> symbolP+              <*> (colon >> {-# SCC "sortedReftP" #-} sortedReftP)+    <|> Opt    <$> (reserved "fixpoint"   >> stringLiteral)+    <|> Def    <$> (reserved "define"     >> defineP)+    <|> Mat    <$> (reserved "match"      >> matchP)+    <|> Fuel   <$> (reserved "fuel"       >> pairsP intP intP)+    <|> Expand <$> (reserved "expand"     >> pairsP intP boolP)+    <|> Syms   <$> (reserved "syms"       >> intP)+    <|> Adt    <$> (reserved "data"       >> dataDeclP) + sortedReftP :: Parser SortedReft sortedReftP = refP (RR <$> (sortP <* spaces)) @@ -759,8 +806,12 @@ intP :: Parser Int intP = fromInteger <$> integer +boolP :: Parser Bool+boolP = (reserved "True" >> return True)+    <|> (reserved "False" >> return False)+ defsFInfo :: [Def a] -> FInfo a-defsFInfo defs = {-# SCC "defsFI" #-} FI cm ws bs lts dts kts qs mempty mempty mempty mempty+defsFInfo defs = {-# SCC "defsFI" #-} FI cm ws bs lts dts kts qs binfo adts mempty mempty ae   where     cm         = M.fromList         [(cid c, c)         | Cst c       <- defs]     ws         = M.fromList         [(thd3 $ wrft w, w) | Wfc w       <- defs]@@ -768,9 +819,16 @@     lts        = fromListSEnv       [(x, t)             | Con x t     <- defs]     dts        = fromListSEnv       [(x, t)             | Dis x t     <- defs]     kts        = KS $ S.fromList    [k                  | Kut k       <- defs]-    -- pks        = Packs $ M.fromList [(k, i)             | Pack k i    <- defs]     qs         =                    [q                  | Qul q       <- defs]+    binfo      = mempty+    fuel       = M.fromList         [(fromIntegral i, f)| Fuel fs     <- defs, (i,f) <- fs]+    expand     = M.fromList         [(fromIntegral i, f)| Expand fs   <- defs, (i,f) <- fs]+    syms       = sum                [s                  | Syms s      <- defs]+    eqs        =                    [e                  | Def e       <- defs]+    rews       =                    [r                  | Mat r       <- defs]     cid        = fromJust . sid+    ae         = AEnv syms eqs rews fuel expand+    adts       =                    [d                  | Adt d       <- defs]     -- msg    = show $ "#Lits = " ++ (show $ length consts)  ---------------------------------------------------------------------@@ -864,10 +922,11 @@  <|> (reserved "distinct" >> (Distinct <$> brackets (sepBy exprP comma)))  cmdVarP :: Parser Command-cmdVarP = do-  x <- bindP-  t <- sortP-  return $ Declare x [] t+cmdVarP = error "UNIMPLEMENTED: cmdVarP"+-- do+  -- x <- bindP+  -- t <- sortP+  -- return $ Declare x [] t  --------------------------------------------------------------------- -- Bundling Parsers into a Typeclass --------------------------------

@@ -30,6 +30,7 @@     , makeContext     , makeContextNoLog     , makeContextWithSEnv+    -- , makeSmtContext     , cleanupContext      -- * Execute Queries@@ -40,10 +41,12 @@     , smtDecl     , smtDecls     , smtAssert+    -- , smtDataDecl+    , smtFuncDecl     , smtAssertAxiom     , smtCheckUnsat     , smtCheckSat-    , smtBracket+    , smtBracket, smtBracketAt     , smtDistinct     , smtPush, smtPop @@ -52,7 +55,6 @@     , checkValid'     , checkValidWithContext     , checkValids-    , makeSmtContext      ) where @@ -64,19 +66,20 @@                                                 , betaEquivalence                                                 , normalForm                                                 , stringTheory)-import           Language.Fixpoint.Misc         (errorstar)+import qualified Language.Fixpoint.Misc          as Misc+import qualified Language.Fixpoint.Types.Visitor as Vis import           Language.Fixpoint.Types.Errors--- import           Language.Fixpoint.SortCheck    (elaborate) import           Language.Fixpoint.Utils.Files-import           Language.Fixpoint.Types hiding (allowHO)+import           Language.Fixpoint.Types         hiding (allowHO)+import qualified Language.Fixpoint.Types         as F import           Language.Fixpoint.Smt.Types import qualified Language.Fixpoint.Smt.Theories as Thy import           Language.Fixpoint.Smt.Serialize ()- import           Control.Applicative      ((<|>)) import           Control.Monad import           Control.Exception import           Data.Char+import qualified Data.HashMap.Strict      as M import           Data.Monoid import qualified Data.Text                as T import           Data.Text.Format@@ -91,9 +94,13 @@ import           System.IO                (Handle, IOMode (..), hClose, hFlush, openFile) import           System.Process import qualified Data.Attoparsec.Text     as A-import qualified Data.HashMap.Strict      as M+-- import qualified Data.HashMap.Strict      as M import           Data.Attoparsec.Internal.Types (Parser) import           Text.PrettyPrint.HughesPJ (text)+import           Language.Fixpoint.SortCheck+-- import qualified Language.Fixpoint.Types as F+-- import           Language.Fixpoint.Types.PrettyPrint (tracepp)+ {- runFile f   = readFile f >>= runString@@ -109,17 +116,28 @@ -}  --- TODO take makeContext's Bool from caller instead of always using False?-makeSmtContext :: Config -> FilePath -> [(Symbol, Sort)] -> IO Context-makeSmtContext cfg f xts = do-  me <- makeContextWithSEnv cfg f $ fromListSEnv xts-  smtDecls me theoryDecls-  smtDecls me xts-  return me+-- TODO: DEPRECATE `makeSmtContext`; instead use just `makeContextWithSEnv`+--       which should call `declare` inside it. Currently broken as the use+--       case is in `instantiate` which needs it BEFORE we `Sanitize` and+--       hence before we can call `symbolEnv` to find the set of all symbols etc... -theoryDecls :: [(Symbol, Sort)]-theoryDecls = [ (x, tsSort ty) | (x, ty) <- M.toList Thy.theorySymbols, not (tsInterp ty)]+-- makeSmtContext :: Config -> FilePath -> [DataDecl] -> [(Symbol, Sort)] -> [Sort]+--                -> IO Context+-- makeSmtContext cfg f dds xts ts = do+  -- let env = makeSmtEnv dds xts ts+  -- me     <- makeContextWithSEnv cfg f env+  -- smtDecls me (theoryDecls env)+  -- smtDecls me xts+  -- return me +-- makeSmtEnv :: [DataDecl] -> [(Symbol, Sort)] -> [Sort] -> SymEnv+-- makeSmtEnv dds xts ts = symEnv (fromListSEnv xts) (Thy.theorySymbols dds) dds ts++_theoryDecls :: SymEnv -> [(Symbol, Sort)]+_theoryDecls env = [ (x, tsSort ty) | (x, ty) <- theorySyms, Uninterp == tsInterp ty]+  where+    theorySyms  = toListSEnv (seTheory env)+ checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool checkValidWithContext me xts p q =   smtBracket me "checkValidWithContext" $@@ -163,7 +181,8 @@ -------------------------------------------------------------------------- command me !cmd       = say cmd >> hear cmd   where-    say               = smtWrite me . Builder.toLazyText . runSmt2+    env               = ctxSymEnv me+    say               = smtWrite me . Builder.toLazyText . runSmt2 env     hear CheckSat     = smtRead me     hear (GetValue _) = smtRead me     hear _            = return Ok@@ -177,7 +196,7 @@     do ln  <- smtReadRaw me        res <- A.parseWith (smtReadRaw me) responseP ln        case A.eitherResult res of-         Left e  -> errorstar $ "SMTREAD:" ++ e+         Left e  -> Misc.errorstar $ "SMTREAD:" ++ e          Right r -> do            maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (ctxLog me)            -- when (verbose me) $ TIO.putStrLn $ format "SMT Says: {}" (Only $ show r)@@ -254,9 +273,12 @@     where        smtFile = extFileName Smt2 f -makeContextWithSEnv :: Config -> FilePath -> SMTEnv -> IO Context-makeContextWithSEnv cfg f env-  = (\cxt -> cxt {ctxSmtEnv = env}) <$> makeContext cfg f+makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context+makeContextWithSEnv cfg f env = do+  ctx     <- makeContext cfg f+  let ctx' = ctx {ctxSymEnv = env}+  declare ctx'+  return ctx'   -- where msg = "makeContextWithSEnv" ++ show env  makeContextNoLog :: Config -> IO Context@@ -279,7 +301,7 @@                   , ctxAeq     = alphaEquivalence cfg                   , ctxBeq     = betaEquivalence  cfg                   , ctxNorm    = normalForm       cfg-                  , ctxSmtEnv  = Thy.theorySEnv+                  , ctxSymEnv  = mempty -- tsSort <$> Thy.theorySymbols -- Thy.theorySEnv                   }  --------------------------------------------------------------------------@@ -333,7 +355,7 @@   | x <  y = False versionGreaterEq _  [] = True versionGreaterEq [] _  = False-versionGreaterEq _ _ = errorstar "Interface.versionGreater called with bad arguments"+versionGreaterEq _ _ = Misc.errorstar "Interface.versionGreater called with bad arguments"  ----------------------------------------------------------------------------- -- | SMT Commands -----------------------------------------------------------@@ -347,10 +369,19 @@ smtDecls = mapM_ . uncurry . smtDecl  smtDecl :: Context -> Symbol -> Sort -> IO ()-smtDecl me x t = interact' me (Declare x ins out)+smtDecl me x t = interact' me (Declare x ins' out')   where+    ins'       = sortSmtSort False env <$> ins+    out'       = sortSmtSort False env     out     (ins, out) = deconSort t+    env        = seData (ctxSymEnv me) +smtFuncDecl :: Context -> Symbol -> ([SmtSort],  SmtSort) -> IO ()+smtFuncDecl me x (ts, t) = interact' me (Declare x ts t)++smtDataDecl :: Context -> DataDecl -> IO ()+smtDataDecl me d = interact' me (DeclData d)+ deconSort :: Sort -> ([Sort], Sort) deconSort t = case functionSort t of                 Just (_, ins, out) -> (ins, out)@@ -367,9 +398,8 @@ smtAssert :: Context -> Expr -> IO () smtAssert me p  = interact' me (Assert Nothing p) - smtAssertAxiom :: Context -> Triggered Expr -> IO ()-smtAssertAxiom me p  = interact' me (AssertAxiom p)+smtAssertAxiom me p  = interact' me (AssertAx p)  smtDistinct :: Context -> [Expr] -> IO () smtDistinct me az = interact' me (Distinct az)@@ -377,6 +407,10 @@ smtCheckUnsat :: Context -> IO Bool smtCheckUnsat me  = respSat <$> command me CheckSat +smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a+smtBracketAt sp x y z = smtBracket x y z `catch` dieAt sp++ smtBracket :: Context -> String -> IO a -> IO a smtBracket me _msg a   = do   smtPush me@@ -410,3 +444,100 @@   = [ "(set-option :auto-config false)"     , "(set-option :model true)"     , "(set-option :model-partial false)"]++++--------------------------------------------------------------------------------+declare :: Context -> IO () -- SolveM ()+--------------------------------------------------------------------------------+declare me = do+  forM_ ds     $           smtDataDecl me+  forM_ thyXTs $ uncurry $ smtDecl     me+  forM_ qryXTs $ uncurry $ smtDecl     me+  forM_ ats    $ uncurry $ smtFuncDecl me+  forM_ ess    $           smtDistinct me+  forM_ axs    $           smtAssert   me+  where+    env        = ctxSymEnv me+    ds         = dataDeclarations          env+    lts        = F.toListSEnv . F.seLits $ env+    ess        = distinctLiterals  lts+    axs        = Thy.axiomLiterals lts+    thyXTs     =                    filter (isKind 1) xts+    qryXTs     = Misc.mapSnd tx <$> filter (isKind 2) xts+    isKind n   = (n ==)  . symKind env . fst+    xts        = F.toListSEnv           (F.seSort env)+    tx         = elaborate    "declare" env+    ats        = funcSortVars env++dataDeclarations :: SymEnv -> [DataDecl]+dataDeclarations = -- (if True then orderDeclarations else id) .+                   orderDeclarations . map snd . F.toListSEnv . F.seData++funcSortVars :: F.SymEnv -> [(F.Symbol, ([F.SmtSort], F.SmtSort))]+funcSortVars env  = [(var applyName  t       , appSort t) | t <- ts]+                 ++ [(var lambdaName t       , lamSort t) | t <- ts]+                 ++ [(var (lamArgSymbol i) t , argSort t) | t@(_,F.SInt) <- ts, i <- [1..Thy.maxLamArg] ]+  where+    var n         = F.symbolAtSmtName n env ()+    ts            = M.keys (F.seAppls env)+    appSort (s,t) = ([F.SInt, s], t)+    lamSort (s,t) = ([s, t], F.SInt)+    argSort (s,_) = ([]    , s)++-- | 'symKind' returns {0, 1, 2} where:+--   0 = Theory-Definition,+--   1 = Theory-Declaration,+--   2 = Query-Binder++symKind :: F.SymEnv -> F.Symbol -> Int+symKind env x = case F.tsInterp <$> F.symEnvTheory x env of+                  Just F.Theory   -> 0+                  Just F.Data     -> 0+                  Just F.Uninterp -> 1+                  Nothing         -> 2+              -- Just t  -> if tsInterp t then 0 else 1+++-- assumes :: [F.Expr] -> SolveM ()+-- assumes es = withContext $ \me -> forM_  es $ smtAssert me++-- | `distinctLiterals` is used solely to determine the set of literals+--   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,+--   or string literals "cat", "dog", "mouse". These should only include+--   non-function sorted values.+distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]+distinctLiterals xts = [ es | (_, es) <- tess ]+   where+    tess             = Misc.groupList [(t, F.expr x) | (x, t) <- xts, notFun t]+    notFun           = not . F.isFunctionSortedReft . (`F.RR` F.trueReft)+    -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)++--------------------------------------------------------------------------------+-- | 'orderDeclarations' sorts the data declarations such that each declarations+--   only refers to preceding ones.+--------------------------------------------------------------------------------+orderDeclarations :: [F.DataDecl] -> [F.DataDecl]+--------------------------------------------------------------------------------+orderDeclarations ds = reverse (Misc.topoSortWith f ds)+  where+    dM               = M.fromList [(F.ddTyCon d, d) | d <- ds]+    f d              = (F.ddTyCon d, dataDeclDeps dM d)++dataDeclDeps :: M.HashMap F.FTycon F.DataDecl -> F.DataDecl -> [F.FTycon]+dataDeclDeps dM = filter (`M.member` dM) . Misc.sortNub . dataDeclFTycons++dataDeclFTycons :: F.DataDecl -> [F.FTycon]+dataDeclFTycons = concatMap dataCtorFTycons . F.ddCtors++dataCtorFTycons :: F.DataCtor -> [F.FTycon]+dataCtorFTycons = concatMap dataFieldFTycons . F.dcFields++dataFieldFTycons :: F.DataField -> [F.FTycon]+dataFieldFTycons = sortFTycons . F.dfSort++sortFTycons :: Sort -> [FTycon]+sortFTycons = Vis.foldSort go []+  where+    go cs (FTC c) = c : cs+    go cs _       = cs

@@ -10,8 +10,9 @@ --   typeclass. We split it into a separate module as it depends on --   Theories (see @smt2App@). -module Language.Fixpoint.Smt.Serialize () where+module Language.Fixpoint.Smt.Serialize (smt2SortMono) where +import           Language.Fixpoint.SortCheck import           Language.Fixpoint.Types import           Language.Fixpoint.Smt.Types import qualified Language.Fixpoint.Smt.Theories as Thy@@ -19,105 +20,151 @@ import qualified Data.Text.Lazy.Builder         as Builder import           Data.Text.Format import           Language.Fixpoint.Misc (errorstar)-import           Data.Maybe (fromMaybe) --- instance SMTLIB2 Sort where---   smt2 s@(FFunc _ _)           = errorstar $ "smt2 FFunc: " ++ showpp s---   smt2 FInt                    = "Int"---   smt2 FReal                   = "Real"---   smt2 t---     | t == boolSort            = "Bool"---   smt2 t---     | Just d <- Thy.smt2Sort t = d---   smt2 _                       = "Int"- instance SMTLIB2 (Symbol, Sort) where-  smt2 c@(sym, t) = build "({} {})" (smt2 sym, smt2Sort c t)+  smt2 env c@(sym, t) = build "({} {})" (smt2 env sym, smt2SortMono c env t) -smt2Sort :: (PPrint a) => a -> Sort -> Builder.Builder-smt2Sort msg = go+smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder.Builder+smt2SortMono = smt2Sort False+smt2SortPoly = smt2Sort True++smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder.Builder+smt2Sort poly _ env t = smt2 env (Thy.sortSmtSort poly (seData env) t)++smt2data :: SymEnv -> DataDecl -> Builder.Builder+smt2data env (DDecl tc n cs) = build "({}) (({} {}))" (tvars, name, ctors)   where-    go s@(FFunc _ _)             = errorstar $ unwords ["smt2 FFunc:", showpp msg, showpp s]-    go FInt                      = "Int"-    go FReal                     = "Real"-    go t-      | t == boolSort            = "Bool"-    go t-      | Just d <- Thy.smt2Sort t = d-    go _                         = "Int"+    tvars                    = smt2many (smt2TV <$> [0..(n-1)])+    name                     = smt2 env (symbol tc)+    ctors                    = smt2many (smt2ctor env <$> cs)+    smt2TV                   = smt2 env . SVar ++smt2ctor :: SymEnv -> DataCtor -> Builder.Builder+smt2ctor env (DCtor c [])  = smt2 env c+smt2ctor env (DCtor c fs)  = build "({} {})" (smt2 env c, fields)+  where+    fields                 = smt2many (smt2field env <$> fs)++smt2field :: SymEnv -> DataField -> Builder.Builder+smt2field env d@(DField x t) = build "({} {})" (smt2 env x, smt2SortPoly d env t)+ instance SMTLIB2 Symbol where-  smt2 s-    | Just t <- Thy.smt2Symbol s = t-  smt2 s                         = Builder.fromText $ symbolSafeText  s+  smt2 env s+    | Just t <- Thy.smt2Symbol env s = t+  smt2 _ s                           = symbolBuilder s ++instance SMTLIB2 LocSymbol where+  smt2 env = smt2 env . val+ instance SMTLIB2 SymConst where-  smt2 = smt2 . symbol+  smt2 env = smt2 env . symbol  instance SMTLIB2 Constant where-  smt2 (I n)   = build "{}" (Only n)-  smt2 (R d)   = build "{}" (Only d)-  smt2 (L t _) = build "{}" (Only t)+  smt2 _ (I n)   = build "{}" (Only n)+  smt2 _ (R d)   = build "{}" (Only d)+  smt2 _ (L t _) = build "{}" (Only t) -instance SMTLIB2 LocSymbol where-  smt2 = smt2 . val  instance SMTLIB2 Bop where-  smt2 Plus   = "+"-  smt2 Minus  = "-"-  smt2 Times  = Builder.fromText $ symbolSafeText mulFuncName-  smt2 Div    = Builder.fromText $ symbolSafeText divFuncName-  smt2 RTimes = "*"-  smt2 RDiv   = "/"-  smt2 Mod    = "mod"+  smt2 _ Plus   = "+"+  smt2 _ Minus  = "-"+  smt2 _ Times  = symbolBuilder mulFuncName+  smt2 _ Div    = symbolBuilder divFuncName+  smt2 _ RTimes = "*"+  smt2 _ RDiv   = "/"+  smt2 _ Mod    = "mod"  instance SMTLIB2 Brel where-  smt2 Eq    = "="-  smt2 Ueq   = "="-  smt2 Gt    = ">"-  smt2 Ge    = ">="-  smt2 Lt    = "<"-  smt2 Le    = "<="-  smt2 _     = errorstar "SMTLIB2 Brel"+  smt2 _ Eq    = "="+  smt2 _ Ueq   = "="+  smt2 _ Gt    = ">"+  smt2 _ Ge    = ">="+  smt2 _ Lt    = "<"+  smt2 _ Le    = "<="+  smt2 _ _     = errorstar "SMTLIB2 Brel"  -- NV TODO: change the way EApp is printed instance SMTLIB2 Expr where-  smt2 (ESym z)         = smt2 z-  smt2 (ECon c)         = smt2 c-  smt2 (EVar x)         = smt2 x-  smt2 e@(EApp _ _)     = smt2App e-  smt2 (ENeg e)         = build "(- {})" (Only $ smt2 e)-  smt2 (EBin o e1 e2)   = build "({} {} {})" (smt2 o, smt2 e1, smt2 e2)-  smt2 (EIte e1 e2 e3)  = build "(ite {} {} {})" (smt2 e1, smt2 e2, smt2 e3)-  smt2 (ECst e _)       = smt2 e-  smt2 (PTrue)          = "true"-  smt2 (PFalse)         = "false"-  smt2 (PAnd [])        = "true"-  smt2 (PAnd ps)        = build "(and {})"   (Only $ smt2s ps)-  smt2 (POr [])         = "false"-  smt2 (POr ps)         = build "(or  {})"   (Only $ smt2s ps)-  smt2 (PNot p)         = build "(not {})"   (Only $ smt2  p)-  smt2 (PImp p q)       = build "(=> {} {})" (smt2 p, smt2 q)-  smt2 (PIff p q)       = build "(= {} {})"  (smt2 p, smt2 q)-  smt2 (PExist [] p)    = smt2 p-  smt2 (PExist bs p)    = build "(exists ({}) {})"  (smt2s bs, smt2 p)-  smt2 (PAll   [] p)    = smt2 p-  smt2 (PAll   bs p)    = build "(forall ({}) {})"  (smt2s bs, smt2 p)+  smt2 env (ESym z)         = smt2 env z+  smt2 env (ECon c)         = smt2 env c+  smt2 env (EVar x)         = smt2 env x+  smt2 env e@(EApp _ _)     = smt2App env e+  smt2 env (ENeg e)         = build "(- {})" (Only $ smt2 env e)+  smt2 env (EBin o e1 e2)   = build "({} {} {})" (smt2 env o, smt2 env e1, smt2 env e2)+  smt2 env (EIte e1 e2 e3)  = build "(ite {} {} {})" (smt2 env e1, smt2 env e2, smt2 env e3)+  smt2 env (ECst e t)       = smt2Cast env e t+  smt2 _   (PTrue)          = "true"+  smt2 _   (PFalse)         = "false"+  smt2 _   (PAnd [])        = "true"+  smt2 env (PAnd ps)        = build "(and {})"   (Only $ smt2s env ps)+  smt2 _   (POr [])         = "false"+  smt2 env (POr ps)         = build "(or  {})"   (Only $ smt2s env ps)+  smt2 env (PNot p)         = build "(not {})"   (Only $ smt2  env p)+  smt2 env (PImp p q)       = build "(=> {} {})" (smt2 env p, smt2 env q)+  smt2 env (PIff p q)       = build "(= {} {})"  (smt2 env p, smt2 env q)+  smt2 env (PExist [] p)    = smt2 env p+  smt2 env (PExist bs p)    = build "(exists ({}) {})"  (smt2s env bs, smt2 env p)+  smt2 env (PAll   [] p)    = smt2 env p+  smt2 env (PAll   bs p)    = build "(forall ({}) {})"  (smt2s env bs, smt2 env p)+  smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2+  smt2 env (ELam b e)       = smt2Lam env b e+  smt2 _   e                = panic ("smtlib2 Pred  " ++ show e) -  smt2 (PAtom r e1 e2)  = mkRel r e1 e2-  smt2 (ELam (x, _) e)  = smt2Lam x e-  smt2  e               = errorstar ("smtlib2 Pred  " ++ show e)+-- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors+--   like Nil, see `tests/pos/adt_list_1.fq` +smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder+smt2Cast env (EVar x) t = smt2Var env x t+smt2Cast env e        _ = smt2    env e -smt2Lam :: Symbol -> Expr -> Builder.Builder-smt2Lam x e = build "({} {} {})" (smt2 lambdaName, smt2 x, smt2 e)+smt2Var :: SymEnv -> Symbol -> Sort -> Builder.Builder+smt2Var env x t+  | isLamArgSymbol x            = smtLamArg env x t+  | Just s <- symEnvSort x env+  , isPolyInst s t              = smt2VarAs env x t+  | otherwise                   = smt2 env x -smt2App :: Expr -> Builder.Builder-smt2App e = fromMaybe (build "({} {})" (smt2 f, smt2s es)) $ Thy.smt2App (eliminate f) $ map smt2 es+smtLamArg :: SymEnv -> Symbol -> Sort -> Builder.Builder+smtLamArg env x t = symbolBuilder $ symbolAtName x env () (FFunc t FInt)+  -- symbolBuilder (symbolAtName x env () t)++smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder.Builder+smt2VarAs env x t = build "(as {} {})" (smt2 env x, smt2SortMono x env t)++isPolyInst :: Sort -> Sort -> Bool+isPolyInst s t = isPoly s && not (isPoly t)++isPoly :: Sort -> Bool+isPoly (FAbs {}) = True+isPoly _         = False++smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder.Builder+smt2Lam env (x, xT) (ECst e eT) = build "({} {} {})" (smt2 env lambda, x', smt2 env e)   where-    (f, es) = splitEApp' e+    x'                          = smtLamArg env x xT+    lambda                      = symbolAtName lambdaName env () (FFunc xT eT) +smt2Lam _ _ e+  = panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e) +smt2App :: SymEnv -> Expr -> Builder.Builder+smt2App env e@(EApp (EApp f e1) e2)+  | Just t <- unApplyAt f+  = build "({} {})" (symbolBuilder (symbolAtName applyName env e t), smt2s env [e1, e2])+smt2App env e+  | Just b <- Thy.smt2App env (unCast f) (smt2 env <$> es)+  = b+  | otherwise+  = build "({} {})" (smt2 env f, smt2s env es)+  where+    (f, es)   =  splitEApp' e++unCast :: Expr -> Expr+unCast (ECst e _) = unCast e+unCast e          = e+ splitEApp' :: Expr -> (Expr, [Expr]) splitEApp'            = go []   where@@ -125,51 +172,42 @@     go acc (ECst e _) = go acc e     go acc e          = (e, acc) -eliminate :: Expr -> Expr-eliminate (ECst e _) = eliminate e-eliminate e          = e--mkRel :: Brel -> Expr -> Expr -> Builder.Builder-mkRel Ne  e1 e2 = mkNe e1 e2-mkRel Une e1 e2 = mkNe e1 e2-mkRel r   e1 e2 = build "({} {} {})" (smt2 r, smt2 e1, smt2 e2)+mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder.Builder+mkRel env Ne  e1 e2 = mkNe env e1 e2+mkRel env Une e1 e2 = mkNe env e1 e2+mkRel env r   e1 e2 = build "({} {} {})" (smt2 env r, smt2 env e1, smt2 env e2) -mkNe :: Expr -> Expr -> Builder.Builder-mkNe  e1 e2              = build "(not (= {} {}))" (smt2 e1, smt2 e2)+mkNe :: SymEnv -> Expr -> Expr -> Builder.Builder+mkNe env e1 e2      = build "(not (= {} {}))" (smt2 env e1, smt2 env e2)  instance SMTLIB2 Command where-  -- NIKI TODO: formalize this transformation-  smt2 c@(Declare x ts t)  = build "(declare-fun {} ({}) {})"     (smt2 x, smt2many (smt2Sort c <$> ts), smt2Sort c t) -- HEREHEREHERE (smt2 x, smt2s ts, smt2 t)-  smt2 c@(Define t)        = build "(declare-sort {})"            (Only $ smt2Sort c t)-  smt2 (Assert Nothing p)  = build "(assert {})"                  (Only $ smt2 p)-  smt2 (Assert (Just i) p) = build "(assert (! {} :named p-{}))"  (smt2 p, i)-  smt2 (Distinct az)-    -- Distinct must have at least 2 arguments-    | length az < 2        = ""-    | otherwise            = build "(assert (distinct {}))"       (Only $ smt2s az)-  smt2 (AssertAxiom t)     = build "(assert {})"                  (Only $ smt2 t)-  smt2 (Push)              = "(push 1)"-  smt2 (Pop)               = "(pop 1)"-  smt2 (CheckSat)          = "(check-sat)"-  smt2 (GetValue xs)       = "(get-value (" <> smt2s xs <> "))"-  smt2 (CMany cmds)        = smt2many (smt2 <$> cmds)+  smt2 env (DeclData d)        = build "(declare-datatypes {})"       (Only $ smt2data env d)+  smt2 env (Declare x ts t)    = build "(declare-fun {} ({}) {})"     (smt2 env x, smt2many (smt2 env <$> ts), smt2 env t)+  smt2 env c@(Define t)        = build "(declare-sort {})"            (Only $ smt2SortMono c env t)+  smt2 env (Assert Nothing p)  = build "(assert {})"                  (Only $ smt2 env p)+  smt2 env (Assert (Just i) p) = build "(assert (! {} :named p-{}))"  (smt2 env p, i)+  smt2 env (Distinct az)+    | length az < 2            = ""+    | otherwise                = build "(assert (distinct {}))"       (Only $ smt2s env az)+  smt2 env (AssertAx t)        = build "(assert {})"                  (Only $ smt2  env t)+  smt2 _   (Push)              = "(push 1)"+  smt2 _   (Pop)               = "(pop 1)"+  smt2 _   (CheckSat)          = "(check-sat)"+  smt2 env (GetValue xs)       = "(get-value (" <> smt2s env xs <> "))"+  smt2 env (CMany cmds)        = smt2many (smt2 env <$> cmds)  instance SMTLIB2 (Triggered Expr) where-  smt2 (TR NoTrigger e)       = smt2 e  -  smt2 (TR _ (PExist [] p))   = smt2 p-  smt2 t@(TR _ (PExist bs p)) = build "(exists ({}) (! {} :pattern({})))"  (smt2s bs, smt2 p, smt2s $ makeTriggers t)-  smt2 (TR _ (PAll   [] p))   = smt2 p-  smt2 t@(TR _ (PAll   bs p)) = build "(forall ({}) (! {} :pattern({})))"  (smt2s bs, smt2 p, smt2s $ makeTriggers t)-  smt2 (TR _ e)               = smt2 e--+  smt2 env (TR NoTrigger e)       = smt2 env e+  smt2 env (TR _ (PExist [] p))   = smt2 env p+  smt2 env t@(TR _ (PExist bs p)) = build "(exists ({}) (! {} :pattern({})))"  (smt2s env bs, smt2 env p, smt2s env (makeTriggers t))+  smt2 env (TR _ (PAll   [] p))   = smt2 env p+  smt2 env t@(TR _ (PAll   bs p)) = build "(forall ({}) (! {} :pattern({})))"  (smt2s env bs, smt2 env p, smt2s env (makeTriggers t))+  smt2 env (TR _ e)               = smt2 env e  {-# INLINE smt2s #-}-smt2s    :: SMTLIB2 a => [a] -> Builder.Builder-smt2s as = smt2many (map smt2 as)+smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder.Builder+smt2s env as = smt2many (smt2 env <$> as) -smt2many :: [Builder.Builder] -> Builder.Builder-smt2many []     = mempty-smt2many [b]    = b-smt2many (b:bs) = b <> mconcat [ " " <> b | b <- bs ] {-# INLINE smt2many #-}+smt2many :: [Builder.Builder] -> Builder.Builder+smt2many = buildMany

@@ -9,7 +9,8 @@        -- * Convert theory applications TODO: merge with smt2symbol        smt2App        -- * Convert theory sorts-     , smt2Sort+     , sortSmtSort+        -- * Convert theory symbols      , smt2Symbol        -- * Preamble to initialize SMT@@ -17,15 +18,11 @@         -- * Bit Vector Operations      , sizeBv-     , toInt+       -- , toInt         -- * Theory Symbols      , theorySymbols-     , theorySEnv -     -- * String-     -- , string-     -- , genLen         -- * Theories      , setEmpty, setEmp, setCap, setSub, setAdd, setMem@@ -33,8 +30,8 @@        -- * Query Theories      , isSmt2App-     , isConName      , axiomLiterals+     , maxLamArg      ) where  import           Prelude hiding (map)@@ -42,8 +39,8 @@ import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types import           Language.Fixpoint.Smt.Types-import qualified Data.HashMap.Strict      as M-import           Data.Maybe (catMaybes, isJust)+-- import qualified Data.HashMap.Strict      as M+import           Data.Maybe (catMaybes) import           Data.Monoid import qualified Data.Text.Lazy           as T import qualified Data.Text.Lazy.Builder   as Builder@@ -91,14 +88,7 @@ strLen    = "strLen" strSubstr = "subString" strConcat = "concatString"--- NOPROP genLen :: Symbol--- NOPROP genLen = "len" --- NOPROP strlen, strsubstr, strconcat :: Raw--- NOPROP strlen    = "strLen"--- NOPROP strsubstr = "subString"--- NOPROP strconcat = "concatString"- z3strlen, z3strsubstr, z3strconcat :: Raw z3strlen    = "str.len" z3strsubstr = "str.substr"@@ -223,48 +213,71 @@   ----------------------------------------------------------------------------------- | Exported API ----------------------------------------------------------------------------------------------------------------------------------------------smt2Symbol :: Symbol -> Maybe Builder.Builder-smt2Symbol x = Builder.fromLazyText . tsRaw <$> M.lookup x theorySymbols+--------------------------------------------------------------------------------+-- | Exported API --------------------------------------------------------------+--------------------------------------------------------------------------------+smt2Symbol :: SymEnv -> Symbol -> Maybe Builder.Builder+smt2Symbol env x = Builder.fromLazyText . tsRaw <$> symEnvTheory x env -smt2Sort :: Sort -> Maybe Builder.Builder-smt2Sort (FApp (FTC c) _)-  | isConName setConName c      = Just $ build "{}" (Only set)-smt2Sort (FApp (FApp (FTC c) _) _)-  | isConName mapConName c      = Just $ build "{}" (Only map)-smt2Sort (FApp (FTC bv) (FTC s))-  | isConName bitVecName bv-  , Just n <- sizeBv s          = Just $ build "(_ BitVec {})" (Only n)-smt2Sort s-  | isString s                  = Just $ build "{}" (Only string)-smt2Sort _                      = Nothing+instance SMTLIB2 SmtSort where+  smt2 _ = smt2SmtSort -smt2App :: Expr -> [Builder.Builder] -> Maybe Builder.Builder-smt2App (EVar f) [d]+smt2SmtSort :: SmtSort -> Builder.Builder+smt2SmtSort SInt         = "Int"+smt2SmtSort SReal        = "Real"+smt2SmtSort SBool        = "Bool"+smt2SmtSort SString      = build "{}" (Only string)+smt2SmtSort SSet         = build "{}" (Only set)+smt2SmtSort SMap         = build "{}" (Only map)+smt2SmtSort (SBitVec n)  = build "(_ BitVec {})" (Only n)+smt2SmtSort (SVar n)     = build "T{}" (Only n)+smt2SmtSort (SData c []) = symbolBuilder c+smt2SmtSort (SData c ts) = build "({} {})" (symbolBuilder c        , smt2SmtSorts ts)+-- smt2SmtSort (SApp ts)    = build "({} {})" (symbolBuilder tyAppName, smt2SmtSorts ts)++smt2SmtSorts :: [SmtSort] -> Builder.Builder+smt2SmtSorts = buildMany . fmap smt2SmtSort++--------------------------------------------------------------------------------+smt2App :: SymEnv -> Expr -> [Builder.Builder] -> Maybe Builder.Builder+--------------------------------------------------------------------------------+smt2App _ (EVar f) [d]   | f == setEmpty = Just $ build "{}"             (Only emp)   | f == setEmp   = Just $ build "(= {} {})"      (emp, d)   | f == setSng   = Just $ build "({} {} {})"     (add, emp, d)-smt2App (EVar f) (d:ds)-  | Just s <- M.lookup f theorySymbols+smt2App env (EVar f) (d:ds)+  | Just s <- {- tracepp ("SYMENVTHEORY: " ++ showpp f) $ -} symEnvTheory f env   = Just $ build "({} {})" (tsRaw s, d <> mconcat [ " " <> d | d <- ds])-smt2App _ _           = Nothing+smt2App _ _ _    = Nothing  -- isSmt2App :: Expr -> [a] -> Bool -- isSmt2App e xs = tracepp ("isSmt2App e := " ++ show e) (isSmt2App' e xs) -isSmt2App :: Expr -> [a] -> Bool-isSmt2App (EVar f) [_]-  | f == setEmpty = True-  | f == setEmp   = True-  | f == setSng   = True-isSmt2App (EVar f) _-  =  isJust $ M.lookup f theorySymbols-isSmt2App _ _-  = False+--------------------------------------------------------------------------------+-- / isSmt2App :: SEnv TheorySymbol -> Expr -> [a] -> Bool+-- / --------------------------------------------------------------------------------+-- / isSmt2App _ (EVar f) [_]+  -- / | f == setEmpty = True+  -- / | f == setEmp   = True+  -- / | f == setSng   = True+-- / isSmt2App env (EVar f) _+  -- / =  isJust (lookupSEnv f env)+-- / isSmt2App _ _ _+  -- / = False +--------------------------------------------------------------------------------+isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int+--------------------------------------------------------------------------------+isSmt2App _ (EVar f)+  | f == setEmpty    = Just 1+  | f == setEmp      = Just 1+  | f == setSng      = Just 1+isSmt2App g (EVar f) = do t  <- tsSort <$> lookupSEnv f g+                          ts <- snd    <$> bkFFunc t+                          Just (length ts - 1)+isSmt2App _ _        = Nothing + preamble :: Config -> SMTSolver -> [T.Text] preamble u Z3   = z3Preamble u preamble u Cvc4 = cvc4Preamble u@@ -278,16 +291,16 @@   -- where     -- msg   = "toInt e = " ++ show e ++ ", t = " ++ show s -toInt :: Expr -> Sort -> Expr-toInt e s+_toInt :: Expr -> Sort -> Expr+_toInt e s   |  (FApp (FTC c) _) <- s-  , isConName setConName c+  , setConName == symbol c   = castWith setToIntName e   | (FApp (FApp (FTC c) _) _) <- s-  , isConName mapConName c+  , mapConName == symbol c   = castWith mapToIntName e   | (FApp (FTC bv) (FTC s)) <- s-  , isConName bitVecName bv+  , bitVecName == symbol bv   , Just _ <- sizeBv s   = castWith bitVecToIntName e   | FTC c <- s@@ -307,18 +320,19 @@ --   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted --   symbols, and `interpSEnv` is for interpreted symbols. ---------------------------------------------------------------------------------theorySEnv :: SEnv Sort-theorySEnv = fromListSEnv . M.toList . fmap tsSort $ theorySymbols+-- theorySEnv :: SEnv Sort+-- theorySEnv = fromListSEnv . M.toList . fmap tsSort $ theorySymbols  -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations, --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)-theorySymbols :: M.HashMap Symbol TheorySymbol-theorySymbols = M.fromList $ uninterpSymbols ++ interpSymbols---- isTheorySymbol :: Symbol -> Bool--- isTheorySymbol x = M.member x theorySymbols+theorySymbols :: [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol+theorySymbols ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols+                                  interpSymbols+                               ++ concatMap dataDeclSymbols ds +-------------------------------------------------------------------------------- interpSymbols :: [(Symbol, TheorySymbol)]+-------------------------------------------------------------------------------- interpSymbols =   [ interpSym setEmp   emp  (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)   , interpSym setEmpty emp  (FAbs 0 $ FFunc intSort (setSort $ FVar 0))@@ -352,66 +366,153 @@   interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)-interpSym x n t = (x, Thy x n t True)--isConName :: Symbol -> FTycon -> Bool-isConName s = (s ==) . val . fTyconSymbol--sizeBv :: FTycon -> Maybe Int-sizeBv tc-  | s == size32Name = Just 32-  | s == size64Name = Just 64-  | otherwise       = Nothing-  where-    s               = val $ fTyconSymbol tc--uninterpSymbols :: [(Symbol, TheorySymbol)]-uninterpSymbols = [ (x, uninterpSym x t) | (x, t) <- uninterpSymbols']+interpSym x n t = (x, Thy x n t Theory) -uninterpSym :: Symbol -> Sort -> TheorySymbol-uninterpSym x t =  Thy x (lt x) t False-  where-    lt           = T.fromStrict . symbolSafeText+-- SHIFTLAM _uninterpSymbols :: [(Symbol, TheorySymbol)]+-- SHIFTLAM _uninterpSymbols = [ (x, uninterpSym x t) | (x, t) <- _uninterpSymbols']+-- SHIFTLAM+-- SHIFTLAM --------------------------------------------------------------------------------+-- SHIFTLAM _uninterpSym :: Symbol -> Sort -> TheorySymbol+-- SHIFTLAM --------------------------------------------------------------------------------+-- SHIFTLAM _uninterpSym x t =  Thy x (symbolRaw x) t Uninterp+-- SHIFTLAM+-- SHIFTLAM _uninterpSymbols' :: [(Symbol, Sort)]+-- SHIFTLAM _uninterpSymbols' = [] -- [ (toIntName,  mkFFunc 1 [FVar 0, FInt]) ] -uninterpSymbols' :: [(Symbol, Sort)]-uninterpSymbols' =-  [ (setToIntName,    FFunc (setSort intSort)   intSort)-  , (bitVecToIntName, FFunc bitVecSort intSort)-  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)-  , (realToIntName,   FFunc realSort   intSort)-  , (lambdaName   ,   FFunc intSort (FFunc intSort intSort))-  ]-  ++ concatMap makeApplies [1..maxLamArg]-  ++ [(makeLamArg s i, s) | i <- [1..maxLamArg], s <- sorts]+  -- SHIFTLAM  [ (setToIntName,    FFunc (setSort intSort)   intSort)+  -- SHIFTLAM  , (bitVecToIntName, FFunc bitVecSort intSort)+  -- SHIFTLAM  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)+  -- SHIFTLAM  , (realToIntName,   FFunc realSort   intSort)+  -- SHIFTLAM  , (lambdaName   ,   FFunc intSort (FFunc intSort intSort))+  -- SHIFTLAM  ]+  -- SHIFTLAM  ++ concatMap makeApplies [1..maxLamArg]+  -- SHIFTLAM  ++ [(lamArgSymbol i, s) | i <- [1..maxLamArg], s <- sorts]+-- SHIFTLAM+-- SHIFTLAM  -- THESE ARE DUPLICATED IN DEFUNCTIONALIZATION --- THESE ARE DUPLICATED IN DEFUNCTIONALIZATION maxLamArg :: Int maxLamArg = 7 -sorts :: [Sort]-sorts = [intSort]+-- SHIFTLAM sorts :: [Sort]+-- SHIFTLAM sorts = [intSort]  -- NIKI TODO: allow non integer lambda arguments -- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort]--makeLamArg :: Sort -> Int  -> Symbol-makeLamArg _ = intArgName+-- makeLamArg :: Sort -> Int  -> Symbol+-- makeLamArg _ = intArgName -makeApplies :: Int -> [(Symbol, Sort)]-makeApplies i =-  [ (intApplyName i,    go i intSort)-  , (setApplyName i,    go i (setSort intSort))-  , (bitVecApplyName i, go i bitVecSort)-  , (mapApplyName i,    go i $ mapSort intSort intSort)-  , (realApplyName i,   go i realSort)-  , (boolApplyName i,   go i boolSort)-  ]-  where-    go 0 s = FFunc intSort s-    go i s = FFunc intSort $ go (i-1) s+-- SHIFTLAM makeApplies :: Int -> [(Symbol, Sort)]+-- SHIFTLAM makeApplies i =+  -- SHIFTLAM [ (intApplyName i,    go i intSort)+  -- SHIFTLAM , (setApplyName i,    go i (setSort intSort))+  -- SHIFTLAM , (bitVecApplyName i, go i bitVecSort)+  -- SHIFTLAM , (mapApplyName i,    go i $ mapSort intSort intSort)+  -- SHIFTLAM , (realApplyName i,   go i realSort)+  -- SHIFTLAM , (boolApplyName i,   go i boolSort)+  -- SHIFTLAM ]+  -- SHIFTLAM where+    -- SHIFTLAM go 0 s = FFunc intSort s+    -- SHIFTLAM go i s = FFunc intSort $ go (i-1) s  axiomLiterals :: [(Symbol, Sort)] -> [Expr] axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]   where     lenAxiom l n  = EEq (EApp (expr (strLen :: Symbol)) (expr l)) (expr n `ECst` intSort)     litLen        = fmap (Data.Text.length .  symbolText) . unLitSymbol++--------------------------------------------------------------------------------+-- | Constructors, Selectors and Tests from 'DataDecl'arations.+--------------------------------------------------------------------------------+dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]+dataDeclSymbols d = {- tracepp "dataDeclSymbols" $ -} ctorSymbols d ++ testSymbols d ++ selectSymbols d++-- | 'selfSort d' returns the _self-sort_ of 'd' :: 'DataDecl'.+--   See [NOTE:DataDecl] for details.++selfSort :: DataDecl -> Sort+selfSort (DDecl c n _) = fAppTC c (FVar <$> [0..(n-1)])++-- | 'fldSort d t' returns the _real-sort_ of 'd' if 't' is the _self-sort_+--   and otherwise returns 't'. See [NOTE:DataDecl] for details.++fldSort :: DataDecl -> Sort -> Sort+fldSort d (FTC c)+  | c == ddTyCon d = selfSort d+fldSort _ s        = s++-- | 'theorify' converts the 'Sort' into a full 'TheorySymbol'++theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)+theorify (x, t) = (x, Thy x (symbolRaw x) t Data)++--------------------------------------------------------------------------------+ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]+--------------------------------------------------------------------------------+ctorSymbols d = ctorSort d <$> ddCtors d++ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)+ctorSort d ctor = (x, Thy x (symbolRaw x) t Data)+  where+    x           = symbol ctor+    t           = mkFFunc n (ts ++ [selfSort d])+    n           = ddVars d+    ts          = fldSort d . dfSort <$> dcFields ctor++--------------------------------------------------------------------------------+testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]+--------------------------------------------------------------------------------+testSymbols d = testTheory t . symbol <$> ddCtors d+  where+    t         = mkFFunc (ddVars d) [selfSort d, boolSort]++testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)+testTheory t x = (sx, Thy sx raw t Data)+  where+    sx         = testSymbol x+    raw        = "is-" <> symbolRaw x++symbolRaw :: Symbol -> T.Text+symbolRaw = T.fromStrict . symbolSafeText++--------------------------------------------------------------------------------+selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]+--------------------------------------------------------------------------------+selectSymbols d = theorify <$> concatMap (ctorSelectors d) (ddCtors d)++ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]+ctorSelectors d ctor = fieldSelector d <$> dcFields ctor++fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)+fieldSelector d f = (symbol f, mkFFunc n [selfSort d, ft])+  where+    ft            = fldSort d $ dfSort f+    n             = ddVars  d++{- | [NOTE:DataDecl]  This note explains the set of symbols generated+     for the below data-declaration:++  data Vec 1 = [+    | nil  { }+    | cons { vHead : @(0), vTail : Vec}+  ]++We call 'Vec' the _self-sort_ of the data-type, and we want to ensure that+in all constructors, tests and selectors, the _self-sort_ is replaced with+the actual sort, namely, 'Vec @(0)'.++Constructors  // ctor : (fld-sorts) => me++        nil   : func(1, [Vec @(0)])+        cons  : func(1, [@(0); Vec @(0); Vec @(0)])++Tests         // is#ctor : (me) => bool++      is#nil  : func(1, [Vec @(0); bool])+      is#cons : func(1, [Vec @(0); bool])++Selectors     // fld : (me) => fld-sort++      vHead   : func(1, [Vec @(0); @(0)])+      vTail   : func(1, [Vec @(0); Vec @(0)])++-}

@@ -9,11 +9,10 @@ module Language.Fixpoint.Smt.Types (      -- * Serialized Representation-      Raw-    , symbolBuilder+    --    symbolBuilder      -- * Commands-    , Command  (..)+      Command  (..)      -- * Responses     , Response (..)@@ -25,40 +24,37 @@     -- * SMTLIB2 Process Context     , Context (..) -    -- * Theory Symbol-    , TheorySymbol (..)-    , SMTEnv     ) where  import           Language.Fixpoint.Types--- import           Language.Fixpoint.Misc   (traceShow) import qualified Data.Text                as T-import qualified Data.Text.Lazy           as LT import qualified Data.Text.Lazy.Builder   as LT-import           Text.PrettyPrint.HughesPJ +import           Text.PrettyPrint.HughesPJ  import           System.IO                (Handle) import           System.Process+-- import           Language.Fixpoint.Misc   (traceShow)  -------------------------------------------------------------------------------- -- | Types --------------------------------------------------------------------- ---------------------------------------------------------------------------------type Raw          = LT.Text -symbolBuilder :: Symbol -> LT.Builder-symbolBuilder = LT.fromText . symbolSafeText+-- symbolBuilder :: Symbol -> LT.Builder+-- symbolBuilder = LT.fromText . symbolSafeText  -- | Commands issued to SMT engine data Command      = Push                   | Pop                   | CheckSat-                  | Declare   !Symbol [Sort] !Sort-                  | Define    !Sort-                  | Assert    !(Maybe Int) !Expr-                  | AssertAxiom  !(Triggered Expr)-                  | Distinct  [Expr] -- {v:[Expr] | 2 <= len v}-                  | GetValue  [Symbol]-                  | CMany [Command]+                  | DeclData !DataDecl+-- /                  | Declare  !Symbol [Sort] !Sort+                  | Declare  !Symbol [SmtSort] !SmtSort+                  | Define   !Sort+                  | Assert   !(Maybe Int) !Expr+                  | AssertAx !(Triggered Expr)+                  | Distinct [Expr] -- {v:[Expr] | 2 <= len v}+                  | GetValue [Symbol]+                  | CMany    [Command]                   deriving (Eq, Show)  instance PPrint Command where@@ -68,10 +64,11 @@ ppCmd Push          = text "Push" ppCmd Pop           = text "Pop" ppCmd CheckSat      = text "CheckSat"+ppCmd (DeclData d)  = text "Data" <+> pprint d ppCmd (Declare {})  = text "Declare ..." ppCmd (Define {})   = text "Define ..." ppCmd (Assert _ e)  = text "Assert" <+> pprint e-ppCmd (AssertAxiom _) = text "AssertAxiom ..."+ppCmd (AssertAx _)  = text "AssertAxiom ..." ppCmd (Distinct {}) = text "Distinct ..." ppCmd (GetValue {}) = text "GetValue ..." ppCmd (CMany {})    = text "CMany ..."@@ -96,26 +93,15 @@   , ctxAeq     :: !Bool              -- ^ flag to enable lambda a-equivalence axioms   , ctxBeq     :: !Bool              -- ^ flag to enable lambda b-equivalence axioms   , ctxNorm    :: !Bool              -- ^ flag to enable lambda normal form equivalence axioms-  , ctxSmtEnv  :: !SMTEnv+  , ctxSymEnv  :: !SymEnv   } -type SMTEnv = SEnv Sort---- | Theory Symbol-data TheorySymbol  = Thy-  { tsSym    :: !Symbol    -- ^ name-  , tsRaw    :: !Raw       -- ^ serialized SMTLIB2 name-  , tsSort   :: !Sort      -- ^ sort-  , tsInterp :: !Bool      -- ^ TRUE = defined (interpreted), FALSE = declared (uninterpreted)-  }-  deriving (Eq, Ord, Show)- -------------------------------------------------------------------------------- -- | AST Conversion: Types that can be serialized ------------------------------ --------------------------------------------------------------------------------  class SMTLIB2 a where-  smt2 :: a -> LT.Builder+  smt2 :: SymEnv -> a -> LT.Builder -runSmt2 :: (SMTLIB2 a) => a -> LT.Builder+runSmt2 :: (SMTLIB2 a) => SymEnv -> a -> LT.Builder runSmt2 = smt2

@@ -40,8 +40,7 @@ import           Language.Fixpoint.Parse            (rr') import           Language.Fixpoint.Types import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars)-import           Language.Fixpoint.Solver.Instantiate (instantiateFInfo)-import           Language.Fixpoint.Smt.Interface (makeSmtContext, smtPush)+import           Language.Fixpoint.Solver.Instantiate (instantiate) import           Control.DeepSeq  ---------------------------------------------------------------------------@@ -49,7 +48,15 @@ --------------------------------------------------------------------------- solveFQ :: Config -> IO ExitCode ----------------------------------------------------------------------------solveFQ cfg = do+solveFQ cfg = solveFQ' cfg `catch` errorExit++errorExit :: Error -> IO ExitCode+errorExit e = do+  colorStrLn Sad ("Oops, unexpected error: " ++ showpp e)+  return (ExitFailure 2)++solveFQ' :: Config -> IO ExitCode+solveFQ' cfg = do     (fi, opts) <- readFInfo file     cfg'       <- withPragmas cfg opts     let fi'     = ignoreQualifiers cfg' fi@@ -73,7 +80,7 @@ -------------------------------------------------------------------------------- -- | Solve FInfo system of horn-clause constraints ----------------------------- ---------------------------------------------------------------------------------solve :: (NFData a, Fixpoint a) => Solver a+solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a -------------------------------------------------------------------------------- solve cfg q   | parts cfg      = partition  cfg        $!! q@@ -83,12 +90,12 @@   | minimizeKs cfg = minKvars cfg solve'   $!! q   | otherwise      = solve'     cfg        $!! q -solve' :: (NFData a, Fixpoint a) => Solver a+solve' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a solve' cfg q = do   when (save cfg) $ saveQuery   cfg q   configSW  cfg     solveNative cfg q -configSW :: (NFData a, Fixpoint a) => Config -> Solver a -> Solver a+configSW :: (NFData a, Fixpoint a, Show a, Loc a) => Config -> Solver a -> Solver a configSW cfg   | multicore cfg = solveParWith   | otherwise     = solveSeqWith@@ -151,7 +158,7 @@ -------------------------------------------------------------------------------- -- | Native Haskell Solver ----------------------------------------------------- ---------------------------------------------------------------------------------solveNative, solveNative' :: (NFData a, Fixpoint a) => Solver a+solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a -------------------------------------------------------------------------------- solveNative !cfg !fi0 = (solveNative' cfg fi0)                           `catch`@@ -172,15 +179,12 @@   -- rnf fi0 `seq` donePhase Loud "Read Constraints"   -- let qs   = quals fi0   -- whenLoud $ print qs-  -- TODO: make this less of a hack-  ctx <- makeSmtContext cfg (srcFile cfg ++ ".evals") []-  smtPush ctx-  fi1 <- instantiateFInfo cfg ctx $ fi0 { quals = remakeQual <$> quals fi0 }   -- whenLoud $ putStrLn $ showFix (quals fi1)+  let fi1   = fi0 { quals = remakeQual <$> quals fi0 }   let si0   = {-# SCC "convertFormat" #-} convertFormat fi1   -- writeLoud $ "fq file after format convert: \n" ++ render (toFixpoint cfg si0)   -- rnf si0 `seq` donePhase Loud "Format Conversion"-  let si1 = either die id $ {-# SCC "sanitize" #-} sanitize $!! si0+  let si1   = either die id $ {-# SCC "sanitize" #-} sanitize $!! si0   -- writeLoud $ "fq file after sanitize: \n" ++ render (toFixpoint cfg si1)   -- rnf si1 `seq` donePhase Loud "Validated Constraints"   graphStatistics cfg si1@@ -193,7 +197,8 @@   loudDump 2 cfg si4   let si5  = {-# SCC "elaborate"  #-} elaborate "solver" (symbolEnv cfg si4) si4   loudDump 3 cfg si5-  res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si5+  si6 <- {-# SCC "Sol.inst"  #-} instantiate cfg $!! si5+  res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si6   -- rnf soln `seq` donePhase Loud "Solve2"   --let stat = resStatus res   saveSolution cfg res

@@ -4,56 +4,39 @@ module Language.Fixpoint.Solver.GradualSolution   ( -- * Create Initial Solution     init--    -- * Update Solution-  , Sol.update--  -- * Lookup Solution-  , lhsPred   ) where  import           Control.Parallel.Strategies-import           Control.Arrow (second)-import qualified Data.HashSet                   as S import qualified Data.HashMap.Strict            as M import qualified Data.List                      as L-import           Data.Maybe                     (fromMaybe, maybeToList, isNothing, catMaybes)+import           Data.Maybe                     (maybeToList, isNothing) import           Data.Monoid                    ((<>)) import           Language.Fixpoint.Types.PrettyPrint ()-import           Language.Fixpoint.Types.Visitor      as V import qualified Language.Fixpoint.SortCheck          as So import           Language.Fixpoint.Misc-import qualified Language.Fixpoint.Smt.Theories       as Thy-import           Language.Fixpoint.Types.Config import qualified Language.Fixpoint.Types              as F-import           Language.Fixpoint.Types                 ((&.&)) import qualified Language.Fixpoint.Types.Solutions    as Sol import           Language.Fixpoint.Types.Constraints  hiding (ws, bs) import           Prelude                              hiding (init, lookup)-import           Language.Fixpoint.Solver.Sanitize   -------------------------------------------------------------------------------- -- | Initial Gradual Solution (from Qualifiers and WF constraints) ------------- ---------------------------------------------------------------------------------init :: Config -> F.SInfo a -> S.HashSet F.KVar -> Sol.GSolution+init :: (F.Fixpoint a) => F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))] ---------------------------------------------------------------------------------init cfg si ks = Sol.fromList senv geqs keqs [] mempty+init si = map (refineG si qs genv) gs `using` parList rdeepseq    where-    keqs       = map (refine si qs genv)  ws `using` parList rdeepseq-    geqs       = map (refineG si qs genv) gs `using` parList rdeepseq      qs         = F.quals si-    ws         = [ w | (k, w) <- ws0, k `S.member` ks]     gs         = snd <$> gs0     genv       = instConstants si-    senv       = symbolEnv cfg si -    (gs0,ws0)  = L.partition (isGWfc . snd) $ M.toList (F.ws si)+    gs0        = L.filter (isGWfc . snd) $ M.toList (F.ws si)   ---------------------------------------------------------------------------------refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (((F.Symbol,F.Sort), F.Expr), Sol.GBind))-refineG fi qs genv w = (k, (((fst3 $ wrft w, snd3 $ wrft w), wexpr w), Sol.qbToGb qb))+refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (F.GWInfo, [F.Expr]))+refineG fi qs genv w = (k, (F.gwInfo w, Sol.qbExprs qb))   where      (k, qb) = refine fi qs genv w  @@ -135,286 +118,4 @@     p             = Sol.eqPred eq     tc            = So.checkSorted env sr  ------------------------------------------------------------------------------------- | Predicate corresponding to LHS of constraint in current solution----------------------------------------------------------------------------------lhsPred :: F.SolEnv -> Sol.GSolution -> F.SimpC a ->  [([(F.KVar, Sol.QBind)], F.Expr)]-lhsPred be s c = gSelectToList (fst <$> applyGradual g s bs)-  where-    g                 = (ci, be, bs)-    bs                = F.senv c-    ci                = sid c--type Cid         = Maybe Integer-type CombinedEnv = (Cid, F.SolEnv, F.IBindEnv)-type ExprInfo    = (F.Expr, KInfo)--applyGradual        :: CombinedEnv -> Sol.GSolution -> F.IBindEnv -> GSelect ExprInfo-applyGradual g s bs = mappendGSelect mappendExprInfo pks (applyKVarsGrad g s ks)-  where-    pgs           = allCombinations $ applyGVars g s gs-    pks           = if null gs -                        then GNone (F.pAnd ps, mempty) -                        else GOpt [(fst (unzip l) , (F.pAnd (ps++snd (unzip l)), mempty)) | l <- pgs ]-    (ps,  ks, gs) = envConcKVars g bs--    mappendExprInfo (e1, i1) (e2, i2) = (F.pAnd [e1, e2], mappend i1 i2)---envConcKVars :: CombinedEnv -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])-envConcKVars g bs = (concat pss, concat kss, L.nubBy (\x y -> F.ksuKVar x == F.ksuKVar y) $ concat gss)-  where-    (pss, kss, gss) = unzip3 [ F.sortedReftConcKVars x sr | (x, sr) <- xrs ]-    xrs             = (\i -> F.lookupBindEnv i be) <$> is-    is              = F.elemsIBindEnv bs-    be              = F.soeBinds (snd3 g)--applyGVars :: CombinedEnv -> Sol.GSolution -> [F.KVSub] -> [[((F.KVar, Sol.QBind), F.Expr)]]-applyGVars g s = map (applyGVar g s)---applyGVar :: CombinedEnv -> Sol.GSolution -> F.KVSub -> [((F.KVar, Sol.QBind), F.Expr)]-applyGVar g s ksu = case Sol.glookup s (F.ksuKVar ksu) of-  Right (Right (e,eqss)) -> [((F.ksuKVar ksu, eqs), F.pAnd ((F.subst su (snd e)):(fst <$> Sol.qbPreds msg s su eqs))) | eqs <- Sol.gbToQbs eqss]-  _                      -> []-  where-    msg     = "applyGVar: " ++ show (fst3 g)-    su      = F.ksuSubst ksu--applyKVarsGrad :: CombinedEnv -> Sol.GSolution -> [F.KVSub] -> GSelect ExprInfo-applyKVarsGrad g s xs = (f <$> (collapseGSelect $ map (applyKVarGrad g s) xs))-  where-    f xs = let (es, is) = unzip xs  in (F.pAnd es, mconcat is)--applyKVarGrad :: CombinedEnv -> Sol.GSolution -> F.KVSub -> GSelect ExprInfo-applyKVarGrad g s ksu = case Sol.glookup s (F.ksuKVar ksu) of-  Left cs                -> hypPredGrad g s ksu cs-  Right (Left eqs)       -> GNone (F.pAnd $ fst <$> Sol.qbPreds msg s (F.ksuSubst ksu) eqs, mempty)-  Right (Right (e,eqss)) -> GOpt [([(F.ksuKVar ksu, eqs)]-                                  , (, mempty) $ F.pAnd ((F.subst su (snd e)):(fst <$> Sol.qbPreds msg s su eqs))) -                                  | eqs <- Sol.gbToQbs eqss]-  where-    msg     = "applyKVar: " ++ show (fst3 g) -    su      = F.ksuSubst ksu---hypPredGrad :: CombinedEnv -> Sol.GSolution -> F.KVSub -> Sol.Hyp  -> GSelect ExprInfo-hypPredGrad g s ksu xs = f <$> (collapseGSelect $ map (cubePredGrad g s ksu) xs)-  where-    f xs = let (es, is) = unzip xs  in (F.pOr es, mconcatPlus is)---{- | `cubePred g s k su c` returns the predicate for--        (k . su)--      defined by using cube--        c := [b1,...,bn] |- (k . su')--      in the binder environment `g`.--        bs' := the subset of "extra" binders in [b1...bn] that are *not* in `g`-        p'  := the predicate corresponding to the "extra" binders-- -}--elabExist :: Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> F.Expr-elabExist s xts = F.pExist xts'-  where-    xts'        = [ (x, elab t) | (x, t) <- xts]-    elab        = So.elaborate "elabExist" env-    env         = Sol.sEnv s---cubePredGrad :: CombinedEnv -> Sol.GSolution -> F.KVSub -> Sol.Cube -> GSelect ExprInfo-cubePredGrad g s ksu c  = ((\((xts,psu,p), kI) -> (elabExist s xts (psu &.& p) , kI)) <$> cubePredExcGrad g s ksu c bs')-  where-    bs'               = delCEnv s k bs-    bs                = Sol.cuBinds c-    k                 = F.ksuKVar ksu---type Binders = [(F.Symbol, F.Sort)]---- | @cubePredExc@ computes the predicate for the subset of binders bs'.---   The output is a tuple, `(xts, psu, p, kI)` such that the actual predicate---   we want is `Exists xts. (psu /\ p)`.---cubePredExcGrad :: CombinedEnv -> Sol.GSolution -> F.KVSub -> Sol.Cube -> F.IBindEnv-            -> GSelect ((Binders, F.Pred, F.Pred), KInfo)-cubePredExcGrad g s ksu c bs' -  = f <$> (applyGradual g' s bs')-  where-    f (p', kI)      = ((xts, psu, elabExist s yts' (p' &.& psu') ), extendKInfo kI (Sol.cuTag c))-    yts'            = symSorts g bs'-    g'              = addCEnv  g bs-    -    (_  , psu')     = substElim sEnv g' k su'-    (xts, psu)      = substElim sEnv g  k su-    su'             = Sol.cuSubst c-    bs              = Sol.cuBinds c-    k               = F.ksuKVar   ksu-    su              = F.ksuSubst  ksu-    sEnv            = F.insertSEnv (F.ksuVV ksu) (F.ksuSort ksu) (Sol.sEnv s)----- TODO: SUPER SLOW! Decorate all substitutions with Sorts in a SINGLE pass.--{- | @substElim@ returns the binders that must be existentially quantified,-     and the equality predicate relating the kvar-"parameters" and their-     actual values. i.e. given--        K[x1 := e1]...[xn := en]--     where e1 ... en have types t1 ... tn-     we want to quantify out--       x1:t1 ... xn:tn--     and generate the equality predicate && [x1 ~~ e1, ... , xn ~~ en]-     we use ~~ because the param and value may have different sorts, see:--        tests/pos/kvar-param-poly-00.hs--     Finally, we filter out binders if they are--     1. "free" in e1...en i.e. in the outer environment.-        (Hmm, that shouldn't happen...?)--     2. are binders corresponding to sorts (e.g. `a : num`, currently used-        to hack typeclasses current.)- -}-substElim :: F.SEnv F.Sort -> CombinedEnv -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)-substElim sEnv g _ (F.Su m) = (xts, p)-  where-    p      = F.pAnd [ mkSubst x (substSort sEnv frees x t) e t | (x, e, t) <- xets  ]-    xts    = [ (x, t)    | (x, _, t) <- xets, not (S.member x frees) ]-    xets   = [ (x, e, t) | (x, e)    <- xes, t <- sortOf e, not (isClass t)]-    xes    = M.toList m-    env    = combinedSEnv g-    frees  = S.fromList (concatMap (F.syms . snd) xes)-    sortOf = maybeToList . So.checkSortExpr env--substSort :: F.SEnv F.Sort -> S.HashSet F.Symbol -> F.Symbol -> F.Sort -> F.Sort-substSort sEnv _frees x _t = fromMaybe (err x) $ F.lookupSEnv x sEnv-  where-    err x            = error $ "Solution.mkSubst: unknown binder " ++ F.showpp x--mkSubst :: F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr-mkSubst x tx ey ty-  | tx == ty    = F.EEq ex ey-  | otherwise   = F.notracepp msg (F.EEq ex' ey')-  where-    msg         = "mkSubst-DIFF:" ++ F.showpp (tx, ty) ++ F.showpp (ex', ey')-    ex          = F.expr x-    ex'         = Thy.toInt ex tx-    ey'         = Thy.toInt ey ty--isClass :: F.Sort -> Bool-isClass F.FNum  = True-isClass F.FFrac = True-isClass _       = False----badExpr :: CombinedEnv -> F.KVar -> F.Expr -> a---badExpr g@(i,_,_) k e-  -- = errorstar $ "substSorts has a badExpr: "-              -- ++ show e-              -- ++ " in cid = "-              -- ++ show i-              -- ++ " for kvar " ++ show k-              -- ++ " in env \n"-              -- ++ show (combinedSEnv g)---- substPred :: F.Subst -> F.Pred--- substPred (F.Su m) = F.pAnd [ F.PAtom F.Eq (F.eVar x) e | (x, e) <- M.toList m]--combinedSEnv :: CombinedEnv -> F.SEnv F.Sort-combinedSEnv (_, se, bs) = F.sr_sort <$> F.fromListSEnv (F.envCs be bs)-  where-    be                   = F.soeBinds se--addCEnv :: CombinedEnv -> F.IBindEnv -> CombinedEnv-addCEnv (x, be, bs) bs' = (x, be, F.unionIBindEnv bs bs')---- delCEnv :: F.IBindEnv -> CombinedEnv -> F.IBindEnv--- delCEnv bs (_, _, bs')  = F.diffIBindEnv bs bs'--delCEnv :: Sol.Sol a Sol.QBind -> F.KVar -> F.IBindEnv -> F.IBindEnv-delCEnv s k bs  = F.diffIBindEnv bs _kbs-                                                -- ORIG: bs'-  where-    _kbs = safeLookup "delCEnv" k (Sol.sScp s)--symSorts :: CombinedEnv -> F.IBindEnv -> [(F.Symbol, F.Sort)]-symSorts (_, se, _) bs = second F.sr_sort <$> F.envCs be  bs-  where-    be                 = F.soeBinds se--_noKvars :: F.Expr -> Bool-_noKvars = null . V.kvars------------------------------------------------------------------------------------- | Information about size of formula corresponding to an "eliminated" KVar.----------------------------------------------------------------------------------data KInfo = KI { kiTags  :: [Tag]-                , kiDepth :: !Int-                , kiCubes :: !Integer-                } deriving (Eq, Ord, Show)--instance Monoid KInfo where-  mempty         = KI [] 0 1-  mappend ki ki' = KI ts d s-    where-      ts         = appendTags (kiTags  ki) (kiTags  ki')-      d          = max        (kiDepth ki) (kiDepth ki')-      s          = (*)        (kiCubes ki) (kiCubes ki')--mplus :: KInfo -> KInfo -> KInfo-mplus ki ki' = (mappend ki ki') { kiCubes = kiCubes ki + kiCubes ki'}--mconcatPlus :: [KInfo] -> KInfo-mconcatPlus = foldr mplus mempty--appendTags :: [Tag] -> [Tag] -> [Tag]-appendTags ts ts' = sortNub (ts ++ ts')--extendKInfo :: KInfo -> F.Tag -> KInfo-extendKInfo ki t = ki { kiTags  = appendTags [t] (kiTags  ki)-                      , kiDepth = 1  +            kiDepth ki }-------------------------------------------------------------------------------------- | Gradual Selection Interface ---------------------------------------------------------------------------------------------------------------------------------data GSelect a = GNone a | GOpt [([(F.KVar, Sol.QBind)], a)] deriving (Show)---gSelectToList :: GSelect a -> [([(F.KVar, Sol.QBind)], a)]-gSelectToList (GNone a) = [([], a)]-gSelectToList (GOpt xs) = xs ---instance Functor GSelect where-  fmap f (GNone a) = GNone  (f a)-  fmap f (GOpt xs) = GOpt [(p, f a) | (p, a) <- xs]--mappendGSelect :: (a -> a -> b) -> GSelect a -> GSelect a -> GSelect b -mappendGSelect f (GNone x) (GNone y) = GNone (f x y)-mappendGSelect f (GNone x) (GOpt ys) = GOpt [(i, f x y) | (i, y) <- ys] -mappendGSelect f (GOpt xs) (GNone y) = GOpt [(i, f x y) | (i, x) <- xs]-mappendGSelect f (GOpt xs) (GOpt ys) = GOpt $ concatMap (\y -> (catMaybes $ map (\x -> g x y) xs)) ys -  where-    g (xs, x) (ys, y)-      | null [ () | (k1, _) <- xs, (k2, _) <- ys, k1 == k2 ]  -      =  Just (xs ++ ys, f x y)-      | and [v1 == v2 | (k1, v1) <- xs, (k2, v2) <- ys, k1 == k2 ] -      = Just (xs ++ [(k, v) | (k, v) <- ys, not (k `elem` (fst <$> xs))], f x y)-      | otherwise-      = Nothing --collapseGSelect :: [GSelect a] -> GSelect [a]-collapseGSelect = foldl (mappendGSelect (\x y -> (x ++ y))) (GNone []) . fmap (fmap (:[])) 

@@ -1,319 +0,0 @@-{-# LANGUAGE PatternGuards     #-}-{-# LANGUAGE TupleSections     #-}-{-# LANGUAGE FlexibleContexts  #-}-{-# LANGUAGE OverloadedStrings #-}------------------------------------------------------------------------------------- | Solve a system of horn-clause constraints --------------------------------------------------------------------------------------------------------------------module Language.Fixpoint.Solver.GradualSolve (solveGradual) where--import           Control.Monad (when, filterM, foldM)-import           Control.Monad.State.Strict (lift)-import           Language.Fixpoint.Misc-import qualified Language.Fixpoint.Types           as F-import qualified Language.Fixpoint.Types.Solutions as Sol-import qualified Language.Fixpoint.SortCheck       as So-import           Language.Fixpoint.Types.PrettyPrint-import           Language.Fixpoint.Types.Config hiding (stats)-import qualified Language.Fixpoint.Solver.GradualSolution  as S-import qualified Language.Fixpoint.Solver.Worklist  as W-import qualified Language.Fixpoint.Solver.Eliminate as E-import           Language.Fixpoint.Solver.Monad-import           Language.Fixpoint.Utils.Progress-import           Language.Fixpoint.Graph-import           Text.PrettyPrint.HughesPJ-import           Text.Printf-import           System.Console.CmdArgs.Verbosity (whenNormal, whenLoud)-import           Control.DeepSeq-import qualified Data.HashMap.Strict as M-import qualified Data.HashSet        as S------------------------------------------------------------------------------------- | Progress Bar----------------------------------------------------------------------------------withProgressFI :: SolverInfo a b -> IO b -> IO b-withProgressFI = withProgress . fromIntegral . cNumScc . siDeps-----------------------------------------------------------------------------------printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()-printStats fi w s = putStrLn "\n" >> ppTs [ ptable fi, ptable s, ptable w ]-  where-    ppTs          = putStrLn . showpp . mconcat-----------------------------------------------------------------------------------solverInfo :: Config -> F.SInfo a -> SolverInfo a b----------------------------------------------------------------------------------solverInfo cfg fI-  | useElim cfg = E.solverInfo cfg fI-  | otherwise   = SI mempty fI cD (siKvars fI)-  where-    cD          = elimDeps fI (kvEdges fI) mempty--siKvars :: F.SInfo a -> S.HashSet F.KVar-siKvars = S.fromList . M.keys . F.ws-------------------------------------------------------------------------------------- | tidyResult ensures we replace the temporary kVarArg names introduced to---   ensure uniqueness with the original names in the given WF constraints.----------------------------------------------------------------------------------tidyResult :: F.Result a -> F.Result a-tidyResult r = r { F.resSolution  =  tidySolution  (F.resSolution r)-                 , F.gresSolution =  gtidySolution (F.gresSolution r) -                 }--tidySolution :: F.FixSolution -> F.FixSolution-tidySolution = fmap tidyPred--gtidySolution :: F.GFixSolution -> F.GFixSolution-gtidySolution = fmap tidyPred --  (\(e, es) -> (tidyPred e, tidyPred <$> es))--tidyPred :: F.Expr -> F.Expr-tidyPred = F.substf (F.eVar . F.tidySymbol)---predKs :: F.Expr -> [(F.KVar, F.Subst)]-predKs (F.PAnd ps)    = concatMap predKs ps-predKs (F.PKVar k su) = [(k, su)]-predKs _              = []-------------------------------------------------------------------------------------minimizeResult :: Config -> M.HashMap F.KVar F.Expr-               -> SolveM (M.HashMap F.KVar F.Expr)----------------------------------------------------------------------------------minimizeResult cfg s-  | minimalSol cfg = mapM minimizeConjuncts s-  | otherwise      = return s--minimizeConjuncts :: F.Expr -> SolveM F.Expr-minimizeConjuncts p = F.pAnd <$> go (F.conjuncts p) []-  where-    go []     acc   = return acc-    go (p:ps) acc   = do b <- isValid (F.pAnd (acc ++ ps)) p-                         if b then go ps acc-                              else go ps (p:acc)----showUnsat :: Bool -> Integer -> F.Pred -> F.Pred -> IO ()-showUnsat u i lP rP = {- when u $ -} do-  putStrLn $ printf   "UNSAT id %s %s" (show i) (show u)-  putStrLn $ showpp $ "LHS:" <+> pprint lP-  putStrLn $ showpp $ "RHS:" <+> pprint rP------------------------------------------------------------------------------------- | Predicate corresponding to RHS of constraint in current solution----------------------------------------------------------------------------------rhsPred :: F.SimpC a -> F.Expr----------------------------------------------------------------------------------rhsPred c-  | isTarget c = F.crhs c-  | otherwise  = errorstar $ "rhsPred on non-target: " ++ show (F.sid c)--isValid :: F.Expr -> F.Expr -> SolveM Bool-isValid p q = (not . null) <$> filterValid p [(q, ())]------------------------------------------------------------------------------------- | solve with edits to allow Gradual types --------------------------------------------------------------------------------------------------------------------solveGradual :: (NFData a, F.Fixpoint a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))--solveGradual cfg fi = do-    (res, stat) <- withProgressFI sI $ runSolverM cfg sI n act-    when (solverStats cfg) $ printStats fi wkl stat-    return res-  where-    act  = solveGradual_ cfg fi s0 ks  wkl-    sI   = solverInfo cfg fi-    wkl  = W.init sI-    n    = fromIntegral $ W.wRanks wkl-    s0   = siSol  sI-    ks   = siVars sI-----------------------------------------------------------------------------------solveGradual_ :: (NFData a, F.Fixpoint a)-       => Config-       -> F.SInfo a-       -> Sol.GSolution -       -> S.HashSet F.KVar-       -> W.Worklist a-       -> SolveM (F.Result (Integer, a), Stats)----------------------------------------------------------------------------------solveGradual_ cfg fi s0 ks wkl = do-  let s1  = mappend s0 $ {-# SCC "sol-init" #-} S.init cfg fi ks-  s2      <- {-# SCC "sol-local"  #-} filterLocal s1-  s       <- {-# SCC "sol-refine" #-} refine s2 wkl-  res     <- {-# SCC "sol-result" #-} result cfg wkl s-  st      <- stats-  let res' = {-# SCC "sol-tidy"   #-} tidyResult res-  return $!! (res', st)--filterLocal :: Sol.GSolution -> SolveM Sol.GSolution -filterLocal sol = do -  gs' <- mapM (initGBind sol) gs -  return $ Sol.updateGMap sol $ M.fromList gs'-  where -    gs = M.toList $ Sol.gMap sol --initGBind :: Sol.GSolution -> (F.KVar, (((F.Symbol, F.Sort), F.Expr), Sol.GBind)) -> SolveM (F.KVar, (((F.Symbol, F.Sort), F.Expr), Sol.GBind))-initGBind sol (k, (e, gb)) = do  -   elems0  <- filterM (isLocal e) (Sol.gbEquals gb)-   elems   <- sortEquals elems0 -   lattice <- makeLattice [] (map (:[]) elems) elems-   return $ ((k,) . (e,) . Sol.equalsGb) lattice-  where-    makeLattice acc new elems-      | null new-      = return acc -      | otherwise-      = do let cands = [e:es |e<-elems, es<-new]-           localCans <- filterM (isLocal e) cands-           newElems  <- filterM (notTrivial (new ++ acc)) localCans -           makeLattice (acc ++ new) newElems elems--    notTrivial [] _     = return True -    notTrivial (x:xs) p = do v <- isValid (mkPred x) (mkPred p)-                             if v then return False -                                  else notTrivial xs p --    mkPred eq = So.elaborate "initBGind.mkPred" (Sol.sEnv sol) (F.pAnd (Sol.eqPred <$> eq))-    isLocal (v, e) eqs = do -      let pp = So.elaborate "filterLocal" (Sol.sEnv sol) $ F.PExist [v] $ F.pAnd (e:(Sol.eqPred <$> eqs)) -      isValid mempty pp--    root      = Sol.trueEqual-    sortEquals xs = (bfs [0]) <$> makeEdges vs [] vs -      where -       vs        = zip [0..] (root:(head <$> xs))--       bfs []     _  = [] -       bfs (i:is) es = (snd $ (vs!!i)) : bfs (is++map snd (filter (\(j,k) ->  (j==i && notElem k is)) es)) es--       makeEdges _   acc []    = return acc-       makeEdges vs acc (x:xs) = do ves  <- concat <$> mapM (makeEdgesOne x) vs-                                    if any (\(i,j) -> elem (j,i) acc) ves -                                      then makeEdges (filter ((/= fst x) . fst) vs) (filter (\(i,j) -> ((i /= fst x) && (j /= fst x))) acc) xs -                                      else makeEdges vs (mergeEdges (ves ++ acc)) xs --    makeEdgesOne (i,_) (j,_) | i == j = return [] -    makeEdgesOne (i,x) (j,y) = do -      ij <- isValid (mkPred [x]) (mkPred [y])-      return (if ij then [(j,i)] else [])--    mergeEdges es = filter (\(i,j) -> (not (any (\k -> ((i,k) `elem` es && (k,j) `elem` es)) (fst <$> es)))) es------------------------------------------------------------------------------------refine :: Sol.GSolution -> W.Worklist a -> SolveM Sol.GSolution----------------------------------------------------------------------------------refine s w-  | Just (c, w', newScc, rnk) <- W.pop w = do-     i       <- tickIter newScc-     (b, s') <- refineC i s c-     lift $ writeLoud $ refineMsg i c b rnk-     let w'' = if b then W.push c w' else w'-     refine s' w''-  | otherwise = return s-  where-    -- DEBUG-    refineMsg i c b rnk = printf "\niter=%d id=%d change=%s rank=%d\n"-                            i (F.subcId c) (show b) rnk-------------------------------------------------------------------------------- | Single Step Refinement ----------------------------------------------------------------------------------------------------------------------------refineC :: Int -> Sol.GSolution -> F.SimpC a -> SolveM (Bool, Sol.GSolution)-----------------------------------------------------------------------------refineC _i s c-  | null rhs  = return (False, s)-  | otherwise = do be      <- getBinds-                   let lhss = snd <$> S.lhsPred be s c-                   kqs     <- filterValidGradual lhss rhs-                   return   $ S.update s ks kqs-  where-    _ci       = F.subcId c-    (ks, rhs) = rhsCands s c-    -- msg       = printf "refineC: iter = %d, sid = %s, soln = \n%s\n"-    --               _i (show (F.sid c)) (showpp s)-    _msg ks xs ys = printf "refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"-                     _i (show _ci) (showpp ks) (length xs) (length ys)---rhsCands :: Sol.GSolution -> F.SimpC a -> ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))-rhsCands s c    = (fst <$> ks, kqs)-  where-    kqs         = [ (p, (k, q)) | (k, su) <- ks, (p, q)  <- cnd k su ]-    ks          = predKs . F.crhs $ c-    cnd k su    = Sol.qbPreds msg s su (Sol.lookupQBind s k)-    msg         = "rhsCands: " ++ show (F.sid c)------------------------------------------------------------------------------------- | Gradual Convert Solution into Result --------------------------------------------------------------------------------------------------------------------------------result :: (F.Fixpoint a) => Config -> W.Worklist a -> Sol.GSolution-       -> SolveM (F.Result (Integer, a))----------------------------------------------------------------------------------result cfg wkl s = do-  lift $ writeLoud "Computing Result"-  stat    <- result_ wkl s -  lift $ whenNormal $ putStrLn $ "RESULT: " ++ show (F.sid <$> stat)-  F.Result (ci <$> stat) <$> solResult cfg s <*> solResultGradual wkl cfg s -  where-    ci c = (F.subcId c, F.sinfo c)--result_ :: Fixpoint a =>  W.Worklist a -> Sol.GSolution -> SolveM (F.FixResult (F.SimpC a))-result_  w s = res <$> filterM (isUnsat s) cs-  where-    cs       = W.unsatCandidates w-    res []   = F.Safe-    res cs'  = F.Unsafe cs'--solResult :: Config -> Sol.GSolution -> SolveM (M.HashMap F.KVar F.Expr)-solResult cfg-  = minimizeResult cfg . Sol.result---solResultGradual :: W.Worklist a -> Config -> Sol.GSolution -> SolveM F.GFixSolution-solResultGradual w _cfg sol -  = F.toGFixSol . Sol.resultGradual <$> updateGradualSolution (W.unsatCandidates w) sol-----------------------------------------------------------------------------------updateGradualSolution :: [F.SimpC a] -> Sol.GSolution -> SolveM (Sol.GSolution)----------------------------------------------------------------------------------updateGradualSolution cs sol = foldM f (Sol.emptyGMap sol) cs-  where-   f s c = do-    be <- getBinds-    let lpi = S.lhsPred be sol c -    let rp  = rhsPred c -    gbs    <- firstValid rp lpi -    return $ Sol.updateGMapWithKey gbs s ---firstValid :: Monoid a =>  F.Expr -> [(a, F.Expr)] -> SolveM a -firstValid _   [] = return mempty -firstValid rhs ((y,lhs):xs) = do-  v <- isValid lhs rhs-  if v then return y else firstValid rhs xs ------------------------------------------------------------------------------------isUnsat :: Fixpoint a => Sol.GSolution -> F.SimpC a -> SolveM Bool----------------------------------------------------------------------------------isUnsat s c = do-  -- lift   $ printf "isUnsat %s" (show (F.subcId c))-  _     <- tickIter True -- newScc-  be    <- getBinds-  let lpi = S.lhsPred be s c-  let rp = rhsPred        c-  res   <- (not . or) <$> mapM (`isValid` rp) (snd <$> lpi)-  lift   $ whenLoud $ showUnsat res (F.subcId c) (F.pOr (snd <$> lpi)) rp-  return res--

@@ -12,25 +12,18 @@ --------------------------------------------------------------------------------  module Language.Fixpoint.Solver.Instantiate (--  instantiateAxioms,-  instantiateFInfo,-+  instantiate   ) where  import           Language.Fixpoint.Types-import           Language.Fixpoint.Types.Config as FC-import qualified Language.Fixpoint.Smt.Theories as FT-import           Language.Fixpoint.Types.Visitor (eapps, kvars, mapMExpr)-import           Language.Fixpoint.Misc          (mapFst)--import Language.Fixpoint.Smt.Interface          ( smtPop, smtPush-                                                , smtDecls, smtAssert-                                                , checkValid', Context(..) )-import Language.Fixpoint.Defunctionalize        (defuncAny, makeLamArg)-import Language.Fixpoint.SortCheck              (elaborate)--import Control.Monad.State+import           Language.Fixpoint.Types.Config  as FC+import qualified Language.Fixpoint.Types.Visitor as Vis+import qualified Language.Fixpoint.Misc          as Misc -- (mapFst)+import qualified Language.Fixpoint.Smt.Interface as SMT+import           Language.Fixpoint.Defunctionalize+import           Language.Fixpoint.SortCheck+import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)+import           Control.Monad.State  -- AT: I've inlined this, but we should have a more elegant solution --     (track predicates instead of selectors!)@@ -41,7 +34,6 @@ import           Data.Maybe           (catMaybes, fromMaybe) import           Data.Char            (isUpper) import           Data.Foldable        (foldlM)--- import           Data.Monoid          ((<>))  (~>) :: (Expr, String) -> Expr -> EvalST Expr (_e,_str) ~> e' = do@@ -49,61 +41,106 @@     -- traceM $ showpp _str ++ " : " ++ showpp _e ++ showpp e'     return (η e') ------------------------- Instantiate Axioms-----------------------instantiateFInfo :: Config -> Context -> FInfo c -> IO (FInfo c)-instantiateFInfo cfg ctx fi = do-    cm' <- sequence $ M.mapWithKey instantiateOne (cm fi)-    return $ fi { cm = cm' }-  where instantiateOne = instantiateAxioms cfg ctx (bs fi) (gLits fi) (ae fi) -instantiateAxioms :: Config -> Context -> BindEnv -> SEnv Sort -> AxiomEnv-                     -> Integer -> SubC c-                     -> IO (SubC c)-instantiateAxioms _ _ _ _ aenv sid sub+--------------------------------------------------------------------------------+-- | Instantiate Axioms+--------------------------------------------------------------------------------+instantiate :: Config -> SInfo a -> IO (SInfo a)+instantiate cfg fi+  | inst      = instantiate' cfg fi+  | otherwise = return fi+  where+    inst      = rewriteAxioms cfg || arithmeticAxioms cfg++-- instantiate' :: Config -> SInfo a -> IO (SInfo a)+-- instantiate' cfg fi = do+    -- ctx <- SMT.makeContextWithSEnv cfg file env+    -- -- ctx <- SMT.makeSmtContext cfg file (ddecls fi) [] (applySorts fi)+    -- SMT.smtPush ctx+    -- ips <- forM cstrs $ \(i, c) -> do+             -- p <- instSimpC cfg ctx (bs fi) (ae fi) i c+             -- return (i, elaborate "PLE-instantiate" env p)+    -- return (strengthenHyp fi ips)++instantiate' :: Config -> GInfo SimpC a -> IO (SInfo a)+instantiate' cfg fi = do+  ctx <- SMT.makeContextWithSEnv cfg file env+  -- ctx <- SMT.makeSmtContext cfg file (ddecls fi) [] (applySorts fi)+  SMT.smtPush ctx+  ips           <- forM cstrs $ \(i, c) ->+                      (i,) <$> instSimpC cfg ctx (bs fi) (ae fi) i c+  let (is, ps)   = unzip ips+  let (ps', axs) = defuncAxioms cfg env ps+  let ps''       = elaborate "PLE1" env <$> ps'+  let axs'       = elaborate "PLE2" env <$> axs+  let fi'        = fi { asserts = axs' ++ asserts fi }+  return         $ strengthenHyp fi' (zip is ps'')+  where+    cstrs        = M.toList (cm fi)+    file         = srcFile cfg ++ ".evals"+    env          = symbolEnv cfg fi++instSimpC :: Config -> SMT.Context -> BindEnv -> AxiomEnv+          -> Integer -> SimpC a+          -> IO Expr+instSimpC _ _ _ aenv sid _   | not (M.lookupDefault False sid (aenvExpand aenv))-  = return sub-instantiateAxioms cfg ctx bds fenv aenv sid sub-  = flip strengthenLhs sub . pAnd . (is0 ++) .-    (if arithmeticAxioms cfg then (is ++) else id) <$>+  = return PTrue+instSimpC cfg ctx bds aenv sid sub+  = -- tracepp ("instSimpC " ++ show sid) .+    pAnd . (is0 ++) .+    (if arithmeticAxioms cfg then (is1 ++) else id) <$>     if rewriteAxioms cfg then evalEqs else return []   where     is0              = eqBody <$> L.filter (null . eqArgs) eqs-    is               = instances maxNumber aenv initOccurences+    is1              = instances maxNumber aenv initOccurences     evalEqs          =        map (uncurry (PAtom Eq)) .        filter (uncurry (/=)) <$>-       evaluate cfg ctx ((vv Nothing, slhs sub):binds) fenv aenv initExpressions-    initExpressions  = expr (slhs sub) : expr (srhs sub) : (expr <$> binds)-    binds            = envCs bds (senv sub)-    initOccurences   = concatMap (makeInitOccurences as eqs) initExpressions+       evaluate cfg ctx ({- (vv Nothing, slhs sub): -} binds) aenv iExprs+    initOccurences   = concatMap (makeInitOccurences as eqs) iExprs+    eqs              = aenvEqs aenv+    (binds, iExprs)  = cstrBindExprs bds sub+    -- fuel calculated and used only by `instances` arith rewrite method+    fuelNumber       = M.lookupDefault 0 sid (aenvFuel aenv)+    as               = (,fuelNumber) . eqName <$> filter (not . null . eqArgs) eqs+    maxNumber        = (aenvSyms aenv * length initOccurences) ^ fuelNumber -    eqs = aenvEqs aenv+cstrBindExprs :: BindEnv -> SimpC a -> ([(Symbol, SortedReft)], [Expr])+cstrBindExprs bds sub = {- tracepp "initExpressions" -} (unElab <$> binds, unElab <$> es)+  where+    es                = {- expr (slhs sub) : -} (crhs sub) : (expr <$> binds)+    binds             = envCs bds (senv sub)+  --   _tx e              = tracepp ("UNELAB e = " ++ showpp e) (unElab e) -    -- fuel calculated and used only by `instances` arith rewrite method-    fuelNumber = M.lookupDefault 0 sid (aenvFuel aenv)-    as         = (,fuelNumber) . eqName <$> filter (not . null . eqArgs) eqs-    maxNumber  = (length (aenvSyms aenv) * length initOccurences) ^ fuelNumber+unElab :: (Vis.Visitable t) => t -> t+unElab = Vis.stripCasts . unApply +unApply :: (Vis.Visitable t) => t -> t+unApply = Vis.trans (Vis.defaultVisitor { Vis.txExpr = const go }) () ()+  where+    go (ECst (EApp (EApp f e1) e2) _)+      | Just _ <- unApplyAt f = EApp e1 e2+    go e                      = e ---------------------------------- Knowledge (SMT Interaction)---------------------------------- AT:@TODO: knSels and knEqs should reall just be the same thing. In this way,++--------------------------------------------------------------------------------+-- | Knowledge (SMT Interaction)+--------------------------------------------------------------------------------+-- AT:@TODO: knSels and knEqs should really just be the same thing. In this way, -- we should also unify knSims and knAms, as well as their analogues in AxiomEnv data Knowledge   = KN { knSels    :: ![(Expr, Expr)]        , knEqs     :: ![(Expr, Expr)]        , knSims    :: ![Rewrite]        , knAms     :: ![Equation]-       , knContext :: IO Context-       , knPreds   :: !([(Symbol, Sort)] -> Expr -> Context -> IO Bool)+       , knContext :: IO SMT.Context+       , knPreds   :: !([(Symbol, Sort)] -> Expr -> SMT.Context -> IO Bool)        , knLams    :: [(Symbol, Sort)]        } -emptyKnowledge :: IO Context -> Knowledge-emptyKnowledge cxt = KN [] [] [] [] cxt (\_ _ _ -> return False) []+emptyKnowledge :: IO SMT.Context -> Knowledge+emptyKnowledge ctx = KN [] [] [] [] ctx (\_ _ _ -> return False) []  lookupKnowledge :: Knowledge -> Expr -> Maybe Expr lookupKnowledge γ e@@ -118,10 +155,10 @@ isValid :: Knowledge -> Expr -> IO Bool isValid γ b = knPreds γ (knLams γ) b =<< knContext γ -makeKnowledge :: Config -> Context -> AxiomEnv -> SEnv Sort+makeKnowledge :: Config -> SMT.Context -> AxiomEnv                  -> [(Symbol, SortedReft)]                  -> ([(Expr, Expr)], Knowledge)-makeKnowledge cfg ctx aenv fenv es = (simpleEqs,) $ (emptyKnowledge context)+makeKnowledge cfg ctx aenv es = (simpleEqs,) $ (emptyKnowledge context)                                      { knSels   = sels                                      , knEqs    = eqs                                      , knSims   = aenvSimpl aenv@@ -129,19 +166,19 @@                                      , knPreds  = \bs e c -> askSMT c bs e                                      }   where-    (xv, sv) = (vv Nothing, sr_sort $ snd $ head es)-    fbinds = toListSEnv fenv ++ [(x, s) | (x, RR s _) <- es]-    senv = fromListSEnv fbinds--    context :: IO Context+    -- (xv, sv) = (vv Nothing, sr_sort $ snd $ head es)+    -- fbinds   = toListSEnv fenv ++ [(x, s) | (x, RR s _) <- es]+    -- senv     = senvCtx { seSort = fromListSEnv fbinds }+    -- thySyms  = seTheory senvCtx+    senv = SMT.ctxSymEnv ctx+    context :: IO SMT.Context     context = do-      smtPop ctx-      smtPush ctx-      smtDecls ctx $ L.nub [(x, toSMT [] s) | (x, s) <- fbinds-                                            , not (M.member x FT.theorySymbols)]-      smtAssert ctx (pAnd ([toSMT [] (PAtom Eq e1 e2) | (e1, e2) <- simpleEqs]-                           ++ filter (null.kvars) ((toSMT [] . expr) <$> es)-                          ))+      SMT.smtPop ctx+      SMT.smtPush ctx+      -- SMT.smtDecls ctx $ L.nub [(x, toSMT [] s) | (x, s) <- fbinds, not (memberSEnv x thySyms)]+      SMT.smtAssert ctx (pAnd ([toSMT [] (PAtom Eq e1 e2) | (e1, e2) <- simpleEqs]+                               ++ filter (null . Vis.kvars) ((toSMT [] . expr) <$> es)+                              ))       return ctx      -- This creates the rewrite rule e1 -> e2@@ -162,26 +199,21 @@     eqs = [(EVar x, ex) | Equ a _ bd <- filter (null . eqArgs) $ aenvEqs aenv                         , PAtom Eq (EVar x) ex <- splitPAnd bd                         , x == a-                        -- AT: no test needs this-                        --, EVar x /= ex                         ] -    toSMT xs = defuncAny cfg (insertSEnv xv sv senv) .-               elaborate "symbolic evaluation"-               (foldl (\env (x,s) -> insertSEnv x s (deleteSEnv x env))-                      (insertSEnv xv sv senv)-                      xs)+    toSMT bs = defuncAny cfg senv . elaborate "makeKnowledge" (elabEnv bs)+    elabEnv  = L.foldl' (\env (x, s) -> insertSymEnv x s env) senv      -- AT: Non-obvious needed invariant: askSMT True is always the     -- totality-effecting one-    askSMT :: Context -> [(Symbol, Sort)] -> Expr -> IO Bool-    askSMT cxt xss e+    askSMT :: SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool+    askSMT ctx bs e       | isTautoPred  e = return True       | isContraPred e = return False-      | null (kvars e) = do-          smtPush cxt-          b <- checkValid' cxt [] PTrue (toSMT xss e)-          smtPop cxt+      | null (Vis.kvars e) = do+          SMT.smtPush ctx+          b <- SMT.checkValid' ctx [] PTrue (toSMT bs e)+          SMT.smtPop ctx           return b       | otherwise      = return False @@ -190,7 +222,6 @@     isSelector  = L.isPrefixOf "select" . symbolString     isProof (_, RR s _) =  showpp s == "Tuple" - makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)] makeSimplifications sis (dc, es, e)  = go =<< sis@@ -215,8 +246,8 @@     | otherwise     = Nothing   where-    (f1, es1) = mapFst getDC $ splitEApp e1-    (f2, es2) = mapFst getDC $ splitEApp e2+    (f1, es1) = Misc.mapFst getDC $ splitEApp e1+    (f2, es2) = Misc.mapFst getDC $ splitEApp e2      -- TODO: Stringy hacks     getDC (EVar x)@@ -239,9 +270,9 @@ splitPAnd (PAnd es) = concatMap splitPAnd es splitPAnd e         = [e] ---------------------------- Creating Measure Info-------------------------+--------------------------------------------------------------------------------+-- | Creating Measure Info+-------------------------------------------------------------------------------- -- AT@TODO do this for all reflected functions, not just DataCons  -- Insert measure info for every constructor@@ -251,7 +282,7 @@ assertSelectors γ e = do    EvalEnv _ _ evaenv <- get    let sims = aenvSimpl evaenv-   _ <- foldlM (\_ s -> mapMExpr (go s) e) e sims+   _ <- foldlM (\_ s -> Vis.mapMExpr (go s) e) e sims    return ()   where     go :: Rewrite -> Expr -> EvalST Expr@@ -266,11 +297,11 @@ addSMTEquality :: Knowledge -> Expr -> Expr -> EvalST (IO ()) addSMTEquality γ e1 e2 =   return $ do ctx <- knContext γ-              smtAssert ctx (PAtom Eq (makeLam γ e1) (makeLam γ e2))+              SMT.smtAssert ctx (PAtom Eq (makeLam γ e1) (makeLam γ e2)) ----------------------------------- Symbolic Evaluation with SMT--------------------------------+--------------------------------------------------------------------------------+-- | Symbolic Evaluation with SMT+-------------------------------------------------------------------------------- data EvalEnv = EvalEnv { evId        :: Int                        , evSequence  :: [(Expr,Expr)]                        , _evAEnv     :: AxiomEnv@@ -278,15 +309,15 @@  type EvalST a = StateT EvalEnv IO a -evaluate :: Config -> Context -> [(Symbol, SortedReft)] -> SEnv Sort -> AxiomEnv+evaluate :: Config -> SMT.Context -> [(Symbol, SortedReft)] -> AxiomEnv             -> [Expr]             -> IO [(Expr, Expr)]-evaluate cfg ctx facts fenv aenv einit+evaluate cfg ctx facts aenv einit   = (eqs ++) <$>     (fmap join . sequence)     (evalOne <$> L.nub (grepTopApps =<< einit))   where-    (eqs, γ) = makeKnowledge cfg ctx aenv fenv facts+    (eqs, γ) = makeKnowledge cfg ctx aenv facts     initEvalSt = EvalEnv 0 [] aenv     -- This adds all intermediate unfoldings into the assumptions     -- no test needs it@@ -296,15 +327,18 @@       (e', st) <- runStateT (eval γ e) initEvalSt       if e' == e then return [] else return ((e, e'):evSequence st) +-- Don't evaluate under Lam, App, Ite, or constants grepTopApps :: Expr -> [Expr]-grepTopApps (PAnd es) = concatMap grepTopApps es+grepTopApps (PAnd es)       = concatMap grepTopApps es+grepTopApps (POr es)        = concatMap grepTopApps es grepTopApps (PAtom _ e1 e2) = grepTopApps e1 ++ grepTopApps e2-grepTopApps e@(EApp _ _) = [e]-grepTopApps _ = []--- POr    ![Expr]--- PNot   !Expr--- PImp   !Expr !Expr--- PIff   !Expr !Expr+grepTopApps (PIff e1 e2)    = grepTopApps e1 ++ grepTopApps e2+grepTopApps (PImp e1 e2)    = grepTopApps e1 ++ grepTopApps e2+grepTopApps (PNot e)        = grepTopApps e+grepTopApps (EBin  _ e1 e2) = grepTopApps e1 ++ grepTopApps e2+grepTopApps (ENeg e)        = grepTopApps e+grepTopApps e@(EApp _ _)    = [e]+grepTopApps _               = []  -- AT: I think makeLam is the adjoint of splitEApp? makeLam :: Knowledge -> Expr -> Expr@@ -312,11 +346,16 @@  eval :: Knowledge -> Expr -> EvalST Expr eval γ e | Just e' <- lookupKnowledge γ e-   = (e, "Knowledge") ~> e'+  = (e, "Knowledge") ~> e' eval γ (ELam (x,s) e)-  = do let x' = makeLamArg s (1+ length (knLams γ))-       e'    <- eval γ{knLams = (x',s):knLams γ} (subst1 e (x, EVar x'))-       return $ ELam (x,s) $ subst1 e' (x', EVar x)+  -- SHIFTLAM (assuming this shifting is redundant if DEFUNC has already happened)+  -- = do let x' = lamArgSymbol (1 + length (knLams γ))+       -- e'    <- eval γ{knLams = (x',s):knLams γ} (subst1 e (x, EVar x'))+       -- return $ ELam (x,s) $ subst1 e' (x', EVar x)++  = do e'    <- eval γ{knLams = (x, s) : knLams γ} e+       return $ ELam (x, s) e'+ eval γ e@(EIte b e1 e2)   = do b' <- eval γ b        evalIte γ e b' e1 e2@@ -508,14 +547,14 @@  makeInitOccurences :: [(Symbol, Fuel)] -> [Equation] -> Expr -> [Occurence] makeInitOccurences xs eqs e-  = [Occ x es xs | (EVar x, es) <- splitEApp <$> eapps e+  = [Occ x es xs | (EVar x, es) <- splitEApp <$> Vis.eapps e                  , Equ x' xs' _ <- eqs, x == x'                  , length xs' == length es]  grepOccurences :: [Equation] -> (Expr, FuelMap) -> [Occurence] grepOccurences eqs (e, fs)   = filter (goodFuelMap . ofuel)-           [Occ x es fs | (EVar x, es) <- splitEApp <$> eapps e+           [Occ x es fs | (EVar x, es) <- splitEApp <$> Vis.eapps e                         , Equ x' xs' _ <- eqs, x == x'                         , length xs' == length es] 

@@ -31,20 +31,19 @@ import           Control.DeepSeq import           GHC.Generics import           Language.Fixpoint.Utils.Progress-import           Language.Fixpoint.Misc    (mapSnd, groupList) import qualified Language.Fixpoint.Types.Config  as C import           Language.Fixpoint.Types.Config  (Config) import qualified Language.Fixpoint.Types   as F+-- import qualified Language.Fixpoint.Misc    as Misc+-- import           Language.Fixpoint.SortCheck import qualified Language.Fixpoint.Types.Solutions as F import           Language.Fixpoint.Types   (pprint) -- import qualified Language.Fixpoint.Types.Errors  as E-import qualified Language.Fixpoint.Smt.Theories as Thy-import           Language.Fixpoint.Smt.Types (tsInterp) import           Language.Fixpoint.Smt.Serialize () import           Language.Fixpoint.Types.PrettyPrint () import           Language.Fixpoint.Smt.Interface+-- import qualified Language.Fixpoint.Smt.Theories as Thy import           Language.Fixpoint.Solver.Sanitize-import           Language.Fixpoint.SortCheck import           Language.Fixpoint.Graph.Types (SolverInfo (..)) -- import           Language.Fixpoint.Solver.Solution -- import           Data.Maybe           (catMaybes)@@ -91,21 +90,21 @@                         ]  ---------------------------------------------------------------------------------runSolverM :: Config -> SolverInfo b c -> Int -> SolveM a -> IO a+runSolverM :: Config -> SolverInfo b c -> SolveM a -> IO a ---------------------------------------------------------------------------------runSolverM cfg sI _ act =+runSolverM cfg sI act =   bracket acquire release $ \ctx -> do     res <- runStateT act' (s0 ctx)     smtWrite ctx "(exit)"-    return $ fst res+    return (fst res)   where     s0 ctx   = SS ctx be (stats0 fi)-    act'     = declare initEnv lts {- ess -} >> assumesAxioms (F.asserts fi) >> act+    act'     = {- declare initEnv >> -} assumesAxioms (F.asserts fi) >> act     release  = cleanupContext     acquire  = makeContextWithSEnv cfg file initEnv     initEnv  = symbolEnv   cfg fi-    lts      = F.toListSEnv (F.dLits fi)-    -- ess   = distinctLiterals fi+    -- lts      = F.toListSEnv (F.dLits fi)+    -- ds       = F.ddecls fi     be       = F.SolEnv (F.bs fi)     file     = C.srcFile cfg     -- only linear arithmentic when: linear flag is on or solver /= Z3@@ -113,7 +112,6 @@     fi       = (siQuery sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)}  - -------------------------------------------------------------------------------- getBinds :: SolveM F.SolEnv --------------------------------------------------------------------------------@@ -177,23 +175,23 @@ -------------------------------------------------------------------------------- -- | `filterValid p [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]` ---------------------------------------------------------------------------------filterValid :: F.Expr -> F.Cand a -> SolveM [a]+filterValid :: F.SrcSpan -> F.Expr -> F.Cand a -> SolveM [a] ---------------------------------------------------------------------------------filterValid p qs = do+filterValid sp p qs = do   qs' <- withContext $ \me ->            smtBracket me "filterValidLHS" $-             filterValid_ p qs me+             filterValid_ sp p qs me   -- stats   incBrkt   incChck (length qs)   incVald (length qs')   return qs' -filterValid_ :: F.Expr -> F.Cand a -> Context -> IO [a]-filterValid_ p qs me = catMaybes <$> do+filterValid_ :: F.SrcSpan -> F.Expr -> F.Cand a -> Context -> IO [a]+filterValid_ sp p qs me = catMaybes <$> do   smtAssert me p   forM qs $ \(q, x) ->-    smtBracket me "filterValidRHS" $ do+    smtBracketAt sp me "filterValidRHS" $ do       smtAssert me (F.PNot q)       valid <- smtCheckUnsat me       return $ if valid then Just x else Nothing@@ -202,7 +200,7 @@  -------------------------------------------------------------------------------- -- | `filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`--- | for some p in the list ps +-- | for some p in the list ps -------------------------------------------------------------------------------- filterValidGradual :: [F.Expr] -> F.Cand a -> SolveM [a] --------------------------------------------------------------------------------@@ -217,12 +215,12 @@   return qs'  filterValidGradual_ :: [F.Expr] -> F.Cand a -> Context -> IO [a]-filterValidGradual_ ps qs me +filterValidGradual_ ps qs me   = (map snd . fst) <$> foldM partitionCandidates ([], qs) ps   where     partitionCandidates :: (F.Cand a, F.Cand a) -> F.Expr -> IO (F.Cand a, F.Cand a)-    partitionCandidates (ok, candidates) p = do -      (valids', invalids')  <- partition snd <$> filterValidOne_ p candidates me +    partitionCandidates (ok, candidates) p = do+      (valids', invalids')  <- partition snd <$> filterValidOne_ p candidates me       let (valids, invalids) = (fst <$> valids', fst <$> invalids')       return (ok ++ valids, invalids) @@ -249,49 +247,10 @@         smtCheckSat me p  ---------------------------------------------------------------------------------declare :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)] -> SolveM ()----------------------------------------------------------------------------------declare env lts = withContext $ \me -> do-  forM_ thyXTs $ uncurry $ smtDecl     me-  forM_ qryXTs $ uncurry $ smtDecl     me-  forM_ ess    $           smtDistinct me-  forM_ axs    $           smtAssert   me-  return ()-  where-    ess        = distinctLiterals  lts-    axs        = Thy.axiomLiterals lts-    thyXTs     =               filter (isKind 1) xts-    qryXTs     = mapSnd tx <$> filter (isKind 2) xts-    isKind n   = (n ==)  . symKind . fst-    xts        = F.toListSEnv           env-    tx         = elaborate    "declare" env---- | symKind returns {0, 1, 2} where:---   0 = Theory-Definition,---   1 = Theory-Declaration,---   2 = Query-Binder--symKind :: F.Symbol -> Int-symKind x = case M.lookup x Thy.theorySymbols of-              Just t  -> if tsInterp t then 0 else 1-              Nothing -> 2- assumesAxioms :: [F.Triggered F.Expr] -> SolveM ()+-------------------------------------------------------------------------------- assumesAxioms es = withContext $ \me -> forM_  es $ smtAssertAxiom me --- assumes :: [F.Expr] -> SolveM ()--- assumes es = withContext $ \me -> forM_  es $ smtAssert me---- | `distinctLiterals` is used solely to determine the set of literals---   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,---   or string literals "cat", "dog", "mouse". These should only include---   non-function sorted values.-distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]-distinctLiterals xts = [ es | (_, es) <- tess ]-   where-    tess             = groupList [(t, F.expr x) | (x, t) <- xts, notFun t]-    notFun           = not . F.isFunctionSortedReft . (`F.RR` F.trueReft)-    -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)  --------------------------------------------------------------------------- stats :: SolveM Stats

@@ -16,7 +16,7 @@  import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Visitor (symConsts, isConcC, isKvarC, mapKVars, mapKVarSubsts)-import           Language.Fixpoint.SortCheck     (isFirstOrder)+import           Language.Fixpoint.SortCheck     (applySorts, isFirstOrder) import qualified Language.Fixpoint.Misc                            as Misc import qualified Language.Fixpoint.Types                           as F import           Language.Fixpoint.Types.Config (Config, allowHO)@@ -208,18 +208,25 @@ banConstraintFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a) banConstraintFreeVars fi0 = Misc.applyNonNull (Right fi0) (Left . badCs) bads   where-    fi = mapKVars (const $ Just F.PTrue) fi0-    bads = [(c, fs) | c <- M.elems $ F.cm fi, Just fs <- [cNoFreeVars fi c]]+    fi      = mapKVars (const $ Just F.PTrue) fi0+    bads    = [(c, fs) | c <- M.elems $ F.cm fi, Just fs <- [cNoFreeVars fi k c]]+    k       = known fi -cNoFreeVars :: F.SInfo a -> F.SimpC a -> Maybe [F.Symbol]-cNoFreeVars fi c = if S.null fv then Nothing else Just (S.toList fv)+known :: F.SInfo a -> F.Symbol -> Bool+known fi  = \x -> F.memberSEnv x lits || F.memberSEnv x prims   where+    lits  = F.gLits fi+    prims = Thy.theorySymbols . F.ddecls $ fi++cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol]+cNoFreeVars fi known c = if S.null fv then Nothing else Just (S.toList fv)+  where     be   = F.bs fi-    lits = fst <$> F.toListSEnv (F.gLits fi)+    -- lits = fst <$> F.toListSEnv (F.gLits fi)     ids  = F.elemsIBindEnv $ F.senv c     cDom = [fst $ F.lookupBindEnv i be | i <- ids]     cRng = concat [S.toList . F.reftFreeVars . F.sr_reft . snd $ F.lookupBindEnv i be | i <- ids]-    fv   = cRng `nubDiff` (lits ++ cDom ++ F.prims)+    fv   = (`nubDiff` cDom) . filter (not . known) $ cRng -- `nubDiff` (lits ++ cDom ++ prims fi)  badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error badCs = E.catErrors . map (E.errFreeVarInConstraint . Misc.mapFst F.subcId)@@ -266,12 +273,19 @@                                           , nest 4 (pprint (F.crhs c)) ]  ----------------------------------------------------------------------------------- | symbol |-> sort for EVERY variable in the FInfo+-- | symbol |-> sort for EVERY variable in the SInfo; 'symbolEnv' can ONLY be+--   called with **sanitized** environments (post the uniqification etc.) or+--   else you get duplicate sorts and other such errors. ---------------------------------------------------------------------------------symbolEnv :: Config -> F.SInfo a -> F.SEnv F.Sort-symbolEnv cfg si = Thy.theorySEnv-                   `mappend`-                   F.fromListSEnv (symbolSorts cfg si)+symbolEnv :: Config -> F.SInfo a -> F.SymEnv+symbolEnv cfg si = F.symEnv sEnv tEnv ds (F.dLits si) ts+  where+    tEnv         = Thy.theorySymbols ds+    ds           = F.ddecls si+    ts           = Misc.hashNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])+    sEnv         = (F.tsSort <$> tEnv) `mappend` (F.fromListSEnv xts)+    xts          = symbolSorts cfg si+  symbolSorts :: Config -> F.GInfo c a -> [(F.Symbol, F.Sort)] symbolSorts cfg fi = either E.die id $ symbolSorts' cfg fi

@@ -23,7 +23,7 @@ import           Language.Fixpoint.Types.Visitor      as V import qualified Language.Fixpoint.SortCheck          as So import           Language.Fixpoint.Misc-import qualified Language.Fixpoint.Smt.Theories       as Thy+-- import qualified Language.Fixpoint.Smt.Theories       as Thy import           Language.Fixpoint.Types.Config import qualified Language.Fixpoint.Types              as F import           Language.Fixpoint.Types                 ((&.&))@@ -164,14 +164,14 @@     be              = F.soeBinds (snd3 g)  applyKVars :: CombinedEnv -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ExprInfo-applyKVars g s = mrExprInfos (applyKVar g s) F.pAnd mconcat +applyKVars g s = mrExprInfos (applyKVar g s) F.pAnd mconcat  applyKVar :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo applyKVar g s ksu = case Sol.lookup s (F.ksuKVar ksu) of   Left cs          -> hypPred g s ksu cs   Right eqs -> (F.pAnd $ fst <$> Sol.qbPreds msg s (F.ksuSubst ksu) eqs, mempty) -- TODO: don't initialize kvars that have a hyp solution   where-    msg     = "applyKVar: " ++ show (fst3 g) +    msg     = "applyKVar: " ++ show (fst3 g)  hypPred :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo hypPred g s ksu = mrExprInfos (cubePred g s ksu) F.pOr mconcatPlus@@ -221,13 +221,13 @@     yts'            = symSorts g bs'     g'              = addCEnv  g bs     (p', kI)        = apply g' s bs'-    (_  , psu')     = substElim sEnv g' k su'-    (xts, psu)      = substElim sEnv g  k su+    (_  , psu')     = substElim (Sol.sEnv s) sEnv g' k su'+    (xts, psu)      = substElim (Sol.sEnv s) sEnv g  k su     su'             = Sol.cuSubst c     bs              = Sol.cuBinds c     k               = F.ksuKVar   ksu     su              = F.ksuSubst  ksu-    sEnv            = F.insertSEnv (F.ksuVV ksu) (F.ksuSort ksu) (Sol.sEnv s)+    sEnv            = F.insertSEnv (F.ksuVV ksu) (F.ksuSort ksu) (F.seSort $ Sol.sEnv s)  -- TODO: SUPER SLOW! Decorate all substitutions with Sorts in a SINGLE pass. @@ -255,10 +255,10 @@      2. are binders corresponding to sorts (e.g. `a : num`, currently used         to hack typeclasses current.)  -}-substElim :: F.SEnv F.Sort -> CombinedEnv -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)-substElim sEnv g _ (F.Su m) = (xts, p)+substElim :: F.SymEnv -> F.SEnv F.Sort -> CombinedEnv -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)+substElim syEnv sEnv g _ (F.Su m) = (xts, p)   where-    p      = F.pAnd [ mkSubst x (substSort sEnv frees x t) e t | (x, e, t) <- xets  ]+    p      = F.pAnd [ mkSubst syEnv x (substSort sEnv frees x t) e t | (x, e, t) <- xets  ]     xts    = [ (x, t)    | (x, _, t) <- xets, not (S.member x frees) ]     xets   = [ (x, e, t) | (x, e)    <- xes, t <- sortOf e, not (isClass t)]     xes    = M.toList m@@ -271,15 +271,18 @@   where     err x            = error $ "Solution.mkSubst: unknown binder " ++ F.showpp x -mkSubst :: F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr-mkSubst x tx ey ty+mkSubst :: F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr+mkSubst env x tx ey ty   | tx == ty    = F.EEq ex ey-  | otherwise   = F.notracepp msg (F.EEq ex' ey')+  | otherwise   = {- F.tracepp _msg -} (F.EEq ex' ey')   where-    msg         = "mkSubst-DIFF:" ++ F.showpp (tx, ty) ++ F.showpp (ex', ey')+    _msg         = "mkSubst-DIFF:" ++ F.showpp (tx, ty) ++ F.showpp (ex', ey')     ex          = F.expr x-    ex'         = Thy.toInt ex tx-    ey'         = Thy.toInt ey ty+    ex'         = elabToInt env ex tx+    ey'         = elabToInt env ey ty++elabToInt :: F.SymEnv -> F.Expr -> F.Sort -> F.Expr+elabToInt env e s = So.elaborate "elabToInt" env (So.toInt env e s)  isClass :: F.Sort -> Bool isClass F.FNum  = True

@@ -1,6 +1,7 @@ {-# LANGUAGE PatternGuards     #-} {-# LANGUAGE TupleSections     #-} {-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}  --------------------------------------------------------------------------------@@ -14,34 +15,39 @@ import           Language.Fixpoint.Misc import qualified Language.Fixpoint.Types           as F import qualified Language.Fixpoint.Types.Solutions as Sol+import qualified Language.Fixpoint.Types.Graduals  as G+import qualified Language.Fixpoint.Solver.GradualSolution as GS import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Config hiding (stats) import qualified Language.Fixpoint.Solver.Solution  as S import qualified Language.Fixpoint.Solver.Worklist  as W import qualified Language.Fixpoint.Solver.Eliminate as E import           Language.Fixpoint.Solver.Monad-import           Language.Fixpoint.Solver.GradualSolve import           Language.Fixpoint.Utils.Progress import           Language.Fixpoint.Graph import           Text.PrettyPrint.HughesPJ import           Text.Printf-import           System.Console.CmdArgs.Verbosity (whenNormal, whenLoud)+import           System.Console.CmdArgs.Verbosity -- (whenNormal, whenLoud) import           Control.DeepSeq import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S+import qualified Data.List as L+import Control.Concurrent.ParallelIO.Global (parallel) +import qualified Language.Fixpoint.SortCheck       as So+import Language.Fixpoint.Solver.Sanitize (symbolEnv) -- DEBUG -- import           Debug.Trace (trace)  ---------------------------------------------------------------------------------solve :: (NFData a, F.Fixpoint a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))+solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a)) ---------------------------------------------------------------------------------solve cfg fi | gradual cfg -  = solveGradual cfg fi +solve cfg fi | gradual cfg+ = solveGradual cfg fi  solve cfg fi = do     -- donePhase Loud "Worklist Initialize"-    (res, stat) <- withProgressFI sI $ runSolverM cfg sI n act+    (res, stat) <- withProgressFI sI $ runSolverM cfg sI act     when (solverStats cfg) $ printStats fi wkl stat     -- print (numIter stat)     return res@@ -49,11 +55,125 @@     act  = solve_ cfg fi s0 ks  wkl     sI   = solverInfo cfg fi     wkl  = W.init sI-    n    = fromIntegral $ W.wRanks wkl     s0   = siSol  sI     ks   = siVars sI + --------------------------------------------------------------------------------+solveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a)+             => Config -> F.SInfo a -> IO (F.Result (Integer, a))+--------------------------------------------------------------------------------+solveGradual cfg fi = do+  -- graphStatistics cfg $ G.uniquify fi+  let fis = zip [1..] $ partition' Nothing $ G.uniquify fi+  if ginteractive cfg+    then snd . traceShow "FINAL SOLUTION\n"  <$> iSolveGradual cfg fis+    else snd . traceShow "FINAL SOLUTION\n" . mconcat <$> parallel (solveGradualOne cfg <$> fis)+++iSolveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> [(Int, F.SInfo a)] -> IO (Maybe G.GSol, F.Result (Integer, a))+iSolveGradual cfg fis+  = mconcat <$> parallel (solveGradualOne cfg <$> fis)+++solveGradualOne :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> (Int, F.SInfo a) -> IO (Maybe G.GSol, F.Result (Integer, a))+solveGradualOne cfg (_, fi) = do+  sols   <- makeSolutions cfg fi+  gradualLoop (cfg{gradual = False}) fi sols++gradualLoop :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> (Maybe [G.GSol]) -> IO (Maybe G.GSol, F.Result (Integer, a))+gradualLoop _ _ Nothing+  = return (Nothing, F.safe)+gradualLoop _ _ (Just [])+  = return (Nothing, F.unsafe)+gradualLoop cfg fi (Just (s:ss))+  = do whenLoud   $ putStrLn ("Solving for " ++ show s)+       whenNormal $ putStr "*"+       v <- getVerbosity+       -- putStr ("Substitution = " ++ show s)+       -- putStr ("BEFORE \n\n"  ++ (show $ F.toFixpoint cfg fi))+       -- putStr ("AFTER \n\n"  ++ (show $ F.toFixpoint cfg $ G.gsubst s fi))+       whenNormal $ setVerbosity Quiet+       r <- solve cfg (G.gsubst s fi)+       setVerbosity v+       whenLoud $ putStrLn ("Solution = " ++ if F.isUnsafe r then "UNSAFE" else "SAFE")+       if F.isUnsafe r+        then gradualLoop cfg fi (Just ss)+        else return (Just s, r)+++makeSolutions :: (NFData a, F.Fixpoint a, Show a) => Config -> F.SInfo a -> IO (Maybe [G.GSol])+makeSolutions cfg fi+  = G.makeSolutions cfg fi <$> makeLocalLattice cfg fi (GS.init fi)++++makeLocalLattice :: Config -> F.SInfo a+                 -> [(F.KVar, (F.GWInfo, [F.Expr]))]+                 -> IO [(F.KVar, (F.GWInfo, [[F.Expr]]))]+makeLocalLattice cfg fi kes = runSolverM cfg sI (act kes)+  where+    sI  = solverInfo cfg fi+    act = mapM (makeLocalLatticeOne cfg fi)+++makeLocalLatticeOne :: Config -> F.SInfo a+            -> (F.KVar, (F.GWInfo, [F.Expr]))+            -> SolveM (F.KVar, (F.GWInfo, [[F.Expr]]))+makeLocalLatticeOne cfg fi (k, (e, es)) = do+   elems0  <- filterM (isLocal e) (map (:[]) es)+   elems   <- sortEquals elems0+   lattice <- makeLattice [] (map (:[]) elems) elems+   return $ ((k,) . (e,)) lattice+  where+    sEnv = symbolEnv cfg fi+    makeLattice acc new elems+      | null new+      = return {- traceShow ("LATTICE FROM ELEMENTS = " ++ showElems elems  ++ showElemss acc) -} acc+      | otherwise+      = do let cands = [e:es | e <- elems, es <- new]+           localCans <- filterM (isLocal e) cands+           newElems  <- filterM (notTrivial (new ++ acc)) localCans+           makeLattice (acc ++ new) newElems elems+    _showElem :: F.Expr -> String+    _showElem e1 = showpp $ F.subst (F.mkSubst [(x, F.EVar $ F.tidySymbol x) | x <- F.syms e1]) e1+    _showElems = unlines . map _showElem+    _showElemss = unlines. map _showElems++    notTrivial [] _     = return True+    notTrivial (x:xs) p = do v <- isValid F.dummySpan (mkPred x) (mkPred p)+                             if v then return False+                                  else notTrivial xs p++    mkPred es = So.elaborate "initBGind.mkPred" sEnv (F.pAnd es)++    isLocal i es = do+      let pp = So.elaborate "filterLocal" sEnv $ F.PExist [(F.gsym i, F.gsort i)] $ F.pAnd (F.gexpr i:es)+      isValid F.dummySpan mempty pp++    root      = mempty+    sortEquals xs = (bfs [0]) <$> makeEdges vs [] vs+      where+       vs        = zip [0..] (root:(head <$> xs))++       bfs []     _  = []+       bfs (i:is) es = (snd $ (vs!!i)) : bfs (is++map snd (filter (\(j,k) ->  (j==i && notElem k is)) es)) es++       makeEdges _   acc []    = return acc+       makeEdges vs acc (x:xs) = do ves  <- concat <$> mapM (makeEdgesOne x) vs+                                    if any (\(i,j) -> elem (j,i) acc) ves+                                      then makeEdges (filter ((/= fst x) . fst) vs) (filter (\(i,j) -> ((i /= fst x) && (j /= fst x))) acc) xs+                                      else makeEdges vs (mergeEdges (ves ++ acc)) xs++    makeEdgesOne (i,_) (j,_) | i == j = return []+    makeEdgesOne (i,x) (j,y) = do+      ij <- isValid F.dummySpan (mkPred [x]) (mkPred [y])+      return (if ij then [(j,i)] else [])++    mergeEdges es = filter (\(i,j) -> (not (any (\k -> ((i,k) `elem` es && (k,j) `elem` es)) (fst <$> es)))) es++--------------------------------------------------------------------------------+ -- | Progress Bar -------------------------------------------------------------------------------- withProgressFI :: SolverInfo a b -> IO b -> IO b@@ -78,7 +198,7 @@ siKvars = S.fromList . M.keys . F.ws  ---------------------------------------------------------------------------------solve_ :: (NFData a, F.Fixpoint a)+solve_ :: (NFData a, F.Fixpoint a, F.Loc a)        => Config        -> F.SInfo a        -> Sol.Solution@@ -86,7 +206,7 @@        -> W.Worklist a        -> SolveM (F.Result (Integer, a), Stats) ---------------------------------------------------------------------------------solve_ cfg fi s0 ks wkl = do +solve_ cfg fi s0 ks wkl = do   let s1  = mappend s0 $ {-# SCC "sol-init" #-} S.init cfg fi ks   s       <- {-# SCC "sol-refine" #-} refine s1 wkl   res     <- {-# SCC "sol-result" #-} result cfg wkl s@@ -108,7 +228,7 @@ tidyPred = F.substf (F.eVar . F.tidySymbol)  ---------------------------------------------------------------------------------refine :: Sol.Solution -> W.Worklist a -> SolveM Sol.Solution+refine :: (F.Loc a) => Sol.Solution -> W.Worklist a -> SolveM Sol.Solution -------------------------------------------------------------------------------- refine s w   | Just (c, w', newScc, rnk) <- W.pop w = do@@ -126,13 +246,14 @@ --------------------------------------------------------------------------- -- | Single Step Refinement ----------------------------------------------- ----------------------------------------------------------------------------refineC :: Int -> Sol.Solution -> F.SimpC a -> SolveM (Bool, Sol.Solution)+refineC :: (F.Loc a) => Int -> Sol.Solution -> F.SimpC a+        -> SolveM (Bool, Sol.Solution) --------------------------------------------------------------------------- refineC _i s c   | null rhs  = return (False, s)   | otherwise = do be     <- getBinds                    let lhs = S.lhsPred be s c-                   kqs    <- filterValid lhs rhs+                   kqs    <- filterValid (cstrSpan c) lhs rhs                    return  $ S.update s ks kqs   where     _ci       = F.subcId c@@ -158,21 +279,21 @@ -------------------------------------------------------------------------------- -- | Convert Solution into Result ---------------------------------------------- ---------------------------------------------------------------------------------result :: (F.Fixpoint a) => Config -> W.Worklist a -> Sol.Solution+result :: (F.Fixpoint a, F.Loc a) => Config -> W.Worklist a -> Sol.Solution        -> SolveM (F.Result (Integer, a)) -------------------------------------------------------------------------------- result cfg wkl s = do   lift $ writeLoud "Computing Result"-  stat    <- result_ wkl s -  lift $ whenNormal $ putStrLn $ "RESULT: " ++ show (F.sid <$> stat)+  stat    <- result_ wkl s+  lift $ whenLoud $ putStrLn $ "RESULT: " ++ show (F.sid <$> stat)   F.Result (ci <$> stat) <$> solResult cfg s <*> return mempty   where     ci c = (F.subcId c, F.sinfo c)  solResult :: Config -> Sol.Solution -> SolveM (M.HashMap F.KVar F.Expr)-solResult cfg = minimizeResult cfg . Sol.result +solResult cfg = minimizeResult cfg . Sol.result -result_ :: W.Worklist a -> Sol.Solution -> SolveM (F.FixResult (F.SimpC a))+result_ :: (F.Loc a) => W.Worklist a -> Sol.Solution -> SolveM (F.FixResult (F.SimpC a)) result_  w s = res <$> filterM (isUnsat s) cs   where     cs       = W.unsatCandidates w@@ -187,7 +308,7 @@ -- --   such that `minimizeConjuncts ps` is a minimal subset of ps where no --   is implied by /\_{q' in qs \ qs}---   see: tests/pos/min00.fq for an example. +--   see: tests/pos/min00.fq for an example. -------------------------------------------------------------------------------- minimizeResult :: Config -> M.HashMap F.KVar F.Expr                -> SolveM (M.HashMap F.KVar F.Expr)@@ -200,12 +321,12 @@ minimizeConjuncts p = F.pAnd <$> go (F.conjuncts p) []   where     go []     acc   = return acc-    go (p:ps) acc   = do b <- isValid (F.pAnd (acc ++ ps)) p+    go (p:ps) acc   = do b <- isValid F.dummySpan (F.pAnd (acc ++ ps)) p                          if b then go ps acc                               else go ps (p:acc)  ---------------------------------------------------------------------------------isUnsat :: Sol.Solution -> F.SimpC a -> SolveM Bool+isUnsat :: (F.Loc a) => Sol.Solution -> F.SimpC a -> SolveM Bool -------------------------------------------------------------------------------- isUnsat s c = do   -- lift   $ printf "isUnsat %s" (show (F.subcId c))@@ -213,7 +334,7 @@   be    <- getBinds   let lp = S.lhsPred be s c   let rp = rhsPred        c-  res   <- not <$> isValid lp rp+  res   <- not <$> isValid (cstrSpan c) lp rp   lift   $ whenLoud $ showUnsat res (F.subcId c) lp rp   return res @@ -232,9 +353,13 @@   | isTarget c = F.crhs c   | otherwise  = errorstar $ "rhsPred on non-target: " ++ show (F.sid c) -isValid :: F.Expr -> F.Expr -> SolveM Bool-isValid p q = (not . null) <$> filterValid p [(q, ())]+--------------------------------------------------------------------------------+isValid :: F.SrcSpan -> F.Expr -> F.Expr -> SolveM Bool+--------------------------------------------------------------------------------+isValid sp p q = (not . null) <$> filterValid sp p [(q, ())] +cstrSpan :: (F.Loc a) => F.SimpC a -> F.SrcSpan+cstrSpan = F.srcSpan . F.sinfo  {- ---------------------------------------------------------------------------@@ -245,3 +370,49 @@   putBlankLn   donePhase Loud msg -}+++-- NV TODO Move to a new file+-------------------------------------------------------------------------------+-- | Interaction with the user when Solving -----------------------------------+-------------------------------------------------------------------------------++_iMergePartitions :: [(Int, F.SInfo a)] -> IO [(Int, F.SInfo a)]+_iMergePartitions ifis = do+  putStrLn "Current Partitions are: "+  putStrLn $ unlines (partitionInfo <$> ifis)+  putStrLn "Merge Partitions? Y/N"+  c <- getChar+  if c == 'N'+    then do putStrLn "Solving Partitions"+            return ifis+    else do+      (i, j) <- getMergePartition (length ifis)+      _iMergePartitions (mergePartitions i j ifis)++getMergePartition :: Int -> IO (Int, Int)+getMergePartition n = do+  putStrLn "Which two partition to merge? (i, j)"+  ic <- getLine+  let (i,j) = read ic :: (Int, Int)+  if i < 1 || n < i || j < 1 || n < j+    then do putStrLn ("Invalid Partition numbers, write (i,j) with 1 <= i <= " ++ show n)+            getMergePartition n+    else return (i,j)++mergePartitions :: Int -> Int -> [(Int, F.SInfo a)] -> [(Int, F.SInfo a)]+mergePartitions i j fis+  = zip [1..] ((takei i `mappend` (takei j){F.bs = mempty}):rest)+  where+    takei i = snd (fis L.!! (i - 1))+    rest = snd <$> filter (\(k,_) -> (k /= i && k /= j)) fis++partitionInfo :: (Int, F.SInfo a) -> String+partitionInfo (i, fi)+  = "Partition number " ++ show i ++ "\n" +++    "Defined ?? " ++ show defs    ++ "\n" +++    "Used ?? "    ++ show uses+  where+    gs   = F.wloc . snd <$> L.filter (F.isGWfc . snd) (M.toList (F.ws fi))+    defs = L.nub (F.gsrc <$> gs)+    uses = L.nub (F.gused <$> gs)

@@ -1,3 +1,5 @@+{-# LANGUAGE Strict                #-}+{-# LANGUAGE StrictData            #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE TypeSynonymInstances  #-} {-# LANGUAGE FlexibleInstances     #-}@@ -5,6 +7,7 @@ {-# LANGUAGE TupleSections         #-} {-# LANGUAGE OverloadedStrings     #-} {-# LANGUAGE PatternGuards         #-}+{-# LANGUAGE BangPatterns          #-}  -- | This module has the functions that perform sort-checking, and related -- operations on Fixpoint expressions and predicates.@@ -39,15 +42,20 @@    -- * Sort-Directed Transformations   , Elaborate (..)+  , applySorts+  , unApplyAt+  , toInt    -- * Predicates on Sorts   , isFirstOrder   , isMono   ) where -+--  import           Control.DeepSeq import           Control.Monad-import           Control.Monad.Except      (MonadError(..))+import           Control.Monad.Except      -- (MonadError(..))+import           Control.Monad.State.Strict+ import qualified Data.HashMap.Strict       as M import qualified Data.List                 as L import           Data.Maybe                (mapMaybe, fromMaybe)@@ -55,8 +63,9 @@ import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Misc import           Language.Fixpoint.Types hiding   (subst)-import           Language.Fixpoint.Types.Visitor  (mapExpr, stripCasts, foldSort)+import qualified Language.Fixpoint.Types.Visitor  as Vis import qualified Language.Fixpoint.Smt.Theories   as Thy+-- import qualified Language.Fixpoint.Smt.Types      as Thy import           Text.PrettyPrint.HughesPJ import           Text.Printf @@ -67,7 +76,7 @@ -------------------------------------------------------------------------------- isMono :: Sort -> Bool ---------------------------------------------------------------------------------isMono             = null . foldSort fv []+isMono             = null . Vis.foldSort fv []   where     fv vs (FVar i) = i : vs     fv vs _        = vs@@ -77,11 +86,11 @@ -- | Elaborate: make polymorphic instantiation explicit via casts, --   make applications monomorphic for SMTLIB. This deals with --   polymorphism by `elaborate`-ing all refinements except for---   KVars. THIS IS NOW MANDATORY as sort-variables can be instantiated---   to `int` and `bool`.+--   KVars. THIS IS NOW MANDATORY as sort-variables can be+--   instantiated to `int` and `bool`. -------------------------------------------------------------------------------- class Elaborate a where-  elaborate :: String -> SEnv Sort -> a -> a+  elaborate :: String -> SymEnv -> a -> a  instance Elaborate (SInfo a) where   elaborate x senv si = si@@ -93,6 +102,9 @@ instance (Elaborate e) => (Elaborate (Triggered e)) where   elaborate x env t = fmap (elaborate x env) t +instance (Elaborate a) => (Elaborate (Maybe a)) where+  elaborate x env t = fmap (elaborate x env) t+ instance Elaborate Sort where   elaborate _ _ = go    where@@ -105,16 +117,16 @@       funSort = FApp . FApp funcSort  instance Elaborate Expr where-  elaborate msg env = elabNumeric . elabApply . elabExpr msg env+    elaborate msg env = elabNumeric . elabApply env . elabExpr msg env  instance Elaborate (Symbol, Sort) where-  elaborate msg env (x, s) = (x,) (elaborate msg env s)+  elaborate msg env (x, s) = (x, elaborate msg env s)  instance Elaborate a => Elaborate [a]  where   elaborate msg env xs = elaborate msg env <$> xs  elabNumeric :: Expr -> Expr-elabNumeric = mapExpr go+elabNumeric = Vis.mapExpr go   where     go (ETimes e1 e2)       | exprSort "txn1" e1 == FReal@@ -131,7 +143,7 @@   elaborate x env (RR s (Reft (v, e))) = RR s (Reft (v, e'))     where       e'   = elaborate x env' e-      env' = insertSEnv v s env+      env' = insertSymEnv v s env  instance Elaborate BindEnv where   elaborate z env = mapBindEnv (\i (x, sr) -> (x, elaborate (z ++ msg i x sr) env sr))@@ -146,28 +158,29 @@                       -- , qBody   = elaborate [env ++ qParams] (qBody q)                       -- } -elabExpr :: String -> SEnv Sort -> Expr -> Expr-elabExpr msg γ e-  = case runCM0 $ elab f e of+elabExpr :: String -> SymEnv -> Expr -> Expr+elabExpr msg env e+  = case runCM0 $ elab (env, f) e of       Left msg -> die $ err dummySpan (d msg)       Right s  -> fst s     where-      f   = (`lookupSEnvWithDistance` γ')-      γ'  = γ `mappend` Thy.theorySEnv-      d m = vcat [ "elaborate" <+> text msg <+> "failed on:"+      sEnv = seSort env+      f    = (`lookupSEnvWithDistance` sEnv)+      -- γ'  = γ `mappend` (Thy.tsSort <$> Thy.theorySymbols)+      d m  = vcat [ "elaborate" <+> text msg <+> "failed on:"                  , nest 4 (pprint e)                  , "with error"                  , nest 4 (text m)                  , "in environment"-                 , nest 4 (pprint $ subEnv γ' e)+                 , nest 4 (pprint $ subEnv sEnv e)                  ] -elabApply :: Expr -> Expr-elabApply = go+elabApply :: SymEnv -> Expr -> Expr+elabApply env = go   where     go e                  = case splitArgs e of                              (e', []) -> step e'-                             (f , es) -> defuncEApp (go f) (mapFst go <$> es)+                             (f , es) -> defuncEApp env (go f) (mapFst go <$> es)     step (PAnd [])        = PTrue     step (POr [])         = PFalse     step (ENeg e)         = ENeg (go  e)@@ -184,7 +197,7 @@     step (PAtom r e1 e2)  = PAtom r (go e1) (go e2)     step e@(EApp {})      = go e     step (ELam b e)       = ELam b (go e)-    step (PGrad k su e)   = PGrad k su (go e)+    step (PGrad k su i e) = PGrad k su i (go e)     step e@(PKVar {})     = e     step e@(ESym {})      = e     step e@(ECon {})      = e@@ -228,60 +241,42 @@ -- | Checking Refinements ------------------------------------------------------ -------------------------------------------------------------------------------- +-- RJ: why are we handrolling monads! -- | Types used throughout checker -type StateM = Int--newtype CheckM a = CM {runCM :: StateM -> (StateM, Either String a)}+-- newtype CheckM a = CM {runCM :: StateM -> (StateM, Either String a)}+-- type CheckM   = ExceptT ChError (State ChState)+type CheckM   = StateT ChState (Either ChError)+type ChError  = String+type ChState  = Int  type Env      = Symbol -> SESearch Sort---instance Monad CheckM where-  return x     = CM $ \i -> (i, Right x)-  (CM m) >>= f = CM $ \i -> case m i of-                             (j, Left s)  -> (j, Left s)-                             (j, Right x) -> runCM (f x) j---instance MonadError String CheckM where-  throwError s = CM $ \i -> (i, Left s)-  (CM m) `catchError` f = CM $ \i -> case m i of-                                      (j, Left s) -> runCM (f s) j-                                      (j, Right x) -> (j, Right x)+type ElabEnv  = (SymEnv, Env)  withError :: CheckM a -> String -> CheckM a act `withError` e' = act `catchError` (\e -> throwError (e ++ "\n  because\n" ++ e')) -instance Functor CheckM where-  fmap f (CM m) = CM $ \i -> case m i of {(j, Left s) -> (j, Left s); (j, Right x) -> (j, Right $ f x)}--instance Applicative CheckM where-  pure x     = CM $ \i -> (i, Right x)-  (CM f) <*> (CM m) = CM $ \i -> case m i of-                             (j, Left s)  -> (j, Left s)-                             (_, Right x) -> case f i of-                                 (k, Left s)  -> (k, Left s)-                                 (k, Right g) -> (k, Right $ g x)--initCM :: StateM-initCM = 42- runCM0 :: CheckM a -> Either String a-runCM0 act = snd $ runCM act initCM+-- runCM0 act = snd $ runCM act initCM+runCM0 act = fst <$> runStateT act initCM -- :: Either ChError (a, ChState)+  where+    initCM = 42 -class Freshable a where-  fresh   :: CheckM a-  refresh :: a -> CheckM a-  refresh _ = fresh -instance Freshable Int where-  fresh = CM (\n -> (n+1, Right n))+-- class Freshable a where+--  fresh   :: CheckM a+--  refresh :: a -> CheckM a+--  refresh _ = fresh -instance Freshable [Int] where-  fresh   = mapM (const fresh) [0..]-  refresh = mapM refresh+-- instance Freshable Int where +fresh :: CheckM Int+fresh = do+  !n <- get+  put (n + 1)+  return n+    -- CM (\n -> (n + 1, Right n))+ -------------------------------------------------------------------------------- -- | Checking Refinements ------------------------------------------------------ --------------------------------------------------------------------------------@@ -369,7 +364,7 @@ checkExpr f (POr ps)       = mapM_ (checkPred f) ps >> return boolSort checkExpr f (PAtom r e e') = checkRel f r e e' >> return boolSort checkExpr _ (PKVar {})     = return boolSort-checkExpr f (PGrad _ _ e)  = checkPred f e >> return boolSort+checkExpr f (PGrad _ _ _ e)  = checkPred f e >> return boolSort  checkExpr f (PAll  bs e )  = checkExpr (addEnv f bs) e checkExpr f (PExist bs e)  = checkExpr (addEnv f bs) e@@ -386,17 +381,17 @@ -------------------------------------------------------------------------------- -- | Elaborate expressions with types to make polymorphic instantiation explicit. ---------------------------------------------------------------------------------elab :: Env -> Expr -> CheckM (Expr, Sort)+elab :: ElabEnv -> Expr -> CheckM (Expr, Sort) ---------------------------------------------------------------------------------elab f e@(EBin o e1 e2) = do+elab f@(_, g) e@(EBin o e1 e2) = do   (e1', s1) <- elab f e1   (e2', s2) <- elab f e2-  s         <- checkExpr f e+  s <- checkOpTy g e s1 s2   return (EBin o (ECst e1' s1) (ECst e2' s2), s)  elab f (EApp e1@(EApp _ _) e2) = do   (e1', _, e2', s2, s) <- elabEApp f e1 e2-  return (eAppC s e1' (ECst e2' s2), s)+  return (eAppC s e1'          (ECst e2' s2), s)  elab f (EApp e1 e2) = do   (e1', s1, e2', s2, s) <- elabEApp f e1 e2@@ -417,22 +412,22 @@ elab _ e@(PKVar _ _) =   return (e, boolSort) -elab f (PGrad k su e) = -  ((, boolSort) . PGrad k su . fst) <$> elab f e +elab f (PGrad k su i e) =+  ((, boolSort) . PGrad k su i . fst) <$> elab f e -elab f e@(EVar x) =+elab (_, f) e@(EVar x) =   (e,) <$> checkSym f x  elab f (ENeg e) = do   (e', s) <- elab f e   return (ENeg e', s) -elab f (EIte p e1 e2) = do-  (p', _)  <- elab f p-  (e1', _) <- elab f e1-  (e2', _) <- elab f e2-  s <- checkIte f p e1 e2-  return (EIte p' e1' e2', s)+elab f@(_,g) (EIte p e1 e2) = do+  (p', _)   <- elab f p+  (e1', s1) <- elab f e1+  (e2', s2) <- elab f e2+  s         <- checkIteTy g p e1' e2' s1 s2+  return (EIte p' (cast e1' s) (cast e2' s), s)  elab f (ECst e t) = do   (e', _) <- elab f e@@ -460,13 +455,13 @@   ps' <- mapM (elab f) ps   return (POr (fst <$> ps'), boolSort) -elab f e@(PAtom Eq e1 e2) = do-  t1        <- checkExpr f e1-  t2        <- checkExpr f e2-  (t1',t2') <- unite f e  t1 t2 `withError` (errElabExpr e)+elab f@(_,g) e@(PAtom Eq e1 e2) = do+  t1        <- checkExpr g e1+  t2        <- checkExpr g e2+  (t1',t2') <- unite g e  t1 t2 `withError` (errElabExpr e)   e1'       <- elabAs f t1' e1   e2'       <- elabAs f t2' e2-  return (PAtom Eq (ECst e1' t1') (ECst e2' t2'), boolSort)+  return (PAtom Eq (ECst e1' t1') (ECst e2' t2') , boolSort)  elab f (PAtom r e1 e2)   | r == Ueq || r == Une = do@@ -474,109 +469,175 @@   (e2', _) <- elab f e2   return (PAtom r e1' e2', boolSort) -elab f (PAtom r e1 e2) = do-  e1' <- uncurry Thy.toInt <$> elab f e1-  e2' <- uncurry Thy.toInt <$> elab f e2+elab f@(env, _) (PAtom r e1 e2) = do+  e1' <- uncurry (toInt env) <$> elab f e1+  e2' <- uncurry (toInt env) <$> elab f e2   return (PAtom r e1' e2', boolSort)  elab f (PExist bs e) = do-  (e', s) <- elab (addEnv f bs) e+  (e', s) <- elab (elabAddEnv f bs) e   let bs' = elaborate "PExist Args" mempty bs   return (PExist bs' e', s)  elab f (PAll bs e) = do-  (e', s) <- elab (addEnv f bs) e+  (e', s) <- elab (elabAddEnv f bs) e   let bs' = elaborate "PAll Args" mempty bs   return (PAll bs' e', s)  elab f (ELam (x,t) e) = do-  (e', s) <- elab (addEnv f [(x,t)]) e+  (e', s) <- elab (elabAddEnv f [(x, t)]) e   let t' = elaborate "ELam Arg" mempty t-  return (ELam (x,t') (ECst e' s), FFunc t s)+  return (ELam (x, t') (ECst e' s), FFunc t s)  elab _ (ETApp _ _) =   error "SortCheck.elab: TODO: implement ETApp" elab _ (ETAbs _ _) =   error "SortCheck.elab: TODO: implement ETAbs" --- elabAs :: Env -> Sort -> Expr -> CheckM Expr--- elabAs f t e = tracepp msg <$> elabAs' f t e---  where---    msg  = "elabAs: t = " ++ show t ++ " e = " ++ show e+elabAddEnv :: Eq a => (t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)+elabAddEnv (g, f) bs = (g, addEnv f bs) -elabAs :: Env -> Sort -> Expr -> CheckM Expr-elabAs f t (EApp e1 e2) = elabAppAs f t e1 e2-elabAs f _ e            = fst <$> elab f e+cast :: Expr -> Sort -> Expr+cast (ECst e _) t = ECst e t+cast e          t = ECst e t -elabAppAs :: Env -> Sort -> Expr -> Expr -> CheckM Expr-elabAppAs f t g e = do-  gT       <- generalize =<< checkExpr f g+elabAs :: ElabEnv -> Sort -> Expr -> CheckM Expr+elabAs f t e = {- tracepp _msg <$> -} go e+  where+    _msg  = "elabAs: t = " ++ showpp t ++ " e = " ++ showpp e+    go (EApp e1 e2)   = elabAppAs f t e1 e2+    -- go (EIte b e1 e2) = EIte b <$> go e1 <*> go e2+    go e              = fst    <$> elab f e++-- DUPLICATION with `checkApp'`+elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr+elabAppAs env@(_, f) t g e = do+  gT       <- checkExpr f g   eT       <- checkExpr f e   (iT, oT, isu) <- checkFunSort gT   let ge    = Just (EApp g e)   su       <- unifyMany f ge isu [oT, iT] [t, eT]   let tg    = apply su gT-  g'       <- elabAs f tg g+  g'       <- elabAs env tg g   let te    = apply su eT-  e'       <- elabAs f te e+  e'       <- elabAs env te e   return    $ EApp (ECst g' tg) (ECst e' te) -elabEApp  :: Env -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort)-elabEApp f e1 e2 = do-  (e1', s1) <- elab f e1-  (e2', s2) <- elab f e2-  s         <- elabAppSort f e1 e2 s1 s2-  return      (e1', s1, e2', s2, s)+elabEApp  :: ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort)+elabEApp f@(_, g) e1 e2 = do+  (e1', s1)     <- elab f e1+  (e2', s2)     <- elab f e2+  (s1', s2', s) <- elabAppSort g e1 e2 s1 s2+  return           (e1', s1', e2', s2', s) +elabAppSort :: Env -> Expr -> Expr -> Sort -> Sort -> CheckM (Sort, Sort, Sort)+elabAppSort f e1 e2 s1 s2 = do+  let e            = Just (EApp e1 e2)+  (sIn, sOut, su) <- checkFunSort s1+  su'             <- unify1 f e su sIn s2 -- unifyMany f e su [sIn] [s2]+  return           $ (apply su' s1, apply su' s2, apply su' sOut)++ -------------------------------------------------------------------------------- -- | defuncEApp monomorphizes function applications. ---------------------------------------------------------------------------------defuncEApp :: Expr -> [(Expr, Sort)] -> Expr-defuncEApp e es-  | Thy.isSmt2App (stripCasts e) es-  = eApps e (fst <$> es)-  | otherwise-  = L.foldl' makeApplication e es+defuncEApp :: SymEnv -> Expr -> [(Expr, Sort)] -> Expr+defuncEApp env e es = L.foldl' makeApplication e' es'+  where+    (e', es')       = takeArgs (seTheory env) e es --- e1 e2 => App (App runFun e1) (toInt e2)+takeArgs :: SEnv TheorySymbol -> Expr -> [(Expr, a)] -> (Expr, [(Expr, a)])+takeArgs env e es =+  case Thy.isSmt2App env (Vis.stripCasts e) of+    Just n  -> let (es1, es2) = splitAt n es+               in (eApps e (fst <$> es1), es2)+    Nothing -> (e, es)++-- 'e1' is the function, 'e2' is the argument, 's' is the OUTPUT TYPE makeApplication :: Expr -> (Expr, Sort) -> Expr-makeApplication e1 (e2, s) = ECst (EApp (EApp (EVar f) e1) e2') s+makeApplication e1 (e2, s) = ECst (EApp (EApp f e1) e2) s   where-    f                      = makeFunSymbol (spec s)-    e2'                    = Thy.toInt e2 (exprSort "makeApplication" e2)-    -- s                      = fromMaybe (resultType e1 e2) sO-    spec                 :: Sort -> Sort-    spec (FAbs _ s)      = spec s-    spec s               = s+    f                      = applyAt (exprSort "makeAppl" e2) s -makeFunSymbol :: Sort -> Symbol-makeFunSymbol s-  | (FApp (FTC c) _) <- s-  , Thy.isConName setConName c-  = setApplyName 1-  | (FApp (FApp (FTC c) _) _) <- s-  , Thy.isConName mapConName c-  = mapApplyName 1-  | (FApp (FTC bv) (FTC s))   <- s-  , Thy.isConName bitVecName bv-  , Just _ <- Thy.sizeBv s-  = bitVecApplyName 1-  | FTC c <- s, c == boolFTyCon-  = boolApplyName 1-  | s == FReal-  = realApplyName 1-  | otherwise-  = intApplyName 1+applyAt :: Sort -> Sort -> Expr+applyAt s t = ECst (EVar applyName) (FFunc s t) +-- JUST make "toInt" call "makeApplication" also, so they are wrapped in apply+-- MAY CAUSE CRASH (apply-on-apply) so rig `isSmt2App` to treat `apply` as SPECIAL.++-- TODO: proper toInt+toInt :: SymEnv -> Expr -> Sort -> Expr+toInt env e s+  | isSmtInt  = e+  | otherwise = ECst (EApp f (ECst e s)) FInt+  where+    isSmtInt  = isInt env s+    f         = toIntAt s++isInt :: SymEnv -> Sort -> Bool+isInt env s = case sortSmtSort False (seData env) s of+  SInt    -> True+  SString -> True+  SReal   -> True+  _       -> False++toIntAt :: Sort -> Expr+toIntAt s = ECst (EVar toIntName) (FFunc s FInt)++unApplyAt :: Expr -> Maybe Sort+unApplyAt (ECst (EVar f) t@(FFunc {}))+  | f == applyName = Just t+unApplyAt _        = Nothing++ splitArgs :: Expr -> (Expr, [(Expr, Sort)]) splitArgs = go []   where     go acc (ECst (EApp e1 e) s) = go ((e, s) : acc) e1+    -- go acc e@(EApp f _)+    --    | Just _ <- unApplyAt f   = (e, acc)     go _   e@EApp{}             = errorstar $ "UNEXPECTED: splitArgs: EApp without output type: " ++ showpp e     -- go acc (ECst e _)           = go acc e     go acc e                    = (e, acc)  --------------------------------------------------------------------------------+{- | [NOTE:apply-monomorphization]++     Because SMTLIB does not support higher-order functions,+     all _non-theory_ function applications++        EApp e1 e2++     are represented, in SMTLIB, as++        (Eapp (EApp apply e1) e2)++     where 'apply' is 'ECst (EVar "apply") t' and+           't'     is 'FFunc a b'+           'a','b' are the sorts of 'e2' and 'e1 e2' respectively.++     Note that *all polymorphism* goes through this machinery.++     Just before sending to the SMT solver, we use the cast 't'+     to generate a special 'apply_at_t' symbol.++     To let us do the above, we populate 'SymEnv' with the _set_+     of all sorts at which 'apply' is used, computed by 'applySorts'.+ -}++--------------------------------------------------------------------------------+applySorts :: Vis.Visitable t => t -> [Sort]+--------------------------------------------------------------------------------+applySorts = {- tracepp "applySorts" . -} (defs ++) . Vis.fold vis () []+  where+    defs   = [FFunc t1 t2 | t1 <- basicSorts, t2 <- basicSorts]+    vis    = (Vis.defaultVisitor :: Vis.Visitor [KVar] t) { Vis.accExpr = go }+    go _ (EApp (ECst (EVar f) t) _)+           | f == applyName+           = [t]+    go _ _ = []++-------------------------------------------------------------------------------- -- | Expressions sort  --------------------------------------------------------- -------------------------------------------------------------------------------- exprSort :: String -> Expr -> Sort@@ -603,7 +664,7 @@ checkSym :: Env -> Symbol -> CheckM Sort checkSym f x   = case f x of-     Found s -> return s+     Found s -> instantiate s      Alts xs -> throwError $ errUnboundAlts x xs  -- | Helper for checking if-then-else expressions@@ -612,9 +673,15 @@   checkPred f p   t1 <- checkExpr f e1   t2 <- checkExpr f e2-  ((`apply` t1) <$> unifys f e' [t1] [t2]) `withError` (errIte e1 e2 t1 t2)+  checkIteTy f p e1 e2 t1 t2++--  ((`apply` t1) <$> unifys f e' [t1] [t2]) `withError` (errIte e1 e2 t1 t2)++checkIteTy :: Env -> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort+checkIteTy f p e1 e2 t1 t2+  = ((`apply` t1) <$> unifys f e' [t1] [t2]) `withError` (errIte e1 e2 t1 t2)   where-    e' = Just (EIte  p e1 e2)+    e' = Just (EIte p e1 e2)  -- | Helper for checking cast expressions checkCst :: Env -> Sort -> Expr -> CheckM Sort@@ -624,17 +691,6 @@   = do t' <- checkExpr f e        ((`apply` t) <$> unifys f (Just e) [t] [t']) `withError` (errCast e t' t) -elabAppSort :: Env -> Expr -> Expr -> Sort -> Sort -> CheckM Sort-elabAppSort f e1 e2 s1 s2 = do-  s1'  <- generalize s1-  let e = Just (EApp e1 e2)-  case s1' of-    FFunc sx s -> (`apply` s) <$> unifys f e [sx] [s2]-    FVar i     -> do j <- refresh 0 -                     k <- refresh 0 -                     (`apply` (FVar k)) <$> unifyMany f e (updateVar i (FFunc (FVar j) (FVar j)) emptySubst) [FVar j] [s2]-    _          -> errorstar ("elabAppSort for expr" ++ showpp (EApp e1 e2) ++ " with sorts" ++ showpp s1  ++ " and " ++ showpp s2 )- checkApp :: Env -> Maybe Sort -> Expr -> Expr -> CheckM Sort checkApp f to g es   = snd <$> checkApp' f to g es@@ -648,42 +704,26 @@        return $ apply θ t  -- | Helper for checking uninterpreted function applications--- | Checking function application should be curried,--- | consider checking+-- | Checking function application should be curried, e.g. -- | fromJust :: Maybe a -> a, f :: Maybe (b -> b), x: c |- fromJust f x+--   RJ: The above comment makes no sense to me :( +-- DUPLICATION with 'elabAppAs' checkApp' :: Env -> Maybe Sort -> Expr -> Expr -> CheckM (TVSubst, Sort) checkApp' f to g e = do-  gt       <- checkExpr f g >>= generalize+  gt       <- checkExpr f g   et       <- checkExpr f e   (it, ot, isu) <- checkFunSort gt   let ge    = Just (EApp g e)-  θ        <- unifyMany f ge isu [it] [et]-  let t     = apply θ ot+  su        <- unifyMany f ge isu [it] [et]+  let t     = apply su ot   case to of-    Nothing    -> return (θ, t)-    Just t'    -> do θ' <- unifyMany f ge θ [t] [t']+    Nothing    -> return (su, t)+    Just t'    -> do θ' <- unifyMany f ge su [t] [t']                      let ti = apply θ' et                      _ <- checkExprAs f ti e                      return (θ', apply θ' t) -{--checkApp' f to g' e-  = do gt           <- checkExpr f g-       gt'          <- generalize gt-       (its, ot)    <- sortFunction (length es) gt'-       ets          <- mapM (checkExpr f) es-       θ            <- unifys f its ets-       let t         = apply θ ot-       case to of-         Nothing    -> return (θ, t)-         Just t'    -> do θ' <- unifyMany f θ [t] [t']-                          let ts = apply θ' <$> ets-                          _ <- zipWithM (checkExprAs f) ts es-                          return (θ', apply θ' t)-  where-    (g, es) = splitEApp $ EApp g' e--}  -- | Helper for checking binary (numeric) operations checkNeg :: Env -> Expr -> CheckM Sort@@ -735,7 +775,6 @@ -------------------------------------------------------------------------------- -- | Checking Predicates ------------------------------------------------------- --------------------------------------------------------------------------------- checkPred                  :: Env -> Expr -> CheckM () checkPred f e = checkExpr f e >>= checkBoolSort e @@ -762,6 +801,7 @@   t2 <- checkExpr f e2   checkRelTy f (PAtom r e1 e2) r t1 t2 + checkRelTy :: Env -> Expr -> Brel -> Sort -> Sort -> CheckM () checkRelTy _ _ Ueq _ _             = return () checkRelTy _ _ Une _ _             = return ()@@ -774,16 +814,10 @@ checkRelTy f _ _ s1    FInt  = checkNumeric    f s1 `withError` (errNonNumeric s1) checkRelTy f _ _ FReal s2    = checkFractional f s2 `withError` (errNonFractional s2) checkRelTy f _ _ s1    FReal = checkFractional f s1 `withError` (errNonFractional s1)---- checkRelTy _ e Eq t1 t2---   | t1 == boolSort || t2 == boolSort = throwError $ errRel e t1 t2--- checkRelTy _ e Ne t1 t2---   | t1 == boolSort || t2 == boolSort = throwError $ errRel e t1 t2--checkRelTy f e Eq t1 t2            = void (unifys f (Just e) [t1] [t2] `withError` (errRel e t1 t2))-checkRelTy f e Ne t1 t2            = void (unifys f (Just e) [t1] [t2] `withError` (errRel e t1 t2))+checkRelTy f e Eq t1 t2      = void (unifys f (Just e) [t1] [t2] `withError` (errRel e t1 t2))+checkRelTy f e Ne t1 t2      = void (unifys f (Just e) [t1] [t2] `withError` (errRel e t1 t2)) -checkRelTy _ e _  t1 t2            = unless (t1 == t2) (throwError $ errRel e t1 t2)+checkRelTy _ e _  t1 t2      = unless (t1 == t2) (throwError $ errRel e t1 t2)  -------------------------------------------------------------------------------- -- | Sort Unification@@ -827,120 +861,137 @@   unify1 :: Env -> Maybe Expr -> TVSubst -> Sort -> Sort -> CheckM TVSubst-unify1 f e θ (FVar i) t+unify1 f e !θ (FVar !i) !t   = unifyVar f e θ i t-unify1 f e θ t (FVar i)+unify1 f e !θ !t (FVar !i)   = unifyVar f e θ i t-unify1 f e θ (FApp t1 t2) (FApp t1' t2')+unify1 f e !θ (FApp !t1 !t2) (FApp !t1' !t2')   = unifyMany f e θ [t1, t2] [t1', t2']-unify1 _ _ θ (FTC l1) (FTC l2)+unify1 _ _ !θ (FTC !l1) (FTC !l2)   | isListTC l1 && isListTC l2   = return θ-unify1 f e θ t1@(FAbs _ _) t2 = do-  t1'<- generalize t1+unify1 f e !θ !t1@(FAbs _ _) !t2 = do+  !t1' <- instantiate t1   unifyMany f e θ [t1'] [t2]-unify1 f e θ t1 t2@(FAbs _ _) = do-  t2' <- generalize t2+unify1 f e !θ !t1 t2@(FAbs _ _) = do+  !t2' <- instantiate t2   unifyMany f e θ [t1] [t2']-unify1 _ _ θ s1 s2+unify1 _ _ !θ !s1 !s2   | isString s1, isString s2   = return θ--unify1 _ _ θ FInt  FReal = return θ+unify1 _ _ !θ !FInt  !FReal = return θ -unify1 _ _ θ FReal FInt  = return θ+unify1 _ _ !θ !FReal !FInt  = return θ -unify1 f e θ t FInt = do+unify1 f e !θ !t FInt = do   checkNumeric f t `withError` (errUnify e t FInt)   return θ -unify1 f e θ FInt t = do+unify1 f e !θ !FInt !t = do   checkNumeric f t `withError` (errUnify e FInt t)   return θ -unify1 f e θ (FFunc t1 t2) (FFunc t1' t2') = do+unify1 f e !θ (FFunc !t1 !t2) (FFunc !t1' !t2') = do   unifyMany f e θ [t1, t2] [t1', t2'] -unify1 _ e θ t1 t2+unify1 _ e θ !t1 !t2   | t1 == t2   = return θ   | otherwise   = throwError $ errUnify e t1 t2 -subst :: (Int, Sort) -> Sort -> Sort-subst (j,tj) t@(FVar i)-  | i == j    = tj-  | otherwise = t-subst su (FApp t1 t2)  = FApp (subst su t1) (subst su t2)-subst _  (FTC l)       = FTC l-subst su (FFunc t1 t2) = FFunc (subst su t1) (subst su t2)-subst (j,tj) (FAbs i t)-  | i == j    = FAbs i t-  | otherwise = FAbs i $ subst (j,tj) t-subst _  s             = s+subst :: Int -> Sort -> Sort -> Sort+subst !j !tj !t@(FVar !i)+  | i == j                  = tj+  | otherwise               = t +subst !j !tj (FApp !t1 !t2)  = FApp t1' t2'+  where+    !t1'                    = subst j tj t1+    !t2'                    = subst j tj t2 -generalize :: Sort -> CheckM Sort-generalize (FAbs i t) = do-  v      <- refresh 0-  let sub = (i, FVar v)-  subst sub <$> generalize t-generalize t =-  return t+-- subst _ _  !(FTC l)         = FTC l+subst !j !tj (FFunc !t1 !t2) = FFunc t1' t2'+  where+    !t1'                    = subst j tj $! t1+    !t2'                    = subst j tj $! t2 +subst !j !tj (FAbs !i !t)+  | i == j                  = FAbs i t+  | otherwise               = FAbs i t'+  where+    !t'                     = subst j tj t++subst _  _   !s             = s++--------------------------------------------------------------------------------+instantiate :: Sort -> CheckM Sort+--------------------------------------------------------------------------------+instantiate !t = go t+  -- / | tn > 10   = go $ tracepp ("SIZE=" ++ show tn) t+  -- / | otherwise = go t+  where+    -- _tn = sortSize t+    go (FAbs !i !t) = do+      !t'    <- instantiate t+      !v     <- fresh+      return  $ subst i (FVar v) t'+    go !t =+      return t++-- instantiate s = do+--  where+--    (is, t)   = unAbs s++_unAbs :: Sort -> ([Int], Sort)+_unAbs = go []+  where+    go !acc (FAbs !i !t) = go (i:acc) t+    go !acc !t           = (reverse acc, t)++_sortSize :: Sort -> Int+_sortSize !t = go t+  where+    go :: Sort -> Int+    go (FApp  !t1 !t2) = go t1 + go t2+    go (FFunc !t1 !t2) = go t1 + go t2+    go (FAbs  _   !t)  = 1     + go t+    go _               = 1++ unifyVar :: Env -> Maybe Expr -> TVSubst -> Int -> Sort -> CheckM TVSubst-unifyVar _ _ θ i t@(FVar j)+unifyVar _ _ θ !i !t@(FVar !j)   = case lookupVar i θ of-      Just t'       -> if t == t' then return θ else return $ updateVar j t' θ-      Nothing       -> return $ updateVar i t θ+      Just !t'      -> if t == t' then return θ else return (updateVar j t' θ)+      Nothing       -> return (updateVar i t θ) -unifyVar f e θ i t+unifyVar f e θ !i !t   = case lookupVar i θ of-      Just (FVar j) -> return $ updateVar i t $ updateVar j t θ-      Just t'       -> if t == t' then return θ else unify1 f e θ t t'-      Nothing       -> return $ updateVar i t θ+      Just (FVar !j) -> return $ updateVar i t $ updateVar j t θ+      Just !t'       -> if t == t' then return θ else unify1 f e θ t t'+      Nothing        -> return (updateVar i t θ)  -------------------------------------------------------------------------------- -- | Applying a Type Substitution ---------------------------------------------- -------------------------------------------------------------------------------- apply :: TVSubst -> Sort -> Sort ---------------------------------------------------------------------------------apply θ          = sortMap f+apply θ          = Vis.mapSort f   where     f t@(FVar i) = fromMaybe t (lookupVar i θ)     f t          = t  ---------------------------------------------------------------------------------sortMap :: (Sort -> Sort) -> Sort -> Sort----------------------------------------------------------------------------------sortMap f (FAbs i t)    = FAbs i (sortMap f t)-sortMap f (FFunc t1 t2) = FFunc (sortMap f t1) (sortMap f t2)-sortMap f (FApp t1 t2)  = FApp  (sortMap f t1) (sortMap f t2)-sortMap f t             = f t---------------------------------------------------------------------------------- -- | Deconstruct a function-sort ----------------------------------------------- --------------------------------------------------------------------------------- checkFunSort :: Sort -> CheckM (Sort, Sort, TVSubst) checkFunSort (FAbs _ t)    = checkFunSort t checkFunSort (FFunc t1 t2) = return (t1, t2, emptySubst)-checkFunSort (FVar i)      = do j <- refresh 0 -                                k <- refresh 0 +checkFunSort (FVar i)      = do j <- fresh+                                k <- fresh                                 return (FVar j, FVar k, updateVar i (FFunc (FVar j) (FVar k)) emptySubst) checkFunSort t             = throwError $ errNonFunction 1 t -{--sortFunction :: Int -> Sort -> CheckM ([Sort], Sort)-sortFunction i t-  = case functionSort t of-     Nothing          -> throwError $ errNonFunction i t-     Just (_, ts, t') -> if length ts < i-                          then throwError $ errNonFunction i t-                          else let (its, ots) = splitAt i ts-                               in return (its, foldl FFunc t' ots)--}- -------------------------------------------------------------------------------- -- | API for manipulating Sort Substitutions ----------------------------------- --------------------------------------------------------------------------------@@ -951,7 +1002,7 @@ lookupVar i (Th m)   = M.lookup i m  updateVar :: Int -> Sort -> TVSubst -> TVSubst-updateVar i t (Th m) = Th (M.insert i t m)+updateVar !i !t (Th m) = Th (M.insert i t m)  emptySubst :: TVSubst emptySubst = Th M.empty

@@ -16,3 +16,4 @@ import Language.Fixpoint.Types.Constraints      as X import Language.Fixpoint.Types.Utils            as X import Language.Fixpoint.Types.Triggers         as X+import Language.Fixpoint.Types.Theories         as X

@@ -81,6 +81,7 @@     , minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)     , minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint     , gradual     :: Bool                -- ^ solve "gradual" constraints+    , ginteractive :: Bool                -- ^ interactive gradual solving     , extensionality   :: Bool           -- ^ allow function extensionality     , alphaEquivalence :: Bool           -- ^ allow lambda alpha equivalence axioms     , betaEquivalence  :: Bool           -- ^ allow lambda beta equivalence axioms@@ -161,6 +162,7 @@   , minimizeKs       = False &= help "Delta debug to minimize fq file (sat with max kvars replaced by True)"   , minimalSol       = False &= help "Shrink fixpoint by removing implied qualifiers"   , gradual          = False &= help "Solve gradual-refinement typing constraints"+  , ginteractive      = False &= help "Interactive Gradual Solving"   , extensionality   = False &= help "Allow function extensionality axioms"   , alphaEquivalence = False &= help "Allow lambda alpha equivalence axioms"   , betaEquivalence  = False &= help "Allow lambda alpha equivalence axioms"

@@ -36,12 +36,14 @@   , SimpC (..)   , Tag   , TaggedC, clhs, crhs-  , strengthenLhs+  -- , strengthenLhs+  , strengthenHyp    -- * Accessing Constraints   , addIds   , sinfo   , shiftVV+  , gwInfo, GWInfo (..)    -- * Qualifiers   , Qualifier (..)@@ -53,6 +55,7 @@   , FixSolution   , GFixSolution, toGFixSol   , Result (..)+  , unsafe, isUnsafe, safe    -- * Cut KVars   , Kuts (..)@@ -68,6 +71,9 @@   , Equation (..)   , Rewrite  (..)   , getEqBody++  -- * Misc  [should be elsewhere but here due to dependencies]+  , substVars   ) where  import qualified Data.Binary as B@@ -111,42 +117,89 @@                     , wrft  :: !(Symbol, Sort, KVar)                     , winfo :: !a                     , wexpr :: !Expr+                    , wloc  :: !GradInfo                     }               deriving (Eq, Generic, Functor) +data GWInfo = GWInfo { gsym  :: Symbol+                     , gsort :: Sort+                     , gexpr :: Expr+                     , ginfo :: GradInfo+                     }+              deriving (Eq, Generic) +gwInfo :: WfC a -> GWInfo+gwInfo (GWfC _ (x,s,_) _ e i)+  = GWInfo x s e i+gwInfo _+  = errorstar "gwInfo"+ updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a updateWfCExpr _ w@(WfC {})  = w updateWfCExpr f w@(GWfC {}) = w{wexpr = f (wexpr w)}  isGWfc :: WfC a -> Bool-isGWfc (GWfC _ _ _ _) = True-isGWfc (WfC _ _ _)    = False+isGWfc (GWfC {}) = True+isGWfc (WfC  {}) = False  type SubcId = Integer -data SubC a = SubC { _senv  :: !IBindEnv-                   , slhs   :: !SortedReft-                   , srhs   :: !SortedReft-                   , _sid   :: !(Maybe SubcId)-                   , _stag  :: !Tag-                   , _sinfo :: !a-                   }-              deriving (Eq, Generic, Functor)+data SubC a = SubC+  { _senv  :: !IBindEnv+  , slhs   :: !SortedReft+  , srhs   :: !SortedReft+  , _sid   :: !(Maybe SubcId)+  , _stag  :: !Tag+  , _sinfo :: !a+  }+  deriving (Eq, Generic, Functor) -data SimpC a = SimpC { _cenv  :: !IBindEnv-                     , _crhs  :: !Expr-                     , _cid   :: !(Maybe Integer)-                     , _ctag  :: !Tag-                     , _cinfo :: !a-                     }-              deriving (Generic, Functor)+data SimpC a = SimpC+  { _cenv  :: !IBindEnv+  , _crhs  :: !Expr+  , _cid   :: !(Maybe Integer)+  , _cbind :: !BindId               -- ^ Id of lhs/rhs binder+  , _ctag  :: !Tag+  , _cinfo :: !a+  }+  deriving (Generic, Functor) -strengthenLhs :: Expr -> SubC a -> SubC a-strengthenLhs e subc = subc {slhs = go (slhs subc)}++strengthenHyp :: SInfo a -> [(Integer, Expr)] -> SInfo a+strengthenHyp si ies = strengthenBinds si bindExprs   where-    go (RR s (Reft(v, r))) = RR s (Reft (v, pAnd [r, e]))+    bindExprs        = safeFromList "strengthenHyp" (mapFst (subcBind si) <$> ies) +subcBind :: SInfo a -> Integer -> BindId+subcBind si i+  | Just c <- M.lookup i (cm si)+  = _cbind c+  | otherwise+  = errorstar $ "Unknown subcId in subcBind: " ++ show i+++strengthenBinds :: SInfo a -> M.HashMap BindId Expr -> SInfo a+strengthenBinds si m = si { bs = mapBindEnv f (bs si) }+  where+    f i (x, sr)      = case M.lookup i m of+                         Nothing -> (x, sr)+                         Just e  -> (x, strengthenSortedReft sr e)++strengthenSortedReft :: SortedReft -> Expr -> SortedReft+strengthenSortedReft (RR s (Reft (v, r))) e = RR s (Reft (v, pAnd [r, e]))++++{-+  [(Int, Expr)]  ==> [(BindId, Expr)]++ -}++-- strengthenLhs :: Expr -> SubC a -> SubC a+-- strengthenLhs e subc = subc {slhs = go (slhs subc)}+--  where+--    go (RR s (Reft(v, r))) = RR s (Reft (v, pAnd [r, e]))+ class TaggedC c a where   senv  :: c a -> IBindEnv   sid   :: c a -> Maybe Integer@@ -206,6 +259,15 @@       soln      = mappend (resSolution r1)  (resSolution r2)       gsoln     = mappend (gresSolution r1) (gresSolution r2) +unsafe, safe :: Result a+unsafe = mempty {resStatus = Unsafe []}+safe   = mempty {resStatus = Safe}++isUnsafe :: Result a -> Bool+isUnsafe r | Unsafe _ <- resStatus r+  = True+isUnsafe _ = False+ instance (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) where   toFix Safe             = text "Safe"   -- toFix (UnknownError d) = text $ "Unknown Error: " ++ d@@ -285,6 +347,7 @@ instance B.Binary Qualifier instance B.Binary Kuts instance B.Binary HOInfo+instance B.Binary GWInfo instance B.Binary GFixSolution instance (B.Binary a) => B.Binary (SubC a) instance (B.Binary a) => B.Binary (WfC a)@@ -295,6 +358,7 @@ instance NFData Kuts instance NFData HOInfo instance NFData GFixSolution+instance NFData GWInfo  instance (NFData a) => NFData (SubC a) instance (NFData a) => NFData (WfC a)@@ -307,11 +371,14 @@ ---------------------------------------------------------------------------  wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]-wfC be sr x = if all isEmptySubst (sus ++ gsus)-                then [WfC be (v, sr_sort sr, k) x | k <- ks] ++ [GWfC be (v, sr_sort sr, k) x e | (k, e) <- gs ]+wfC be sr x = if all isEmptySubst (sus ) -- ++ gsus)+                 -- NV TO RJ This tests fails with [LT:=GHC.Types.LT][EQ:=GHC.Types.EQ][GT:=GHC.Types.GT]]+                 -- NV TO RJ looks like a resolution issue+                then [WfC be (v, sr_sort sr, k) x      | k         <- ks ]+                  ++ [GWfC be (v, sr_sort sr, k) x e i | (k, e, i) <- gs ]                 else errorstar msg   where-    msg             = "wfKvar: malformed wfC " ++ show sr+    msg             = "wfKvar: malformed wfC " ++ show sr ++ "\n" ++ show (sus ++ gsus)     Reft (v, ras)   = sr_reft sr     (ks, sus)       = unzip $ go ras     (gs, gsus)      = unzip $ go' ras@@ -320,7 +387,7 @@     go (PAnd es)    = [(k, su) | PKVar k su <- es]     go _            = [] -    go' (PGrad k su e) = [((k, e), su)]+    go' (PGrad k su i e) = [((k, e, i), su)]     go' (PAnd es)      = concatMap go' es     go' _              = [] @@ -481,8 +548,9 @@    -> Bool    -> [Triggered Expr]    -> AxiomEnv+   -> [DataDecl]    -> GInfo SubC a-fi cs ws binds ls ds ks qs bi aHO aHOq es axe+fi cs ws binds ls ds ks qs bi aHO aHOq es axe adts   = FI { cm       = M.fromList $ addIds cs        , ws       = M.fromListWith err [(k, w) | w <- ws, let (_, _, k) = wrft w]        , bs       = binds@@ -494,6 +562,7 @@        , hoInfo   = HOI aHO aHOq        , asserts  = es        , ae       = axe+       , ddecls   = adts        }   where     --TODO handle duplicates gracefully instead (merge envs by intersect?)@@ -518,22 +587,21 @@ allowHOquals = hoQuals . hoInfo  data GInfo c a =-  FI { cm       :: !(M.HashMap SubcId (c a)) -- ^ cst id |-> Horn Constraint+  FI { cm       :: !(M.HashMap SubcId (c a))  -- ^ cst id |-> Horn Constraint      , ws       :: !(M.HashMap KVar (WfC a))  -- ^ Kvar  |-> WfC defining its scope/args      , bs       :: !BindEnv                   -- ^ Bind  |-> (Symbol, SortedReft)      , gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols      , dLits    :: !(SEnv Sort)               -- ^ Distinct Constant symbols      , kuts     :: !Kuts                      -- ^ Set of KVars *not* to eliminate-  --    , packs    :: !Packs                     -- ^ Pack-sets of related KVars      , quals    :: ![Qualifier]               -- ^ Abstract domain      , bindInfo :: !(M.HashMap BindId a)      -- ^ Metadata about binders+     , ddecls   :: ![DataDecl]                -- ^ User-defined data declarations      , hoInfo   :: !HOInfo                    -- ^ Higher Order info      , asserts  :: ![Triggered Expr]      , ae       :: AxiomEnv      }   deriving (Eq, Show, Functor, Generic) - instance Monoid HOInfo where   mempty        = HOI False False   mappend i1 i2 = HOI { hoBinds = hoBinds i1 || hoBinds i2@@ -541,19 +609,19 @@                       }  instance Monoid (GInfo c a) where-  mempty        = FI M.empty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty+  mempty        = FI M.empty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty   mappend i1 i2 = FI { cm       = mappend (cm i1)       (cm i2)                      , ws       = mappend (ws i1)       (ws i2)                      , bs       = mappend (bs i1)       (bs i2)                      , gLits    = mappend (gLits i1)    (gLits i2)                      , dLits    = mappend (dLits i1)    (dLits i2)                      , kuts     = mappend (kuts i1)     (kuts i2)-                     -- , packs    = mappend (packs i1)    (packs i2)                      , quals    = mappend (quals i1)    (quals i2)                      , bindInfo = mappend (bindInfo i1) (bindInfo i2)+                     , ddecls   = mappend (ddecls i1)   (ddecls i2)                      , hoInfo   = mappend (hoInfo i1)   (hoInfo i2)                      , asserts  = mappend (asserts i1)  (asserts i2)-                     , ae  = mappend (ae i1)  (ae i2)+                     , ae       = mappend (ae i1)       (ae i2)                      }  instance PTable (SInfo a) where@@ -576,6 +644,7 @@                   $++$ csDoc    x'                   $++$ wsDoc    x'                   $++$ binfoDoc x'+                  $++$ aeDoc    x'                   $++$ text "\n"   where     cfgDoc cfg    = text ("// " ++ show cfg)@@ -587,6 +656,7 @@     -- packsDoc      = toFix    . packs     bindsDoc      = toFix    . bs     qualsDoc      = vcat     . map toFix . quals+    aeDoc         = toFix    . ae     metaDoc (i,d) = toFixMeta (text "bind" <+> toFix i) (toFix d)     mdata         = metadata cfg     binfoDoc@@ -604,33 +674,37 @@ writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO () writeFInfo cfg fq f = writeFile f (render $ toFixpoint cfg fq) ---------------------------------------------------------------------------+-------------------------------------------------------------------------------- -- | Query Conversions: FInfo to SInfo----------------------------------------------------------------------------+-------------------------------------------------------------------------------- convertFormat :: (Fixpoint a) => FInfo a -> SInfo a-----------------------------------------------------------------------------convertFormat fi = fi' { cm = subcToSimpc <$> cm fi' }+--------------------------------------------------------------------------------+convertFormat fi = fi' { cm = subcToSimpc bindm <$> cm fi' }   where-    fi'          = M.foldlWithKey' blowOutVV fi $ cm fi+    (bindm, fi') = M.foldlWithKey' outVV (M.empty, fi) $ cm fi -subcToSimpc :: SubC a -> SimpC a-subcToSimpc s = SimpC-  { _cenv     = senv s-  , _crhs     = reftPred $ sr_reft $ srhs s-  , _cid      = sid s-  , _ctag     = stag s-  , _cinfo    = sinfo s+subcToSimpc :: BindM -> SubC a -> SimpC a+subcToSimpc m s = SimpC+  { _cenv       = senv s+  , _crhs       = reftPred $ sr_reft $ srhs s+  , _cid        = sid s+  , _cbind      = safeLookup "subcToSimpc" (subcId s) m+  , _ctag       = stag s+  , _cinfo      = sinfo s   } -blowOutVV :: FInfo a -> Integer -> SubC a -> FInfo a-blowOutVV fi i subc = fi { bs = be', cm = cm' }+outVV :: (BindM, FInfo a) -> Integer -> SubC a -> (BindM, FInfo a)+outVV (m, fi) i c = (m', fi')   where-    sr            = slhs subc+    fi'           = fi { bs = be', cm = cm' }+    m'            = M.insert i bId m+    (bId, be')    = insertBindEnv x sr $ bs fi+    cm'           = M.insert i c' $ cm fi+    c'            = c { _senv = insertsIBindEnv [bId] $ senv c }+    sr            = slhs c     x             = reftBind $ sr_reft sr-    (bindId, be') = insertBindEnv x sr $ bs fi-    subc'         = subc { _senv = insertsIBindEnv [bindId] $ senv subc }-    cm'           = M.insert i subc' $ cm fi +type BindM = M.HashMap Integer BindId  --------------------------------------------------------------------------- -- | Top level Solvers ----------------------------------------------------@@ -662,7 +736,7 @@ --------------------------------------------------------------------------- -- | Axiom Instantiation Information -------------------------------------- ----------------------------------------------------------------------------data AxiomEnv = AEnv { aenvSyms    :: ![Symbol]+data AxiomEnv = AEnv { aenvSyms    :: !Int                      , aenvEqs     :: ![Equation]                      , aenvSimpl   :: ![Rewrite]                      , aenvFuel    :: M.HashMap SubcId Int@@ -682,9 +756,9 @@ instance NFData Eliminate  instance Monoid AxiomEnv where-  mempty = AEnv [] [] [] (M.fromList []) (M.fromList [])+  mempty = AEnv 0 [] [] (M.fromList []) (M.fromList [])   mappend a1 a2 = AEnv aenvSyms' aenvEqs' aenvSimpl' aenvFuel' aenvExpand'-    where aenvSyms'    = mappend (aenvSyms a1) (aenvSyms a2)+    where aenvSyms'    = aenvSyms a1 + aenvSyms a2           aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)           aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)           aenvFuel'    = mappend (aenvFuel a1) (aenvFuel a2)@@ -696,6 +770,10 @@                     }   deriving (Eq, Show, Generic) +instance PPrint Equation where+  pprintTidy k (Equ f xs e) = "def" <+> pprint f <+> intersperse " " (pprint <$> xs) <+> ":=" <+> pprintTidy k e++ -- eg  SMeasure (f D [x1..xn] e) -- for f (D x1 .. xn) = e data Rewrite  = SMeasure  { smName  :: Symbol         -- eg. f@@ -704,6 +782,29 @@                           , smBody  :: Expr           -- eg. e[xs]                           }   deriving (Eq, Show, Generic)++instance Fixpoint AxiomEnv where+  toFix axe = vcat ((toFix <$> aenvEqs axe) ++ (toFix <$> aenvSimpl axe))+              $+$ text "syms" <+> text (show (aenvSyms axe))+              $+$ text "fuel" <+> toFix (pairdoc <$> M.toList (aenvFuel axe))+              $+$ text "expand" <+> toFix (pairdoc <$> M.toList(aenvExpand axe))+    where pairdoc (x,y) = text $ show x ++ " : " ++ show y++-- teehee+instance Fixpoint Doc where+  toFix = id++instance Fixpoint Equation where+  toFix (Equ f xs e)  = text "define"+                     <+> toFix f <+> hsep (toFix <$> xs) <+> text " = "+                     <+> lparen <> toFix e <> rparen+instance Fixpoint Rewrite where+  toFix (SMeasure f d xs e)+    = text "match"+   <+> toFix f+   <+> parens (toFix d <+> hsep (toFix <$> xs))+   <+> text " = "+   <+> lparen <> toFix e <> rparen  getEqBody :: Equation -> Maybe Expr getEqBody (Equ  x xs (PAnd ((PAtom Eq fxs e):_)))

@@ -31,6 +31,7 @@   , insertsIBindEnv   , deleteIBindEnv   , elemsIBindEnv+  , fromListIBindEnv   , memberIBindEnv   , unionIBindEnv   , diffIBindEnv@@ -187,6 +188,8 @@ elemsIBindEnv :: IBindEnv -> [BindId] elemsIBindEnv (FB s) = S.toList s +fromListIBindEnv :: [BindId] -> IBindEnv+fromListIBindEnv = FB . S.fromList  -- | Functions for Global Binder Environment insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)

@@ -38,7 +38,9 @@   , catErrors    -- * Fatal Exit+  , panic   , die+  , dieAt   , exit    -- * Some popular errors@@ -48,7 +50,6 @@   ) where  import           Control.Exception--- import qualified Control.Monad.Error           as E import           Data.Serialize                (Serialize (..)) import           Data.Generics                 (Data) import           Data.Typeable@@ -128,9 +129,22 @@ err sp d = Error [Error1 sp d]  ---------------------------------------------------------------------+panic :: String -> a+---------------------------------------------------------------------+panic = die . err dummySpan . text . (panicMsg ++)++panicMsg :: String+panicMsg = "PANIC: Please file an issue at https://github.com/ucsd-progsys/liquid-fixpoint \n"++--------------------------------------------------------------------- die :: Error -> a --------------------------------------------------------------------- die = throw++---------------------------------------------------------------------+dieAt :: SrcSpan -> Error -> a+---------------------------------------------------------------------+dieAt sp (Error es) = die (Error [ e {errLoc = sp} | e <- es])  --------------------------------------------------------------------- exit :: a -> IO a -> IO a

@@ -0,0 +1,258 @@+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE NoMonomorphismRestriction  #-}+{-# LANGUAGE OverloadedStrings          #-}+{-# LANGUAGE UndecidableInstances       #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE TypeOperators              #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE PatternGuards              #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE TupleSections              #-}++-- | This module contains the top-level SOLUTION data types,+--   including various indices used for solving.++module Language.Fixpoint.Types.Graduals (+  uniquify,++  makeSolutions,++  GSol,++  Gradual (..)+  ) where++import Language.Fixpoint.Types.Refinements+import Language.Fixpoint.Types.Constraints+import Language.Fixpoint.Types.Config+import Language.Fixpoint.Types.PrettyPrint+import Language.Fixpoint.Types.Environments+import Language.Fixpoint.Types.Substitutions+import Language.Fixpoint.Types.Visitor+import Language.Fixpoint.Types.Spans+import Language.Fixpoint.Types.Theories+import Language.Fixpoint.Types.Names        (gradIntSymbol, tidySymbol)+import Language.Fixpoint.Misc               (allCombinations, errorstar)++import Control.DeepSeq++import qualified Data.HashMap.Strict       as M+import qualified Data.List                 as L++import Control.Monad.State.Lazy+import Data.Maybe (fromMaybe)+import qualified Language.Fixpoint.SortCheck       as So+import Language.Fixpoint.Solver.Sanitize (symbolEnv)+++data GSol = GSol !SymEnv !(M.HashMap KVar (Expr, GradInfo))++instance Monoid GSol where+  mempty = GSol mempty mempty+  mappend (GSol e1 m1) (GSol e2 m2) = GSol (mappend e1 e2) (mappend m1 m2)++instance Show GSol where+  show (GSol _ m) = "GSOL = \n" ++ unlines ((\(k,(e, i)) -> showpp k ++ showInfo i ++  " |-> " ++ showpp (tx e)) <$> M.toList m)+    where+      tx e = subst (mkSubst $ [(x, EVar $ tidySymbol x) | x <- syms e]) e+      showInfo i = show i+++makeSolutions :: (NFData a, Fixpoint a, Show a)+              => Config -> SInfo a+              -> [(KVar, (GWInfo, [[Expr]]))]+              -> Maybe [GSol]++makeSolutions _ _ []+  = Nothing+makeSolutions cfg fi kes+  = Just $ map (GSol env . M.fromList) (allCombinations (go  <$> kes))+  where+    go (k, (i, es)) = [(k, (pAnd (gexpr i:e'), ginfo i)) | e' <- es]+    env = symbolEnv cfg fi+++-------------------------------------------------------------------------------+-- |  Make each gradual appearence unique -------------------------------------+-------------------------------------------------------------------------------+uniquify :: (NFData a, Fixpoint a, Loc a) => SInfo a -> (SInfo a)++uniquify fi = fi{cm = cm', ws = ws', bs = bs'}+  where+  (cm', km, bs') = uniquifyCS (bs fi) (cm fi)+  ws'            = expandWF km (ws fi)++uniquifyCS :: (NFData a, Fixpoint a, Loc a)+           => BindEnv+           -> M.HashMap SubcId (SimpC a)+           -> (M.HashMap SubcId (SimpC a), M.HashMap KVar [(KVar, Maybe SrcSpan)], BindEnv)+uniquifyCS bs cs+  = (x, km, benv st)+--   = (x, km, mapBindEnv (\i (x,r) -> if i `elem` ubs st then (x, ungrad r) else (x, r)) $ benv st)+  where+    (x, st) = runState (uniq cs) (initUniqueST bs)+    km      = kmap st+    -- gs      = [x | xs <- M.elems km, (x,_) <- xs]+++class Unique a where+   uniq :: a -> UniqueM a++instance Unique a => Unique (M.HashMap SubcId a) where+  uniq m = M.fromList <$> mapM (\(i,x) -> (i,) <$> uniq x) (M.toList m)++instance Loc a => Unique (SimpC a) where+  uniq cs = do+    updateLoc $ srcSpan $ _cinfo cs+    rhs <- uniq (_crhs cs)+    env <- uniq (_cenv cs)+    return cs{_crhs = rhs, _cenv = env}++instance Unique IBindEnv where+  uniq env = withCache (fromListIBindEnv <$> mapM uniq (elemsIBindEnv env))++instance Unique BindId where+  uniq i = do+    bs <- benv <$> get+    let (x, t) = lookupBindEnv i bs+    resetChange+    t' <- uniq t+    hasChanged <- change <$> get+    if hasChanged+      then do let (i', bs') = insertBindEnv x t' bs+              updateBEnv i bs'+              return i'+      else return i++instance Unique SortedReft where+  uniq (RR s r) = RR s <$> uniq r++instance Unique Reft where+  uniq (Reft (x,e)) = (Reft . (x,)) <$> uniq e++instance Unique Expr where+  uniq = mapMExpr go+   where+    go (PGrad k su i e) = do+      k'  <- freshK k+      src <- uloc <$> get+      return $ PGrad k' su (i{gused = src}) e+    go e              = return e++-------------------------------------------------------------------------------+-- | The Unique Monad ---------------------------------------------------------+-------------------------------------------------------------------------------++type UniqueM = State UniqueST+data UniqueST+  = UniqueST { freshId :: Integer+             , kmap    :: M.HashMap KVar [(KVar, Maybe SrcSpan)]+             , change  :: Bool+             , cache   :: M.HashMap KVar KVar+             , uloc    :: Maybe SrcSpan+             , ubs     :: [BindId]+             , benv    :: BindEnv+             }++updateLoc :: SrcSpan -> UniqueM ()+updateLoc x = modify $ \s -> s{uloc = Just x}++withCache :: UniqueM a -> UniqueM a+withCache act = do+  emptyCache+  a <- act+  emptyCache+  return a++emptyCache :: UniqueM ()+emptyCache = modify $ \s -> s{cache = mempty}++addCache :: KVar -> KVar -> UniqueM ()+addCache k k' = modify $ \s -> s{cache = M.insert k k' (cache s)}++updateBEnv :: BindId -> BindEnv -> UniqueM ()+updateBEnv i bs = modify $ \s -> s{benv = bs, ubs = i:(ubs s)}++setChange :: UniqueM ()+setChange = modify $ \s -> s{change = True}++resetChange :: UniqueM ()+resetChange = modify $ \s -> s{change = False}++initUniqueST :: BindEnv ->  UniqueST+initUniqueST = UniqueST 0 mempty False mempty Nothing mempty++freshK, freshK' :: KVar -> UniqueM KVar+freshK k  = do+  setChange+  cached <- cache <$> get+  case M.lookup k cached of+    {- OPTIMIZATION: Only create one fresh occurence of ? per constraint environment. -}+    Just k' -> return  k'+    Nothing -> freshK' k++freshK' k = do+  i <- freshId <$> get+  modify $ (\s -> s{freshId = i + 1})+  let k' = KV $ gradIntSymbol i+  addK k k'+  addCache k k'+  return k'++addK :: KVar -> KVar -> UniqueM ()+addK key val =+  modify $ (\s -> s{kmap = M.insertWith (++) key [(val, uloc s)] (kmap s)})++-------------------------------------------------------------------------------+-- | expandWF -----------------------------------------------------------------+-------------------------------------------------------------------------------++expandWF :: (NFData a, Fixpoint a)+         => M.HashMap KVar [(KVar, Maybe SrcSpan)]+         -> M.HashMap KVar (WfC a)+         -> M.HashMap KVar (WfC a)+expandWF km ws+  = M.fromList $+       ([(k, updateKVar k src w) | (i, w) <- gws, (kw, ks) <- km', kw == i, (k, src) <- ks]+        ++ kws)+  where+    (gws, kws)       = L.partition (isGWfc . snd) $ M.toList ws+    km'              = M.toList km+    updateKVar k src wfc = wfc { wrft = (\(v,s,_) -> (v,s,k)) $ wrft wfc+                               , wloc = (wloc wfc){gused = src}+                               }++-------------------------------------------------------------------------------+-- |  Substitute Gradual Solution ---------------------------------------------+-------------------------------------------------------------------------------++class Gradual a where+  gsubst :: GSol -> a -> a++instance Gradual Expr where+  gsubst (GSol env m) e   = mapGVars' (\(k, _) -> Just (fromMaybe (err k) (mknew k))) e+    where+      mknew k = So.elaborate "initBGind.mkPred" env $ fst <$> M.lookup k m+      err   k = errorstar ("gradual substitution: Cannot find " ++ showpp k)++instance Gradual Reft where+  gsubst su (Reft (x, e)) = Reft (x, gsubst su e)++instance Gradual SortedReft where+  gsubst su r = r {sr_reft = gsubst su (sr_reft r)}++instance Gradual (SimpC a) where+  gsubst su c = c {_crhs = gsubst su (_crhs c)}++instance Gradual BindEnv where+  gsubst su = mapBindEnv (\_ (x, r) -> (x, gsubst su r))++instance Gradual v => Gradual (M.HashMap k v) where+  gsubst su = M.map (gsubst su)++instance Gradual (SInfo a) where+  gsubst su fi = fi { bs = gsubst su (bs fi)+                    , cm = gsubst su (cm fi)+                    }

@@ -30,12 +30,16 @@   , symbolSafeString   , symbolText   , symbolString+  , symbolBuilder+  , buildMany    -- Predicates   , isPrefixOfSym   , isSuffixOfSym   , isNonSymbol   , isLitSymbol+  , isTestSymbol+  -- , isCtorSymbol   , isNontrivialVV   , isDummy @@ -62,9 +66,11 @@   , dummySymbol   , intSymbol   , tempSymbol+  , gradIntSymbol    -- * Wrapping Symbols   , litSymbol+  , testSymbol   , renameSymbol   , kArgSymbol   , existSymbol@@ -83,8 +89,6 @@   , tupConName   , setConName   , mapConName-  -- , propConName-  -- , hpropConName   , strConName   , nilName   , consName@@ -94,16 +98,19 @@   , bitVecName   , bvAndName   , bvOrName+  -- HKT , tyAppName   , prims   , mulFuncName   , divFuncName    -- * Casting function names-  , setToIntName, bitVecToIntName, mapToIntName, boolToIntName, realToIntName+  , setToIntName, bitVecToIntName, mapToIntName, boolToIntName, realToIntName, toIntName   , setApplyName, bitVecApplyName, mapApplyName, boolApplyName, realApplyName, intApplyName+  , applyName    , lambdaName-  , intArgName+  , lamArgSymbol+  , isLamArgSymbol  ) where @@ -111,6 +118,7 @@ import           Control.Arrow               (second) import           Data.Char                   (ord) import           Data.Maybe                  (fromMaybe)+import           Data.Monoid                 ((<>)) import           Data.Generics               (Data) import           Data.Hashable               (Hashable (..)) import qualified Data.HashSet                as S@@ -118,10 +126,10 @@ import           Data.Interned.Internal.Text import           Data.String                 (IsString(..)) import qualified Data.Text                   as T+import qualified Data.Text.Lazy.Builder      as Builder import           Data.Binary                 (Binary (..)) import           Data.Typeable               (Typeable) import           GHC.Generics                (Generic)- import           Text.PrettyPrint.HughesPJ   (text) import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Spans@@ -391,6 +399,19 @@ vvCon       = vvName `suffixSymbol` "F" dummySymbol = dummyName +-- ctorSymbol :: Symbol -> Symbol+-- ctorSymbol s = ctorPrefix `mappendSym` s++-- isCtorSymbol :: Symbol -> Bool+-- isCtorSymbol = isPrefixOfSym ctorPrefix++-- | 'testSymbol c' creates the `is-c` symbol for the adt-constructor named 'c'.+testSymbol :: Symbol -> Symbol+testSymbol s = testPrefix `mappendSym` s++isTestSymbol :: Symbol -> Bool+isTestSymbol = isPrefixOfSym testPrefix+ litSymbol :: Symbol -> Symbol litSymbol s = litPrefix `mappendSym` s @@ -415,13 +436,22 @@ existSymbol :: Symbol -> Integer -> Symbol existSymbol prefix = intSymbol (existPrefix `mappendSym` prefix) +gradIntSymbol :: Integer -> Symbol+gradIntSymbol = intSymbol gradPrefix -tempPrefix, anfPrefix, renamePrefix, litPrefix  :: Symbol+tempPrefix, anfPrefix, renamePrefix, litPrefix, gradPrefix :: Symbol tempPrefix   = "lq_tmp$" anfPrefix    = "lq_anf$" renamePrefix = "lq_rnm$" litPrefix    = "lit$"+gradPrefix   = "grad$" +testPrefix  :: Symbol+testPrefix   = "is$"++-- ctorPrefix  :: Symbol+-- ctorPrefix   = "mk$"+ kArgPrefix, existPrefix :: Symbol kArgPrefix   = "lq_karg$" existPrefix  = "lq_ext$"@@ -467,6 +497,14 @@ instance Symbolic Symbol where   symbol = id +symbolBuilder :: (Symbolic a) => a -> Builder.Builder+symbolBuilder = Builder.fromText . symbolSafeText . symbol++{-# INLINE buildMany #-}+buildMany :: [Builder.Builder] -> Builder.Builder+buildMany []     = mempty+buildMany [b]    = b+buildMany (b:bs) = b <> mconcat [ " " <> b | b <- bs ] ---------------------------------------------------------------------------- --------------- Global Name Definitions ------------------------------------ ----------------------------------------------------------------------------@@ -474,14 +512,21 @@ lambdaName :: Symbol lambdaName = "smt_lambda" -intArgName :: Int -> Symbol-intArgName = intSymbol "lam_int_arg"+lamArgPrefix :: Symbol+lamArgPrefix = "lam_arg" -setToIntName, bitVecToIntName, mapToIntName, realToIntName :: Symbol+lamArgSymbol :: Int -> Symbol+lamArgSymbol = intSymbol lamArgPrefix++isLamArgSymbol :: Symbol -> Bool+isLamArgSymbol = isPrefixOfSym lamArgPrefix++setToIntName, bitVecToIntName, mapToIntName, realToIntName, toIntName :: Symbol setToIntName    = "set_to_int" bitVecToIntName = "bitvec_to_int" mapToIntName    = "map_to_int" realToIntName   = "real_to_int"+toIntName       = "cast_as_int"  boolToIntName :: (IsString a) => a boolToIntName   = "bool_to_int"@@ -494,6 +539,8 @@ realApplyName   = intSymbol "real_apply_" intApplyName    = intSymbol "int_apply_" +applyName :: Symbol+applyName = "apply"  preludeName, dummyName, boolConName, funConName :: Symbol preludeName  = "Prelude"@@ -501,6 +548,7 @@ boolConName  = "Bool" funConName   = "->" + listConName, listLConName, tupConName, _propConName, _hpropConName, vvName, setConName, mapConName :: Symbol listConName  = "[]" listLConName = "List"@@ -527,6 +575,9 @@ bitVecName   = "BitVec" bvOrName     = "bvor" bvAndName    = "bvand"++-- HKT tyAppName :: Symbol+-- HKT tyAppName    = "LF-App"  mulFuncName, divFuncName :: Symbol mulFuncName  = "Z3_OP_MUL"

@@ -88,6 +88,7 @@ showTable :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> String showTable k = render . pprintKVs k +-- | Please do not alter this. tracepp :: (PPrint a) => String -> a -> a tracepp s x = trace ("\nTrace: [" ++ s ++ "] : " ++ showpp x) x @@ -118,6 +119,22 @@   pprintTidy k (x, y, z)  = parens $ pprintTidy k x <> "," <+>                                      pprintTidy k y <> "," <+>                                      pprintTidy k z++++instance (PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) where+  pprintTidy k (w, x, y, z)  = parens $ pprintTidy k w <> "," <+>+                                        pprintTidy k x <> "," <+>+                                        pprintTidy k y <> "," <+>+                                        pprintTidy k z++instance (PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e) where+  pprintTidy k (v, w, x, y, z)  = parens $ pprintTidy k v <> "," <+>+                                           pprintTidy k w <> "," <+>+                                           pprintTidy k x <> "," <+>+                                           pprintTidy k y <> "," <+>+                                           pprintTidy k z+   instance (PPrint a, PPrint b) => PPrint (a,b) where

@@ -24,6 +24,7 @@   , Bop (..)   , Brel (..)   , Expr (..), Pred+  , GradInfo (..)   , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot   , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv   , pattern EEq@@ -88,7 +89,8 @@    -- * Gradual Type Manipulation   , pGAnds, pGAnd-  , isGradual+  , HasGradual (..)+  , srcGradInfo    ) where @@ -118,7 +120,9 @@ -- import qualified Data.HashSet              as S  instance NFData KVar+instance NFData SrcSpan instance NFData Subst+instance NFData GradInfo instance NFData Constant instance NFData SymConst instance NFData Brel@@ -131,8 +135,10 @@   put = B.put . M.toList   get = M.fromList <$> B.get +instance B.Binary SrcSpan instance B.Binary KVar instance B.Binary Subst+instance B.Binary GradInfo instance B.Binary Constant instance B.Binary SymConst instance B.Binary Brel@@ -151,10 +157,35 @@ isKvar (PKVar _ _) = True isKvar _           = False -isGradual :: Expr -> Bool-isGradual (PGrad _ _ _) = True-isGradual _             = False+class HasGradual a where+  isGradual :: a -> Bool+  gVars     :: a -> [KVar]+  ungrad    :: a -> a +instance HasGradual Expr where+  isGradual (PGrad {}) = True+  isGradual (PAnd xs)  = any isGradual xs+  isGradual _          = False++  gVars (PGrad k _ _ _) = [k]+  gVars (PAnd xs)       = concatMap gVars xs+  gVars _               = []++  ungrad (PGrad {}) = PTrue+  ungrad (PAnd xs)  = PAnd (ungrad <$> xs )+  ungrad e          = e+++instance HasGradual Reft where+  isGradual (Reft (_,r)) = isGradual r+  gVars (Reft (_,r))     = gVars r+  ungrad (Reft (x,r))    = Reft(x, ungrad r)++instance HasGradual SortedReft where+  isGradual = isGradual . sr_reft+  gVars     = gVars . sr_reft+  ungrad r  = r {sr_reft = ungrad (sr_reft r)}+ refaConjuncts :: Expr -> [Expr] refaConjuncts p = [p' | p' <- conjuncts p, not $ isTautoPred p'] @@ -246,7 +277,7 @@           | PKVar  !KVar !Subst           | PAll   ![(Symbol, Sort)] !Expr           | PExist ![(Symbol, Sort)] !Expr-          | PGrad  !KVar !Subst !Expr+          | PGrad  !KVar !Subst !GradInfo !Expr           deriving (Eq, Show, Data, Typeable, Generic)  type Pred = Expr@@ -262,6 +293,12 @@ pattern ERDiv e1 e2   = EBin RDiv   e1 e2  +data GradInfo = GradInfo {gsrc :: SrcSpan, gused :: Maybe SrcSpan}+          deriving (Eq, Show, Data, Typeable, Generic)++srcGradInfo :: SourcePos -> GradInfo+srcGradInfo src = GradInfo (SS src src) Nothing+ mkEApp :: LocSymbol -> [Expr] -> Expr mkEApp = eApps . EVar . val @@ -277,8 +314,7 @@ eAppC :: Sort -> Expr -> Expr -> Expr eAppC s e1 e2 = ECst (EApp e1 e2) s --+-------------------------------------------------------------------------------- debruijnIndex :: Expr -> Int debruijnIndex = go   where@@ -302,7 +338,7 @@     go (PAll _ e)      = go e     go (PExist _ e)    = go e     go (PKVar _ _)     = 1-    go (PGrad _ _ e)   = go e+    go (PGrad _ _ _ e) = go e   -- | Parsed refinement of @Symbol@ as @Expr@@@ -370,6 +406,7 @@   toFix (ENeg e)       = parens $ text "-"  <+> parens (toFix e)   toFix (EBin o e1 e2) = parens $ toFix e1  <+> toFix o <+> toFix e2   toFix (EIte p e1 e2) = parens $ text "if" <+> toFix p <+> text "then" <+> toFix e1 <+> text "else" <+> toFix e2+  -- toFix (ECst e _so)   = toFix e   toFix (ECst e so)    = parens $ toFix e   <+> text " : " <+> toFix so   -- toFix (EBot)         = text "_|_"   -- toFix PTop           = text "???"@@ -388,7 +425,7 @@                                         $+$ ("." <+> toFix p))   toFix (ETApp e s)      = text "tapp" <+> toFix e <+> toFix s   toFix (ETAbs e s)      = text "tabs" <+> toFix e <+> toFix s-  toFix (PGrad _ _ e)    = toFix e <+> text "&&" <+> text "??" -- <+> toFix k <+> toFix su+  toFix (PGrad k _ _ e)  = toFix e <+> text "&&" <+> toFix k -- text "??" -- <+> toFix k <+> toFix su   toFix (ELam (x,s) e)   = text "lam" <+> toFix x <+> ":" <+> toFix s <+> "." <+> toFix e    simplify (PAnd [])     = PTrue@@ -396,9 +433,9 @@   simplify (PAnd [p])    = simplify p   simplify (POr  [p])    = simplify p -  simplify (PGrad k su e)+  simplify (PGrad k su i e)     | isContraPred e      = PFalse-    | otherwise           = PGrad k su (simplify e)+    | otherwise           = PGrad k su i (simplify e)    simplify (PAnd ps)     | any isContraPred ps = PFalse@@ -525,8 +562,9 @@                                    "else" <+> pprintPrec (zi+1) k e2     where zi = 1 -  -- pprintPrec _ k (ECst e so)     = parens $ pprint e <+> ":" <+> const (text "...") (pprintTidy k so)-  pprintPrec z k (ECst e _)      = pprintPrec z k e+  -- RJ: DO NOT DELETE!+  pprintPrec _ k (ECst e so)     = parens $ pprint e <+> ":" <+> {- const (text "...") -} (pprintTidy k so)+  -- pprintPrec z k (ECst e _)      = pprintPrec z k e   pprintPrec _ _ PTrue           = trueD   pprintPrec _ _ PFalse          = falseD   pprintPrec z k (PNot p)        = parensIf (z > zn) $@@ -559,7 +597,7 @@   pprintPrec _ _ p@(PKVar {})    = toFix p   pprintPrec _ _ (ETApp e s)     = "ETApp" <+> toFix e <+> toFix s   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s-  pprintPrec z k (PGrad _ _ e)   = pprintPrec z k e <+> "&&" <+> "??"+  pprintPrec z k (PGrad x _ _ e) = pprintPrec z k e <+> "&&" <+> toFix x -- "??"  pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc pprintQuant k d xts p = (d <+> toFix xts)@@ -721,8 +759,8 @@ pGAnds = foldl pGAnd PTrue  pGAnd :: Expr -> Expr -> Expr-pGAnd (PGrad k su p) q = PGrad k su (pAnd [p, q])-pGAnd p (PGrad k su q) = PGrad k su (pAnd [p, q])+pGAnd (PGrad k su i p) q = PGrad k su i (pAnd [p, q])+pGAnd p (PGrad k su i q) = PGrad k su i (pAnd [p, q]) pGAnd p q              = pAnd [p,q]  ------------------------------------------------------------

@@ -30,8 +30,8 @@   , eQual   , trueEqual -  -- * Gradual Solution elements   -  , qbToGb, gbToQbs, gbEquals, equalsGb, emptyGMap   +  -- * Gradual Solution elements+  , qbToGb, gbToQbs, gbEquals, equalsGb, emptyGMap, qbExprs    -- * Solution Candidates (move to SolverMonad?)   , Cand@@ -78,6 +78,7 @@ import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts+import           Language.Fixpoint.Types.Theories import           Language.Fixpoint.Types.Refinements import           Language.Fixpoint.Types.Environments import           Language.Fixpoint.Types.Constraints@@ -122,11 +123,11 @@ newtype QBind = QB [EQual]   deriving (Show, Data, Typeable, Generic, Eq) newtype GBind = GB [[EQual]] deriving (Show, Data, Typeable, Generic) -emptyGMap :: GSolution -> GSolution +emptyGMap :: GSolution -> GSolution emptyGMap sol = mapGMap sol (\(x,_) -> (x, GB []))  updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution-updateGMapWithKey kqs sol = sol {gMap =  foldl (\m (k, (QB eq)) -> M.adjust (\(x, GB eqs) -> (x, GB (if eq `elem` eqs then eqs else eq:eqs))) k m) (gMap sol) kqs } +updateGMapWithKey kqs sol = sol {gMap =  foldl (\m (k, (QB eq)) -> M.adjust (\(x, GB eqs) -> (x, GB (if eq `elem` eqs then eqs else eq:eqs))) k m) (gMap sol) kqs }  qb :: [EQual] -> QBind qb = QB@@ -134,21 +135,24 @@ qbEQuals :: QBind -> [EQual] qbEQuals (QB xs) = xs +qbExprs :: QBind -> [Expr]+qbExprs (QB xs) = eqPred <$> xs+ qbToGb :: QBind -> GBind qbToGb (QB xs) = GB $ map (:[]) xs  gbToQbs :: GBind -> [QBind]-gbToQbs (GB [])  = [QB [trueEqual]] +gbToQbs (GB [])  = [QB [trueEqual]] gbToQbs (GB ess) = QB <$> ess  gbEquals :: GBind -> [[EQual]]-gbEquals (GB eqs) = eqs +gbEquals (GB eqs) = eqs  equalsGb :: [[EQual]] -> GBind-equalsGb = GB +equalsGb = GB  gbFilterM :: Monad m => ([EQual] -> m Bool) -> GBind -> m GBind-gbFilterM f (GB eqs) = GB <$> filterM f eqs +gbFilterM f (GB eqs) = GB <$> filterM f eqs  qbSize :: QBind -> Int qbSize = length . qbEQuals@@ -167,19 +171,18 @@ --   in particular, to compute `lhsPred` for any given constraint. -------------------------------------------------------------------------------- data Sol b a = Sol-  { sEnv  :: !(SEnv Sort)                -- ^ Environment used to elaborate solutions+  { sEnv  :: !SymEnv                     -- ^ Environment used to elaborate solutions   , sMap  :: !(M.HashMap KVar a)         -- ^ Actual solution (for cut kvar)-  , gMap  :: !(M.HashMap KVar b)         -- ^ Solution for gradual variables +  , gMap  :: !(M.HashMap KVar b)         -- ^ Solution for gradual variables   , sHyp  :: !(M.HashMap KVar Hyp)       -- ^ Defining cubes  (for non-cut kvar)-  -- , sBot  :: !(M.HashMap KVar ())        -- ^ set of BOT (cut kvars)   , sScp  :: !(M.HashMap KVar IBindEnv)  -- ^ set of allowed binders for kvar   } -updateGMap :: Sol b a -> M.HashMap KVar b -> Sol b a +updateGMap :: Sol b a -> M.HashMap KVar b -> Sol b a updateGMap sol gmap = sol {gMap = gmap}  -mapGMap :: Sol b a -> (b -> b) -> Sol b a +mapGMap :: Sol b a -> (b -> b) -> Sol b a mapGMap sol f = sol {gMap = M.map f (gMap sol)}  @@ -194,7 +197,7 @@                       }  instance Functor (Sol a) where-  fmap f (Sol e s m1 m2 m3) = Sol e (f <$> s) m1 m2 m3 +  fmap f (Sol e s m1 m2 m3) = Sol e (f <$> s) m1 m2 m3  instance (PPrint a, PPrint b) => PPrint (Sol a b) where   pprintTidy k = pprintTidy k . sMap@@ -227,15 +230,15 @@ resultGradual :: GSolution -> M.HashMap KVar (Expr, [Expr]) -------------------------------------------------------------------------------- resultGradual s = fmap go' (gMap s)-  where -    go' ((_,e), GB eqss) +  where+    go' ((_,e), GB eqss)      = (e, [PAnd $ fmap eqPred eqs | eqs <- eqss])   -------------------------------------------------------------------------------- -- | Create a Solution --------------------------------------------------------- ---------------------------------------------------------------------------------fromList :: SEnv Sort -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> M.HashMap KVar IBindEnv -> Sol a b+fromList :: SymEnv -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> M.HashMap KVar IBindEnv -> Sol a b fromList env kGs kXs kYs = Sol env kXm kGm kYm -- kBm   where     kXm              = M.fromList   kXs@@ -313,7 +316,7 @@   } deriving (Eq, Show, Data, Typeable, Generic)  trueEqual :: EQual-trueEqual = EQL trueQual mempty [] +trueEqual = EQL trueQual mempty []  instance PPrint EQual where   pprintTidy k = pprintTidy k . eqPred

@@ -21,20 +21,31 @@    -- * Embedding to Fixpoint Types     Sort (..)+   , Sub (..)   , FTycon, TCEmb   , sortFTycon-  , intFTyCon, boolFTyCon, realFTyCon, numFTyCon, strFTyCon, setFTyCon  -- TODO: hide these+  , intFTyCon+  , boolFTyCon+  , realFTyCon+  , numFTyCon+  , strFTyCon+  , setFTyCon+  , mapFTyCon -- TODO: hide these -  , intSort, realSort, boolSort, strSort, funcSort+  , basicSorts, intSort, realSort, boolSort, strSort, funcSort   , setSort, bitVecSort, mapSort   , listFTyCon   , isListTC+  , sizeBv   , isFirstOrder   , mappendFTC   , fTyconSymbol, symbolFTycon, fTyconSort, symbolNumInfoFTyCon-  , fApp, fApp', fAppTC+  , fApp+  , fAppTC   , fObj+  , unFApp+  , unAbs    , sortSubst   , functionSort@@ -42,6 +53,12 @@   , bkFFunc    , isNumeric, isReal, isString++  -- * User-defined ADTs+  , DataField (..)+  , DataCtor (..)+  , DataDecl (..)+   ) where  import qualified Data.Binary as B@@ -65,6 +82,8 @@ data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic) type TCEmb a  = M.HashMap a FTycon +instance Symbolic FTycon where+  symbol (TC s _) = symbol s  instance Eq FTycon where   (TC s _) == (TC s' _) = val s == val s'@@ -90,7 +109,8 @@ defRealInfo = False defStrInfo  = False -charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon, strFTyCon, listFTyCon, setFTyCon :: FTycon+charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon+strFTyCon, listFTyCon, mapFTyCon, setFTyCon :: FTycon intFTyCon  = TC (dummyLoc "int"      ) numTcInfo boolFTyCon = TC (dummyLoc "bool"     ) defTcInfo realFTyCon = TC (dummyLoc "real"     ) realTcInfo@@ -100,6 +120,7 @@ listFTyCon = TC (dummyLoc listConName) defTcInfo charFTyCon = TC (dummyLoc "Char"     ) defTcInfo setFTyCon  = TC (dummyLoc setConName ) defTcInfo+mapFTyCon  = TC (dummyLoc mapConName ) defTcInfo  isListConName :: LocSymbol -> Bool isListConName x = c == listConName || c == listLConName --"List"@@ -109,6 +130,14 @@ isListTC :: FTycon -> Bool isListTC (TC z _) = isListConName z +sizeBv :: FTycon -> Maybe Int+sizeBv tc+  | s == size32Name = Just 32+  | s == size64Name = Just 64+  | otherwise       = Nothing+  where+    s               = val $ fTyconSymbol tc+ fTyconSymbol :: FTycon -> Located Symbol fTyconSymbol (TC s _) = s @@ -132,12 +161,20 @@ fAppTC :: FTycon -> [Sort] -> Sort fAppTC = fApp . fTyconSort -fApp' :: Sort -> ListNE Sort-fApp' = go []+-- | fApp' (FApp (FApp "Map" key) val) ===> ["Map", key, val]+--   That is, `fApp'` is used to split a type application into+--   the FTyCon and its args.++unFApp :: Sort -> ListNE Sort+unFApp = go []   where     go acc (FApp t1 t2) = go (t2 : acc) t1     go acc t            = t : acc +unAbs :: Sort -> Sort+unAbs (FAbs _ s) = unAbs s+unAbs s          = s+ fObj :: LocSymbol -> Sort fObj = fTyconSort . (`TC` defTcInfo) @@ -161,10 +198,9 @@     go vs ss (FFunc s1 s2) = go vs (s1:ss) s2     go vs ss t             = (reverse vs, reverse ss, t) ------------------------------------------------------------------------------------------------------- Sorts --------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Sorts ---------------------------------------------------------------------+-------------------------------------------------------------------------------- data Sort = FInt           | FReal           | FNum                 -- ^ numeric kind for Num tyvars@@ -175,11 +211,34 @@           | FAbs  !Int !Sort     -- ^ type-abstraction           | FTC   !FTycon           | FApp  !Sort !Sort    -- ^ constructed type-              deriving (Eq, Ord, Show, Data, Typeable, Generic)+            deriving (Eq, Ord, Show, Data, Typeable, Generic) +data DataField = DField+  { dfName :: !LocSymbol          -- ^ Field Name+  , dfSort :: !Sort               -- ^ Field Sort+  } deriving (Eq, Ord, Show, Data, Typeable, Generic) -isFirstOrder, isFunction :: Sort -> Bool+data DataCtor = DCtor+  { dcName   :: !LocSymbol        -- ^ Ctor Name+  , dcFields :: ![DataField]      -- ^ Ctor Fields+  } deriving (Eq, Ord, Show, Data, Typeable, Generic) +data DataDecl = DDecl+  { ddTyCon :: !FTycon            -- ^ Name of defined datatype+  , ddVars  :: !Int               -- ^ Number of type variables+  , ddCtors :: [DataCtor]         -- ^ Datatype Ctors+  } deriving (Eq, Ord, Show, Data, Typeable, Generic)++instance Symbolic DataDecl where+  symbol = symbol . ddTyCon++instance Symbolic DataField where+  symbol = val . dfName++instance Symbolic DataCtor where+  symbol = val . dcName++isFirstOrder, isFunction :: Sort -> Bool isFirstOrder (FFunc sx s) = not (isFunction sx) && isFirstOrder s isFirstOrder (FAbs _ s)   = isFirstOrder s isFirstOrder (FApp s1 s2) = (not $ isFunction s1) && (not $ isFunction s2)@@ -257,8 +316,10 @@ instance Fixpoint Sort where   toFix = toFixSort ++ toFixSort :: Sort -> Doc-toFixSort (FVar i)     = text "@"   <> parens (toFix i)+toFixSort (FVar i)     = text "@" <> parens (toFix i) toFixSort FInt         = text "int" toFixSort FReal        = text "real" toFixSort FFrac        = text "frac"@@ -267,7 +328,7 @@ toFixSort t@(FAbs _ _) = toFixAbsApp t toFixSort t@(FFunc _ _)= toFixAbsApp t toFixSort (FTC c)      = toFix c-toFixSort t@(FApp _ _) = toFixFApp (fApp' t)+toFixSort t@(FApp _ _) = toFixFApp (unFApp t)  toFixAbsApp :: Sort -> Doc toFixAbsApp t = text "func" <> parens (toFix n <> text ", " <> toFix ts)@@ -280,11 +341,36 @@ toFixFApp [t]        = toFixSort t toFixFApp [FTC c, t]   | isListTC c       = brackets $ toFixSort t-toFixFApp ts         = parens $ intersperse space (toFixSort <$> ts)+toFixFApp ts         = parens $ intersperse (text "") (toFixSort <$> ts)  instance Fixpoint FTycon where-  toFix (TC s _)       = toFix s+  toFix (TC s _)       = toFix (val s) +instance Fixpoint DataField where+  toFix (DField x t) = toFix x <+> text ":" <+> toFix t++instance Fixpoint DataCtor where+  toFix (DCtor x flds) = toFix x <+> braces (intersperse comma (toFix <$> flds))++instance Fixpoint DataDecl where+  toFix (DDecl tc n ctors) = vcat ([header] ++ body ++ [footer])+    where+      header               = {- text "data" <+> -} toFix tc <+> toFix n <+> text "= ["+      body                 = [nest 2 (text "|" <+> toFix ct) | ct <- ctors]+      footer               = text "]"++instance PPrint FTycon where+  pprintTidy _ = toFix++instance PPrint DataField where+  pprintTidy _ = toFix++instance PPrint DataCtor where+  pprintTidy _ = toFix++instance PPrint DataDecl where+  pprintTidy _ = toFix+ ------------------------------------------------------------------------- -- | Exported Basic Sorts ----------------------------------------------- -------------------------------------------------------------------------@@ -315,6 +401,9 @@   | c == numFTyCon  = FNum   | otherwise       = FTC c +basicSorts :: [Sort]+basicSorts = [FInt, boolSort] -- , setSort, mapSort, bitVecSort]+ ------------------------------------------------------------------------ sortSubst                  :: M.HashMap Symbol Sort -> Sort -> Sort ------------------------------------------------------------------------@@ -328,11 +417,21 @@ instance B.Binary FTycon instance B.Binary TCInfo instance B.Binary Sort+instance B.Binary DataField+instance B.Binary DataCtor+instance B.Binary DataDecl instance B.Binary Sub -instance NFData FTycon+instance NFData FTycon where+  rnf (TC x i) = x `seq` i `seq` ()++-- data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic)+ instance NFData TCInfo instance NFData Sort+instance NFData DataField+instance NFData DataCtor+instance NFData DataDecl instance NFData Sub  

@@ -42,6 +42,7 @@ import           Text.Printf -- import           Debug.Trace + ----------------------------------------------------------------------- -- | Located Values --------------------------------------------------- -----------------------------------------------------------------------@@ -167,6 +168,9 @@  instance Hashable SrcSpan where   hashWithSalt i z = hashWithSalt i (sp_start z, sp_stop z)++instance Loc () where+  srcSpan _ = dummySpan  dummySpan :: SrcSpan dummySpan = SS l l

@@ -121,7 +121,7 @@   substf f (PAtom r e1 e2) = PAtom r (substf f e1) (substf f e2)   substf _ p@(PKVar _ _)   = p   substf _  (PAll _ _)     = errorstar "substf: FORALL"-  substf f (PGrad k su e)  = PGrad k su (substf f e)+  substf f (PGrad k su i e)= PGrad k su i (substf f e)   substf _  p              = p  @@ -139,7 +139,7 @@   subst su (PIff p1 p2)    = PIff (subst su p1) (subst su p2)   subst su (PAtom r e1 e2) = PAtom r (subst su e1) (subst su e2)   subst su (PKVar k su')   = PKVar k $ su' `catSubst` su-  subst su (PGrad k su' e) = PGrad k (su' `catSubst` su)  (subst su e)+  subst su (PGrad k su' i e) = PGrad k (su' `catSubst` su) i (subst su e)   subst su (PAll bs p)           | disjoint su bs = PAll bs $ subst su p --(substExcept su (fst <$> bs)) p           | otherwise      = errorstar "subst: PAll (without disjoint binds)"

@@ -0,0 +1,275 @@+{- LANGUAGE FlexibleInstances         #-}+{- LANGUAGE FlexibleContexts          #-}+{- LANGUAGE NoMonomorphismRestriction #-}+{- LANGUAGE OverloadedStrings         #-}+{- LANGUAGE UndecidableInstances      #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE PatternGuards              #-}+{-# LANGUAGE DeriveDataTypeable         #-}++-- | This module contains the types defining an SMTLIB2 interface.++module Language.Fixpoint.Types.Theories (++    -- * Serialized Representation+      Raw++    -- * Theory Symbol+    , TheorySymbol (..)+    , Sem (..)++    -- * Theory Sorts+    , SmtSort (..)+    , sortSmtSort+    , isIntSmtSort++    -- * Symbol Environments+    , SymEnv (..)+    , symEnv+    , symEnvSort+    , symEnvTheory+    , insertSymEnv+    , symbolAtName+    , symbolAtSmtName+++    ) where+++import           Data.Generics             (Data)+import           Data.Typeable             (Typeable)+import           Data.Hashable+import           GHC.Generics              (Generic)+import           Control.DeepSeq+import           Language.Fixpoint.Types.PrettyPrint+import           Language.Fixpoint.Types.Names+import           Language.Fixpoint.Types.Sorts+import           Language.Fixpoint.Types.Errors+import           Language.Fixpoint.Types.Environments++import           Text.PrettyPrint.HughesPJ+import qualified Data.Text.Lazy           as LT+import qualified Data.Binary              as B+import qualified Data.HashMap.Strict      as M+import qualified Language.Fixpoint.Misc   as Misc -- (sortNub, errorstar) -- traceShow)++--------------------------------------------------------------------------------+-- | 'Raw' is the low-level representation for SMT values+--------------------------------------------------------------------------------+type Raw          = LT.Text++--------------------------------------------------------------------------------+-- | 'SymEnv' is used to resolve the 'Sort' and 'Sem' of each 'Symbol'+--------------------------------------------------------------------------------+data SymEnv = SymEnv+  { seSort    :: !(SEnv Sort)              -- ^ Sorts of *all* defined symbols+  , seTheory  :: !(SEnv TheorySymbol)      -- ^ Information about theory-specific Symbols+  , seData    :: !(SEnv DataDecl)          -- ^ User-defined data-declarations+  , seLits    :: !(SEnv Sort)              -- ^ Distinct Constant symbols+  , seAppls   :: !(M.HashMap FuncSort Int) -- ^ Types at which `apply` was used;+                                           --   see [NOTE:apply-monomorphization]+  }+  deriving (Eq, Show, Data, Typeable, Generic)++{- type FuncSort = {v:Sort | isFFunc v} @-}+type FuncSort = (SmtSort, SmtSort)++instance NFData   SymEnv+instance B.Binary SymEnv++instance Monoid SymEnv where+  mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv mempty+  mappend e1 e2 = SymEnv { seSort   = seSort   e1 `mappend` seSort   e2+                         , seTheory = seTheory e1 `mappend` seTheory e2+                         , seData   = seData   e1 `mappend` seData   e2+                         , seLits   = seLits   e1 `mappend` seLits   e2+                         , seAppls  = seAppls  e1 `mappend` seAppls  e2+                         }++symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv+symEnv xEnv fEnv ds ls ts = SymEnv xEnv' fEnv dEnv ls sortMap+  where+    xEnv'                 = unionSEnv xEnv wiredInEnv+    dEnv                  = fromListSEnv [(symbol d, d) | d <- ds]+    sortMap               = M.fromList (zip smts [0..])+    smts                  = funcSorts dEnv ts -- tracepp "smt-apply-sorts" $ Misc.sortNub $ (SInt, SInt) : [ (tx t1, tx t2) | FFunc t1 t2 <- ts]++-- | These are "BUILT-in" polymorphic functions which are+--   UNININTERPRETED but POLYMORPHIC, hence need to go through+--   the apply-defunc stuff.++wiredInEnv :: M.HashMap Symbol Sort+wiredInEnv = M.fromList [(toIntName, mkFFunc 1 [FVar 0, FInt])]+++-- | 'smtSorts' attempts to compute a list of all the input-output sorts+--   at which applications occur. This is a gross hack; as during unfolding+--   we may create _new_ terms with wierd new sorts. Ideally, we MUST allow+--   for EXTENDING the apply-sorts with those newly created terms.+--   the solution is perhaps to *preface* each VC query of the form+--+--      push+--      assert p+--      check-sat+--      pop+--+--   with the declarations needed to make 'p' well-sorted under SMT, i.e.+--   change the above to+--+--      declare apply-sorts+--      push+--      assert p+--      check-sat+--      pop+--+--   such a strategy would NUKE the entire apply-sort machinery from the CODE base.+--   [TODO]: dynamic-apply-declaration++funcSorts :: SEnv a -> [Sort] -> [FuncSort]+funcSorts dEnv ts = [ (t1, t2) | t1 <- smts, t2 <- smts]+  where+    smts         = Misc.sortNub $ concat [ [tx t1, tx t2] | FFunc t1 t2 <- ts]+    tx           = applySmtSort dEnv+++symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol+symEnvTheory x env = lookupSEnv x (seTheory env)++symEnvSort :: Symbol -> SymEnv -> Maybe Sort+symEnvSort   x env = lookupSEnv x (seSort env)++insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv+insertSymEnv x t env = env { seSort = insertSEnv x t (seSort env) }++symbolAtName :: (PPrint a) => Symbol -> SymEnv -> a -> Sort -> Symbol+symbolAtName mkSym env e = symbolAtSmtName mkSym env e . ffuncSort env++symbolAtSmtName :: (PPrint a) => Symbol -> SymEnv -> a -> FuncSort -> Symbol+symbolAtSmtName mkSym env e = intSymbol mkSym . funcSortIndex env e++funcSortIndex :: (PPrint a) => SymEnv -> a -> FuncSort -> Int+funcSortIndex env e z = M.lookupDefault err z (seAppls env)+  where+    err               = panic ("Unknown func-sort: " ++ showpp z ++ " for " ++ showpp e)++ffuncSort :: SymEnv -> Sort -> FuncSort+ffuncSort env t      = (tx t1, tx t2)+  where+    tx               = applySmtSort (seData env)+    (t1, t2)         = args t+    args (FFunc a b) = (a, b)+    args _           = (FInt, FInt)++applySmtSort :: SEnv a -> Sort -> SmtSort+applySmtSort = sortSmtSort False++isIntSmtSort :: SEnv a -> Sort -> Bool+isIntSmtSort env s = SInt == applySmtSort env s++--------------------------------------------------------------------------------+-- | 'TheorySymbol' represents the information about each interpreted 'Symbol'+--------------------------------------------------------------------------------+data TheorySymbol  = Thy+  { tsSym    :: !Symbol          -- ^ name+  , tsRaw    :: !Raw             -- ^ serialized SMTLIB2 name+  , tsSort   :: !Sort            -- ^ sort+  , tsInterp :: !Sem             -- ^ TRUE = defined (interpreted), FALSE = declared (uninterpreted)+  }+  deriving (Eq, Ord, Show, Data, Typeable, Generic)++instance NFData Sem+instance NFData TheorySymbol+instance B.Binary TheorySymbol++instance PPrint Sem where+  pprintTidy _ = text . show++instance Fixpoint TheorySymbol where+  toFix (Thy x _ t d) = text "TheorySymbol" <+> pprint (x, t) <+> parens (pprint d)++instance PPrint TheorySymbol where+  pprintTidy k (Thy x _ t d) = text "TheorySymbol" <+> pprintTidy k (x, t) <+> parens (pprint d)++--------------------------------------------------------------------------------+-- | 'Sem' describes the SMT semantics for a given symbol+--------------------------------------------------------------------------------++data Sem+  = Uninterp                     -- ^ for UDF: `len`, `height`, `append`+  | Data                         -- ^ for ADT ctors & accessor: `cons`, `nil`, `head`+  | Theory                       -- ^ for theory ops: mem, cup, select+  deriving (Eq, Ord, Show, Data, Typeable, Generic)++instance B.Binary Sem+++--------------------------------------------------------------------------------+-- | A Refinement of 'Sort' that describes SMTLIB Sorts+--------------------------------------------------------------------------------+data SmtSort+  = SInt+  | SBool+  | SReal+  | SString+  | SSet+  | SMap+  | SBitVec !Int+  | SVar    !Int+  | SData   !FTycon ![SmtSort]+  -- HKT | SApp            ![SmtSort]           -- ^ Representing HKT+  deriving (Eq, Ord, Show, Data, Typeable, Generic)++instance Hashable SmtSort+instance NFData   SmtSort+instance B.Binary SmtSort++-- | 'smtSort True  msg t' serializes a sort 't' using type variables,+--   'smtSort False msg t' serializes a sort 't' using 'Int' instead of tyvars.++sortSmtSort :: Bool -> SEnv a -> Sort -> SmtSort+sortSmtSort poly env  = go+  where+    go (FFunc _ _)    = SInt+    go FInt           = SInt+    go FReal          = SReal+    go t+      | t == boolSort = SBool+    go (FVar i)+      | poly          = SVar i+      | otherwise     = SInt+    go t              = fappSmtSort poly env ct ts where (ct:ts)= unFApp t++fappSmtSort :: Bool -> SEnv a -> Sort -> [Sort] -> SmtSort+fappSmtSort poly env = go+  where+-- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))+    go (FTC c) _+      | setConName == symbol c  = SSet+    go (FTC c) _+      | mapConName == symbol c  = SMap+    go (FTC bv) [FTC s]+      | bitVecName == symbol bv+      , Just n <- sizeBv s      = SBitVec n+    go s []+      | isString s              = SString+    go (FTC c) ts+      | symEnvData c env        = SData c (sortSmtSort poly env <$> ts)+    go _ _                      = SInt++symEnvData :: (Symbolic x) => x -> SEnv a -> Bool+symEnvData = memberSEnv . symbol++instance PPrint SmtSort where+  pprintTidy _ SInt         = text "Int"+  pprintTidy _ SBool        = text "Bool"+  pprintTidy _ SReal        = text "Real"+  pprintTidy _ SString      = text "Str"+  pprintTidy _ SSet         = text "Set"+  pprintTidy _ SMap         = text "Map"+  pprintTidy _ (SBitVec n)  = text "BitVec" <+> int n+  pprintTidy _ (SVar i)     = text "@" <> int i+--  HKT pprintTidy k (SApp ts)    = ppParens k (pprintTidy k tyAppName) ts+  pprintTidy k (SData c ts) = ppParens k (pprintTidy k c)         ts++ppParens :: (PPrint d) => Tidy -> Doc -> [d] -> Doc+ppParens k d ds = parens $ Misc.intersperse (text "") (d : (pprintTidy k <$> ds))