Tactic.Derive.DecEq: faster variant

Author: omelkonian

Meta/Init.agda

@@ -5,8 +5,6 @@ module Meta.Init where
 open import Reflection.Debug public
 open import Reflection.TCI public
 open import Reflection.Syntax public
-open import Reflection.AST.Term public
-  using (vΠ[_∶_]_)
 
 instance
   iMonad-TC = Monad-TC

Reflection/Syntax.agda

@@ -4,40 +4,39 @@ module Reflection.Syntax where
 
 open import Meta.Prelude
 
-open import Reflection.AST.Argument public
-  hiding (map)
-open import Reflection.AST.Term public
-  hiding (_≟_; getName)
-open import Reflection.AST.Name public
-  hiding (_≟_; _≡ᵇ_; _≈_; _≈?_)
 open import Reflection.AST.Definition public
-  hiding (_≟_)
-open import Reflection.AST.Meta public
-  hiding (_≟_; _≡ᵇ_; _≈_; _≈?_)
+  using (Definition; function; data-type; axiom; record′; constructor′; primitive′)
+open import Reflection.AST.Pattern public
+  using (Pattern; con; dot; var; lit; proj; absurd)
+open import Reflection.AST.Term public
+  using ( Term; pi; var; con; def; lam; pat-lam; sort; lit; meta; unknown
+        ; vLam; hLam; iLam; Π[_∶_]_; vΠ[_∶_]_; hΠ[_∶_]_; iΠ[_∶_]_
+        ; Type; Telescope
+        ; Sort; set; prop; propLit; inf
+        ; Clause; Clauses; clause; absurd-clause
+        )
 open import Reflection.AST.Abstraction public
-  using (unAbs)
-
-open import Agda.Builtin.Reflection public
-  using (ArgInfo; Modality; Visibility; Literal; Meta)
-
+  using (Abs; abs; unAbs)
 open import Reflection.AST.Argument public
-  using (Arg; arg)
+  using (Arg; Args; arg; vArg; hArg; iArg; unArg; _⟨∷⟩_; map-Args)
+open import Reflection.AST.Literal public
+  using (Literal)
+open import Reflection.AST.Meta public
+  using (Meta)
+open import Reflection.AST.Name public
+  using (Name)
 open import Reflection.AST.Argument.Visibility public
   using (Visibility; visible; hidden; instance′)
 open import Reflection.AST.Argument.Information public
   using (ArgInfo; arg-info)
-open import Reflection.AST.Abstraction public
-  using (Abs; abs; unAbs)
-open import Reflection.AST.Argument public
-  using (vArg; hArg; iArg; unArg; _⟨∷⟩_; map-Args)
+open import Reflection.AST.Argument.Modality public
+  using (Modality; modality)
+open import Reflection.AST.Argument.Relevance public
+  using (Relevance; relevant; irrelevant)
 open import Reflection public
-  using ( Name; Meta; Literal; Pattern; Clause
-        ; ErrorPart; strErr
-        ; Term; Type; pi; var; con; def; lam; pat-lam; agda-sort; lit; meta; unknown
-        ; Definition; data-cons; data-type; record-type
-        )
+  using (ErrorPart; strErr)
 
-open import Reflection using (hidden; instance′; TC)
+open import Reflection using (TC)
 
 -- ** Smart constructors
 
@@ -103,7 +102,7 @@ pattern _◇ n = Pattern.con n []
 pattern _◇⟦_⟧ n x = Pattern.con n (vArg x ∷ [])
 pattern _◇⟦_∣_⟧ n x y = Pattern.con n (vArg x ∷ vArg y ∷ [])
 
-pattern `Set = agda-sort (set (quote 0ℓ ∙))
+pattern `Set = sort (set (quote 0ℓ ∙))
 
 -- ** useful type aliases
 PatTelescope = Telescope

Reflection/Utils/Args.agda

@@ -2,7 +2,7 @@
 module Reflection.Utils.Args where
 
 open import Meta.Prelude
-open import Meta.Init hiding (toℕ)
+open import Meta.Init
 
 open import Data.List using (map; zip)
 open import Data.Fin using (toℕ)

Reflection/Utils/Core.agda

@@ -49,6 +49,11 @@ argTys = proj₁ ∘ viewTy′
 resultTy : Type → Type
 resultTy = proj₂ ∘ viewTy′
 
+tyTele : Type → Telescope
+tyTele = λ where
+  (Π[ s ∶ a ] ty) → (s , a) ∷ tyTele ty
+  _ → []
+
 -- ** definitions
 
 record DataDef : Set where

