Skip to content

Commit 185a4ee

Browse files
jmougeotjmougeot
authored
[Import] Reflection (#2643)
* [Import] * base
1 parent e65f729 commit 185a4ee

17 files changed

+97
-103
lines changed

‎src/Reflection/AST/Abstraction.agda

+5-5
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@
88

99
module Reflection.AST.Abstraction where
1010

11-
open import Data.String.Base as String using (String)
12-
open import Data.String.Properties as String using (_≟_)
13-
open import Data.Product.Base using (_×_; <_,_>; uncurry)
11+
open import Data.String.Base as String using (String)
12+
open import Data.String.Properties as String using (_≟_)
13+
open import Data.Product.Base using (_×_; <_,_>; uncurry)
1414
open import Level using (Level)
15-
open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
16-
open import Relation.Binary.Definitions using (DecidableEquality)
15+
open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
16+
open import Relation.Binary.Definitions using (DecidableEquality)
1717
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
1818

1919
private

‎src/Reflection/AST/AlphaEquality.agda

+14-15
Original file line numberDiff line numberDiff line change
@@ -8,21 +8,20 @@
88

99
module Reflection.AST.AlphaEquality where
1010

11-
open import Data.Bool.Base using (Bool; true; false; _∧_)
12-
open import Data.List.Base using ([]; _∷_)
13-
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_)
14-
open import Data.Product.Base using (_,_)
15-
open import Relation.Nullary.Decidable.Core using (⌊_⌋)
16-
open import Relation.Binary.Definitions using (DecidableEquality)
17-
18-
open import Reflection.AST.Abstraction
19-
open import Reflection.AST.Argument
20-
open import Reflection.AST.Argument.Information as ArgInfo
21-
open import Reflection.AST.Argument.Modality as Modality
22-
open import Reflection.AST.Argument.Visibility as Visibility
23-
open import Reflection.AST.Meta as Meta
24-
open import Reflection.AST.Name as Name
25-
open import Reflection.AST.Literal as Literal
11+
open import Data.Bool.Base using (Bool; true; false; _∧_)
12+
open import Data.List.Base using ([]; _∷_)
13+
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_)
14+
open import Data.Product.Base using (_,_)
15+
open import Relation.Nullary.Decidable.Core using (⌊_⌋)
16+
open import Relation.Binary.Definitions using (DecidableEquality)
17+
open import Reflection.AST.Abstraction using (Abs; abs)
18+
open import Reflection.AST.Argument using (Arg; arg; Args)
19+
open import Reflection.AST.Argument.Information as ArgInfo using (ArgInfo)
20+
open import Reflection.AST.Argument.Modality as Modality using (Modality)
21+
open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
22+
open import Reflection.AST.Meta as Meta using (Meta)
23+
open import Reflection.AST.Name as Name using (Name)
24+
open import Reflection.AST.Literal as Literal using (Literal)
2625
open import Reflection.AST.Term
2726
open import Level using (Level)
2827

‎src/Reflection/AST/Argument.agda

+5-6
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,12 @@
88

99
module Reflection.AST.Argument where
1010

11-
open import Data.List.Base as List using (List; []; _∷_)
12-
open import Data.Product.Base using (_×_; <_,_>; uncurry)
13-
open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
14-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Data.List.Base as List using (List; []; _∷_)
12+
open import Data.Product.Base using (_×_; <_,_>; uncurry)
13+
open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
14+
open import Relation.Binary.Definitions using (DecidableEquality)
1515
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
16-
open import Level
17-
16+
open import Level using (Level)
1817
open import Reflection.AST.Argument.Visibility
1918
open import Reflection.AST.Argument.Relevance
2019
open import Reflection.AST.Argument.Quantity

‎src/Reflection/AST/Argument/Information.agda

+3-4
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,10 @@
88

99
module Reflection.AST.Argument.Information where
1010

11-
open import Data.Product.Base using (_×_; <_,_>; uncurry)
12-
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
13-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Data.Product.Base using (_×_; <_,_>; uncurry)
12+
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
13+
open import Relation.Binary.Definitions using (DecidableEquality)
1414
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
15-
1615
open import Reflection.AST.Argument.Modality as Modality using (Modality)
1716
open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
1817

‎src/Reflection/AST/Argument/Modality.agda

+3-4
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,10 @@
88

99
module Reflection.AST.Argument.Modality where
1010

11-
open import Data.Product.Base using (_×_; <_,_>; uncurry)
12-
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
13-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Data.Product.Base using (_×_; <_,_>; uncurry)
12+
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
13+
open import Relation.Binary.Definitions using (DecidableEquality)
1414
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
15-
1615
open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
1716
open import Reflection.AST.Argument.Quantity as Quantity using (Quantity)
1817

‎src/Reflection/AST/Argument/Quantity.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Reflection.AST.Argument.Quantity where
1010

11-
open import Relation.Nullary.Decidable.Core using (yes; no)
12-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Relation.Nullary.Decidable.Core using (yes; no)
12+
open import Relation.Binary.Definitions using (DecidableEquality)
1313
open import Relation.Binary.PropositionalEquality.Core using (refl)
1414

