oquechy · oquechy · Dec 5, 2022 · Dec 5, 2022 · Dec 5, 2022 · Dec 9, 2022
diff --git a/.gitignore b/.gitignore
@@ -61,3 +61,5 @@ tests/**/*.o-boot
 
 .idea
 *.iml
+
+.DS_Store
diff --git a/liquid-fixpoint b/liquid-fixpoint
diff --git a/src-ghc/Liquid/GHC/Misc.hs b/src-ghc/Liquid/GHC/Misc.hs
@@ -97,6 +97,20 @@ stringVar s t = mkLocalVar VanillaId name Many t vanillaIdInfo
       name = mkInternalName (mkUnique 'x' 25) occ noSrcSpan
       occ  = mkVarOcc s
 
+mkLocVar :: Int -> String -> Type -> Var
+mkLocVar i s t = mkLocalVar VanillaId name Many t vanillaIdInfo
+  where
+    name   = mkInternalName unique occ noSrcSpan
+    unique = mkLocalUnique i
+    occ    = mkVarOcc s
+
+{-
+Taken from GHC.Types.Unique
+url: https://hackage.haskell.org/package/ghc-9.4.4/docs/src/GHC.Types.Unique.html#Unique
+-}
+mkLocalUnique :: Int -> Unique
+mkLocalUnique i = mkUnique 'X' i
+
 -- FIXME: plugging in dummy type like this is really dangerous
 maybeAuxVar :: Symbol -> Maybe Var
 maybeAuxVar s

diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -91,7 +91,8 @@ consAct γ cfg info = do
   when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc))
   γ' <- foldM (consCBTop cfg info) γ (giCbs gSrc)
   (ψ, γ'') <- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc ++ gsRelation sSpc)
-  mapM_ (consRelTop cfg info γ'' ψ) (gsRelation sSpc)
+  relErrs <- gets relWf
+  mapM_ (consRelTop cfg info cconsE consE γ'' ψ) (if null relErrs then gsRelation sSpc else [])
   mapM_ (consClass γ) (gsMethods $ gsSig $ giSpec info)
   hcs <- gets hsCs
   hws <- gets hsWfs

diff --git a/src/Language/Haskell/Liquid/Constraint/Init.hs b/src/Language/Haskell/Liquid/Constraint/Init.hs
@@ -38,6 +38,8 @@ import           Language.Haskell.Liquid.Constraint.Types
 
 import           Language.Haskell.Liquid.Types hiding (binds, Loc, loc, freeTyVars, Def)
 
+import qualified Text.PrettyPrint.HughesPJ    as Doc
+
 --------------------------------------------------------------------------------
 initEnv :: TargetInfo -> CG CGEnv
 --------------------------------------------------------------------------------
@@ -260,6 +262,8 @@ initCGI cfg info = CGInfo {
   , ebinds     = []
   , annotMap   = AI M.empty
   , holesMap   = M.empty
+  , relHints   = Doc.empty
+  , relWf      = []
   , newTyEnv   = M.fromList (mapSnd val <$> gsNewTypes (gsSig spc))
   , tyConInfo  = tyi
   , tyConEmbed = tce
Original file line number	Diff line number	Diff line change
Expand Up		@@ -61,3 +61,5 @@ tests/*/.o-boot

		.idea
		*.iml

		.DS_Store
+10 −4		.github/workflows/cabal.yml
+1 −1		.github/workflows/hlint.yml
+3 −3		.github/workflows/stack.yml
+49 −0		.github/workflows/stan.yml
+3 −0		.gitignore
+125 −0		.stan.toml
+7 −12		README.md
+43 −0		flake.lock
+109 −0		flake.nix
+6 −2		liquid-fixpoint.cabal
+0 −2		nixpkgs.nix
+0 −16		shell-stack.nix
+0 −25		shell.nix
+4 −1		src/Language/Fixpoint/Defunctionalize.hs
+4 −6		src/Language/Fixpoint/Graph/Partition.hs
+3 −3		src/Language/Fixpoint/Horn/Transformations.hs
+2 −26		src/Language/Fixpoint/Misc.hs
+1 −1		src/Language/Fixpoint/Parse.hs
+2 −1		src/Language/Fixpoint/Smt/Bitvector.hs
+19 −25		src/Language/Fixpoint/Smt/Interface.hs
+102 −3		src/Language/Fixpoint/Smt/Theories.hs
+4 −3		src/Language/Fixpoint/Smt/Types.hs
+5 −4		src/Language/Fixpoint/Solver/Extensionality.hs
+3 −5		src/Language/Fixpoint/Solver/Instantiate.hs
+18 −31		src/Language/Fixpoint/Solver/PLE.hs
+1 −0		src/Language/Fixpoint/Solver/Sanitize.hs
+1 −0		src/Language/Fixpoint/Types/Constraints.hs
+1 −1		src/Language/Fixpoint/Types/Errors.hs
+5 −3		src/Language/Fixpoint/Types/Refinements.hs
+1 −1		src/Language/Fixpoint/Types/Solutions.hs
+2 −2		src/Language/Fixpoint/Types/Sorts.hs
+4 −19		src/Language/Fixpoint/Types/Visitor.hs
+1 −0		src/Language/Fixpoint/Utils/Builder.hs
+1 −2		stack.yaml
+9 −0		tests/neg/maps02.fq
+16 −0		tests/pos/maps02.fq
+10 −0		tests/pos/maps03.fq
+39 −0		tests/pos/maps04.fq
+9 −0		tests/pos/maps05.fq
+1 −1		tests/test.hs