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.hs134
1 files changed, 94 insertions, 40 deletions
diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
index 1ba4fa2..bc124d4 100644
--- a/src/full/Agda/Syntax/Concrete.hs
+++ b/src/full/Agda/Syntax/Concrete.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances #-}
{-| The concrete syntax is a raw representation of the program text
without any desugaring at all. This is what the parser produces.
@@ -62,6 +62,8 @@ import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.List
+import Data.Set (Set)
+
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
@@ -70,6 +72,7 @@ import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Name
+import qualified Agda.Syntax.Abstract.Name as A
import Agda.Utils.Lens
@@ -101,7 +104,14 @@ data Expr
| Underscore !Range (Maybe String) -- ^ ex: @_@ or @_A_5@
| RawApp !Range [Expr] -- ^ before parsing operators
| App !Range Expr (NamedArg Expr) -- ^ ex: @e e@, @e {e}@, or @e {x = e}@
- | OpApp !Range QName [NamedArg (OpApp Expr)] -- ^ ex: @e + e@
+ | OpApp !Range QName (Set A.Name)
+ [NamedArg (OpApp Expr)] -- ^ ex: @e + e@
+ -- The 'QName' is
+ -- possibly ambiguous,
+ -- but it must
+ -- correspond to one of
+ -- the names in the
+ -- set.
| WithApp !Range Expr [Expr] -- ^ ex: @e | e1 | .. | en@
| HiddenArg !Range (Named_ Expr) -- ^ ex: @{e}@ or @{x=e}@
| InstanceArg !Range (Named_ Expr) -- ^ ex: @{{e}}@ or @{{x=e}}@
@@ -131,7 +141,7 @@ data Expr
| Equal !Range Expr Expr -- ^ ex: @a = b@, used internally in the parser
deriving (Typeable)
-instance NFData Expr
+instance NFData Expr where rnf x = seq x ()
-- | Concrete patterns. No literals in patterns at the moment.
data Pattern
@@ -139,7 +149,12 @@ data Pattern
| QuoteP !Range -- ^ @quote@
| AppP Pattern (NamedArg Pattern) -- ^ @p p'@ or @p {x = p'}@
| RawAppP !Range [Pattern] -- ^ @p1..pn@ before parsing operators
- | OpAppP !Range QName [NamedArg Pattern] -- ^ eg: @p => p'@ for operator @_=>_@
+ | OpAppP !Range QName (Set A.Name)
+ [NamedArg Pattern] -- ^ eg: @p => p'@ for operator @_=>_@
+ -- The 'QName' is possibly
+ -- ambiguous, but it must
+ -- correspond to one of
+ -- the names in the set.
| HiddenP !Range (Named_ Pattern) -- ^ @{p}@ or @{x = p}@
| InstanceP !Range (Named_ Pattern) -- ^ @{{p}}@ or @{{x = p}}@
| ParenP !Range Pattern -- ^ @(p)@
@@ -150,7 +165,7 @@ data Pattern
| LitP Literal -- ^ @0@, @1@, etc.
deriving (Typeable)
-instance NFData Pattern
+instance NFData Pattern where rnf x = seq x ()
-- | A lambda binding is either domain free or typed.
type LamBinding = LamBinding' TypedBindings
@@ -162,11 +177,14 @@ data LamBinding' a
-- | A sequence of typed bindings with hiding information. Appears in dependent
-- function spaces, typed lambdas, and telescopes.
+--
+-- If the individual binding contains hiding information as well, the
+-- 'Hiding' in @TypedBindings@ must be the unit 'NotHidden'.
type TypedBindings = TypedBindings' TypedBinding
data TypedBindings' a = TypedBindings !Range (Arg a)
- -- ^ . @(xs : e)@ or @{xs : e}@
+ -- ^ . @(xs : e)@ or @{xs : e}@ or something like @(x {y} _ : e)@.
deriving (Typeable, Functor, Foldable, Traversable)
data BoundName = BName
@@ -187,7 +205,7 @@ mkBoundName x f = BName x x f
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
- = TBind !Range [BoundName] e -- ^ Binding @(x1 ... xn : A)@.
+ = TBind !Range [WithHiding BoundName] e -- ^ Binding @(x1 ... xn : A)@.
| TLet !Range [Declaration] -- ^ Let binding @(let Ds)@ or @(open M args)@.
deriving (Typeable, Functor, Foldable, Traversable)
@@ -239,15 +257,7 @@ data LHSCore
}
deriving (Typeable)
-instance NFData LHSCore
-
-{- TRASH
-lhsCoreToPattern :: LHSCore -> Pattern
-lhsCoreToPattern (LHSHead f args) = OpAppP (fuseRange f args) (unqualify f) args
-lhsCoreToPattern (LHSProj d ps1 lhscore ps2) = OpAppP (fuseRange d ps) (unqualify) ps
- where p = lhsCoreToPattern lhscore
- ps = ps1 ++ p : ps2
--}
+instance NFData LHSCore where rnf x = seq x ()
type RHS = RHS' Expr
data RHS' e
@@ -440,7 +450,7 @@ patternHead p =
AppP p p' -> patternHead p
RawAppP _ [] -> __IMPOSSIBLE__
RawAppP _ (p:_) -> patternHead p
- OpAppP _ name ps -> return $ unqualify name
+ OpAppP _ name _ ps -> return $ unqualify name
HiddenP _ (namedPat) -> patternHead (namedThing namedPat)
ParenP _ p -> patternHead p
WildP _ -> Nothing
@@ -460,7 +470,7 @@ patternNames p =
IdentP x -> [unqualify x]
AppP p p' -> concatMap patternNames [p, namedArg p']
RawAppP _ ps -> concatMap patternNames ps
- OpAppP _ name ps -> unqualify name : concatMap (patternNames . namedArg) ps
+ OpAppP _ name _ ps -> unqualify name : concatMap (patternNames . namedArg) ps
HiddenP _ (namedPat) -> patternNames (namedThing namedPat)
ParenP _ p -> patternNames p
WildP _ -> []
@@ -475,6 +485,26 @@ patternNames p =
Instances
--------------------------------------------------------------------------}
+-- Lenses
+------------------------------------------------------------------------
+
+instance LensRelevance TypedBindings where
+ getRelevance (TypedBindings _ b) = getRelevance b
+ mapRelevance f (TypedBindings r b) = TypedBindings r $ mapRelevance f b
+
+instance LensHiding TypedBindings where
+ getHiding (TypedBindings _ b) = getHiding b
+ mapHiding f (TypedBindings r b) = TypedBindings r $ mapHiding f b
+
+instance LensHiding LamBinding where
+ getHiding (DomainFree ai _) = getHiding ai
+ getHiding (DomainFull a) = getHiding a
+ mapHiding f (DomainFree ai x) = DomainFree (mapHiding f ai) x
+ mapHiding f (DomainFull a) = DomainFull $ mapHiding f a
+
+-- HasRange instances
+------------------------------------------------------------------------
+
instance HasRange e => HasRange (OpApp e) where
getRange e = case e of
Ordinary e -> getRange e
@@ -489,7 +519,7 @@ instance HasRange Expr where
Underscore r _ -> r
App r _ _ -> r
RawApp r _ -> r
- OpApp r _ _ -> r
+ OpApp r _ _ _ -> r
WithApp r _ _ -> r
Lam r _ _ -> r
AbsurdLam r _ -> r
@@ -617,7 +647,7 @@ instance HasRange AsName where
instance HasRange Pattern where
getRange (IdentP x) = getRange x
getRange (AppP p q) = fuseRange p q
- getRange (OpAppP r _ _) = r
+ getRange (OpAppP r _ _ _) = r
getRange (RawAppP r _) = r
getRange (ParenP r _) = r
getRange (WildP r) = r
@@ -629,6 +659,30 @@ instance HasRange Pattern where
getRange (InstanceP r _) = r
getRange (DotP r _) = r
+-- SetRange instances
+------------------------------------------------------------------------
+
+instance SetRange TypedBindings where
+ setRange r (TypedBindings _ b) = TypedBindings r b
+
+instance SetRange Pattern where
+ setRange r (IdentP x) = IdentP (setRange r x)
+ setRange r (AppP p q) = AppP (setRange r p) (setRange r q)
+ setRange r (OpAppP _ x ns ps) = OpAppP r x ns ps
+ setRange r (RawAppP _ ps) = RawAppP r ps
+ setRange r (ParenP _ p) = ParenP r p
+ setRange r (WildP _) = WildP r
+ setRange r (AsP _ x p) = AsP r (setRange r x) p
+ setRange r (AbsurdP _) = AbsurdP r
+ setRange r (LitP l) = LitP (setRange r l)
+ 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
+
+-- KillRange instances
+------------------------------------------------------------------------
+
instance KillRange AsName where
killRange (AsName n _) = killRange1 (flip AsName noRange) n
@@ -666,7 +720,7 @@ instance KillRange Expr where
killRange (Underscore _ n) = Underscore noRange n
killRange (RawApp _ e) = killRange1 (RawApp noRange) e
killRange (App _ e a) = killRange2 (App noRange) e a
- killRange (OpApp _ n o) = killRange2 (OpApp noRange) n o
+ killRange (OpApp _ n ns o) = killRange3 (OpApp noRange) n ns o
killRange (WithApp _ e es) = killRange2 (WithApp noRange) e es
killRange (HiddenArg _ n) = killRange1 (HiddenArg noRange) n
killRange (InstanceArg _ n) = killRange1 (InstanceArg noRange) n
@@ -720,19 +774,19 @@ instance KillRange e => KillRange (OpApp e) where
killRange (Ordinary e) = killRange1 Ordinary e
instance KillRange Pattern where
- killRange (IdentP q) = killRange1 IdentP q
- killRange (AppP p n) = killRange2 AppP p n
- killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
- killRange (OpAppP _ n p) = killRange2 (OpAppP noRange) n p
- killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n
- killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n
- killRange (ParenP _ p) = killRange1 (ParenP noRange) p
- 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 (LitP l) = killRange1 LitP l
- killRange (QuoteP _) = QuoteP noRange
+ killRange (IdentP q) = killRange1 IdentP q
+ killRange (AppP p n) = killRange2 AppP p n
+ killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p
+ killRange (OpAppP _ n ns p) = killRange3 (OpAppP noRange) n ns p
+ killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n
+ killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n
+ killRange (ParenP _ p) = killRange1 (ParenP noRange) p
+ 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 (LitP l) = killRange1 LitP l
+ killRange (QuoteP _) = QuoteP noRange
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s