Use a record type Globals collecting scopes for definitions, construc…

…tors, and their fields
jespercockx · Jan 17, 2024 · bd95f4b · bd95f4b
1 parent f2e8d9c
commit bd95f4b
Show file tree

Hide file tree

Showing 9 changed files with 78 additions and 83 deletions.
diff --git a/src/Context.agda b/src/Context.agda
@@ -1,9 +1,6 @@
 
-open import Scope.Core
-open import Scope.Split
-open import Scope.Sub
-open import Scope.In
-open import Scope.All
+open import Scope
+open import GlobalScope
 
 open import Haskell.Extra.Dec
 open import Utils.Either
@@ -17,13 +14,11 @@ import Reduce
 
 module Context
   {@0 name  : Set}
-  (@0 defs     : Scope name)
-  (@0 cons     : Scope name)
-  (@0 conArity : All (λ _ → Scope name) cons)
+  (@0 globals : Globals)
   where
 
-open Syntax defs cons conArity
-open Reduce defs cons conArity
+open Syntax globals
+open Reduce globals
 
 private variable
   @0 x y : name

diff --git a/src/Conversion.agda b/src/Conversion.agda
@@ -1,8 +1,5 @@
-open import Scope.Core
-open import Scope.Split
-open import Scope.Sub
-open import Scope.In
-open import Scope.All
+open import Scope
+open import GlobalScope
 
 open import Haskell.Extra.Dec
 open import Utils.Either
@@ -15,16 +12,14 @@ import Syntax
 
 module Conversion
   {@0 name  : Set}
-  (@0 defs     : Scope name)
-  (@0 cons     : Scope name)
-  (@0 conArity : All (λ _ → Scope name) cons)
-  (@0 defType  : All (λ _ → Syntax.Type defs cons conArity mempty) defs)
+  (@0 globals : Globals)
+  (@0 defType : All (λ _ → Syntax.Type globals mempty) (Globals.defScope globals))
   where
 
-open Syntax defs cons conArity
-open import Substitute defs cons conArity
-open import Reduce defs cons conArity
-open import Context defs cons conArity
+open Syntax globals
+open import Substitute globals
+open import Reduce globals
+open import Context globals
 
 private variable
   @0 x y z : name

diff --git a/src/GlobalScope.agda b/src/GlobalScope.agda
@@ -0,0 +1,12 @@
+
+open import Scope
+
+open import Haskell.Prelude hiding (All; s; t)
+
+module GlobalScope {@0 name  : Set} where
+
+record Globals : Set where
+  field
+    defScope   : Scope name
+    conScope   : Scope name
+    fieldScope : All (λ _ → Scope name) conScope
diff --git a/src/Reduce.agda b/src/Reduce.agda
@@ -1,9 +1,6 @@
 
-open import Scope.Core
-open import Scope.Split
-open import Scope.Sub
-open import Scope.In
-open import Scope.All
+open import Scope
+open import GlobalScope
 
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Loop
@@ -20,13 +17,11 @@ import Substitute
 
 module Reduce
   {@0 name  : Set}
-  (@0 defs     : Scope name)
-  (@0 cons     : Scope name)
-  (@0 conArity : All (λ _ → Scope name) cons)
+  (@0 globals : Globals)
   where
 
-open Syntax defs cons conArity
-open Substitute defs cons conArity
+open Syntax globals
+open Substitute globals
 
 private variable
   @0 x     : name
