NotificationsYou must be signed in to change notification settings
Fork149
Star1.3k

Commit9e1d8b7

authored

Merge pull request#2589 from ucsd-progsys/fd/remove-pgrad2

Update LF after second round of PGrad removal

2 parents1fe3372 +755b72c commit9e1d8b7Copy full SHA for 9e1d8b7

File tree

14 files changed

-222

lines changed

liquid-fixpoint
liquidhaskell-boot/src/Language/Haskell/Liquid
- Constraint
  - Generate.hs
  - ToFixpoint.hs
- UX
  - CmdLine.hs
  - Config.hs
tests/gradual
- neg
- pos
- todo
  - Measures.hs

14 files changed

-222

lines changed

`‎liquid-fixpoint‎`

Submoduleliquid-fixpoint updated12 files

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs‎`

Lines changed: 1 addition & 2 deletions

Original file line number	Diff line number	Diff line change
`@@ -69,7 +69,7 @@ import Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult, r`
`69`	`69`	`importLanguage.Haskell.Liquid.Bare.DataType (dataConMap,makeDataConChecker)`
`70`	`70`	`importLanguage.Haskell.Liquid.UX.Config`
`71`	`71`	`(HasConfig(getConfig),`
`72`		`-Config(typeclass,gradual,checkDerived,extensionality,`
	`72`	`+Config(typeclass,checkDerived,extensionality,`
`73`	`73`	`nopolyinfer,noADT,dependantCase,exactDC,rankNTypes),`
`74`	`74`	`patternFlag,`
`75`	`75`	`higherOrderFlag )`
`@@ -88,7 +88,6 @@ consAct :: CGEnv -> Config -> TargetInfo -> CG ()`
`88`	`88`	`consAct γ cfg info=do`
`89`	`89`	`let sSpc= gsSig. giSpec$ info`
`90`	`90`	`let gSrc= giSrc info`
`91`		`- when (gradual cfg) (mapM_ (addW.WfC γ. val.snd) (gsTySigs sSpc++ gsAsmSigs sSpc))`
`92`	`91`	`γ'<- foldM (consCBTop cfg info) γ (giCbs gSrc)`
`93`	`92`	`-- Relational Checking: the following only runs when the list of relational specs is not empty`
`94`	`93`	`(ψ, γ'')<- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc++ gsRelation sSpc)`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs‎`

Lines changed: 0 additions & 2 deletions

Original file line number	Diff line number	Diff line change
`@@ -54,8 +54,6 @@ fixConfig tgt cfg = def`
`54`	`54`	`,FC.allowHOqs= higherorderqs cfg`
`55`	`55`	`,FC.smtTimeout= smtTimeout cfg`
`56`	`56`	`,FC.stringTheory= stringTheory cfg`
`57`		`- ,FC.gradual= gradual cfg`
`58`		`- ,FC.ginteractive= ginteractive cfg`
`59`	`57`	`,FC.noslice= noslice cfg`
`60`	`58`	`,FC.rewriteAxioms= allowPLE cfg`
`61`	`59`	`,FC.pleUndecGuards= pleWithUndecidedGuards cfg`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs‎`

Lines changed: 0 additions & 13 deletions

Original file line number	Diff line number	Diff line change
`@@ -165,23 +165,10 @@ defConfig = Config {`
`165`	`165`	`= def&= name"no-structural-termination"`
`166`	`166`	`&= help"Disable structural termination check"`
`167`	`167`
`168`		`- , gradual`
`169`		`-=False&= help"Enable gradual refinement type checking"`
`170`		`-&= name"gradual"`
`171`		`-`
`172`	`168`	`, bscope`
`173`	`169`	`=False&= help"scope of the outer binders on the inner refinements"`
`174`	`170`	`&= name"bscope"`
`175`	`171`
`176`		`- , gdepth`
`177`		`-=1`
`178`		`-&= help"Size of gradual conretizations, 1 by default"`
`179`		`-&= name"gradual-depth"`
`180`		`-`
`181`		`- , ginteractive`
`182`		`-=False&= help"Interactive Gradual Solving"`
`183`		`-&= name"ginteractive"`
`184`		`-`
`185`	`172`	`, totalHaskell`
`186`	`173`	`=False&= help"Check for termination and totality; overrides no-termination flags"`
`187`	`174`	`&= name"total-Haskell"`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs‎`

Lines changed: 0 additions & 3 deletions

Original file line number	Diff line number	Diff line change
`@@ -56,10 +56,7 @@ data Config = Config`
`56`	`56`	`,noclasscheck::Bool--^ disable checking class instances`
`57`	`57`	`-- , structuralTerm :: Bool -- ^ use structural termination checker`
`58`	`58`	`,nostructuralterm::Bool--^ disable structural termination check`
`59`		`- ,gradual::Bool--^ enable gradual type checking`
`60`	`59`	`,bscope::Bool--^ scope of the outer binders on the inner refinements`
`61`		`- ,gdepth::Int--^ depth of gradual concretization`
`62`		`- ,ginteractive::Bool--^ interactive gradual solving`
`63`	`60`	`,totalHaskell::Bool--^ Check for termination and totality, Overrides no-termination flags`
`64`	`61`	`,nowarnings::Bool--^ disable warnings output (only show errors)`
`65`	`62`	`,noannotations::Bool--^ disable creation of intermediate annotation files`

`‎tests/gradual/neg/Gradual.hs‎`

Lines changed: 0 additions & 18 deletions

This file was deleted.

`‎tests/gradual/neg/Interpretations.hs‎`

Lines changed: 0 additions & 18 deletions

This file was deleted.

`‎tests/gradual/neg/Intro.hs‎`

Lines changed: 0 additions & 34 deletions

This file was deleted.

`‎tests/gradual/pos/Discussion.hs‎`

Lines changed: 0 additions & 35 deletions

This file was deleted.

`‎tests/gradual/pos/Dynamic.hs‎`

Lines changed: 0 additions & 14 deletions

This file was deleted.

0 commit comments

Comments

(0)

Movatterモバイル変換

Navigation Menu

Search code, repositories, users, issues, pull requests...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Commit9e1d8b7

File tree

14 files changed

14 files changed

`‎liquid-fixpoint‎`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs‎`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs‎`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs‎`

`‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs‎`

`‎tests/gradual/neg/Gradual.hs‎`

`‎tests/gradual/neg/Interpretations.hs‎`

`‎tests/gradual/neg/Intro.hs‎`

`‎tests/gradual/pos/Discussion.hs‎`

`‎tests/gradual/pos/Dynamic.hs‎`

0 commit comments