Skip to content

Commit

Permalink
[ #4743 ] Added support for erased modules.
Browse files Browse the repository at this point in the history
  • Loading branch information
@nad
nad committed Nov 5, 2022
1 parent 29e6923 commit 7993a7b
Show file tree
Hide file tree
Showing 52 changed files with 771 additions and 204 deletions.
28 changes: 27 additions & 1 deletion doc/release-notes/future.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ Erasure
@0 f≡ : f ≡ λ { unit → unit }
f≡ = refl
* One can now mark data and record types as erased (see
* One can now mark data and record types and modules as erased (see
[#4743](https://github.com/agda/agda/issues/4743)).
If a data type is marked as erased, then it can only be used in
Expand Down Expand Up @@ -79,6 +79,32 @@ Erasure
x : R₁
```

If a module is marked as erased, then all definitions inside the
module are erased. A module is marked as erased by writing `@0` or
`@erased` right after the `module` keyword:
```agda
module @0 _ where
F : @0 Set → Set
F A = A
module M (A : Set) where
record R : Set where
field
@0 x : A
module @0 N (@0 A : Set) = M A
G : (@0 A : Set) → let module @0 M₂ = M A in Set
G A = M.R B
module @0 _ where
B : Set
B = A
```
If an erased module is defined by a module application, then erased
names can be used in the application, as in the definition of `N` above.

Pragmas and Options
-------------------

Expand Down
46 changes: 37 additions & 9 deletions doc/user-manual/language/runtime-irrelevance.lagda.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,12 +127,12 @@ declared as erased, but that are treated as erased because they were
defined using Cubical Agda, and are used in a module that uses the
option :option:`--erased-cubical`.)

Finally it is possible to mark data and record types as erased. Such
types can only be used in erased positions, their constructors and
projections are erased, and definitions in record modules for erased
record types are erased. A data or record type is marked as erased by
writing ``@0`` or ``@erased`` right after the ``data`` or ``record``
keyword of the data or record type's declaration:
One can also mark data and record types as erased. Such types can only
be used in erased positions, their constructors and projections are
erased, and definitions in record modules for erased record types are
erased. A data or record type is marked as erased by writing ``@0`` or
``@erased`` right after the ``data`` or ``record`` keyword of the data
or record type's declaration:

::

Expand Down Expand Up @@ -161,6 +161,32 @@ keyword of the data or record type's declaration:
field
x : R₁

Finally one can mark modules as erased. The module identifier itself
does not become erased, but all definitions inside the module. A
module is marked as erased by writing ``@0`` or ``@erased`` right
after the ``module`` keyword:

::

module @0 _ where

F : @0 Set → Set
F A = A

module M (A : Set) where

record R : Set where
field
@0 x : A

module @0 N (@0 A : Set) = M A

G : (@0 A : Set) → let module @0 M₂ = M A in Set
G A = M.R C
module @0 _ where
C : Set
C = A

.. _run-time-irrelevance-rules:

Rules
Expand Down Expand Up @@ -201,8 +227,10 @@ match on the length first, the type checker complains:
The type checker enters compile-time mode when

- checking erased arguments to a constructor or function,
- checking the body of an erased definition,
- checking erased arguments to a constructor, function or module
application,
- checking the body of an erased definition (including an erased
module application),
- checking the body of a clause that matches on an erased constructor,
- checking the domain of an erased Π type, or
- checking a type, i.e. when moving to the right of a ``:``, with some
Expand All @@ -228,7 +256,7 @@ mode:

- Absurd lambdas.
- Non-erased pattern-matching lambdas.
- Module definitions ("``module M … = …``") or applications
- Non-erased module definitions ("``module M … = …``") or applications
("``M …``").
- Applications of ``♯`` (see :ref:`old-coinduction`).

Expand Down
10 changes: 6 additions & 4 deletions src/full/Agda/Interaction/Highlighting/FromAbstract.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,8 +203,9 @@ instance Hilite A.Declaration where
A.Field _di x e -> hlField x <> hl e
A.Primitive _di x e -> hl x <> hl e
A.Mutual _mi ds -> hl ds
A.Section _r x tel ds -> hl x <> hl tel <> hl ds
A.Apply mi x a _ci dir -> hl mi <> hl x <> hl a <> hl dir
A.Section _r er x tel ds -> hl er <> hl x <> hl tel <> hl ds
A.Apply mi er x a _ci dir -> hl mi <> hl er <> hl x <>
hl a <> hl dir
A.Import mi x dir -> hl mi <> hl x <> hl dir
A.Open mi x dir -> hl mi <> hl x <> hl dir
A.FunDef _di x _delayed cs -> hl x <> hl cs
Expand Down Expand Up @@ -352,8 +353,9 @@ instance Hilite A.LetBinding where
hilite = \case
A.LetBind _r ai x t e -> hl ai <> hl x <> hl t <> hl e
A.LetPatBind _r p e -> hl p <> hl e
A.LetApply mi x es _ci dir -> hl mi <> hl x <> hl es <> hl dir
A.LetOpen mi x dir -> hl mi <> hl x <> hl dir
A.LetApply mi er x es _c dir -> hl mi <> hl er <> hl x <>
hl es <> hl dir
A.LetOpen mi x dir -> hl mi <> hl x <> hl dir
A.LetDeclaredVariable x -> hl x
where
hl x = hilite x
Expand Down
27 changes: 14 additions & 13 deletions src/full/Agda/Syntax/Abstract.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,14 +167,14 @@ data Declaration
| Field DefInfo QName (Arg Type) -- ^ record field
| Primitive DefInfo QName (Arg Type) -- ^ primitive function
| Mutual MutualInfo [Declaration] -- ^ a bunch of mutually recursive definitions
| Section Range ModuleName GeneralizeTelescope [Declaration]
| Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
| Section Range Erased ModuleName GeneralizeTelescope [Declaration]
| Apply ModuleInfo Erased ModuleName ModuleApplication
ScopeCopyInfo ImportDirective
-- ^ The @ImportDirective@ is for highlighting purposes.
| Import ModuleInfo ModuleName ImportDirective
-- ^ The @ImportDirective@ is for highlighting purposes.
| Pragma Range Pragma
| Open ModuleInfo ModuleName ImportDirective
-- ^ only retained for highlighting purposes
| FunDef DefInfo QName Delayed [Clause] -- ^ sequence of function clauses
| DataSig DefInfo Erased QName GeneralizeTelescope Type -- ^ lone data signature
| DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
Expand Down Expand Up @@ -232,7 +232,8 @@ data LetBinding
-- ^ @LetBind info rel name type defn@
| LetPatBind LetInfo Pattern Expr
-- ^ Irrefutable pattern binding.
| LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
| LetApply ModuleInfo Erased ModuleName ModuleApplication
ScopeCopyInfo ImportDirective
-- ^ @LetApply mi newM (oldM args) renamings dir@.
-- The @ImportDirective@ is for highlighting purposes.
| LetOpen ModuleInfo ModuleName ImportDirective
Expand Down Expand Up @@ -594,8 +595,8 @@ instance Eq Declaration where
Field a1 b1 c1 == Field a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Primitive a1 b1 c1 == Primitive a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Mutual a1 b1 == Mutual a2 b2 = (a1, b1) == (a2, b2)
Section a1 b1 c1 d1 == Section a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
Apply a1 b1 c1 d1 e1 == Apply a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
Section a1 b1 c1 d1 e1 == Section a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
Apply a1 b1 c1 d1 e1 f1 == Apply a2 b2 c2 d2 e2 f2 = (a1, b1, c1, d1, e1, f1) == (a2, b2, c2, d2, e2, f2)
Import a1 b1 c1 == Import a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Pragma a1 b1 == Pragma a2 b2 = (a1, b1) == (a2, b2)
Open a1 b1 c1 == Open a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Expand Down Expand Up @@ -670,8 +671,8 @@ instance HasRange Declaration where
getRange (Generalize _ i _ _ _) = getRange i
getRange (Field i _ _ ) = getRange i
getRange (Mutual i _ ) = getRange i
getRange (Section i _ _ _ ) = getRange i
getRange (Apply i _ _ _ _) = getRange i
getRange (Section i _ _ _ _ ) = getRange i
getRange (Apply i _ _ _ _ _) = getRange i
getRange (Import i _ _ ) = getRange i
getRange (Primitive i _ _ ) = getRange i
getRange (Pragma i _ ) = getRange i
Expand Down Expand Up @@ -729,7 +730,7 @@ instance HasRange WhereDeclarations where
instance HasRange LetBinding where
getRange (LetBind i _ _ _ _ ) = getRange i
getRange (LetPatBind i _ _ ) = getRange i
getRange (LetApply i _ _ _ _ ) = getRange i
getRange (LetApply i _ _ _ _ _ ) = getRange i
getRange (LetOpen i _ _ ) = getRange i
getRange (LetDeclaredVariable x) = getRange x

Expand Down Expand Up @@ -806,8 +807,8 @@ instance KillRange Declaration where
killRange (Generalize s i j x e ) = killRange4 (Generalize s) i j x e
killRange (Field i a b ) = killRange3 Field i a b
killRange (Mutual i a ) = killRange2 Mutual i a
killRange (Section i a b c ) = killRange4 Section i a b c
killRange (Apply i a b c d ) = killRange5 Apply i a b c d
killRange (Section i a b c d ) = killRange5 Section i a b c d
killRange (Apply i a b c d e ) = killRange6 Apply i a b c d e
killRange (Import i a b ) = killRange3 Import i a b
killRange (Primitive i a b ) = killRange3 Primitive i a b
killRange (Pragma i a ) = Pragma (killRange i) a
Expand Down Expand Up @@ -875,7 +876,7 @@ instance KillRange WhereDeclarations where
instance KillRange LetBinding where
killRange (LetBind i info a b c) = killRange5 LetBind i info a b c
killRange (LetPatBind i a b ) = killRange3 LetPatBind i a b
killRange (LetApply i a b c d ) = killRange5 LetApply i a b c d
killRange (LetApply i a b c d e ) = killRange6 LetApply i a b c d e
killRange (LetOpen i x dir ) = killRange3 LetOpen i x dir
killRange (LetDeclaredVariable x) = killRange1 LetDeclaredVariable x

Expand Down Expand Up @@ -929,7 +930,7 @@ instance AnyAbstract Declaration where
anyAbstract (Field i _ _) = defAbstract i == AbstractDef
anyAbstract (Mutual _ ds) = anyAbstract ds
anyAbstract (ScopedDecl _ ds) = anyAbstract ds
anyAbstract (Section _ _ _ ds) = anyAbstract ds
anyAbstract (Section _ _ _ _ ds) = anyAbstract ds
anyAbstract (FunDef i _ _ _) = defAbstract i == AbstractDef
anyAbstract (DataDef i _ _ _ _) = defAbstract i == AbstractDef
anyAbstract (RecDef i _ _ _ _ _ _) = defAbstract i == AbstractDef
Expand Down
21 changes: 12 additions & 9 deletions src/full/Agda/Syntax/Abstract/Views.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,12 +109,15 @@ deepUnscopeDecls :: [A.Declaration] -> [A.Declaration]
deepUnscopeDecls = concatMap deepUnscopeDecl

deepUnscopeDecl :: A.Declaration -> [A.Declaration]
deepUnscopeDecl (A.ScopedDecl _ ds) = deepUnscopeDecls ds
deepUnscopeDecl (A.Mutual i ds) = [A.Mutual i (deepUnscopeDecls ds)]
deepUnscopeDecl (A.Section i m tel ds) = [A.Section i m (deepUnscope tel) (deepUnscopeDecls ds)]
deepUnscopeDecl (A.RecDef i x uc dir bs e ds) =
[ A.RecDef i x uc dir (deepUnscope bs) (deepUnscope e) (deepUnscopeDecls ds) ]
deepUnscopeDecl d = [deepUnscope d]
deepUnscopeDecl = \case
A.ScopedDecl _ ds -> deepUnscopeDecls ds
A.Mutual i ds -> [A.Mutual i (deepUnscopeDecls ds)]
A.Section i e m tel ds -> [A.Section i e m (deepUnscope tel)
(deepUnscopeDecls ds)]
A.RecDef i x uc dir bs e ds -> [ A.RecDef i x uc dir (deepUnscope bs)
(deepUnscope e)
(deepUnscopeDecls ds) ]
d -> [deepUnscope d]

-- * Traversal
---------------------------------------------------------------------------
Expand Down Expand Up @@ -433,8 +436,8 @@ instance ExprLike Declaration where
Field i x e -> Field i x <$> rec e
Primitive i x e -> Primitive i x <$> rec e
Mutual i ds -> Mutual i <$> rec ds
Section i m tel ds -> Section i m <$> rec tel <*> rec ds
Apply i m a ci d -> (\ a -> Apply i m a ci d) <$> rec a
Section i e m tel ds -> Section i e m <$> rec tel <*> rec ds
Apply i e m a ci d -> (\a -> Apply i e m a ci d) <$> rec a
Import{} -> pure d
Pragma i p -> Pragma i <$> rec p
Open{} -> pure d
Expand Down Expand Up @@ -512,7 +515,7 @@ instance DeclaredNames Declaration where
UnquoteData _ d _ _ cs _ -> singleton (WithKind DataName d) <> (fromList $ map (WithKind ConName) cs) -- singleton _ <> map (WithKind ConName) cs
FunDef _ q _ cls -> singleton (WithKind FunName q) <> declaredNames cls
ScopedDecl _ decls -> declaredNames decls
Section _ _ _ decls -> declaredNames decls
Section _ _ _ _ decls -> declaredNames decls
Pragma _ pragma -> declaredNames pragma
Apply{} -> mempty
Import{} -> mempty
Expand Down
43 changes: 25 additions & 18 deletions src/full/Agda/Syntax/Concrete.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -368,7 +368,7 @@ data WhereClause' decls
| AnyWhere Range decls
-- ^ Ordinary @where@. 'Range' of the @where@ keyword.
-- List of declarations can be empty.
| SomeWhere Range Name Access decls
| SomeWhere Range Erased Name Access decls
-- ^ Named where: @module M where ds@.
-- 'Range' of the keywords @module@ and @where@.
-- The 'Access' flag applies to the 'Name' (not the module contents!)
Expand Down Expand Up @@ -477,8 +477,9 @@ data Declaration
| Primitive Range [TypeSignature]
| Open Range QName ImportDirective
| Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
| ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
| Module Range QName Telescope [Declaration]
| ModuleMacro Range Erased Name ModuleApplication !OpenShortHand
ImportDirective
| Module Range Erased QName Telescope [Declaration]
| UnquoteDecl Range [Name] Expr
-- ^ @unquoteDecl xs = e@
| UnquoteDef Range [Name] Expr
Expand Down Expand Up @@ -849,9 +850,9 @@ instance HasRange BoundName where
getRange = getRange . boundName

instance HasRange WhereClause where
getRange NoWhere = noRange
getRange (AnyWhere r ds) = getRange (r, ds)
getRange (SomeWhere r x _ ds) = getRange (r, x, ds)
getRange NoWhere = noRange
getRange (AnyWhere r ds) = getRange (r, ds)
getRange (SomeWhere r e x _ ds) = getRange (r, e, x, ds)

instance HasRange ModuleApplication where
getRange (SectionApp r _ _) = r
Expand Down Expand Up @@ -887,14 +888,15 @@ instance HasRange Declaration where
getRange (Abstract r _) = r
getRange (Generalize r _) = r
getRange (Open r _ _) = r
getRange (ModuleMacro r _ _ _ _) = r
getRange (ModuleMacro r _ _ _ _ _)
= r
getRange (Import r _ _ _ _) = r
getRange (InstanceB r _) = r
getRange (Macro r _) = r
getRange (Private r _ _) = r
getRange (Postulate r _) = r
getRange (Primitive r _) = r
getRange (Module r _ _ _) = r
getRange (Module r _ _ _ _) = r
getRange (Infix f _) = getRange f
getRange (Syntax n _) = getRange n
getRange (PatternSyn r _ _ _) = r
Expand Down Expand Up @@ -1046,8 +1048,11 @@ instance KillRange Declaration where
killRange (Primitive _ t) = killRange1 (Primitive noRange) t
killRange (Open _ q i) = killRange2 (Open noRange) q i
killRange (Import _ q a o i) = killRange3 (\q a -> Import noRange q a o) q a i
killRange (ModuleMacro _ n m o i) = killRange3 (\n m -> ModuleMacro noRange n m o) n m i
killRange (Module _ q t d) = killRange3 (Module noRange) q t d
killRange (ModuleMacro _ e n m o i)
= killRange4
(\e n m -> ModuleMacro noRange e n m o)
e n m i
killRange (Module _ e q t d) = killRange4 (Module noRange) e q t d
killRange (UnquoteDecl _ x t) = killRange2 (UnquoteDecl noRange) x t
killRange (UnquoteDef _ x t) = killRange2 (UnquoteDef noRange) x t
killRange (UnquoteData _ xs cs t) = killRange3 (UnquoteData noRange) xs cs t
Expand Down Expand Up @@ -1161,9 +1166,10 @@ instance KillRange TypedBinding where
killRange (TLet r ds) = killRange2 TLet r ds

instance KillRange WhereClause where
killRange NoWhere = NoWhere
killRange (AnyWhere r d) = killRange1 (AnyWhere noRange) d
killRange (SomeWhere r n a d) = killRange3 (SomeWhere noRange) n a d
killRange NoWhere = NoWhere
killRange (AnyWhere r d) = killRange1 (AnyWhere noRange) d
killRange (SomeWhere r e n a d) =
killRange4 (SomeWhere noRange) e n a d

------------------------------------------------------------------------
-- NFData instances
Expand Down Expand Up @@ -1262,8 +1268,9 @@ instance NFData Declaration where
rnf (Primitive _ a) = rnf a
rnf (Open _ a b) = rnf a `seq` rnf b
rnf (Import _ a b _ c) = rnf a `seq` rnf b `seq` rnf c
rnf (ModuleMacro _ a b _ c) = rnf a `seq` rnf b `seq` rnf c
rnf (Module _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (ModuleMacro _ a b c _ d)
= rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (Module _ a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
rnf (UnquoteDecl _ a b) = rnf a `seq` rnf b
rnf (UnquoteDef _ a b) = rnf a `seq` rnf b
rnf (UnquoteData _ a b c) = rnf a `seq` rnf b `seq` rnf c
Expand Down Expand Up @@ -1330,9 +1337,9 @@ instance NFData ModuleAssignment where
rnf (ModuleAssignment a b c) = rnf a `seq` rnf b `seq` rnf c

instance NFData a => NFData (WhereClause' a) where
rnf NoWhere = ()
rnf (AnyWhere _ a) = rnf a
rnf (SomeWhere _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf NoWhere = ()
rnf (AnyWhere _ a) = rnf a
rnf (SomeWhere _ a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d

instance NFData LamClause where
rnf (LamClause a b c) = rnf (a, b, c)
Expand Down
Loading

0 comments on commit 7993a7b

Please sign in to comment.