summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs35
1 files changed, 13 insertions, 22 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
index d96198a..543118d 100644
--- a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
+++ b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
@@ -9,6 +9,7 @@ module Agda.TypeChecking.Rules.Builtin.Coinduction where
import Control.Applicative
import qualified Data.Map as Map
+import qualified Data.Set as Set
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
@@ -82,7 +83,6 @@ bindBuiltinSharp e =
, recInduction = Just CoInductive
, recClause = Nothing
, recConHead = ConHead sharp CoInductive [] -- flat is added later
- , recConType = sharpType
, recNamedCon = True
, recFields = [] -- flat is added later
, recTel = fieldTel
@@ -99,6 +99,7 @@ bindBuiltinSharp e =
, conData = defName infDefn
, conAbstr = ConcreteDef
, conInd = CoInductive
+ , conErased = []
}
}
return sharpE
@@ -130,8 +131,8 @@ bindBuiltinFlat e =
{ clauseRange = noRange
, clauseTel = tel
, namedClausePats = [ argN $ Named Nothing $
- ConP sharpCon cpi [ argN $ Named Nothing $ VarP (0,"x") ] ]
- , clauseBody = Bind $ Abs "x" $ Body $ var 0
+ ConP sharpCon cpi [ argN $ Named Nothing $ debruijnNamedVar "x" 0 ] ]
+ , clauseBody = Just $ var 0
, clauseType = Just $ defaultArg $ El (varSort 2) $ var 1
, clauseCatchall = False
}
@@ -141,30 +142,20 @@ bindBuiltinFlat e =
Map.empty
Nothing
projection = Projection
- { projProper = Just flat
- , projFromType = inf
+ { projProper = True
+ , projOrig = flat
+ , projFromType = defaultArg inf
, projIndex = 3
- , projDropPars = teleNoAbs (take 2 $ telToList tel) $ Lam defaultArgInfo $ Abs "x" $ Var 0 [Proj flat]
- , projArgInfo = defaultArgInfo
+ , projLams = ProjLams $ [ argH "a" , argH "A" , argN "x" ]
}
addConstant flat $
flatDefn { defPolarity = []
, defArgOccurrences = [StrictPos] -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
- , theDef = Function
- { funClauses = [clause]
- , funCompiled = Just $ cc
- , funTreeless = Nothing
- , funInv = NotInjective
- , funMutual = []
- , funAbstr = ConcreteDef
- , funDelayed = NotDelayed
- , funProjection = Just projection
- , funSmashable = False
- , funStatic = False
- , funInline = False
- , funTerminates = Just True
- , funExtLam = Nothing
- , funWith = Nothing
+ , theDef = emptyFunction
+ { funClauses = [clause]
+ , funCompiled = Just $ cc
+ , funProjection = Just projection
+ , funTerminates = Just True
, funCopatternLHS = isCopatternLHS [clause]
}
}