Interpreter only on LHS

src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -1180,7 +1180,7 @@ caseEnv γ x _   (DataAlt c) ys pIs = do
   let ys''         = F.symbol <$> filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) ys
   let r1           = dataConReft   c   ys''
   let r2           = dataConMsReft rtd ys''
-  let xt           = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2))
+  xt              <- markDataConType ((xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2)))
   let cbs          = safeZip "cconsCase" (x':ys') (xt0 : yts)
   cγ'             <- addBinders γ   x' cbs
   addBinders cγ' x' [(x', xt)]
@@ -1192,6 +1192,12 @@ caseEnv γ x acs a _ _ = do
   cγ     <- addBinders γ x' [(x', xt')]
   return cγ
 
+
+markDataConType :: (TyConable c, F.Reftable (f1 F.Reft), Functor f1) 
+                =>  RType c tv (f1 F.Reft) -> CG (RType c tv (f1 F.Reft))
+markDataConType t@(RApp _ _ _ _) = (shiftVV t . F.dataconSymbol) <$> fresh
+markDataConType t                = return t 
+
 --------------------------------------------------------------------------------
 -- | `projectTypes` masks (i.e. true's out) all types EXCEPT those
 --   at given indices; it is used to simplify the environment used

src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs

@@ -58,6 +58,7 @@ fixConfig tgt cfg = def
   , FC.oldPLE                   = oldPLE cfg
   , FC.rwTerminationCheck       = rwTerminationCheck cfg
   , FC.noLazyPLE                = noLazyPLE cfg
+  , FC.useInterpreter           = useInterpreter cfg
   , FC.fuel                     = fuel      cfg
   , FC.noEnvironmentReduction   = not (environmentReduction cfg)
   , FC.inlineANFBindings        = inlineANFBindings cfg

src/Language/Haskell/Liquid/Types/Types.hs

@@ -1090,6 +1090,9 @@ instance F.Fixpoint RTyCon where
 instance F.Fixpoint BTyCon where
   toFix = text . F.symbolString . F.val . btc_tc
 
+instance F.PPrint Cinfo where
+  pprintTidy _ = text . show
+
 instance F.Fixpoint Cinfo where
   toFix = text . showPpr . ci_loc
 

src/Language/Haskell/Liquid/UX/CmdLine.hs

@@ -437,6 +437,12 @@ config = cmdArgsMode $ Config {
         &= explicit
         &= name "no-environment-reduction"
         &= help "Don't perform environment reduction"
+  , useInterpreter
+    = def
+        &= explicit
+        &= help "Interpretation of reflected functions"
+        &= name "interpreter"
+
   , inlineANFBindings
     = False
         &= explicit
@@ -702,6 +708,7 @@ defConfig = Config
   , environmentReduction     = False
   , noEnvironmentReduction   = False
   , inlineANFBindings        = False
+  , useInterpreter           = False
   }
 
 

src/Language/Haskell/Liquid/UX/Config.hs

@@ -97,6 +97,7 @@ data Config = Config
   , maxMatchDepth            :: Int
   , maxAppDepth              :: Int
   , maxArgsDepth             :: Int
+  , useInterpreter           :: Bool
   , rwTerminationCheck       :: Bool       -- ^ Enable termination checking for rewriting
   , skipModule               :: Bool       -- ^ Skip this module entirely (don't even compile any specs in it)
   , noLazyPLE                :: Bool

tests/interpreter/neg/Fib.hs

@@ -0,0 +1,19 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--no-termination" @-}
+{-@ LIQUID "--reflection"  @-}
+{-@ LIQUID "--ple"         @-}
+{-@ LIQUID "--interpreter" @-}
+
+module Fib where
+
+
+{-@ thm :: () -> {fib 7 = 24} @-}
+thm :: () -> ()
+thm _ = ()
+
+{-@ reflect fib @-}
+fib :: Int -> Int 
+fib 0 = 0 
+fib 1 = 1 
+fib i = fib (i-1) + fib (i-2)

tests/interpreter/pos/Fib.hs

@@ -0,0 +1,24 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--no-termination" @-}
+{-@ LIQUID "--reflection"  @-}
+{-@ LIQUID "--ple"         @-}
+{-@ LIQUID "--interpreter" @-}
+
+module Fib where
+
+
+{-@ thm10 :: () -> {fib 10 = 55} @-}
+thm10 :: () -> ()
+thm10 _ = ()
+
+{-@ thm7 :: () -> {fib 7 = 13} @-}
+thm7 :: () -> ()
+thm7 _ = ()
+
+
+{-@ reflect fib @-}
+fib :: Int -> Int 
+fib 0 = 0 
+fib 1 = 1 
+fib i = fib (i-1) + fib (i-2)

tests/interpreter/pos/LambdaToy.hs

@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTs #-}
+
+{-@ LIQUID "--no-termination" @-}
+{-@ LIQUID "--reflection"  @-}
+{-@ LIQUID "--ple"         @-}
+{-@ LIQUID "--interpreter" @-}
+
+module LambdaToy where
+
+{-@ reflect isPred @-}
+{-@ isPred :: e:Expr -> { b:Bool | (isTerm e => b) } @-}
+isPred :: Expr -> Bool --     (outside of refinements of course)
+isPred (Bc _)           = True
+isPred (App e e')       = isTerm e && isTerm e'
+
+
+
+
+data Expr = Bc Bool                   -- True, False
+          | App Expr Expr             -- e e'          applications
+{-@ type Term = { e:Expr | isTerm e } @-}
+
+{-@ reflect isTerm @-} -- a legal program term is an expression that does not contain Conj
+{-@ isTerm :: e:Expr -> { b:Bool | b => isPred e } @-}
+isTerm :: Expr -> Bool --     (outside of refinements of course)
+isTerm (Bc _)           = True
+isTerm (App e e')       = isTerm e && isTerm e'
+

tests/test.hs

@@ -290,6 +290,8 @@ microTests = group "Micro"
   , mkMicroNeg "absref-neg"     "tests/absref/neg"
   -- , mkMicroPos "import-lib"     "tests/import/lib"      -- NOT disabled; but via CHECK-IMPORTS
   , mkMicroPos "import-cli"     "tests/import/client"
+  , mkMicroPos "interpreter-pos"    "tests/interpreter/pos"
+  , mkMicroNeg "interpreter-neg"    "tests/interpreter/neg"
   , mkMicroPos "class-pos"      "tests/classes/pos"
   , mkMicroNeg "class-neg"      "tests/classes/neg"
   , mkMicroPos "ple-pos"        "tests/ple/pos"