1515
------------------------------------------------------------------------

‎src/Reflection/AST/Argument/Relevance.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Reflection.AST.Argument.Relevance where
1010

11-
open import Relation.Nullary.Decidable.Core using (yes; no)
12-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Relation.Nullary.Decidable.Core using (yes; no)
12+
open import Relation.Binary.Definitions using (DecidableEquality)
1313
open import Relation.Binary.PropositionalEquality.Core using (refl)
1414

1515
------------------------------------------------------------------------

‎src/Reflection/AST/Argument/Visibility.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Reflection.AST.Argument.Visibility where
1010

11-
open import Relation.Nullary.Decidable.Core using (yes; no)
12-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
open import Relation.Nullary.Decidable.Core using (yes; no)
12+
open import Relation.Binary.Definitions using (DecidableEquality)
1313
open import Relation.Binary.PropositionalEquality.Core using (refl)
1414

1515
------------------------------------------------------------------------

‎src/Reflection/AST/DeBruijn.agda

+4-5
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,13 @@
88

99
module Reflection.AST.DeBruijn where
1010

11-
open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
12-
open import Data.Nat.Base using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
11+
open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
12+
open import Data.Nat.Base using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
1313
open import Data.List.Base using (List; []; _∷_; _++_)
1414
open import Data.Maybe.Base using (Maybe; nothing; just)
15-
import Data.Maybe.Effectful as Maybe
16-
import Function.Identity.Effectful as Identity
15+
import Data.Maybe.Effectful as Maybe using (applicative)
16+
import Function.Identity.Effectful as Identity using (applicative)
1717
open import Effect.Applicative using (RawApplicative; mkRawApplicative)
18-
1918
open import Reflection
2019
open import Reflection.AST.Argument.Visibility using (Visibility)
2120
import Reflection.AST.Traversal as Traverse

‎src/Reflection/AST/Definition.agda

+9-10
Original file line numberDiff line numberDiff line change
@@ -8,17 +8,16 @@
88

99
module Reflection.AST.Definition where
1010

11-
import Data.List.Properties as List using (≡-dec)
12-
import Data.Nat.Properties as ℕ using (_≟_)
13-
open import Data.Product.Base using (_×_; <_,_>; uncurry)
14-
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; yes; no)
15-
open import Relation.Binary.Definitions using (DecidableEquality)
11+
import Data.List.Properties as List using (≡-dec)
12+
import Data.Nat.Properties as ℕ using (_≟_)
13+
open import Data.Product.Base using (_×_; <_,_>; uncurry)
14+
open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; yes; no)
15+
open import Relation.Binary.Definitions using (DecidableEquality)
1616
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
17-
18-
import Reflection.AST.Argument as Arg
19-
import Reflection.AST.Argument.Quantity as Quantity
20-
import Reflection.AST.Name as Name
21-
import Reflection.AST.Term as Term
17+
import Reflection.AST.Argument as Arg using (Arg; ≡-dec)
18+
import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≟_)
19+
import Reflection.AST.Name as Name using (Name; _≟_)
20+
import Reflection.AST.Term as Term using (Term; _≟-Clauses_)
2221

2322
------------------------------------------------------------------------
2423
-- Re-exporting type publicly

‎src/Reflection/AST/Literal.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ import Data.String.Properties as String
1616
import Data.Word64.Properties as Word64
1717
import Reflection.AST.Meta as Meta
1818
import Reflection.AST.Name as Name
19-
open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes)
20-
open import Relation.Binary.Definitions using (DecidableEquality)
19+
open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes)
20+
open import Relation.Binary.Definitions using (DecidableEquality)
2121
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
2222

2323
------------------------------------------------------------------------

‎src/Reflection/AST/Meta.agda

+6-6
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@
88

99
module Reflection.AST.Meta where
1010

11-
import Data.Nat.Properties as ℕ
12-
open import Function.Base using (_on_)
13-
open import Relation.Nullary.Decidable.Core using (map′)
14-
open import Relation.Binary.Core using (Rel)
15-
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
16-
import Relation.Binary.Construct.On as On
11+
import Data.Nat.Properties as ℕ using (_≟_)
12+
open import Function.Base using (_on_)
13+
open import Relation.Nullary.Decidable.Core using (map′)
14+
open import Relation.Binary.Core using (Rel)
15+
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
16+
import Relation.Binary.Construct.On as On using (decidable)
1717
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
1818

1919
open import Agda.Builtin.Reflection public

‎src/Reflection/AST/Name.agda

+7-7
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,14 @@
88

99
module Reflection.AST.Name where
1010

11-
open import Data.List.Base using (List)
11+
open import Data.List.Base using (List)
1212
import Data.Product.Properties as Prodₚ using (≡-dec)
13-
import Data.Word64.Properties as Wₚ using (_≟_)
14-
open import Function.Base using (_on_)
15-
open import Relation.Nullary.Decidable.Core using (map′)
16-
open import Relation.Binary.Core using (Rel)
17-
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
18-
open import Relation.Binary.Construct.On using (decidable)
13+
import Data.Word64.Properties as Wₚ using (_≟_)
14+
open import Function.Base using (_on_)
15+
open import Relation.Nullary.Decidable.Core using (map′)
16+
open import Relation.Binary.Core using (Rel)
17+
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
18+
open import Relation.Binary.Construct.On using (decidable)
1919
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
2020

