Fixing handling of LH assumption arguments

BillHallahan · Oct 2, 2024 · eca8a69 · eca8a69
1 parent 1beadde
commit eca8a69
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/G2/Liquid/Conversion.hs b/src/G2/Liquid/Conversion.hs
@@ -44,6 +44,8 @@ import qualified Data.Map as M
 import Data.Maybe
 import qualified Data.Text as T
 
+import Debug.Trace
+
 -- | A mapping of TyVar Name's, to Id's for the LH dict's
 type LHDictMap = HM.HashMap Name Id
 

diff --git a/src/G2/Liquid/ConvertCurrExpr.hs b/src/G2/Liquid/ConvertCurrExpr.hs
@@ -204,10 +204,11 @@ addCurrExprAssumption ifi (Bindings {fixed_inputs = fi}) = do
  -- fi <- fixedInputs
  eenv <- exprEnv
  inames <- inputNames
+ let inames' = take (length $ argumentTypes ifi) inames
 
  lh <- mapM (lhTCDict' HM.empty) $ mapMaybe typeType fi'
 
- let is = catMaybes (map (E.getIdFromName eenv) inames) 
+ let is = catMaybes (map (E.getIdFromName eenv) inames') 
  let (typs, ars) = span isType $ fi' ++ map Var is
 
  case assumpt of