Skip to content

Enable choice of term ordering for REST #1930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
zgrannan wants to merge 13 commits into
base: develop
Choose a base branch
from
Open

Enable choice of term ordering for REST #1930

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
000c0ab
Allow different ordering constraints
zgrannan Nov 9, 2021
03505b4
Update liquid-fixpoint
zgrannan Nov 23, 2021
f90b8c8
Merge remote-tracking branch 'upstream/develop' into rest2
zgrannan Feb 8, 2022
a0e764b
Update Liquid-Fixpoint, REST
zgrannan Feb 8, 2022
809b4e9
Update fixpoint
zgrannan Feb 10, 2022
c1f66d4
Update fixpoint, add KBO test
zgrannan Feb 11, 2022
97d716c
Update fixpoint
zgrannan Feb 11, 2022
1c44174
Merge remote-tracking branch 'upstream/develop' into upgrade-rest
zgrannan Feb 11, 2022
2c262e4
Slightly improve help message
zgrannan Feb 11, 2022
d971c6d
Update docs/mkDocs/docs/options.md
zgrannan Feb 14, 2022
3329bfa
Merge
zgrannan Feb 14, 2022
b0c7f57
Merge remote-tracking branch 'origin/upgrade-rest' into upgrade-rest
zgrannan Feb 14, 2022
406fad0
Update fixpoint
zgrannan Feb 15, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion liquid-fixpoint
Open in desktop
Submodule liquid-fixpoint updated 4 files
+19 −14 src/Language/Fixpoint/Solver/PLE.hs
+40 −7 src/Language/Fixpoint/Solver/Rewrite.hs
+29 −0 src/Language/Fixpoint/Types/Config.hs
+2 −2 stack.yaml
1 change: 1 addition & 0 deletions src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ fixConfig tgt cfg = def
, FC.fuel = fuel cfg
, FC.noEnvironmentReduction = not (environmentReduction cfg)
, FC.inlineANFBindings = inlineANFBindings cfg
, FC.restOrdering = read (restOrdering cfg)
}

cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo)
Expand Down
7 changes: 6 additions & 1 deletion src/Language/Haskell/Liquid/UX/CmdLine.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,11 @@ config = cmdArgsMode $ Config {
, "Sometimes improves performance and sometimes worsens it."
, "Disabled by --no-environment-reduction"
])
, pandocHtml
, restOrdering
= "rpo"
&= name "rest-ordering"
&= help "Ordering Constraints Algebra to use for REST"
, pandocHtml
= False
&= name "pandoc-html"
&= help "Use pandoc to generate html."
Expand Down Expand Up @@ -720,6 +724,7 @@ defConfig = Config
, environmentReduction = False
, noEnvironmentReduction = False
, inlineANFBindings = False
, restOrdering = "rpo"
, pandocHtml = False
}

Expand Down
1 change: 1 addition & 0 deletions src/Language/Haskell/Liquid/UX/Config.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,7 @@ data Config = Config
, noEnvironmentReduction :: Bool -- ^ Don't perform environment reduction
, inlineANFBindings :: Bool -- ^ Inline ANF bindings.
-- Sometimes improves performance and sometimes worsens it.
, restOrdering :: String -- ^ The ordering to use for REST
, pandocHtml :: Bool -- ^ Use pandoc to generate html
} deriving (Generic, Data, Typeable, Show, Eq)

Expand Down
4 changes: 2 additions & 2 deletions stack.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ packages:
- .
extra-deps:
- hashable-1.3.0.0
- git: https://github.com/facundominguez/rest
commit: 31e974979c90e910efe5199ee0d3721b791667f6
- git: https://github.com/zgrannan/rest
commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6

resolver: lts-18.14
compiler: ghc-8.10.7
Expand Down
14 changes: 7 additions & 7 deletions stack.yaml.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,15 @@ packages:
hackage: hashable-1.3.0.0
- completed:
name: rest-rewrite
version: 0.2.0
git: https://github.com/facundominguez/rest
version: 0.2.1
git: https://github.com/zgrannan/rest
pantry-tree:
size: 4013
sha256: 2a91674ccab6b0bd43dcc41fa5e2cb60cbfd35ad585df8293c2884466091d0c0
commit: 31e974979c90e910efe5199ee0d3721b791667f6
size: 4368
sha256: 725fad92ed6299d02fb26aec13b6dd383be111f09377532363277228d2c28658
commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6
original:
git: https://github.com/facundominguez/rest
commit: 31e974979c90e910efe5199ee0d3721b791667f6
git: https://github.com/zgrannan/rest
commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6
snapshots:
- completed:
size: 586069
Expand Down