2121
------------------------------------------------------------------------

‎src/Reflection/AST/Term.agda

+15-16
Original file line numberDiff line numberDiff line change
@@ -8,25 +8,24 @@
88

99
module Reflection.AST.Term where
1010

11-
open import Data.List.Base as List hiding (_++_)
12-
open import Data.List.Properties using (∷-dec)
13-
open import Data.Nat.Base using (ℕ; zero; suc)
14-
import Data.Nat.Properties as ℕ
15-
open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
16-
open import Data.Product.Properties using (,-injective)
17-
open import Data.Maybe.Base using (Maybe; just; nothing)
18-
open import Data.String.Base using (String)
19-
open import Data.String.Properties as String hiding (_≟_)
20-
open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
21-
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
11+
open import Data.List.Base as List hiding (_++_)
12+
open import Data.List.Properties using (∷-dec)
13+
open import Data.Nat.Base using (ℕ; zero; suc)
14+
import Data.Nat.Properties as ℕ using (_≟_)
15+
open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
16+
open import Data.Product.Properties using (,-injective)
17+
open import Data.Maybe.Base using (Maybe; just; nothing)
18+
open import Data.String.Base using (String)
19+
open import Data.String.Properties as String hiding (_≟_)
20+
open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
21+
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
2222
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
23-
24-
open import Reflection.AST.Abstraction
25-
open import Reflection.AST.Argument
23+
open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec)
24+
open import Reflection.AST.Argument as Arg
2625
open import Reflection.AST.Argument.Information using (visibility)
2726
open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_)
28-
import Reflection.AST.Literal as Literal
29-
import Reflection.AST.Meta as Meta
27+
import Reflection.AST.Literal as Literal using (Literal; _≟_)
28+
import Reflection.AST.Meta as Meta using (Meta; _≟_)
3029
open import Reflection.AST.Name as Name using (Name)
3130

3231
------------------------------------------------------------------------

‎src/Reflection/AST/Traversal.agda

+5-5
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,12 @@ open import Effect.Applicative using (RawApplicative)
1111
module Reflection.AST.Traversal
1212
{F : Set → Set} (AppF : RawApplicative F) where
1313

14-
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
15-
open import Data.List.Base using (List; []; _∷_; _++_; reverse; length)
16-
open import Data.String.Base using (String)
14+
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
15+
open import Data.List.Base using (List; []; _∷_; _++_; reverse; length)
16+
open import Data.String.Base using (String)
1717
open import Data.Product.Base using (_×_; _,_)
18-
open import Function.Base using (_∘_)
19-
open import Reflection hiding (pure)
18+
open import Function.Base using (_∘_)
19+
open import Reflection hiding (pure)
2020

2121
open RawApplicative AppF
2222

‎src/Reflection/AST/Universe.agda

+5-5
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@
88

99
module Reflection.AST.Universe where
1010

11-
open import Data.List.Base using (List)
12-
open import Data.String.Base using (String)
13-
open import Data.Product.Base using (_×_)
14-
open import Reflection.AST.Argument using (Arg)
11+
open import Data.List.Base using (List)
12+
open import Data.String.Base using (String)
13+
open import Data.Product.Base using (_×_)
14+
open import Reflection.AST.Argument using (Arg)
1515
open import Reflection.AST.Abstraction using (Abs)
16-
open import Reflection.AST.Term using (Term; Pattern; Sort; Clause)
16+
open import Reflection.AST.Term using (Term; Pattern; Sort; Clause)
1717

1818
data Univ : Set where
1919
⟨term⟩ : Univ

‎src/Reflection/AnnotatedAST/Free.agda

+8-7
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,17 @@
88

99
module Reflection.AnnotatedAST.Free where
1010

11-
open import Data.Bool.Base using (if_then_else_)
12-
open import Data.Nat.Base using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
13-
open import Data.List.Base using (List; []; _∷_; [_]; concatMap; length)
11+
open import Data.Bool.Base using (if_then_else_)
12+
open import Data.Nat.Base using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
13+
open import Data.List.Base using (List; []; _∷_; [_]; concatMap; length)
1414
open import Data.List.Relation.Unary.All using (_∷_)
15-
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
16-
open import Data.String.Base using (String)
17-
18-
open import Reflection
15+
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
16+
open import Data.String.Base using (String)
1917
open import Reflection.AST.Universe
18+
using (⟨term⟩; ⟨pat⟩; ⟨clause⟩; ⟨abs⟩; ⟨tel⟩; ⟦_⟧)
2019
open import Reflection.AnnotatedAST
20+
using (Annotated; AnnotationFun; annotate; defaultAnn; ⟨_⟩_; var; absurd
21+
; clause; absurd-clause; abs)
2122

2223
------------------------------------------------------------------------
2324
-- Free variable sets as lists of natural numbers

0 commit comments

Comments
 (0)