@@ -83,9 +78,9 @@ unState r (MkState e v s) = substTerm (envToSubst r e) (applyElims v s)
 
 {-# COMPILE AGDA2HS unState #-}
 
-lookupBranch : Branches α → (@0 c : name) (p : c ∈ cons)
-             → Maybe ( Rezz _ (lookupAll conArity p)
-                     × Term ((lookupAll conArity p) <> α))
+lookupBranch : Branches α → (@0 c : name) (p : c ∈ conScope)
+             → Maybe ( Rezz _ (lookupAll fieldScope p)
+                     × Term ((lookupAll fieldScope p) <> α))
 lookupBranch [] c k = Nothing
 lookupBranch (BBranch c' k' aty u ∷ bs) c p =
   case decIn k' p of λ where

diff --git a/src/Substitute.agda b/src/Substitute.agda
@@ -1,24 +1,19 @@
 
-open import Scope.Core
-open import Scope.Split
-open import Scope.Sub
-open import Scope.In
-open import Scope.All
+open import Scope
+open import GlobalScope
 
 open import Haskell.Extra.Dec
+open import Haskell.Extra.Erase
 open import Utils.Either
 
 open import Haskell.Prelude hiding (All)
 
 module Substitute
   {@0 name  : Set}
-  (@0 defs     : Scope name)
-  (@0 cons     : Scope name)
-  (@0 conArity : All (λ _ → Scope name) cons)
+  (@0 globalS : Globals)
   where
 
-open import Syntax defs cons conArity
-open import Haskell.Extra.Erase
+open import Syntax globalS
 
 private variable
   @0 x     : name

diff --git a/src/Syntax.agda b/src/Syntax.agda
@@ -7,16 +7,17 @@ open import Haskell.Extra.Erase
 
 open import Utils.Misc
 
--- NOTE(flupe): make Scope export all of the following
 open import Scope
+open import GlobalScope
 
 module Syntax
   {@0 name     : Set}
-  (@0 defs     : Scope name)
-  (@0 cons     : Scope name)
-  (@0 conArity : All (λ _ → Scope name) cons)
+  (@0 globals  : Globals)
   where
 
+module @0 TheGlobals = Globals globals
+open TheGlobals public
+
 private variable
   @0 x     : name
   @0 α β γ : Scope name
@@ -48,9 +49,9 @@ syntax Subst α β = α ⇒ β
 data Term α where
   -- NOTE(flupe): removed tactic arguments for now because hidden arguments not supported yet #217
   TVar  : (@0 x : name) → x ∈ α → Term α
-  TDef  : (@0 d : name) → d ∈ defs → Term α
-  TCon  : (@0 c : name) (c∈cons : c ∈ cons)
-        → (lookupAll conArity c∈cons) ⇒ α → Term α
+  TDef  : (@0 d : name) → d ∈ defScope → Term α
+  TCon  : (@0 c : name) (c∈cons : c ∈ conScope)
+        → (lookupAll fieldScope c∈cons) ⇒ α → Term α
   TLam  : (@0 x : name) (v : Term (x ◃ α)) → Term α
   TApp  : (u : Term α) (es : Elim α) → Term α
   TPi   : (@0 x : name) (su sv : Sort α) (u : Term α) (v : Term (x ◃ α)) → Term α
@@ -71,7 +72,7 @@ funSort (STyp a) (STyp b) = STyp (max a b)
 
 data Elim α where
   EArg  : Term α → Elim α
-  EProj : (@0 x : name) → x ∈ defs → Elim α
+  EProj : (@0 x : name) → x ∈ defScope → Elim α
   ECase : (bs : Branches α) → Elim α
   -- TODO: do we need a type annotation for the return type of case?
 {-# COMPILE AGDA2HS Elim     #-}
@@ -80,9 +81,9 @@ Elims α = List (Elim α)
 {-# COMPILE AGDA2HS Elims #-}
 
 data Branch α where
-  BBranch : (@0 c : name) → (c∈cons : c ∈ cons)
-          → Rezz _ (lookupAll conArity c∈cons)
-          → Term (lookupAll conArity c∈cons <> α) → Branch α
+  BBranch : (@0 c : name) → (c∈cons : c ∈ conScope)
+          → Rezz _ (lookupAll fieldScope c∈cons)
+          → Term (lookupAll fieldScope c∈cons <> α) → Branch α
 {-# COMPILE AGDA2HS Branch   #-}
 
 Branches α = List (Branch α)

diff --git a/src/TestReduce.agda b/src/TestReduce.agda
@@ -8,11 +8,8 @@ open import Haskell.Extra.Erase
 open import Haskell.Extra.Refinement
 open import Haskell.Extra.Delay
 
-open import Scope.Core
-open import Scope.In
-open import Scope.All
-open import Scope.Split
-open import Scope.Sub
+open import Scope
+open import GlobalScope
 
 name = String
 
@@ -34,8 +31,15 @@ cons = bind "true" $ bind "false" mempty
 conArity : All (λ _ → Scope name) cons
 conArity = allJoin (allSingl mempty) (allJoin (allSingl mempty) allEmpty)
 
-open import Syntax defs cons conArity
-open import Reduce defs cons conArity
+globals : Globals
+globals = record 
+  { defScope = defs
+  ; conScope = cons
+  ; fieldScope = conArity
+  }
+
+open import Syntax globals
+open import Reduce globals
 
 opaque
   unfolding lookupAll inHere inThere splitRefl splitJoinRight subBindDrop subLeft

diff --git a/src/Typechecker.agda b/src/Typechecker.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Scope
+open import GlobalScope
 import Syntax
 import Reduce
 import Typing
@@ -14,16 +15,14 @@ open import Agda.Primitive
 
 module Typechecker
     {@0 name  : Set}
-    (defs     : Scope name)
-    (cons     : Scope name)
-    (conArity : All (λ _ → Scope name) cons)
-    (defType  : All (λ _ → Syntax.Type defs cons conArity mempty) defs)
+    (@0 globals : Globals)
+    (defType  : All (λ _ → Syntax.Type globals (mempty {{iMonoidScope}})) (Globals.defScope globals))
   where
 
-open Syntax defs cons conArity
-open Typing defs cons conArity defType
-open Context defs cons conArity
-open Conversion defs cons conArity defType
+open Syntax globals
+open Context globals
+open Conversion globals defType
+open Typing globals defType
 
 private
   variable @0 α : Scope name
@@ -82,7 +81,7 @@ inferTySort : (s : Sort α)
 inferTySort = {!!}
 
 checkDef : (@0 f : name)
-           (p : f ∈ defs)
+           (p : f ∈ defScope)
            (ty : Type α)
            → TCM (Γ ⊢ TDef f p ∷ ty)
 checkDef = {!!}

diff --git a/src/Typing.agda b/src/Typing.agda
@@ -2,6 +2,7 @@
 -- open import Utils
 -- open Variables
 open import Scope
+open import GlobalScope
 import Syntax
 import Reduce
 import Context
@@ -14,17 +15,15 @@ open import Haskell.Extra.Loop
 
 module Typing
     {@0 name  : Set}
-    (@0 defs     : Scope name)
-    (@0 cons     : Scope name)
-    (@0 conArity : All (λ _ → Scope name) cons)
-    (@0 defType  : All (λ _ → Syntax.Type defs cons conArity mempty) defs)
+    (@0 globals : Globals)
+    (@0 defType : All (λ _ → Syntax.Type globals (mempty {{iMonoidScope}})) (Globals.defScope globals))
   where
 
-open Syntax defs cons conArity
-open Reduce defs cons conArity
-open Context defs cons conArity
-open Conversion defs cons conArity defType
-open Substitute defs cons conArity
+open Syntax globals
+open Substitute globals
+open Reduce globals
+open Context globals
+open Conversion globals defType
 
 private variable
   @0 x y : name
@@ -57,7 +56,7 @@ data TyTerm {α} Γ where
         -------------------
         → Γ ⊢ TVar x p ∷ (lookupVar Γ x p)
 
-    TyDef : (@0 f : name) {@0 p : f ∈ defs}
+    TyDef : (@0 f : name) {@0 p : f ∈ defScope}
 
         -------------------------------------------------
         → Γ ⊢ TDef f p ∷ (weaken subEmpty (defType ! f))