Many => Any

src/Quox/Ctx.idr

@@ -1,98 +0,0 @@
-module Quox.Ctx
-
-import Data.Nat
-import Data.Fin
-import Data.SnocList
-import Data.DPair
-
-
-%default total
-
-public export
-data Ctx : Nat -> (Nat -> Type) -> Type where
-  Lin  : Ctx 0 f
-  (:<) : Ctx n f -> f n -> Ctx (S n) f
-
-%name Ctx ctx
-
-
-public export
-0 Ctx' : Nat -> Type -> Type
-Ctx' n a = Ctx n (\_ => a)
-
-
-public export
-toSList : Ctx n f -> SnocList (Exists f)
-toSList [<]        = [<]
-toSList (ctx :< x) = toSList ctx :< Evidence _ x
-
-public export
-toSList' : Ctx' n a -> SnocList a
-toSList' ctx = map (.snd) $ toSList ctx
-
-public export
-fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
-fromSList' [<]       = [<]
-fromSList' (sx :< x) = fromSList' sx :< x
-
-
-public export
-0 Weaken : (Nat -> Type) -> Type
-Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)
-
-public export
-interface Weak f where weakN : Weaken f
-
-public export
-weak : Weak f => (1 x : f n) -> f (S n)
-weak = weakN 1
-
-
-public export
-lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
-lookBy w = go 0 where
-  go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
-  go by (ctx :< x) (FZ {k})   =
-    rewrite sym $ plusSuccRightSucc by k in w (S by) x
-  go by (ctx :< x) (FS {k} i) =
-    rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i
-
-public export
-look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
-look = lookBy weakN
-
-infixl 9 !!
-public export
-(!!) : Ctx' n a -> (1 _ : Fin n) -> a
-(!!) = lookBy (\_, x => x)
-
-
-public export
-map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
-map f [<]        = [<]
-map f (ctx :< x) = map f ctx :< f x
-
-
-public export
-(forall n. Eq (f n)) => Eq (Ctx n f) where
-  [<]         == [<]         = True
-  (ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y
-
-public export
-(forall n. Ord (f n)) => Ord (Ctx n f) where
-  compare [<]         [<]         = EQ
-  compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y
-
-
-||| like `Exists` but only shows the second part
-private
-data ShowWrapper : (Nat -> Type) -> Type where
-  SW : f n -> ShowWrapper f
-
-private
-(forall n. Show (f n)) => Show (ShowWrapper f) where
-  showPrec d (SW x) = showPrec d x
-
-export
-(forall n. Show (f n)) => Show (Ctx n f) where
-  show = show . map (\x => SW {f} x.snd) . toSList

src/Quox/Name.idr

@@ -9,7 +9,7 @@ public export
 data BaseName =
     UN String -- user-given name
 
-private 0 BRepr : Type
+private BRepr : Type
 BRepr = String
 
 private %inline brepr : BaseName -> BRepr
@@ -33,7 +33,7 @@ record Name where
   mods : SnocList String
   base : BaseName
 
-private 0 Repr : Type
+private Repr : Type
 Repr = (SnocList String, BRepr)
 
 private %inline repr : Name -> Repr

src/Quox/Pretty.idr

@@ -26,7 +26,7 @@ data HL
   | Free
   | Syntax
 
-private 0 HLRepr : Type
+private HLRepr : Type
 HLRepr = Nat
 
 private %inline hlRepr : HL -> Nat
@@ -54,7 +54,7 @@ data PPrec
   | SApp -- substitution application
   | Arg
 
-private 0 PrecRepr : Type
+private PrecRepr : Type
 PrecRepr = Nat
 
 private %inline precRepr : PPrec -> PrecRepr
@@ -109,16 +109,16 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export %inline 0 HasEnv : (Type -> Type) -> Type
+public export %inline HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
 export
 ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
-ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
+ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
 
 export
 parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
-parensIfM d doc = pure $ parensIf (prec !ask > d) doc
+parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
 
 export
 withPrec : HasEnv m => PPrec -> m a -> m a
@@ -137,11 +137,11 @@ public export
 interface PrettyHL a where
   prettyM : HasEnv m => a -> m (Doc HL)
 
-public export %inline
+export %inline
 pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
-public export %inline
+export %inline
 pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
 pretty0 x {unicode} =
   let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
@@ -164,9 +164,8 @@ export PrettyHL Name     where prettyM = pure . pretty . toDots
 export
 prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
 prettyStr {unicode} =
-  renderString .
+  let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
-  layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
+  renderString . layout . pretty0 {unicode}
-  pretty0 {unicode}
 
 
 export

src/Quox/Syntax/Dim.idr

@@ -30,14 +30,14 @@ PrettyHL (Dim n) where
 
 
 public export
-0 DSubst : Nat -> Nat -> Type
+DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
 export %inline
 prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
 prettyDSubst th =
-  prettySubstM prettyM (dnames !ask) DVar
+  prettySubstM prettyM (!ask).dnames DVar
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 

src/Quox/Syntax/Qty.idr

@@ -6,14 +6,14 @@ import Data.Fin
 
 
 public export
-data Qty = Zero | One | Many
+data Qty = Zero | One | Any
 %name Qty.Qty pi, rh
 
 private Repr : Type
 Repr = Fin 3
 
 private %inline repr : Qty -> Repr
-repr pi = case pi of Zero => 0; One => 1; Many => 2
+repr pi = case pi of Zero => 0; One => 1; Any => 2
 
 export Eq  Qty where (==) = (==) `on` repr
 export Ord Qty where compare = compare `on` repr
@@ -25,7 +25,7 @@ PrettyHL Qty where
     case pi of
       Zero => ifUnicode "𝟬" "0"
       One  => ifUnicode "𝟭" "1"
-      Many => ifUnicode "𝛚" "*"
+      Any  => ifUnicode "𝛚" "*"
 
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
@@ -38,7 +38,7 @@ public export
 (+) : Qty -> Qty -> Qty
 Zero + rh   = rh
 pi   + Zero = pi
-_    + _    = Many
+_    + _    = Any
 
 public export
 (*) : Qty -> Qty -> Qty
@@ -46,9 +46,9 @@ Zero * _    = Zero
 _    * Zero = Zero
 One  * rh   = rh
 pi   * One  = pi
-Many * Many = Many
+Any  * Any  = Any
 
 infix 6 <=.
 public export
 (<=.) : Qty -> Qty -> Bool
-pi <=. rh = rh == Many || pi == rh
+pi <=. rh = rh == Any || pi == rh

src/Quox/Syntax/Shift.idr

@@ -49,7 +49,7 @@ toEqv Refl {by = SZ}      = EqSZ
 toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
 
 
-public export
+export
 0 shiftDiff : (by : Shift from to) -> to = by.nat + from
 shiftDiff SZ      = Refl
 shiftDiff (SS by) = cong S $ shiftDiff by

src/Quox/Syntax/Subst.idr

@@ -38,7 +38,7 @@ interface FromVar env => CanSubst env term where
   (//) : term from -> Subst env from to -> term to
 
 public export
-0 CanSubst1 : (Nat -> Type) -> Type
+CanSubst1 : (Nat -> Type) -> Type
 CanSubst1 f = CanSubst f f
 
 
@@ -118,4 +118,4 @@ prettySubstM pr names bnd op cl th =
 ||| prints with [square brackets] and the `TVar` highlight for variables
 export
 PrettyHL (f to) => PrettyHL (Subst f from to) where
-  prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th
+  prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th

src/Quox/Syntax/Term.idr

@@ -1,6 +1,5 @@
 module Quox.Syntax.Term
 
-import public Quox.Ctx
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
@@ -25,8 +24,8 @@ infixl 8 :#
 infixl 9 :@
 mutual
   public export
-  0 TSubst : Nat -> Nat -> Nat -> Type
+  TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (Elim d)
+  TSubst d = Subst (\n => Elim d n)
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -36,17 +35,17 @@ mutual
 
     ||| function type
     Pi  : (qty, qtm : Qty) -> (x : Name) ->
-          (a : Term d n) -> (b : Term d (S n)) -> Term d n
+          (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
-    Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
+    Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
 
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
     ||| term closure/suspended substitution
-    CloT  : (s : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
     ||| dimension closure/suspended substitution
-    DCloT : (s : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
@@ -57,15 +56,15 @@ mutual
     B : (i : Var n) -> Elim d n
 
     ||| term application
-    (:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
+    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
 
     ||| type-annotated term
-    (:#) : (s, a : Term d n) -> Elim d n
+    (:#) : (tm, ty : Term d n) -> Elim d n
 
     ||| term closure/suspended substitution
-    CloE  : (e : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
     ||| dimension closure/suspended substitution
-    DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
 
 %name Term s, t, r
 %name Elim e, f
@@ -167,7 +166,7 @@ mutual
 
   export covering
   prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
-  prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
+  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
 
   export covering
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
@@ -269,19 +268,23 @@ isCloT (E e)       = isCloE e
 isCloT _           = False
 
 ||| an elimination which is not a top level closure
-public export 0 NotCloElim : Nat -> Nat -> Type
+public export NotCloElim : Nat -> Nat -> Type
 NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
 
 ||| a term which is not a top level closure
-public export 0 NotCloTerm : Nat -> Nat -> Type
+public export NotCloTerm : Nat -> Nat -> Type
 NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
 
 
 mutual
+  ||| if the input term has any top-level closures, push them under one layer of
+  ||| syntax
   export
   pushSubstsT : Term d n -> NotCloTerm d n
   pushSubstsT s = pushSubstsT' id id s
 
+  ||| if the input elimination has any top-level closures, push them under one
+  ||| layer of syntax
   export
   pushSubstsE : Elim d n -> NotCloElim d n
   pushSubstsE e = pushSubstsE' id id e
@@ -296,7 +299,7 @@ mutual
   pushSubstsT' th ph (Lam x t) =
     Element (Lam x $ subs t th $ push ph) Oh
   pushSubstsT' th ph (E e) =
-    case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
+    let Element e prf = pushSubstsE' th ph e in Element (E e) prf
   pushSubstsT' th ph (CloT  s ps) =
     pushSubstsT' th (comp' th ps ph) s
   pushSubstsT' th ph (DCloT s ps) =
@@ -320,11 +323,11 @@ mutual
 
 
 parameters {auto _ : Alternative f}
-  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
+  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)]`
   export
   betaLam1 : Elim d n -> f (Elim d n)
-  betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
+  betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
-    pure $ (t :# b) // (s :# a ::: id)
+    pure $ (body :# res) // (s :# arg ::: id)
   betaLam1 _ = empty
 
   ||| `(e ⦂ A) >>> e`    [if `e` is an elim]
@@ -333,10 +336,10 @@ parameters {auto _ : Alternative f}
   upsilon1 (E e :# _) = pure e
   upsilon1 _          = empty
 
-  public export
+  export
   step : Elim d n -> f (Elim d n)
   step e = betaLam1 e <|> upsilon1 e
 
-public export
+export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e

src/Quox/Syntax/Var.idr

@@ -68,7 +68,7 @@ public export %inline
 V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
 V i {p} = fromNatWith i p
 
-public export %inline
+export %inline
 tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
 tryFromNat n i =
   case i `isLT` n of
@@ -99,14 +99,6 @@ toFromNat 0     (LTESucc x) = Refl
 toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
-public export
-(.int) : Var n -> Integer
-i.int = natToInteger i.nat
-%builtin NaturalToInteger Var.(.int)
-
-public export Cast (Var n) Integer where cast i = i.int
-
-
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
 -- to be a bug?