summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/Epic/Forcing.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Compiler/Epic/Forcing.hs')
-rw-r--r--src/full/Agda/Compiler/Epic/Forcing.hs9
1 files changed, 4 insertions, 5 deletions
diff --git a/src/full/Agda/Compiler/Epic/Forcing.hs b/src/full/Agda/Compiler/Epic/Forcing.hs
index 41992f5..18b5394 100644
--- a/src/full/Agda/Compiler/Epic/Forcing.hs
+++ b/src/full/Agda/Compiler/Epic/Forcing.hs
@@ -1,6 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE FlexibleContexts #-}
module Agda.Compiler.Epic.Forcing where
@@ -141,7 +140,7 @@ insertTele er n ins term (ExtendTel x xs) = do
-- TODO: restore fields in ConHead
mkCon :: QName -> Int -> Term
-mkCon c n = I.Con (I.ConHead c Inductive []) $ map (defaultArg . I.var) $ downFrom n
+mkCon c n = I.Con (I.ConHead c Inductive []) ConOSystem $ map (defaultArg . I.var) $ downFrom n
unifyI :: Telescope -> FlexibleVars -> Type -> Args -> Args -> Compile TCM [Maybe Term]
unifyI tele flex typ a1 a2 = lift $ typeError $ NotImplemented "using the new unification algorithm for forcing"
@@ -285,7 +284,7 @@ replaceForced (vars,uvars) tele (fvar : fvars) unif e = do
buildTerm :: Var -> Nat -> Term -> Compile TCM (Expr -> Expr, Var)
buildTerm var idx (I.Shared p) = buildTerm var idx $ I.derefPtr p
buildTerm var idx (I.Var i _) | idx == i = return (id, var)
-buildTerm var idx (I.Con con args) = do
+buildTerm var idx (I.Con con _ args) = do
let c = I.conName con
vs <- replicateM (length args) newName
(pos , arg) <- fromMaybe __IMPOSSIBLE__ <$> findPosition idx (map (Just . unArg) args)
@@ -308,7 +307,7 @@ findPosition var ts = (listToMaybe . catMaybes <$>) . forM (zip [0..] ts) $ \ (n
pred :: Term -> Compile TCM Bool
pred t = case I.ignoreSharing t of
I.Var i _ | var == i -> return True
- I.Con c args -> do
+ I.Con c _ args -> do
forc <- getForcedArgs $ I.conName c
or <$> mapM (pred . unArg) (notForced forc args)
- _ -> return False
+ _ -> return False