summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Abstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Abstract.hs')
-rw-r--r--src/full/Agda/Syntax/Abstract.hs79
1 files changed, 47 insertions, 32 deletions
diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs
index 406e8f9..ea02ed4 100644
--- a/src/full/Agda/Syntax/Abstract.hs
+++ b/src/full/Agda/Syntax/Abstract.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ DeriveFoldable,
+ DeriveFunctor,
+ DeriveTraversable,
+ FlexibleInstances,
+ MultiParamTypeClasses,
+ TemplateHaskell #-}
{-| The abstract syntax. This is what you get after desugaring and scope
analysis of the concrete syntax. The type checker works on abstract syntax,
@@ -117,7 +117,7 @@ data Axiom
deriving (Typeable, Eq, Ord, Show)
-- | Renaming (generic).
-type Ren a = Map a a
+type Ren a = [(a, a)]
data Declaration
= Axiom Axiom DefInfo ArgInfo QName Expr -- ^ type signature (can be irrelevant and colored, but not hidden)
@@ -170,6 +170,9 @@ data ModuleApplication
data Pragma
= OptionsPragma [String]
| BuiltinPragma String Expr
+ | BuiltinNoDefPragma String QName
+ -- ^ Builtins that do not come with a definition,
+ -- but declare a name for an Agda concept.
| RewritePragma QName
| CompiledPragma QName String
| CompiledExportPragma QName String
@@ -209,20 +212,25 @@ data TypedBindings = TypedBindings Range (Arg TypedBinding)
-- ^ . @(xs : e)@ or @{xs : e}@
deriving (Typeable, Show)
--- | A typed binding. Appears in dependent function spaces, typed lambdas, and
--- telescopes. I might be tempting to simplify this to only bind a single
--- name at a time. This would mean that we would have to typecheck the type
--- several times (@(x y : A)@ vs. @(x : A)(y : A)@).
--- In most cases this wouldn't really be a problem, but it's good
--- principle to not do extra work unless you have to.
+-- | A typed binding. Appears in dependent function spaces, typed lambdas, and
+-- telescopes. It might be tempting to simplify this to only bind a single
+-- name at a time, and translate, say, @(x y : A)@ to @(x : A)(y : A)@
+-- before type-checking. However, this would be slightly problematic:
--
--- (Andreas, 2013-12-10: The more serious problem would that the translation
--- from @(x y : ?)@ to @(x : ?) (y : ?)@ duplicates the hole @?@.
+-- 1. We would have to typecheck the type @A@ several times.
+--
+-- 2. If @A@ contains a meta variable or hole, it would be duplicated
+-- by such a translation.
+--
+-- While 1. is only slightly inefficient, 2. would be an outright bug.
+-- Duplicating @A@ could not be done naively, we would have to make sure
+-- that the metas of the copy are aliases of the metas of the original.
+
data TypedBinding
- = TBind Range [Name] Expr
+ = TBind Range [WithHiding Name] Expr
-- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@.
| TLet Range [LetBinding]
- -- ^
+ -- ^ E.g. @(let x = e)@ or @(let open M)@.
deriving (Typeable, Show)
type Telescope = [TypedBindings]
@@ -244,7 +252,7 @@ data RHS
| AbsurdRHS
| WithRHS QName [Expr] [Clause]
-- ^ The 'QName' is the name of the with function.
- | RewriteRHS [QName] [Expr] RHS [Declaration]
+ | RewriteRHS [(QName, Expr)] RHS [Declaration]
-- ^ The 'QName's are the names of the generated with functions.
-- One for each 'Expr'.
-- The RHS shouldn't be another @RewriteRHS@.
@@ -399,6 +407,16 @@ instance IsProjP a => IsProjP (Named n a) where
Instances
--------------------------------------------------------------------------}
+instance LensHiding TypedBindings where
+ getHiding (TypedBindings _ a) = getHiding a
+ mapHiding f (TypedBindings r a) = TypedBindings r $ mapHiding f a
+
+instance LensHiding LamBinding where
+ getHiding (DomainFree ai _) = getHiding ai
+ getHiding (DomainFull tb) = getHiding tb
+ mapHiding f (DomainFree ai x) = mapHiding f ai `DomainFree` x
+ mapHiding f (DomainFull tb) = DomainFull $ mapHiding f tb
+
instance HasRange LamBinding where
getRange (DomainFree _ x) = getRange x
getRange (DomainFull b) = getRange b
@@ -488,7 +506,7 @@ instance HasRange RHS where
getRange AbsurdRHS = noRange
getRange (RHS e) = getRange e
getRange (WithRHS _ e cs) = fuseRange e cs
- getRange (RewriteRHS _ es rhs wh) = getRange (es, rhs, wh)
+ getRange (RewriteRHS xes rhs wh) = getRange (map snd xes, rhs, wh)
instance HasRange LetBinding where
getRange (LetBind i _ _ _ _ ) = getRange i
@@ -531,17 +549,15 @@ instance KillRange Expr where
killRange (App i e1 e2) = killRange3 App i e1 e2
killRange (WithApp i e es) = killRange3 WithApp i e es
killRange (Lam i b e) = killRange3 Lam i b e
- killRange (AbsurdLam i h) = killRange1 AbsurdLam i h
+ killRange (AbsurdLam i h) = killRange2 AbsurdLam i h
killRange (ExtendedLam i n d ps) = killRange4 ExtendedLam i n d ps
killRange (Pi i a b) = killRange3 Pi i a b
killRange (Fun i a b) = killRange3 Fun i a b
- killRange (Set i n) = Set (killRange i) n
+ killRange (Set i n) = killRange2 Set i n
killRange (Prop i) = killRange1 Prop i
killRange (Let i ds e) = killRange3 Let i ds e
- killRange (Rec i fs) = Rec (killRange i) (map (id -*- killRange) fs)
- killRange (RecUpdate i e fs) = RecUpdate (killRange i)
- (killRange e)
- (map (id -*- killRange) fs)
+ killRange (Rec i fs) = killRange2 Rec i fs
+ killRange (RecUpdate i e fs) = killRange3 RecUpdate i e fs
killRange (ETel tel) = killRange1 ETel tel
killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
killRange (QuoteGoal i x e) = killRange3 QuoteGoal i x e
@@ -549,7 +565,7 @@ instance KillRange Expr where
killRange (Quote i) = killRange1 Quote i
killRange (QuoteTerm i) = killRange1 QuoteTerm i
killRange (Unquote i) = killRange1 Unquote i
- killRange (DontCare e) = DontCare e
+ killRange (DontCare e) = killRange1 DontCare e
killRange (PatternSyn x) = killRange1 PatternSyn x
instance KillRange Declaration where
@@ -608,7 +624,7 @@ instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
killRange (RHS e) = killRange1 RHS e
killRange (WithRHS q e cs) = killRange3 WithRHS q e cs
- killRange (RewriteRHS x es rhs wh) = killRange4 RewriteRHS x es rhs wh
+ killRange (RewriteRHS xes rhs wh) = killRange3 RewriteRHS xes rhs wh
instance KillRange LetBinding where
killRange (LetBind i info a b c) = killRange5 LetBind i info a b c
@@ -685,7 +701,7 @@ instance AllNames RHS where
allNames (RHS e) = allNames e
allNames AbsurdRHS{} = Seq.empty
allNames (WithRHS q _ cls) = q <| allNames cls
- allNames (RewriteRHS qs _ rhs cls) = Seq.fromList qs >< allNames rhs >< allNames cls
+ allNames (RewriteRHS qes rhs cls) = Seq.fromList (map fst qes) >< allNames rhs >< allNames cls
instance AllNames Expr where
allNames Var{} = Seq.empty
@@ -892,4 +908,3 @@ insertImplicitPatSynArgs wild r ns as = matchArgs r ns as
matchArgs r (n:ns) as = do
(p, as) <- matchNextArg r n as
first ((unArg n, p) :) <$> matchArgs (getRange p) ns as
-