Mikan port

.github/workflows/build.yml

@@ -58,15 +58,15 @@ jobs:
       - name: Typecheck 👩‍🏫
         run: |
           nix-shell --run "$build_command"
-        # Run Agda as a separate stage so it doesn't have to be subject to
+        # Run Mikan as a separate stage so it doesn't have to be subject to
         # the absolutely spartan GC tuning parameters we run the build in
         # CI with
         env:
           NIX_BUILD_SHELL: bash
           build_command: |
             set -eu
             1lab-shake _build/all-pages.agda
-            agda-nodebug _build/all-pages.agda -j4 +RTS -s -RTS
+            mikan-nodebug _build/all-pages.agda -j4 +RTS -s -RTS
 
       - name: Build 🛠️
         run: |

1lab.agda-lib

@@ -4,12 +4,8 @@ include:
   wip
   _build
 flags:
-  --cubical
+  --prop
   --no-load-primitives
   --postfix-projections
-  --rewriting
-  --guardedness
-  --two-level
   -W noUnsupportedIndexedMatch
-  -W noRewriteVariablesBoundInSingleton
   --experimental-lazy-instances

cabal.project

@@ -1,12 +1,12 @@
 packages: support/shake/1lab-shake.cabal
 
 -- To build outside of the Nix shell, uncomment the following stanza
--- and replace `master` with the `rev` field from `support/nix/dep/Agda/github.json`.
+-- and replace `main` with the `rev` field from `support/nix/dep/mikan/github.json`.
 --
 -- If you want to avoid polluting your Git tree, you can move this to
 -- `cabal.project.local`, which is ignored by Git.
 
 -- source-repository-package
 --   type: git
---   location: https://github.com/agda/agda.git
+--   location: https://codeberg.org/1lab/mikan.git
 --   tag: master

default.nix

@@ -98,7 +98,7 @@ in
 
     passthru = {
       inherit pkgs shakefile deps sort-imports nodeModules;
-      inherit (pkgs.labHaskellPackages) Agda;
+      inherit (pkgs.labHaskellPackages) Mikan;
       texlive = our-texlive;
     };
   }

shell.nix

