summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete.hs')
-rw-r--r--src/full/Agda/Syntax/Concrete.hs66
1 files changed, 38 insertions, 28 deletions
diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
index 201fcc3..dacb521 100644
--- a/src/full/Agda/Syntax/Concrete.hs
+++ b/src/full/Agda/Syntax/Concrete.hs
@@ -1,9 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
{-| The concrete syntax is a raw representation of the program text
without any desugaring at all. This is what the parser produces.
@@ -72,6 +68,8 @@ import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
import qualified Agda.Syntax.Abstract.Name as A
+import Agda.TypeChecking.Positivity.Occurrence
+
import Agda.Utils.Lens
import Agda.Utils.Null
@@ -150,6 +148,7 @@ data Expr
| RecUpdate Range Expr [FieldAssignment] -- ^ ex: @record e {x = a; y = b}@
| Let Range [Declaration] Expr -- ^ ex: @let Ds in e@
| Paren Range Expr -- ^ ex: @(e)@
+ | IdiomBrackets Range Expr -- ^ ex: @(| e |)@
| Absurd Range -- ^ ex: @()@ or @{}@, only in patterns
| As Range Name Expr -- ^ ex: @x\@p@, only in patterns
| Dot Range Expr -- ^ ex: @.p@, only in patterns
@@ -182,7 +181,7 @@ data Pattern
| WildP Range -- ^ @_@
| AbsurdP Range -- ^ @()@
| AsP Range Name Pattern -- ^ @x\@p@ unused
- | DotP Range Expr -- ^ @.e@
+ | DotP Range Origin Expr -- ^ @.e@
| LitP Literal -- ^ @0@, @1@, etc.
| RecP Range [FieldAssignment' Pattern] -- ^ @record {x = p; y = q}@
deriving (Typeable)
@@ -285,7 +284,10 @@ type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
= NoWhere -- ^ No @where@ clauses.
| AnyWhere decls -- ^ Ordinary @where@.
- | SomeWhere Name decls -- ^ Named where: @module M where@.
+ | SomeWhere Name Access decls
+ -- ^ Named where: @module M where@.
+ -- The 'Access' flag applies to the 'Name' (not the module contents!)
+ -- and is propagated from the parent function.
deriving (Typeable, Functor, Foldable, Traversable)
-- | An expression followed by a where clause.
@@ -338,7 +340,10 @@ data Declaration
| PatternSyn Range Name [Arg Name] Pattern
| Mutual Range [Declaration]
| Abstract Range [Declaration]
- | Private Range [Declaration]
+ | Private Range Origin [Declaration]
+ -- ^ In "Agda.Syntax.Concrete.Definitions" we generate private blocks
+ -- temporarily, which should be treated different that user-declared
+ -- private blocks. Thus the 'Origin'.
| InstanceB Range [Declaration]
| Macro Range [Declaration]
| Postulate Range [TypeSignatureOrInstanceBlock]
@@ -367,7 +372,7 @@ data OpenShortHand = DoOpen | DontOpen
data Pragma
= OptionsPragma Range [String]
| BuiltinPragma Range String Expr
- | RewritePragma Range QName
+ | RewritePragma Range [QName]
| CompiledDataPragma Range QName String [String]
| CompiledDeclareDataPragma Range QName String
| CompiledTypePragma Range QName String
@@ -378,7 +383,6 @@ data Pragma
| CompiledUHCPragma Range QName String
| CompiledDataUHCPragma Range QName String [String]
| HaskellCodePragma Range String
- | NoSmashingPragma Range QName
| StaticPragma Range QName
| InlinePragma Range QName
| ImportPragma Range String
@@ -390,6 +394,7 @@ data Pragma
| CatchallPragma Range
| DisplayPragma Range Pattern Expr
| NoPositivityCheckPragma Range
+ | PolarityPragma Range Name [Occurrence]
deriving (Typeable)
---------------------------------------------------------------------------
@@ -419,7 +424,7 @@ spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
spanAllowedBeforeModule = span isAllowedBeforeModule
where
isAllowedBeforeModule (Pragma OptionsPragma{}) = True
- isAllowedBeforeModule (Private _ ds) = all isAllowedBeforeModule ds
+ isAllowedBeforeModule (Private _ _ ds) = all isAllowedBeforeModule ds
isAllowedBeforeModule Import{} = True
isAllowedBeforeModule ModuleMacro{} = True
isAllowedBeforeModule Open{} = True
@@ -442,15 +447,17 @@ mapLhsOriginalPattern f lhs@LHS{ lhsOriginalPattern = p } =
data AppView = AppView Expr [NamedArg Expr]
appView :: Expr -> AppView
-appView (App r e1 e2) = vApp (appView e1) e2
+appView e =
+ case e of
+ App r e1 e2 -> vApp (appView e1) e2
+ RawApp _ (e:es) -> AppView e $ map arg es
+ _ -> AppView e []
where
vApp (AppView e es) arg = AppView e (es ++ [arg])
-appView (RawApp _ (e:es)) = AppView e $ map arg es
- where
+
arg (HiddenArg _ e) = setHiding Hidden $ defaultArg e
arg (InstanceArg _ e) = setHiding Instance $ defaultArg e
arg e = defaultArg (unnamed e)
-appView e = AppView e []
{--------------------------------------------------------------------------
Patterns
@@ -541,6 +548,7 @@ instance HasRange Expr where
SetN r _ -> r
Let r _ _ -> r
Paren r _ -> r
+ IdiomBrackets r _ -> r
As r _ _ -> r
Dot r _ -> r
Absurd r -> r
@@ -579,7 +587,7 @@ instance HasRange BoundName where
instance HasRange WhereClause where
getRange NoWhere = noRange
getRange (AnyWhere ds) = getRange ds
- getRange (SomeWhere _ ds) = getRange ds
+ getRange (SomeWhere _ _ ds) = getRange ds
instance HasRange ModuleApplication where
getRange (SectionApp r _ _) = r
@@ -606,7 +614,7 @@ instance HasRange Declaration where
getRange (Import r _ _ _ _) = r
getRange (InstanceB r _) = r
getRange (Macro r _) = r
- getRange (Private r _) = r
+ getRange (Private r _ _) = r
getRange (Postulate r _) = r
getRange (Primitive r _) = r
getRange (Module r _ _ _) = r
@@ -643,7 +651,6 @@ instance HasRange Pragma where
getRange (CompiledUHCPragma r _ _) = r
getRange (CompiledDataUHCPragma r _ _ _) = r
getRange (HaskellCodePragma r _) = r
- getRange (NoSmashingPragma r _) = r
getRange (StaticPragma r _) = r
getRange (InlinePragma r _) = r
getRange (ImportPragma r _) = r
@@ -653,6 +660,7 @@ instance HasRange Pragma where
getRange (CatchallPragma r) = r
getRange (DisplayPragma r _ _) = r
getRange (NoPositivityCheckPragma r) = r
+ getRange (PolarityPragma r _ _) = r
instance HasRange AsName where
getRange a = getRange (asRange a, asName a)
@@ -670,7 +678,7 @@ instance HasRange Pattern where
getRange (QuoteP r) = r
getRange (HiddenP r _) = r
getRange (InstanceP r _) = r
- getRange (DotP r _) = r
+ getRange (DotP r _ _) = r
getRange (RecP r _) = r
-- SetRange instances
@@ -692,7 +700,7 @@ instance SetRange Pattern where
setRange r (QuoteP _) = QuoteP r
setRange r (HiddenP _ p) = HiddenP r p
setRange r (InstanceP _ p) = InstanceP r p
- setRange r (DotP _ e) = DotP r e
+ setRange r (DotP _ o e) = DotP r o e
setRange r (RecP _ fs) = RecP r fs
-- KillRange instances
@@ -723,7 +731,7 @@ instance KillRange Declaration where
killRange (PatternSyn _ n ns p) = killRange3 (PatternSyn noRange) n ns p
killRange (Mutual _ d) = killRange1 (Mutual noRange) d
killRange (Abstract _ d) = killRange1 (Abstract noRange) d
- killRange (Private _ d) = killRange1 (Private noRange) d
+ killRange (Private _ o d) = killRange2 (Private noRange) o d
killRange (InstanceB _ d) = killRange1 (InstanceB noRange) d
killRange (Macro _ d) = killRange1 (Macro noRange) d
killRange (Postulate _ t) = killRange1 (Postulate noRange) t
@@ -759,6 +767,7 @@ instance KillRange Expr where
killRange (RecUpdate _ e ne) = killRange2 (RecUpdate noRange) e ne
killRange (Let _ d e) = killRange2 (Let noRange) d e
killRange (Paren _ e) = killRange1 (Paren noRange) e
+ killRange (IdiomBrackets _ e) = killRange1 (IdiomBrackets noRange) e
killRange (Absurd _) = Absurd noRange
killRange (As _ n e) = killRange2 (As noRange) n e
killRange (Dot _ e) = killRange1 (Dot noRange) e
@@ -799,7 +808,7 @@ instance KillRange Pattern where
killRange (WildP _) = WildP noRange
killRange (AbsurdP _) = AbsurdP noRange
killRange (AsP _ n p) = killRange2 (AsP noRange) n p
- killRange (DotP _ e) = killRange1 (DotP noRange) e
+ killRange (DotP _ o e) = killRange1 (DotP noRange) o e
killRange (LitP l) = killRange1 LitP l
killRange (QuoteP _) = QuoteP noRange
killRange (RecP _ fs) = killRange1 (RecP noRange) fs
@@ -807,7 +816,7 @@ instance KillRange Pattern where
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e
- killRange (RewritePragma _ q) = killRange1 (RewritePragma noRange) q
+ killRange (RewritePragma _ qs) = killRange1 (RewritePragma noRange) qs
killRange (CompiledDataPragma _ q s ss) = killRange1 (\q -> CompiledDataPragma noRange q s ss) q
killRange (CompiledDeclareDataPragma _ q s) = killRange1 (\q -> CompiledDeclareDataPragma noRange q s) q
killRange (CompiledTypePragma _ q s) = killRange1 (\q -> CompiledTypePragma noRange q s) q
@@ -818,7 +827,6 @@ instance KillRange Pragma where
killRange (CompiledUHCPragma _ q s) = killRange1 (\q -> CompiledUHCPragma noRange q s) q
killRange (CompiledDataUHCPragma _ q s ss) = killRange1 (\q -> CompiledDataUHCPragma noRange q s ss) q
killRange (HaskellCodePragma _ s) = HaskellCodePragma noRange s
- killRange (NoSmashingPragma _ q) = killRange1 (NoSmashingPragma noRange) q
killRange (StaticPragma _ q) = killRange1 (StaticPragma noRange) q
killRange (InlinePragma _ q) = killRange1 (InlinePragma noRange) q
killRange (ImportPragma _ s) = ImportPragma noRange s
@@ -828,6 +836,7 @@ instance KillRange Pragma where
killRange (CatchallPragma _) = CatchallPragma noRange
killRange (DisplayPragma _ lhs rhs) = killRange2 (DisplayPragma noRange) lhs rhs
killRange (NoPositivityCheckPragma _) = NoPositivityCheckPragma noRange
+ killRange (PolarityPragma _ q occs) = killRange1 (\q -> PolarityPragma noRange q occs) q
instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
@@ -843,7 +852,7 @@ instance KillRange TypedBindings where
instance KillRange WhereClause where
killRange NoWhere = NoWhere
killRange (AnyWhere d) = killRange1 AnyWhere d
- killRange (SomeWhere n d) = killRange2 SomeWhere n d
+ killRange (SomeWhere n a d) = killRange3 SomeWhere n a d
------------------------------------------------------------------------
-- NFData instances
@@ -873,6 +882,7 @@ instance NFData Expr where
rnf (RecUpdate _ a b) = rnf a `seq` rnf b
rnf (Let _ a b) = rnf a `seq` rnf b
rnf (Paren _ a) = rnf a
+ rnf (IdiomBrackets _ a)= rnf a
rnf (Absurd _) = ()
rnf (As _ a b) = rnf a `seq` rnf b
rnf (Dot _ a) = rnf a
@@ -900,7 +910,7 @@ instance NFData Pattern where
rnf (WildP _) = ()
rnf (AbsurdP _) = ()
rnf (AsP _ a b) = rnf a `seq` rnf b
- rnf (DotP _ a) = rnf a
+ rnf (DotP _ a b) = rnf a `seq` rnf b
rnf (LitP a) = rnf a
rnf (RecP _ a) = rnf a
@@ -919,7 +929,7 @@ instance NFData Declaration where
rnf (PatternSyn _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (Mutual _ a) = rnf a
rnf (Abstract _ a) = rnf a
- rnf (Private _ a) = rnf a
+ rnf (Private _ _ a) = rnf a
rnf (InstanceB _ a) = rnf a
rnf (Macro _ a) = rnf a
rnf (Postulate _ a) = rnf a
@@ -948,7 +958,6 @@ instance NFData Pragma where
rnf (CompiledUHCPragma _ a b) = rnf a `seq` rnf b
rnf (CompiledDataUHCPragma _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (HaskellCodePragma _ s) = rnf s
- rnf (NoSmashingPragma _ a) = rnf a
rnf (StaticPragma _ a) = rnf a
rnf (InlinePragma _ a) = rnf a
rnf (ImportPragma _ a) = rnf a
@@ -958,6 +967,7 @@ instance NFData Pragma where
rnf (CatchallPragma _) = ()
rnf (DisplayPragma _ a b) = rnf a `seq` rnf b
rnf (NoPositivityCheckPragma _) = ()
+ rnf (PolarityPragma _ a b) = rnf a `seq` rnf b
-- | Ranges are not forced.
@@ -1002,7 +1012,7 @@ instance NFData ModuleAssignment where
instance NFData a => NFData (WhereClause' a) where
rnf NoWhere = ()
rnf (AnyWhere a) = rnf a
- rnf (SomeWhere a b) = rnf a `seq` rnf b
+ rnf (SomeWhere a b c) = rnf a `seq` rnf b `seq` rnf c
instance NFData a => NFData (LamBinding' a) where
rnf (DomainFree a b) = rnf a `seq` rnf b