Reflection/Utils/Metas.agda

@@ -20,7 +20,7 @@ mutual
     (lam _ (abs _ x)) → findMetas x
     (pat-lam cs as)   → findMetasCl cs ++ findMetas* as
     (pi (arg _ a) (abs _ b)) → findMetas a ++ findMetas b
-    (agda-sort _) → []
+    (sort _)      → []
     (lit _)       → []
     m@(meta x as) → m ∷ findMetas* as
     unknown       → []
@@ -33,5 +33,5 @@ mutual
   findMetasCl : List Clause → List Term
   findMetasCl = λ where
     [] → []
-    (Clause.clause _ _ t ∷ c)      → findMetas t ++ findMetasCl c
-    (Clause.absurd-clause _ _ ∷ c) → findMetasCl c
+    (clause _ _ t      ∷ c) → findMetas t ++ findMetasCl c
+    (absurd-clause _ _ ∷ c) → findMetasCl c

Reflection/Utils/Substitute.agda

@@ -28,7 +28,7 @@ mutual
     (lam v t)      → lam v (substAbs x s t)
     (pat-lam _ _)  → unknown  -- ignoring for now
     (pi a b)       → pi (substArg x s a) (substAbs x s b)
-    (agda-sort st) → agda-sort (substSort x s st)
+    (sort st)      → sort (substSort x s st)
     (lit l)        → lit l
     (meta m as)    → meta m (substArgs x s as)
     unknown        → unknown
@@ -75,8 +75,8 @@ module _ (f : ℕ → ℕ) where
         → pat-lam (mapFreeVarsᶜ∗ bound cs) (mapFreeVars∗ bound as)
       (pi (arg i t) (abs x t′))
         → pi (arg i (mapFreeVars bound t)) (abs x (mapFreeVars (suc bound) t′))
-      (agda-sort s)
-        → agda-sort (mapFreeVarsˢ bound s)
+      (sort s)
+        → sort (mapFreeVarsˢ bound s)
       (meta x as)
         → meta x (mapFreeVars∗ bound as)
       t → t

Reflection/Utils/TCI.agda

@@ -78,7 +78,7 @@ ensureNoMetas = λ where
   (lam v (abs _ t)) → ensureNoMetas t
   (pat-lam cs args) → noMetaClauses cs >> noMetaArgs args
   (pi a b) → noMetaArg a >> noMetaAbs b
-  (agda-sort s) → noMetaSort s
+  (sort s) → noMetaSort s
   (lit l) → return _
   -- (meta x _) → errorP "meta found!"
   (meta x _) → blockOnMeta x
@@ -233,7 +233,7 @@ getDataDef n = inDebugPath "getDataDef" do
 
 getRecordDef : Name → M RecordDef
 getRecordDef n = do
-  (record-type c fs) ← getDefinition n
+  (record′ c fs) ← getDefinition n
     where _ → error1 "Not a record definition!"
   args ← proj₁ <$> getType' n
   return (record { name = c ; fields = fs ; params = args })
@@ -260,7 +260,7 @@ getFuel s = do
 
 isSort : Term → M Bool
 isSort t = do
-  (agda-sort _) ← normalise t
+  (sort _) ← normalise t
     where _ → return false
   return true
 

Tactic.agda

@@ -18,6 +18,7 @@ open import Tactic.J public
 open import Tactic.ReduceDec public
 
 open import Tactic.Derive.DecEq public
+open import Tactic.Derive.DecEqFast
 open import Tactic.Derive.Show public
 open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests
 open import Tactic.Derive.Convertible public

Tactic/Derive/Convertible.agda

@@ -119,7 +119,7 @@ doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
 -- Deriving a Convertible instance. Usage
 --   unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
 deriveConvertible : Name → Name → Name → R.TC ⊤
-deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
+deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (sort (lit 0)) do
   agdaDef ← getDefinition agdaName
   hsDef   ← getDefinition hsName
   -- instName ← freshName $ "Convertible" S.++ show hsName

Tactic/Derive/DecEq.agda

@@ -21,6 +21,7 @@ open import Relation.Nullary
 open import Reflection.Tactic
 open import Reflection.QuotedDefinitions
 open import Reflection.AST.DeBruijn
+open import Reflection.AST.Pattern using () renaming (_≟_ to _≟-Pattern_)
 
 open import Class.DecEq.Core
 open import Class.Functor