@@ -11,10 +11,10 @@ the1lab.overrideAttrs (old: {
 
   nativeBuildInputs = old.nativeBuildInputs or [] ++ [
     (with pkgs.labHaskellPackages; pkgs.symlinkJoin {
-      name  = "agda-nodebug";
-      paths = [ Agda sort-imports ];
+      name  = "mikan";
+      paths = [ Mikan sort-imports ];
       postBuild = ''
-        ln -sf ${Agda.nodebug}/bin/agda $out/bin/agda-nodebug
+        ln -sf ${Mikan.nodebug}/bin/mikan $out/bin/mikan-nodebug
       '';
     })
   ];

src/1Lab/Equiv.lagda.md

@@ -118,9 +118,7 @@ inverse is again an isomorphism.
 
 ```agda
   inverse : is-iso from
-  inverse .from = f
-  inverse .rinv = linv
-  inverse .linv = rinv
+  inverse = record { from = f ; rinv = linv ; linv = rinv }
 ```
 
 <!--

src/1Lab/Reflection.lagda.md

@@ -22,7 +22,6 @@ open import Data.String.Base public
 open import Meta.Traversable public
 open import Data.Float.Base public
 open import Data.Maybe.Base public
-open import Data.Word.Base public
 open import Meta.Idiom public
 open import Meta.Bind public
 open import Meta.Alt public
@@ -103,9 +102,6 @@ private module P where
   -- "blocking" constraints.
     noConstraints : ∀ {a} {A : Type a} → TC A → TC A
 
-  -- Run the given computation at the type level, allowing use of erased things.
-    work-on-types : ∀ {a} {A : Type a} → TC A → TC A
-
   -- Run the given TC action and return the first component. Resets to
   -- the old TC state if the second component is 'false', or keep the
   -- new TC state if it is 'true'.
@@ -116,7 +112,7 @@ private module P where
     get-instances : Meta → TC (List Term)
 
     declareData      : Name → Nat → Term → TC ⊤
-    defineData       : Name → List (Name × Quantity × Term) → TC ⊤
+    defineData       : Name → List (Name × Term) → TC ⊤
 ```
 
 <details>
@@ -161,7 +157,6 @@ private module P where
   {-# BUILTIN AGDATCMASKEXPANDLAST     askExpandLast              #-}
   {-# BUILTIN AGDATCMASKREDUCEDEFS     askReduceDefs              #-}
   {-# BUILTIN AGDATCMNOCONSTRAINTS     noConstraints              #-}
-  {-# BUILTIN AGDATCMWORKONTYPES       work-on-types              #-}
   {-# BUILTIN AGDATCMRUNSPECULATIVE    run-speculative            #-}
   {-# BUILTIN AGDATCMGETINSTANCES      get-instances              #-}
   {-# BUILTIN AGDATCMDECLAREDATA       declareData                #-}
@@ -201,7 +196,7 @@ idfun : ∀ {ℓ} (A : Type ℓ) → A → A
 idfun A x = x
 
 under-abs : ∀ {ℓ} {A : Type ℓ} → Term → TC A → TC A
-under-abs (lam v (abs nm _)) m = extend-context nm (arg (arginfo v (modality relevant quantity-ω)) unknown) m
+under-abs (lam v (abs nm _)) m = extend-context nm (arg (arginfo v) unknown) m
 under-abs (pi a (abs nm _))  m = extend-context nm a m
 under-abs _ m = m
 
@@ -294,9 +289,9 @@ blocking-meta (lit l)          = nothing
 blocking-meta (meta x _)       = just (blocker-meta x)
 blocking-meta unknown          = nothing
 
-blocking-meta* (arg (arginfo visible _)   tm ∷ _) = blocking-meta tm
-blocking-meta* (arg (arginfo instance' _) tm ∷ _) = blocking-meta tm
-blocking-meta* (arg (arginfo hidden _)    tm ∷ as) = blocking-meta* as
+blocking-meta* (arg (arginfo visible)   tm ∷ _) = blocking-meta tm
+blocking-meta* (arg (arginfo instance') tm ∷ _) = blocking-meta tm
+blocking-meta* (arg (arginfo hidden)    tm ∷ as) = blocking-meta* as
 
 blocking-meta* [] = nothing
 

src/1Lab/Reflection/Copattern.agda

@@ -202,9 +202,9 @@ private module Test where
   module _ (r : Record Nat) where
     open Record r
     via-function : Record Nat
-    via-function .c = suc c
-    via-function .f = suc ∘ f
-    via-function .const = ap suc const
+    via-function .Record.c = suc c
+    via-function .Record.f = suc ∘ f
+    via-function .Record.const = ap suc const
 
   -- Also works when applied to the result of a function.
   unquoteDecl copat-decl-via-function = declare-copattern copat-decl-via-function (via-function via-ctor)

src/1Lab/Reflection/Deriving/Show.agda

@@ -105,14 +105,14 @@ private
 
   -- Create the clause of shows-prec for a constructor.
   show-clause : Constructor → TC Clause
-  show-clause (conhead conm _ _ args _) = do
+  show-clause (conhead conm _ args _) = do
     let
       -- We'll only show the visible arguments to the constructor.
       -- Moreover, since Agda can infer the types in the telescope
       -- better than we can specify them here, we replace everything
       -- with `unknown`.
       tele = map (λ (s , arg i t) → s , arg i unknown) $
-        filter (λ { (_ , arg (arginfo visible _) _) → true
+        filter (λ { (_ , arg (arginfo visible) _) → true
                   ; _ → false
                   })
           args
@@ -198,9 +198,6 @@ instance
 
   unquoteDecl Show-Literal    = derive-show Show-Literal    (quote Literal)
   unquoteDecl Show-Visibility = derive-show Show-Visibility (quote Visibility)
-  unquoteDecl Show-Relevance  = derive-show Show-Relevance  (quote Relevance)
-  unquoteDecl Show-Quantity   = derive-show Show-Quantity   (quote Quantity)
-  unquoteDecl Show-Modality   = derive-show Show-Modality   (quote Modality)
   unquoteDecl Show-ArgInfo    = derive-show Show-ArgInfo    (quote ArgInfo)
   unquoteDecl Show-Abs        = derive-show Show-Abs        (quote Abs)
   unquoteDecl Show-Arg        = derive-show Show-Arg        (quote Arg)

src/1Lab/Reflection/Induction.agda

@@ -234,8 +234,7 @@ private
           -- Otherwise, add m : T to the telescope and replace the corresponding
           -- constructor with m henceforth.
           method ← ("P" <>_) <$> render-name c
-          q ← get-con-quantity c
-          let argC = arg (arginfo visible (modality relevant q))
+          let argC = arg (arginfo visible)
           let
             ps = raise 1 ps
             P = raise 1 P
@@ -244,7 +243,7 @@ private
             ×-map₁₂ ((method , argC methodT) ∷_) (α ∷_)
 
 make-elim-with : Elim-options → Name → Name → TC ⊤
-make-elim-with opts elim D = work-on-types $ withNormalisation true do
+make-elim-with opts elim D = withNormalisation true do
   DT ← get-type D >>= normalise -- D : (ps : Γ) (is : Ξ) → Type _
   data-type pars cs ← get-definition D
     where _ → typeError [ "not a data type: " , nameErr D ]
@@ -260,7 +259,7 @@ make-elim-with opts elim D = work-on-types $ withNormalisation true do
     argP = if hide-motive then argH else argN
     motiveTel = ("ℓ" , argH (quoteTerm Level))
               -- P : DTel → Type ℓ
-              ∷ ("P" , argP (unpi-view (PTel DTel) (agda-sort (set (var (length (PTel DTel)) [])))))
+              ∷ ("P" , argP (unpi-view (PTel DTel) (agda-sort (type (var (length (PTel DTel)) [])))))
               ∷ []
     DTel = raise 1 DTel
     -- We want to take is-hlevel as an argument, but we need to work in a context

src/1Lab/Reflection/Marker.agda

@@ -50,7 +50,7 @@ abstract-marker = go 0 where
     a ← go k a
     pure (pi (arg i a) (abs x t))
   go k (agda-sort s) with s
-  ... | set t = agda-sort ∘ set <$> go k t
+  ... | type t = agda-sort ∘ type <$> go k t
   ... | lit n = pure (agda-sort (lit n))
   ... | prop t = agda-sort ∘ prop <$> go k t
   ... | propLit n = pure (agda-sort (propLit n))

src/1Lab/Reflection/Record.agda

@@ -154,7 +154,7 @@ make-record-iso-sigma declare? nm `R = do
 
   let fields = field-names→paths fields
 
-  when declare? $ work-on-types do
+  when declare? do
     `R-ty ← normalise =<< get-type `R
     con-ty ← normalise =<< get-type `R-con
     let con-ty = instantiate' `R-ty con-ty
@@ -210,8 +210,7 @@ make-record-path declare? nm `R = do
   let ps' = filter id ps
       n = length ps'
 
-  when declare? $ work-on-types do
-    declare (argN nm) ty
+  when declare? $ declare (argN nm) ty
 
   define-function nm
     [ clause

src/1Lab/Reflection/Regularity.agda

@@ -189,7 +189,7 @@ module Regularity where
 -- Test cases.
 module
   _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f g : A → B) (x : A)
-    (a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ ._ → A) ])
+    (a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ _ → A) ])
   where private
 
   p : (h : ∀ x → f x ≡ g x)

src/1Lab/Reflection/Signature.agda

@@ -22,12 +22,6 @@ get-record-type n = get-definition n >>= λ where
   (record-type conm fields) → pure (conm , fields)
   _ → typeError [ "get-record-type: definition " , nameErr n , " is not a record type." ]
 
--- Look up a constructor's quantity in the signature.
-get-con-quantity : Name → TC Quantity
-get-con-quantity n = get-definition n >>= λ where
-  (data-cons _ q) → pure q
-  _ → typeError [ "get-con-erasure: definition " , nameErr n , " is not a constructor." ]
-
 -- Representation of a data/record constructor.
 record Constructor : Type where
   constructor conhead
@@ -38,9 +32,6 @@ record Constructor : Type where
     -- Name of the data type:
     con-data      : Name
 
-    -- Quantity of the constructor.
-    con-quantity  : Quantity
-
     -- Argument telescope for the constructor, with the datatype's
     -- parameters removed.
     con-arguments : Telescope
@@ -64,23 +55,22 @@ get-type-constructors n = datatype <|> recordtype where
   datatype = do
     (npars , cons) ← get-data-type n
     for cons λ qn → do
-      q ← get-con-quantity qn
       (args , ty) ← pi-view <$> get-type qn
-      pure (conhead qn n q (drop npars args) ty)
+      pure (conhead qn n (drop npars args) ty)
 
   recordtype = do
     (c  , _)    ← get-record-type n
     (np , _)    ← pi-view <$> get-type n
     (args , ty) ← pi-view <$> get-type c
-    pure ((conhead c n quantity-ω (drop (length np) args) ty) ∷ [])
+    pure ((conhead c n (drop (length np) args) ty) ∷ [])
 
 -- Look up a constructor in the signature.
 get-constructor : Name → TC Constructor
 get-constructor n = get-definition n >>= λ where
-  (data-cons t q) → do
+  (data-cons t) → do
     (npars , cons) ← get-data-type t
     (args , ty)    ← pi-view <$> get-type n
-    pure (conhead n t q (drop npars args) ty)
+    pure (conhead n t (drop npars args) ty)
   _ → typeError [ "get-constructor: " , nameErr n , " is not a data constructor." ]
 
 -- If a term reduces to an application of a record type, return
@@ -121,7 +111,7 @@ instance
 private
   it-worker : Name → TC Term
   it-worker n = get-definition n <&> λ where
-    (data-cons _ _) →
+    (data-cons _) →
       def₀ (quote Has-constr.from-constr) ##ₙ def₀ (quote auto) ##ₙ lit (name n)
     _ →
       def₀ (quote Has-def.from-def) ##ₙ def₀ (quote auto) ##ₙ lit (name n)
@@ -161,7 +151,7 @@ macro
     tm   ← it-worker n
     args ← get-argument-tele n
     let
-      args = filter (λ { (_ , arg (arginfo visible _) _) → true ; _ → false }) args
+      args = filter (λ { (_ , arg (arginfo visible) _) → true ; _ → false }) args
 
       tm = def (quote applyⁿᵉ) (argN tm ∷ argN (list-term (reverse (map-up (λ i _ → it argN ##ₙ var₀ i) 0 args))) ∷ [])
       tm = foldr (λ _ y → lam visible (abs "_" y)) tm args
@@ -190,8 +180,8 @@ render-name def-nm = do
   d ← is-defined def-nm
   let
     fancy = get-definition def-nm >>= λ where
-      (data-cons _ _) → formatErrorParts [ termErr (con₀ def-nm) ]
-      _               → formatErrorParts [ termErr (def₀ def-nm) ]
+      (data-cons _ ) → formatErrorParts [ termErr (con₀ def-nm) ]
+      _              → formatErrorParts [ termErr (def₀ def-nm) ]
     plain = show def-nm
   if d then fancy else pure plain
 

src/1Lab/Reflection/Subst.agda

@@ -135,7 +135,7 @@ subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subs
 subst-tm ρ (lit l) = (lit l)
 subst-tm ρ unknown = unknown
 subst-tm ρ (agda-sort s) with s
-… | set t     = agda-sort (set (subst-tm ρ t))
+… | type t    = agda-sort (type (subst-tm ρ t))
 … | lit n     = agda-sort (lit n)
 … | prop t    = agda-sort (prop (subst-tm ρ t))
 … | propLit n = agda-sort (propLit n)