From 4c008577b4c48f630a7f138455a9653b24b6d715 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 27 May 2024 21:28:22 +0200 Subject: [PATCH] wip make qtys into polynomials --- lib/Quox/Context.idr | 65 ++++ lib/Quox/Decidable.idr | 6 + lib/Quox/Definition.idr | 99 +++-- lib/Quox/Displace.idr | 16 +- lib/Quox/FreeVars.idr | 38 +- lib/Quox/Loc.idr | 7 + lib/Quox/Pretty.idr | 23 +- lib/Quox/Syntax/Builtin.idr | 4 +- lib/Quox/Syntax/Qty.idr | 214 +++++++---- lib/Quox/Syntax/Term/Base.idr | 269 +++++++------- lib/Quox/Syntax/Term/Pretty.idr | 593 ++++++++++++++++-------------- lib/Quox/Syntax/Term/Subst.idr | 338 +++++++++++------ lib/Quox/Syntax/Term/Tighten.idr | 118 +++--- lib/Quox/Typing.idr | 71 ++-- lib/Quox/Typing/Context.idr | 339 ++++++++++------- lib/Quox/Typing/Error.idr | 237 +++++------- lib/Quox/Whnf/Coercion.idr | 197 +++++----- lib/Quox/Whnf/ComputeElimType.idr | 64 ++-- lib/Quox/Whnf/Interface.idr | 36 +- lib/Quox/Whnf/Main.idr | 82 +++-- lib/Quox/Whnf/TypeCase.idr | 80 ++-- tests/Tests/Qty.idr | 8 + 22 files changed, 1650 insertions(+), 1254 deletions(-) create mode 100644 tests/Tests/Qty.idr diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index c93b20f..3ff37c6 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -13,7 +13,9 @@ import Data.SnocList import Data.SnocVect import Data.Vect import Control.Monad.Identity +import Derive.Prelude +%language ElabReflection %default total @@ -402,3 +404,66 @@ namespace BContext export toNames : BTelescope {} -> SnocList BaseName toNames = foldl (\xs, x => xs :< x.val) [<] + + +public export +record NameContexts q d n where + constructor MkNameContexts + {auto qtyLen : Singleton q} + {auto dimLen : Singleton d} + {auto termLen : Singleton n} + qnames : BContext q + dnames : BContext d + tnames : BContext n +%runElab deriveIndexed "NameContexts" [Show] + +namespace NameContexts + export + MkNameContexts' : (qnames : BContext q) -> (dnames : BContext d) -> + (tnames : BContext n) -> NameContexts q d n + MkNameContexts' {qnames, dnames, tnames} = + MkNameContexts { + qnames, dnames, tnames, + qtyLen = lengthPrf0 qnames, + dimLen = lengthPrf0 dnames, + termLen = lengthPrf0 tnames + } + + export + fromQNames : BContext q -> NameContexts q 0 0 + fromQNames qnames = + MkNameContexts qnames [<] [<] {qtyLen = lengthPrf0 qnames} + + export %inline + empty : NameContexts 0 0 0 + empty = fromQNames [<] + + export + extendQtyN' : BTelescope q q' -> NameContexts q d n -> NameContexts q' d n + extendQtyN' xs = {qnames $= (. xs), qtyLen $= lengthPrfSing xs} + + export + extendDimN' : BTelescope d d' -> NameContexts q d n -> NameContexts q d' n + extendDimN' xs = {dnames $= (. xs), dimLen $= lengthPrfSing xs} + + export + extendDimN : {s : Nat} -> BContext s -> + NameContexts q d n -> NameContexts q (s + d) n + extendDimN xs = {dnames $= (++ toSnocVect' xs), dimLen $= map (s +)} + + export + extendDim : BindName -> NameContexts q d n -> NameContexts q (S d) n + extendDim i = extendDimN [< i] + + export + extendTermN' : BTelescope n n' -> NameContexts q d n -> NameContexts q d n' + extendTermN' xs = {tnames $= (. xs), termLen $= lengthPrfSing xs} + + export + extendTermN : {s : Nat} -> BContext s -> + NameContexts q d n -> NameContexts q d (s + n) + extendTermN xs = {tnames $= (++ toSnocVect' xs), termLen $= map (s +)} + + export + extendTerm : BindName -> NameContexts q d n -> NameContexts q d (S n) + extendTerm x = extendTermN [< x] diff --git a/lib/Quox/Decidable.idr b/lib/Quox/Decidable.idr index 680b341..f809f9a 100644 --- a/lib/Quox/Decidable.idr +++ b/lib/Quox/Decidable.idr @@ -47,6 +47,12 @@ Yes _ && No n2 = No $ n2 . snd No n1 && _ = No $ n1 . fst +public export +map : p <=> q -> Dec p -> Dec q +map (MkEquivalence l r) (Yes y) = Yes $ l y +map (MkEquivalence l r) (No n) = No $ n . r + + public export reflectToDec : p `Reflects` b -> Dec p reflectToDec (RTrue y) = Yes y diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 900536d..b8fee86 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -12,74 +12,93 @@ import Decidable.Decidable public export -data DefBody = - Concrete (Term 0 0) - | Postulate +data DefBody : (q : Nat) -> Type where + MonoDef : Term 0 0 0 -> DefBody 0 + PolyDef : (0 nz : IsSucc q) => Term q 0 0 -> DefBody q + Postulate : DefBody q namespace DefBody public export - (.term0) : DefBody -> Maybe (Term 0 0) - (Concrete t).term0 = Just t - (Postulate).term0 = Nothing + (.term0) : DefBody q -> Maybe (Term q 0 0) + (MonoDef t).term0 = Just t + (PolyDef t).term0 = Just t + (Postulate).term0 = Nothing public export record Definition where constructor MkDef qty : GQty - type0 : Term 0 0 - body0 : DefBody + {qlen : Nat} + qargs : BContext qlen + type0 : Term qlen 0 0 + body0 : DefBody qlen scheme : Maybe String isMain : Bool loc_ : Loc public export %inline -mkPostulate : GQty -> (type0 : Term 0 0) -> Maybe String -> Bool -> Loc -> - Definition -mkPostulate qty type0 scheme isMain loc_ = - MkDef {qty, type0, body0 = Postulate, scheme, isMain, loc_} +mkPostulate : GQty -> BContext q -> Term q 0 0 -> + Maybe String -> Bool -> Loc -> Definition +mkPostulate qty qargs type0 scheme isMain loc_ = + let Val q = lengthPrf0 qargs in + MkDef {qty, qargs, type0, body0 = Postulate, scheme, isMain, loc_} public export %inline -mkDef : GQty -> (type0, term0 : Term 0 0) -> Maybe String -> Bool -> Loc -> - Definition -mkDef qty type0 term0 scheme isMain loc_ = - MkDef {qty, type0, body0 = Concrete term0, scheme, isMain, loc_} +mkDef : GQty -> BContext q -> (type0, term0 : Term q 0 0) -> Maybe String -> + Bool -> Loc -> Definition +mkDef qty qargs type0 term0 scheme isMain loc_ = + case (lengthPrf0 qargs) of + Val 0 => + MkDef {qty, qargs, type0, body0 = MonoDef term0, scheme, isMain, loc_} + Val (S _) => + MkDef {qty, qargs, type0, body0 = PolyDef term0, scheme, isMain, loc_} export Located Definition where def.loc = def.loc_ export Relocatable Definition where setLoc loc = {loc_ := loc} +public export +record Poly (0 tm : TermLike) d n where + constructor P + qlen : Nat + type : tm qlen d n + + parameters {d, n : Nat} public export %inline - (.type) : Definition -> Term d n - g.type = g.type0 // shift0 d // shift0 n + (.type) : Definition -> Poly Term d n + def.type = P def.qlen $ def.type0 // shift0 d // shift0 n public export %inline - (.typeAt) : Definition -> Universe -> Term d n - g.typeAt u = displace u g.type + (.typeAt) : Definition -> Universe -> Poly Term d n + def.typeAt u = {type $= displace u} def.type public export %inline - (.term) : Definition -> Maybe (Term d n) - g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n + (.term) : Definition -> Maybe (Poly Term d n) + def.term = def.body0.term0 <&> \t => P def.qlen $ t // shift0 d // shift0 n public export %inline - (.termAt) : Definition -> Universe -> Maybe (Term d n) - g.termAt u = displace u <$> g.term + (.termAt) : Definition -> Universe -> Maybe (Poly Term d n) + def.termAt u = {type $= displace u} <$> def.term public export %inline - toElim : Definition -> Universe -> Maybe $ Elim d n - toElim def u = pure $ Ann !(def.termAt u) (def.typeAt u) def.loc + toElim : Definition -> Universe -> Maybe (Poly Elim d n) + toElim def u = do + tm <- def.body0.term0; let ty = def.type0 + pure $ P def.qlen $ Ann tm ty def.loc // shift0 d // shift0 n public export -(.typeWith) : Definition -> Singleton d -> Singleton n -> Term d n -g.typeWith (Val d) (Val n) = g.type +(.typeWith) : Definition -> Singleton d -> Singleton n -> Poly Term d n +def.typeWith (Val d) (Val n) = def.type public export -(.typeWithAt) : Definition -> Singleton d -> Singleton n -> Universe -> Term d n -g.typeWithAt d n u = displace u $ g.typeWith d n +(.typeWithAt) : Definition -> Singleton d -> Singleton n -> + Universe -> Poly Term d n +def.typeWithAt (Val d) (Val n) u = def.typeAt u public export -(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Term d n) +(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Poly Term d n) g.termWith (Val d) (Val n) = g.term @@ -108,20 +127,28 @@ DefsState : Type -> Type DefsState = StateL DEFS Definitions public export %inline -lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n) +lookupElim : {d, n : Nat} -> + Name -> Universe -> Definitions -> Maybe (Poly Elim d n) lookupElim x u defs = toElim !(lookup x defs) u public export %inline -lookupElim0 : Name -> Universe -> Definitions -> Maybe (Elim 0 0) +lookupElim0 : Name -> Universe -> Definitions -> Maybe (Poly Elim 0 0) lookupElim0 = lookupElim +export +prettyQBinders : {opts : LayoutOpts} -> BContext q -> Eff Pretty (Doc opts) +prettyQBinders [<] = pure empty +prettyQBinders qnames = + qbrackets . separateTight !commaD =<< traverse prettyQBind (toList' qnames) + export prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts) prettyDef name def = withPrec Outer $ do - qty <- prettyQty def.qty.qty + qty <- prettyQConst def.qty.qconst dot <- dotD name <- prettyFree name + qargs <- prettyQBinders def.qargs colon <- colonD - type <- prettyTerm [<] [<] def.type - hangDSingle (hsep [hcat [qty, dot, name], colon]) type + type <- prettyTerm (fromQNames def.qargs) def.type0 + hangDSingle (hsep [hcat [qty, dot, name, qargs], colon]) type diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr index 6f8e1ed..c48409f 100644 --- a/lib/Quox/Displace.idr +++ b/lib/Quox/Displace.idr @@ -7,12 +7,12 @@ import Quox.Syntax parameters (k : Universe) namespace Term - export doDisplace : Term d n -> Term d n - export doDisplaceS : ScopeTermN s d n -> ScopeTermN s d n - export doDisplaceDS : DScopeTermN s d n -> DScopeTermN s d n + export doDisplace : Term q d n -> Term q d n + export doDisplaceS : ScopeTermN s q d n -> ScopeTermN s q d n + export doDisplaceDS : DScopeTermN s q d n -> DScopeTermN s q d n namespace Elim - export doDisplace : Elim d n -> Elim d n + export doDisplace : Elim q d n -> Elim q d n namespace Term doDisplace (TYPE l loc) = TYPE (k + l) loc @@ -41,6 +41,8 @@ parameters (k : Universe) CloT (Sub (doDisplace t) (assert_total $ map doDisplace th)) doDisplace (DCloT (Sub t th)) = DCloT (Sub (doDisplace t) th) + doDisplace (QCloT (SubR t th)) = + QCloT (SubR (doDisplace t) th) doDisplaceS (S names (Y body)) = S names $ Y $ doDisplace body doDisplaceS (S names (N body)) = S names $ N $ doDisplace body @@ -80,16 +82,18 @@ parameters (k : Universe) CloE (Sub (doDisplace e) (assert_total $ map doDisplace th)) doDisplace (DCloE (Sub e th)) = DCloE (Sub (doDisplace e) th) + doDisplace (QCloE (SubR e th)) = + QCloE (SubR (doDisplace e) th) namespace Term export - displace : Universe -> Term d n -> Term d n + displace : Universe -> Term q d n -> Term q d n displace 0 t = t displace u t = doDisplace u t namespace Elim export - displace : Universe -> Elim d n -> Elim d n + displace : Universe -> Elim q d n -> Elim q d n displace 0 t = t displace u t = doDisplace u t diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr index 13b711f..8b9f59e 100644 --- a/lib/Quox/FreeVars.idr +++ b/lib/Quox/FreeVars.idr @@ -88,7 +88,7 @@ interface HasFreeVars (0 tm : Nat -> Type) where fv : {n : Nat} -> tm n -> FreeVars n public export -interface HasFreeDVars (0 tm : TermLike) where +interface HasFreeDVars (0 tm : Nat -> Nat -> Type) where constructor HFDV fdv : {d, n : Nat} -> tm d n -> FreeVars d @@ -101,7 +101,7 @@ fdvWith : HasFreeDVars tm => Singleton d -> Singleton n -> tm d n -> FreeVars d fdvWith (Val d) (Val n) = fdv export -Fdv : (0 tm : TermLike) -> {n : Nat} -> +Fdv : (0 tm : _) -> {n : Nat} -> HasFreeDVars tm => HasFreeVars (\d => tm d n) Fdv tm @{HFDV fdv} = HFV fdv @@ -139,7 +139,7 @@ where fdv (S _ (N body)) = fdv body export -fvD : {0 tm : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) => +fvD : {0 tm : _} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) => Scoped s (\d => tm d n) d -> FreeVars n fvD (S _ (Y body)) = fv body fvD (S _ (N body)) = fv body @@ -174,11 +174,10 @@ where foldMap (uncurry guardM) (zipWith (,) (fv term).vars (fdvEach subst)) -export HasFreeVars (Term d) -export HasFreeVars (Elim d) +export HasFreeVars (Term q d) +export HasFreeVars (Elim q d) -export -HasFreeVars (Term d) where +HasFreeVars (Term q d) where fv (TYPE {}) = none fv (IOState {}) = none fv (Pi {arg, res, _}) = fv arg <+> fv res @@ -200,9 +199,9 @@ HasFreeVars (Term d) where fv (E e) = fv e fv (CloT s) = fv s fv (DCloT s) = fv s.term + fv (QCloT s) = fv s.term -export -HasFreeVars (Elim d) where +HasFreeVars (Elim q d) where fv (F {}) = none fv (B i _) = only i fv (App {fun, arg, _}) = fv fun <+> fv arg @@ -224,6 +223,7 @@ HasFreeVars (Elim d) where fv ty <+> fv ret <+> fv def <+> foldMap (\x => fv x.snd) (toList arms) fv (CloE s) = fv s fv (DCloE s) = fv s.term + fv (QCloE s) = fv s.term @@ -253,11 +253,10 @@ fdvSubst : {d, n : Nat} -> (Located2 tm, HasFreeDVars tm) => fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th -export HasFreeDVars Term -export HasFreeDVars Elim +export HasFreeDVars (Term q) +export HasFreeDVars (Elim q) -export -HasFreeDVars Term where +HasFreeDVars (Term q) where fdv (TYPE {}) = none fdv (IOState {}) = none fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res @@ -279,9 +278,9 @@ HasFreeDVars Term where fdv (E e) = fdv e fdv (CloT s) = fdv s @{WithSubst} fdv (DCloT s) = fdvSubst s + fdv (QCloT s) = fdv s.term -export -HasFreeDVars Elim where +HasFreeDVars (Elim q) where fdv (F {}) = none fdv (B {}) = none fdv (App {fun, arg, _}) = fdv fun <+> fdv arg @@ -298,12 +297,13 @@ HasFreeDVars Elim where fdv fun <+> fv arg fdv (Ann {tm, ty, _}) = fdv tm <+> fdv ty - fdv (Coe {ty, p, q, val, _}) = - fdv @{DScope} ty <+> fv p <+> fv q <+> fdv val - fdv (Comp {ty, p, q, val, r, zero, one, _}) = - fdv ty <+> fv p <+> fv q <+> fdv val <+> + fdv (Coe {ty, p, p', val, _}) = + fdv @{DScope} ty <+> fv p <+> fv p' <+> fdv val + fdv (Comp {ty, p, p', val, r, zero, one, _}) = + fdv ty <+> fv p <+> fv p' <+> fdv val <+> fv r <+> fdv @{DScope} zero <+> fdv @{DScope} one fdv (TypeCase {ty, ret, arms, def, _}) = fdv ty <+> fdv ret <+> fdv def <+> foldMap (\x => fdvT x.snd) (toList arms) fdv (CloE s) = fdv s @{WithSubst} fdv (DCloE s) = fdvSubst s + fdv (QCloE s) = fdv s.term diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr index 5e25d13..196bb6f 100644 --- a/lib/Quox/Loc.idr +++ b/lib/Quox/Loc.idr @@ -138,6 +138,9 @@ public export Located2 f = forall x, y. Located (f x y) public export +0 Located3 : (a -> b -> c -> Type) -> Type +Located3 f = forall x, y, z. Located (f x y z) + public export interface Located a => Relocatable a where constructor MkRelocatable @@ -151,6 +154,10 @@ public export 0 Relocatable2 : (a -> b -> Type) -> Type Relocatable2 f = forall x, y. Relocatable (f x y) +public export +0 Relocatable3 : (a -> b -> c -> Type) -> Type +Relocatable3 f = forall x, y, z. Relocatable (f x y z) + export locs : Located a => Foldable t => t a -> Loc diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index 1083951..0e20161 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -39,7 +39,8 @@ data HL = Delim | Free | TVar | Dim | DVar -| Qty | Universe +| Qty | QVar +| Universe | Syntax | Constant %runElab derive "HL" [Eq, Ord, Show] @@ -82,6 +83,7 @@ toSGR TVar = [SetForeground BrightYellow] toSGR Dim = [SetForeground BrightGreen] toSGR DVar = [SetForeground BrightGreen] toSGR Qty = [SetForeground BrightMagenta] +toSGR QVar = [SetForeground BrightMagenta] toSGR Universe = [SetForeground BrightRed] toSGR Syntax = [SetForeground BrightCyan] toSGR Constant = [SetForeground BrightRed] @@ -98,6 +100,7 @@ toClass TVar = "tv" toClass Dim = "dc" toClass DVar = "dv" toClass Qty = "qt" +toClass QVar = "qv" toClass Universe = "un" toClass Syntax = "sy" toClass Constant = "co" @@ -205,6 +208,10 @@ parameters {opts : LayoutOpts} {auto _ : Foldable t} separateTight : Doc opts -> t (Doc opts) -> Doc opts separateTight d = sep . exceptLast (<+> d) . toList + export + sepSingleTight : Doc opts -> t (Doc opts) -> Doc opts + sepSingleTight d = sepSingle . exceptLast (<+> d) . toList + export hseparateTight : Doc opts -> t (Doc opts) -> Doc opts hseparateTight d = hsep . exceptLast (<+> d) . toList @@ -238,6 +245,10 @@ export %inline withPrec : PPrec -> Eff Pretty a -> Eff Pretty a withPrec = localAt_ PREC +export %inline +qbrackets : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts) +qbrackets doc = tightDelims !(ifUnicode "โ€น" ".{") !(ifUnicode "โ€บ" "}") doc + export prettyName : Name -> Doc opts @@ -259,12 +270,16 @@ export prettyDBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts) prettyDBind = hl DVar . prettyBind' +export +prettyQBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts) +prettyQBind = hl QVar . prettyBind' export %inline typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD, ofD, dotD, -zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD : +zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD, +qplusD, qtimesD : {opts : LayoutOpts} -> Eff Pretty (Doc opts) typeD = hl Syntax . text =<< ifUnicode "โ˜…" "Type" ioStateD = hl Syntax $ text "IOState" @@ -298,6 +313,8 @@ fstD = hl Syntax $ text "fst" sndD = hl Syntax $ text "snd" letD = hl Syntax $ text "let" inD = hl Syntax $ text "in" +qplusD = hl Syntax $ text "+" +qtimesD = hl Syntax . text =<< ifUnicode "ยท" "*" export @@ -311,7 +328,7 @@ prettyApp ind f args = export prettyAppD : {opts : LayoutOpts} -> Doc opts -> List (Doc opts) -> Eff Pretty (Doc opts) -prettyAppD f args = pure $ prettyApp !(askAt INDENT) f args +prettyAppD f args = parensIfM App $ prettyApp !(askAt INDENT) f args export diff --git a/lib/Quox/Syntax/Builtin.idr b/lib/Quox/Syntax/Builtin.idr index 09ac392..15ea3d9 100644 --- a/lib/Quox/Syntax/Builtin.idr +++ b/lib/Quox/Syntax/Builtin.idr @@ -21,7 +21,7 @@ builtinDesc Main = "a function declared as #[main]" public export builtinTypeDoc : {opts : LayoutOpts} -> Builtin -> Eff Pretty (Doc opts) builtinTypeDoc Main = - prettyTerm [<] [<] $ - Pi One (IOState noLoc) + prettyTerm empty $ + Pi {q = 0} (one noLoc) (IOState noLoc) (SN $ Sig (Enum (fromList [!(ifUnicode "๐‘Ž" "a")]) noLoc) (SN (IOState noLoc)) noLoc) noLoc diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr index d0d3d79..50cd519 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -4,10 +4,14 @@ ||| it's worth in a language that has other stuff going on too module Quox.Syntax.Qty +import public Quox.Polynomial +import Quox.Name +import Quox.Syntax.Subst import Quox.Pretty import Quox.Decidable import Quox.PrettyValExtra import Data.DPair +import Data.Singleton import Derive.Prelude %default total @@ -20,61 +24,124 @@ import Derive.Prelude ||| - 1: a variable is used exactly once at run time ||| - ฯ‰ (or #): don't care. an ฯ‰ variable *can* also be used 0/1 time public export -data Qty = Zero | One | Any -%runElab derive "Qty" [Eq, Ord, Show, PrettyVal] -%name Qty.Qty pi, rh +data QConst = Zero | One | Any +%runElab derive "QConst" [Eq, Ord, Show, PrettyVal] +%name QConst q, r export -prettyQty : {opts : _} -> Qty -> Eff Pretty (Doc opts) -prettyQty Zero = hl Qty $ text "0" -prettyQty One = hl Qty $ text "1" -prettyQty Any = hl Qty =<< ifUnicode (text "ฯ‰") (text "#") +prettyQConst : {opts : _} -> QConst -> Eff Pretty (Doc opts) +prettyQConst Zero = hl Qty $ text "0" +prettyQConst One = hl Qty $ text "1" +prettyQConst Any = hl Qty =<< ifUnicode (text "ฯ‰") (text "#") + +-- ||| prints in a form that can be a suffix of "case" +-- public export +-- prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts) +-- prettySuffix = prettyQty + + +namespace QConst + ||| e.g. if in the expression `(s, t)`, the variable `x` is + ||| used ฯ€ times in `s` and ฯ times in `t`, then it's used + ||| (ฯ€ + ฯ) times in the whole expression + public export + plus : QConst -> QConst -> QConst + plus Zero rh = rh + plus pi Zero = pi + plus _ _ = Any + + ||| e.g. if a function `f` uses its argument ฯ€ times, + ||| and `f x` occurs in a ฯƒ context, then `x` is used `ฯ€ฯƒ` times overall + public export + times : QConst -> QConst -> QConst + times Zero _ = Zero + times _ Zero = Zero + times One rh = rh + times pi One = pi + times Any Any = Any + + -- ||| "ฯ€ โˆจ ฯ" + -- ||| + -- ||| returns a quantity ฯ„ with ฯ€ โ‰ค ฯ„ and ฯ โ‰ค ฯ„. + -- ||| if ฯ€ = ฯ, then it's that, otherwise it's ฯ‰. + -- public export + -- lub : QConst -> QConst -> QConst + -- lub p q = if p == q then p else Any + +export %inline +AddMonoid QConst where zero = Zero; (+.) = plus; isZero = (== Zero) + +export %inline +TimesMonoid QConst where one = One; (*.) = times + -||| prints in a form that can be a suffix of "case" public export -prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts) -prettySuffix = prettyQty +record Qty n where + constructor Q + value : Polynomial QConst n + loc : Loc +%runElab deriveIndexed "Qty" [Eq, Ord] + +export %hint +ShowQty : {n : Nat} -> Show (Qty n) +ShowQty = deriveShow + +export %hint +PrettyValQty : {n : Nat} -> PrettyVal (Qty n) +PrettyValQty = derivePrettyVal -||| e.g. if in the expression `(s, t)`, the variable `x` is -||| used ฯ€ times in `s` and ฯ times in `t`, then it's used -||| (ฯ€ + ฯ) times in the whole expression -public export -(+) : Qty -> Qty -> Qty -Zero + rh = rh -pi + Zero = pi -_ + _ = Any +export +zero, one, any : {n : Nat} -> Loc -> Qty n +zero = Q zero +one = Q one +any = Q $ pconst Any -||| e.g. if a function `f` uses its argument ฯ€ times, -||| and `f x` occurs in a ฯƒ context, then `x` is used `ฯ€ฯƒ` times overall -public export -(*) : Qty -> Qty -> Qty -Zero * _ = Zero -_ * Zero = Zero -One * rh = rh -pi * One = pi -Any * Any = Any +export +(+) : Qty n -> Qty n -> Qty n +Q xs l1 + Q ys l2 = Q (xs +. ys) (l1 `or` l2) + +export +(*) : Qty n -> Qty n -> Qty n +Q xs l1 * Q ys l2 = Q (xs *. ys) (l1 `or` l2) + +export +isAny : Qty n -> Bool +isAny (Q pi _) = pi.at0 == Any + +export +lub : {n : Nat} -> Qty n -> Qty n -> Qty n +lub pi rh = if pi == rh then pi else any pi.loc ||| "ฯ€ โ‰ค ฯ" ||| -||| if a variable is bound with quantity ฯ, then it can be used with a total +||| if a variable is bound with quantity ฯ, then it can be used with an actual ||| quantity ฯ€ as long as ฯ€ โ‰ค ฯ. for example, an ฯ‰ variable can be used any ||| number of times, so ฯ€ โ‰ค ฯ‰ for any ฯ€. public export -compat : Qty -> Qty -> Bool -compat pi Any = True -compat pi rh = pi == rh +compat : Qty n -> Qty n -> Bool +compat pi rh = isAny rh || pi == rh -||| "ฯ€ โˆจ ฯ" -||| -||| returns a quantity ฯ„ with ฯ€ โ‰ค ฯ„ and ฯ โ‰ค ฯ„. -||| if ฯ€ = ฯ, then it's that, otherwise it's ฯ‰. -public export -lub : Qty -> Qty -> Qty -lub p q = if p == q then p else Any +private +toVarString : BContext n -> Monom n -> List BindName +toVarString ns ds = fold $ zipWith replicate ds ns +private +prettyTerm : {opts : LayoutOpts} -> + BContext n -> Monom n -> QConst -> Eff Pretty (Doc opts) +prettyTerm ns ds pi = do + pi <- prettyQConst pi + xs <- traverse prettyQBind (toVarString ns ds) + pure $ separateTight !qtimesD $ pi :: xs + +export +prettyQty : {opts : LayoutOpts} -> BContext n -> Qty n -> Eff Pretty (Doc opts) +prettyQty ns (Q q _) = + let Val _ = lengthPrf0 ns in + separateLoose !qplusD <$> + traverse (uncurry $ prettyTerm ns) (toList q) ||| to maintain subject reduction, only 0 or 1 can occur ||| for the subject of a typing judgment. see @qtt, ยง2.3 for more detail @@ -87,9 +154,8 @@ data SQty = SZero | SOne ||| ||| ฯƒ โจด ฯ€ is 0 if either of ฯƒ or ฯ€ are, otherwise it is ฯƒ. public export -subjMult : SQty -> Qty -> SQty -subjMult _ Zero = SZero -subjMult sg _ = sg +subjMult : SQty -> Qty n -> SQty +subjMult sg pi = if isZero pi.value then SZero else sg ||| it doesn't make much sense for a top level declaration to have a @@ -100,12 +166,6 @@ data GQty = GZero | GAny %runElab derive "GQty" [Eq, Ord, Show, PrettyVal] %name GQty rh -public export -toGlobal : Qty -> Maybe GQty -toGlobal Zero = Just GZero -toGlobal Any = Just GAny -toGlobal One = Nothing - ||| when checking a definition, a 0 definition is checked at 0, ||| but an ฯ‰ definition is checked at 1 since ฯ‰ isn't a subject quantity public export %inline @@ -114,18 +174,6 @@ globalToSubj GZero = SZero globalToSubj GAny = SOne -public export -DecEq Qty where - decEq Zero Zero = Yes Refl - decEq Zero One = No $ \case _ impossible - decEq Zero Any = No $ \case _ impossible - decEq One Zero = No $ \case _ impossible - decEq One One = Yes Refl - decEq One Any = No $ \case _ impossible - decEq Any Zero = No $ \case _ impossible - decEq Any One = No $ \case _ impossible - decEq Any Any = Yes Refl - public export DecEq SQty where decEq SZero SZero = Yes Refl @@ -143,12 +191,48 @@ DecEq GQty where namespace SQty public export %inline - (.qty) : SQty -> Qty - (SZero).qty = Zero - (SOne).qty = One + toQty : {n : Nat} -> Loc -> SQty -> Qty n + toQty loc SZero = zero loc + toQty loc SOne = one loc + + public export %inline + (.qconst) : SQty -> QConst + (SZero).qconst = Zero + (SOne).qconst = One namespace GQty public export %inline - (.qty) : GQty -> Qty - (GZero).qty = Zero - (GAny).qty = Any + toQty : {n : Nat} -> Loc -> GQty -> Qty n + toQty loc GZero = zero loc + toQty loc GAny = any loc + + public export %inline + (.qconst) : GQty -> QConst + (GZero).qconst = Zero + (GAny).qconst = Any + + +export +prettySQty : {opts : _} -> SQty -> Eff Pretty (Doc opts) +prettySQty sg = prettyQConst sg.qconst + +export +prettyGQty : {opts : _} -> GQty -> Eff Pretty (Doc opts) +prettyGQty pi = prettyQConst pi.qconst + + +public export +QSubst : Nat -> Nat -> Type +QSubst = Subst Qty + +export +FromVarR Qty where + fromVarR i loc = Q (fromVarR i loc) loc + +export +CanShift Qty where + Q p loc // by = Q (p // by) loc + +export +CanSubstSelfR Qty where + Q q loc //? th = Q (q //? map (.value) th) loc diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 75bae76..029f80c 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -32,11 +32,11 @@ import Derive.Prelude public export TermLike : Type -TermLike = Nat -> Nat -> Type +TermLike = (q, d, n : Nat) -> Type public export TSubstLike : Type -TSubstLike = Nat -> Nat -> Nat -> Type +TSubstLike = (q, d, n1, n2 : Nat) -> Type public export Universe : Type @@ -50,156 +50,162 @@ TagVal = String mutual public export TSubst : TSubstLike - TSubst d = Subst $ \n => Elim d n + TSubst q d = Subst $ \n => Elim q d n ||| first argument `d` is dimension scope size; ||| second `n` is term scope size public export - data Term : (d, n : Nat) -> Type where + data Term : (q, d, n : Nat) -> Type where ||| type of types - TYPE : (l : Universe) -> (loc : Loc) -> Term d n + TYPE : (l : Universe) -> (loc : Loc) -> Term q d n ||| IO state token. this is a builtin because otherwise #[main] being a ||| builtin makes no sense - IOState : (loc : Loc) -> Term d n + IOState : (loc : Loc) -> Term q d n ||| function type - Pi : (qty : Qty) -> (arg : Term d n) -> - (res : ScopeTerm d n) -> (loc : Loc) -> Term d n + Pi : (qty : Qty q) -> (arg : Term q d n) -> + (res : ScopeTerm q d n) -> (loc : Loc) -> Term q d n ||| function term - Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n + Lam : (body : ScopeTerm q d n) -> (loc : Loc) -> Term q d n ||| pair type - Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n + Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> (loc : Loc) -> + Term q d n ||| pair value - Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n + Pair : (fst, snd : Term q d n) -> (loc : Loc) -> Term q d n ||| enumeration type - Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n + Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term q d n ||| enumeration value - Tag : (tag : TagVal) -> (loc : Loc) -> Term d n + Tag : (tag : TagVal) -> (loc : Loc) -> Term q d n ||| equality type - Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n + Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> (loc : Loc) -> + Term q d n ||| equality term - DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n + DLam : (body : DScopeTerm q d n) -> (loc : Loc) -> Term q d n ||| natural numbers (temporary until ๐– gets added) - NAT : (loc : Loc) -> Term d n - Nat : (val : Nat) -> (loc : Loc) -> Term d n - Succ : (p : Term d n) -> (loc : Loc) -> Term d n + NAT : (loc : Loc) -> Term q d n + Nat : (val : Nat) -> (loc : Loc) -> Term q d n + Succ : (p : Term q d n) -> (loc : Loc) -> Term q d n ||| strings - STRING : (loc : Loc) -> Term d n - Str : (str : String) -> (loc : Loc) -> Term d n + STRING : (loc : Loc) -> Term q d n + Str : (str : String) -> (loc : Loc) -> Term q d n ||| "box" (package a value up with a certain quantity) - BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n - Box : (val : Term d n) -> (loc : Loc) -> Term d n + BOX : (qty : Qty q) -> (ty : Term q d n) -> (loc : Loc) -> Term q d n + Box : (val : Term q d n) -> (loc : Loc) -> Term q d n - Let : (qty : Qty) -> (rhs : Elim d n) -> - (body : ScopeTerm d n) -> (loc : Loc) -> Term d n + Let : (qty : Qty q) -> (rhs : Elim q d n) -> + (body : ScopeTerm q d n) -> (loc : Loc) -> Term q d n ||| elimination - E : (e : Elim d n) -> Term d n + E : (e : Elim q d n) -> Term q d n ||| term closure/suspended substitution - CloT : WithSubst (Term d) (Elim d) n -> Term d n + CloT : WithSubst (Term q d) (Elim q d) n -> Term q d n ||| dimension closure/suspended substitution - DCloT : WithSubst (\d => Term d n) Dim d -> Term d n + DCloT : WithSubst (\d => Term q d n) Dim d -> Term q d n + ||| quantity closure/suspended substitution + QCloT : WithSubstR (\q => Term q d n) Qty q -> Term q d n %name Term s, t, r ||| first argument `d` is dimension scope size, second `n` is term scope size public export - data Elim : (d, n : Nat) -> Type where + data Elim : (q, d, n : Nat) -> Type where ||| free variable, possibly with a displacement (see @crude, or @mugen for a ||| more abstract and formalised take) ||| ||| e.g. if f : โ˜…โ‚€ โ†’ โ˜…โ‚, then fยน : โ˜…โ‚ โ†’ โ˜…โ‚‚ - F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n + F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim q d n ||| bound variable - B : (i : Var n) -> (loc : Loc) -> Elim d n + B : (i : Var n) -> (loc : Loc) -> Elim q d n ||| term application - App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n + App : (fun : Elim q d n) -> (arg : Term q d n) -> (loc : Loc) -> Elim q d n ||| pair destruction ||| ||| `CasePair ๐œ‹ ๐‘’ ([๐‘Ÿ], ๐ด) ([๐‘ฅ, ๐‘ฆ], ๐‘ก)` is ||| `๐œ๐š๐ฌ๐ž ๐œ‹ ยท ๐‘’ ๐ซ๐ž๐ญ๐ฎ๐ซ๐ง ๐‘Ÿ โ‡’ ๐ด ๐จ๐Ÿ { (๐‘ฅ, ๐‘ฆ) โ‡’ ๐‘ก }` - CasePair : (qty : Qty) -> (pair : Elim d n) -> - (ret : ScopeTerm d n) -> - (body : ScopeTermN 2 d n) -> + CasePair : (qty : Qty q) -> (pair : Elim q d n) -> + (ret : ScopeTerm q d n) -> + (body : ScopeTermN 2 q d n) -> (loc : Loc) -> - Elim d n + Elim q d n ||| first element of a pair. only works in non-linear contexts. - Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n + Fst : (pair : Elim q d n) -> (loc : Loc) -> Elim q d n ||| second element of a pair. only works in non-linear contexts. - Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n + Snd : (pair : Elim q d n) -> (loc : Loc) -> Elim q d n ||| enum matching - CaseEnum : (qty : Qty) -> (tag : Elim d n) -> - (ret : ScopeTerm d n) -> - (arms : CaseEnumArms d n) -> + CaseEnum : (qty : Qty q) -> (tag : Elim q d n) -> + (ret : ScopeTerm q d n) -> + (arms : CaseEnumArms q d n) -> (loc : Loc) -> - Elim d n + Elim q d n ||| nat matching - CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) -> - (ret : ScopeTerm d n) -> - (zero : Term d n) -> - (succ : ScopeTermN 2 d n) -> + CaseNat : (qty, qtyIH : Qty q) -> (nat : Elim q d n) -> + (ret : ScopeTerm q d n) -> + (zero : Term q d n) -> + (succ : ScopeTermN 2 q d n) -> (loc : Loc) -> - Elim d n + Elim q d n ||| unboxing - CaseBox : (qty : Qty) -> (box : Elim d n) -> - (ret : ScopeTerm d n) -> - (body : ScopeTerm d n) -> + CaseBox : (qty : Qty q) -> (box : Elim q d n) -> + (ret : ScopeTerm q d n) -> + (body : ScopeTerm q d n) -> (loc : Loc) -> - Elim d n + Elim q d n ||| dim application - DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n + DApp : (fun : Elim q d n) -> (arg : Dim d) -> (loc : Loc) -> Elim q d n ||| type-annotated term - Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim d n + Ann : (tm, ty : Term q d n) -> (loc : Loc) -> Elim q d n ||| coerce a value along a type equality, or show its coherence ||| [@xtt; ยง2.1.1] - Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> - (val : Term d n) -> (loc : Loc) -> Elim d n + Coe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> + (val : Term q d n) -> (loc : Loc) -> Elim q d n ||| "generalised composition" [@xtt; ยง2.1.2] - Comp : (ty : Term d n) -> (p, q : Dim d) -> - (val : Term d n) -> (r : Dim d) -> - (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n + Comp : (ty : Term q d n) -> (p, p' : Dim d) -> + (val : Term q d n) -> (r : Dim d) -> + (zero, one : DScopeTerm q d n) -> (loc : Loc) -> Elim q d n ||| match on types. needed for b.s. of coercions [@xtt; ยง2.2] - TypeCase : (ty : Elim d n) -> (ret : Term d n) -> - (arms : TypeCaseArms d n) -> (def : Term d n) -> + TypeCase : (ty : Elim q d n) -> (ret : Term q d n) -> + (arms : TypeCaseArms q d n) -> (def : Term q d n) -> (loc : Loc) -> - Elim d n + Elim q d n ||| term closure/suspended substitution - CloE : WithSubst (Elim d) (Elim d) n -> Elim d n + CloE : WithSubst (Elim q d) (Elim q d) n -> Elim q d n ||| dimension closure/suspended substitution - DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n + DCloE : WithSubst (\d => Elim q d n) Dim d -> Elim q d n + ||| quantity closure/suspended substitution + QCloE : WithSubstR (\q => Elim q d n) Qty q -> Elim q d n %name Elim e, f public export CaseEnumArms : TermLike - CaseEnumArms d n = SortedMap TagVal (Term d n) + CaseEnumArms q d n = SortedMap TagVal (Term q d n) public export TypeCaseArms : TermLike - TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n) + TypeCaseArms q d n = SortedDMap TyConKind (\k => TypeCaseArmBody k q d n) public export TypeCaseArm : TermLike - TypeCaseArm d n = (k ** TypeCaseArmBody k d n) + TypeCaseArm q d n = (k ** TypeCaseArmBody k q d n) public export TypeCaseArmBody : TyConKind -> TermLike @@ -208,35 +214,27 @@ mutual public export ScopeTermN, DScopeTermN : Nat -> TermLike - ScopeTermN s d n = Scoped s (Term d) n - DScopeTermN s d n = Scoped s (\d => Term d n) d + ScopeTermN s q d n = Scoped s (Term q d) n + DScopeTermN s q d n = Scoped s (\d => Term q d n) d public export ScopeTerm, DScopeTerm : TermLike ScopeTerm = ScopeTermN 1 DScopeTerm = DScopeTermN 1 -mutual - export %hint - EqTerm : Eq (Term d n) - EqTerm = assert_total {a = Eq (Term d n)} deriveEq +export %hint EqTerm : Eq (Term q d n) +export %hint EqElim : Eq (Elim q d n) +EqTerm = assert_total {a = Eq (Term q d n)} deriveEq +EqElim = assert_total {a = Eq (Elim q d n)} deriveEq - export %hint - EqElim : Eq (Elim d n) - EqElim = assert_total {a = Eq (Elim d n)} deriveEq - -mutual - export %hint - ShowTerm : Show (Term d n) - ShowTerm = assert_total {a = Show (Term d n)} deriveShow - - export %hint - ShowElim : Show (Elim d n) - ShowElim = assert_total {a = Show (Elim d n)} deriveShow +-- export %hint ShowTerm : {q, d, n : Nat} -> Show (Term q d n) +-- export %hint ShowElim : {q, d, n : Nat} -> Show (Elim q d n) +-- ShowTerm = assert_total {a = Show (Term q d n)} deriveShow +-- ShowElim = assert_total {a = Show (Elim q d n)} deriveShow export -Located (Elim d n) where +Located (Elim q d n) where (F _ _ loc).loc = loc (B _ loc).loc = loc (App _ _ loc).loc = loc @@ -253,30 +251,32 @@ Located (Elim d n) where (TypeCase _ _ _ _ loc).loc = loc (CloE (Sub e _)).loc = e.loc (DCloE (Sub e _)).loc = e.loc + (QCloE (SubR e _)).loc = e.loc export -Located (Term d n) where - (TYPE _ loc).loc = loc - (IOState loc).loc = loc - (Pi _ _ _ loc).loc = loc - (Lam _ loc).loc = loc - (Sig _ _ loc).loc = loc - (Pair _ _ loc).loc = loc - (Enum _ loc).loc = loc - (Tag _ loc).loc = loc - (Eq _ _ _ loc).loc = loc - (DLam _ loc).loc = loc - (NAT loc).loc = loc - (Nat _ loc).loc = loc - (STRING loc).loc = loc - (Str _ loc).loc = loc - (Succ _ loc).loc = loc - (BOX _ _ loc).loc = loc - (Box _ loc).loc = loc - (Let _ _ _ loc).loc = loc - (E e).loc = e.loc - (CloT (Sub t _)).loc = t.loc - (DCloT (Sub t _)).loc = t.loc +Located (Term q d n) where + (TYPE _ loc).loc = loc + (IOState loc).loc = loc + (Pi _ _ _ loc).loc = loc + (Lam _ loc).loc = loc + (Sig _ _ loc).loc = loc + (Pair _ _ loc).loc = loc + (Enum _ loc).loc = loc + (Tag _ loc).loc = loc + (Eq _ _ _ loc).loc = loc + (DLam _ loc).loc = loc + (NAT loc).loc = loc + (Nat _ loc).loc = loc + (STRING loc).loc = loc + (Str _ loc).loc = loc + (Succ _ loc).loc = loc + (BOX _ _ loc).loc = loc + (Box _ loc).loc = loc + (Let _ _ _ loc).loc = loc + (E e).loc = e.loc + (CloT (Sub t _)).loc = t.loc + (DCloT (Sub t _)).loc = t.loc + (QCloT (SubR t _)).loc = t.loc export Located1 f => Located (ScopedBody s f n) where @@ -289,7 +289,7 @@ Located1 f => Located (Scoped s f n) where export -Relocatable (Elim d n) where +Relocatable (Elim q d n) where setLoc loc (F x u _) = F x u loc setLoc loc (B i _) = B i loc setLoc loc (App fun arg _) = App fun arg loc @@ -317,9 +317,11 @@ Relocatable (Elim d n) where CloE $ Sub (setLoc loc term) subst setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst + setLoc loc (QCloE (SubR term subst)) = + QCloE $ SubR (setLoc loc term) subst export -Relocatable (Term d n) where +Relocatable (Term q d n) where setLoc loc (TYPE l _) = TYPE l loc setLoc loc (IOState _) = IOState loc setLoc loc (Pi qty arg res _) = Pi qty arg res loc @@ -341,6 +343,7 @@ Relocatable (Term d n) where setLoc loc (E e) = E $ setLoc loc e setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst + setLoc loc (QCloT (SubR term subst)) = QCloT $ SubR (setLoc loc term) subst export Relocatable1 f => Relocatable (ScopedBody s f n) where @@ -354,93 +357,93 @@ Relocatable1 f => Relocatable (Scoped s f n) where ||| more convenient Pi public export %inline -PiY : (qty : Qty) -> (x : BindName) -> - (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n +PiY : (qty : Qty q) -> (x : BindName) -> + (arg : Term q d n) -> (res : Term q d (S n)) -> (loc : Loc) -> Term q d n PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc} ||| more convenient Lam public export %inline -LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n +LamY : (x : BindName) -> (body : Term q d (S n)) -> (loc : Loc) -> Term q d n LamY {x, body, loc} = Lam {body = SY [< x] body, loc} public export %inline -LamN : (body : Term d n) -> (loc : Loc) -> Term d n +LamN : (body : Term q d n) -> (loc : Loc) -> Term q d n LamN {body, loc} = Lam {body = SN body, loc} ||| non dependent function type public export %inline -Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n +Arr : (qty : Qty q) -> (arg, res : Term q d n) -> (loc : Loc) -> Term q d n Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc} ||| more convenient Sig public export %inline -SigY : (x : BindName) -> (fst : Term d n) -> - (snd : Term d (S n)) -> (loc : Loc) -> Term d n +SigY : (x : BindName) -> (fst : Term q d n) -> + (snd : Term q d (S n)) -> (loc : Loc) -> Term q d n SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc} ||| non dependent pair type public export %inline -And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n +And : (fst, snd : Term q d n) -> (loc : Loc) -> Term q d n And {fst, snd, loc} = Sig {fst, snd = SN snd, loc} ||| more convenient Eq public export %inline -EqY : (i : BindName) -> (ty : Term (S d) n) -> - (l, r : Term d n) -> (loc : Loc) -> Term d n +EqY : (i : BindName) -> (ty : Term q (S d) n) -> + (l, r : Term q d n) -> (loc : Loc) -> Term q d n EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc} ||| more convenient DLam public export %inline -DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n +DLamY : (i : BindName) -> (body : Term q (S d) n) -> (loc : Loc) -> Term q d n DLamY {i, body, loc} = DLam {body = SY [< i] body, loc} public export %inline -DLamN : (body : Term d n) -> (loc : Loc) -> Term d n +DLamN : (body : Term q d n) -> (loc : Loc) -> Term q d n DLamN {body, loc} = DLam {body = SN body, loc} ||| non dependent equality type public export %inline -Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n +Eq0 : (ty, l, r : Term q d n) -> (loc : Loc) -> Term q d n Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc} ||| same as `F` but as a term public export %inline -FT : Name -> Universe -> Loc -> Term d n +FT : Name -> Universe -> Loc -> Term q d n FT x u loc = E $ F x u loc ||| same as `B` but as a term public export %inline -BT : Var n -> (loc : Loc) -> Term d n +BT : Var n -> (loc : Loc) -> Term q d n BT i loc = E $ B i loc ||| abbreviation for a bound variable like `BV 4` instead of ||| `B (VS (VS (VS (VS VZ))))` public export %inline -BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n +BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim q d n BV i loc = B (V i) loc ||| same as `BV` but as a term public export %inline -BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n +BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term q d n BVT i loc = E $ BV i loc public export %inline -Zero : Loc -> Term d n +Zero : Loc -> Term q d n Zero = Nat 0 public export %inline -enum : List TagVal -> Loc -> Term d n +enum : List TagVal -> Loc -> Term q d n enum ts loc = Enum (SortedSet.fromList ts) loc public export %inline -typeCase : Elim d n -> Term d n -> - List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n +typeCase : Elim q d n -> Term q d n -> + List (TypeCaseArm q d n) -> Term q d n -> Loc -> Elim q d n typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc public export %inline -typeCase1Y : Elim d n -> Term d n -> - (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) -> +typeCase1Y : Elim q d n -> Term q d n -> + (k : TyConKind) -> BContext (arity k) -> Term q d (arity k + n) -> (loc : Loc) -> - {default (NAT loc) def : Term d n} -> - Elim d n + {default (NAT loc) def : Term q d n} -> + Elim q d n typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 36d9320..d22fc19 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -5,6 +5,7 @@ import Quox.Syntax.Term.Subst import Quox.Context import Quox.Pretty +import Quox.SingletonExtra import Data.Vect import Derive.Prelude @@ -13,21 +14,23 @@ import Derive.Prelude export -prettyUniverse : {opts : _} -> Universe -> Eff Pretty (Doc opts) +prettyUniverse : {opts : LayoutOpts} -> Universe -> Eff Pretty (Doc opts) prettyUniverse = hl Universe . text . show export -prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n -> - Eff Pretty (Doc opts) +prettyTerm : {opts : LayoutOpts} -> + NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts) export -prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n -> - Eff Pretty (Doc opts) +prettyElim : {opts : LayoutOpts} -> + NameContexts q d n -> Elim q d n -> Eff Pretty (Doc opts) -private -BTelescope : Nat -> Nat -> Type -BTelescope = Telescope' BindName + +export +prettyQty : {opts : LayoutOpts} -> + NameContexts q d n -> Qty q -> Eff Pretty (Doc opts) +prettyQty names pi = let Val q = names.qtyLen in prettyQty names.qnames pi private @@ -40,109 +43,111 @@ superscript = pack . map sup . unpack where private -PiBind : Nat -> Nat -> Type -PiBind d n = (Qty, BindName, Term d n) +PiBind : TermLike +PiBind q d n = (Qty q, BindName, Term q d n) private -pbname : PiBind d n -> BindName +pbname : PiBind q d n -> BindName pbname (_, x, _) = x private -record SplitPi d n where +record SplitPi q d n where constructor MkSplitPi {0 inner : Nat} - binds : Telescope (PiBind d) n inner - cod : Term d inner + binds : Telescope (PiBind q d) n inner + cod : Term q d inner private -splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n -splitPi binds (Pi qty arg res _) = +splitPi : {q : Nat} -> + Telescope (PiBind q d) n n' -> Term q d n' -> SplitPi q d n +splitPi binds cod@(Pi qty arg res _) = splitPi (binds :< (qty, res.name, arg)) $ - assert_smaller res $ pushSubsts' res.term + assert_smaller cod $ pushSubsts' res.term splitPi binds cod = MkSplitPi {binds, cod} private -prettyPiBind1 : {opts : _} -> - Qty -> BindName -> BContext d -> BContext n -> Term d n -> +prettyPiBind1 : {opts : LayoutOpts} -> + NameContexts q d n -> Qty q -> BindName -> Term q d n -> Eff Pretty (Doc opts) -prettyPiBind1 pi (BN Unused _) dnames tnames s = +prettyPiBind1 names pi (BN Unused _) s = hcat <$> sequence - [prettyQty pi, dotD, - withPrec Arg $ assert_total prettyTerm dnames tnames s] -prettyPiBind1 pi x dnames tnames s = hcat <$> sequence - [prettyQty pi, dotD, - hl Delim $ text "(", - hsep <$> sequence - [prettyTBind x, hl Delim $ text ":", - withPrec Outer $ assert_total prettyTerm dnames tnames s], - hl Delim $ text ")"] + [prettyQty names pi, dotD, + withPrec Arg $ assert_total prettyTerm names s] +prettyPiBind1 names pi x s = + hcat <$> sequence + [prettyQty names pi, dotD, + hl Delim $ text "(", + hsep <$> sequence + [prettyTBind x, hl Delim $ text ":", + withPrec Outer $ assert_total prettyTerm names s], + hl Delim $ text ")"] private -prettyPiBinds : {opts : _} -> - BContext d -> BContext n -> - Telescope (PiBind d) n n' -> +prettyPiBinds : {opts : LayoutOpts} -> + NameContexts q d n -> + Telescope (PiBind q d) n n' -> Eff Pretty (SnocList (Doc opts)) -prettyPiBinds _ _ [<] = pure [<] -prettyPiBinds dnames tnames (binds :< (q, x, t)) = - let tnames' = tnames . map pbname binds in - [|prettyPiBinds dnames tnames binds :< - prettyPiBind1 q x dnames tnames' t|] +prettyPiBinds _ [<] = pure [<] +prettyPiBinds names (binds :< (q, x, t)) = + let names' = extendTermN' (map pbname binds) names in + [|prettyPiBinds names binds :< + prettyPiBind1 names' q x t|] private -SigBind : Nat -> Nat -> Type -SigBind d n = (BindName, Term d n) +SigBind : TermLike +SigBind q d n = (BindName, Term q d n) private -record SplitSig d n where +record SplitSig q d n where constructor MkSplitSig {0 inner : Nat} - binds : Telescope (SigBind d) n inner - last : Term d inner + binds : Telescope (SigBind q d) n inner + last : Term q d inner private -splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n +splitSig : {q : Nat} -> + Telescope (SigBind q d) n n' -> Term q d n' -> SplitSig q d n splitSig binds (Sig fst snd _) = splitSig (binds :< (snd.name, fst)) $ assert_smaller snd $ pushSubsts' snd.term splitSig binds last = MkSplitSig {binds, last} private -prettySigBind1 : {opts : _} -> - BindName -> BContext d -> BContext n -> Term d n -> +prettySigBind1 : {opts : LayoutOpts} -> + NameContexts q d n -> BindName -> Term q d n -> Eff Pretty (Doc opts) -prettySigBind1 (BN Unused _) dnames tnames s = - withPrec InTimes $ assert_total prettyTerm dnames tnames s -prettySigBind1 x dnames tnames s = hcat <$> sequence +prettySigBind1 names (BN Unused _) s = + withPrec InTimes $ assert_total prettyTerm names s +prettySigBind1 names x s = hcat <$> sequence [hl Delim $ text "(", hsep <$> sequence [prettyTBind x, hl Delim $ text ":", - withPrec Outer $ assert_total prettyTerm dnames tnames s], + withPrec Outer $ assert_total prettyTerm names s], hl Delim $ text ")"] private -prettySigBinds : {opts : _} -> - BContext d -> BContext n -> - Telescope (SigBind d) n n' -> +prettySigBinds : {opts : LayoutOpts} -> + NameContexts q d n -> Telescope (SigBind q d) n n' -> Eff Pretty (SnocList (Doc opts)) -prettySigBinds _ _ [<] = pure [<] -prettySigBinds dnames tnames (binds :< (x, t)) = - let tnames' = tnames . map fst binds in - [|prettySigBinds dnames tnames binds :< - prettySigBind1 x dnames tnames' t|] +prettySigBinds _ [<] = pure [<] +prettySigBinds names (binds :< (x, t)) = + let names' = extendTermN' (map fst binds) names in + [|prettySigBinds names binds :< + prettySigBind1 names' x t|] private -prettyTypeLine : {opts : _} -> - BContext d -> BContext n -> - DScopeTerm d n -> +prettyTypeLine : {opts : LayoutOpts} -> + NameContexts q d n -> DScopeTerm q d n -> Eff Pretty (Doc opts) -prettyTypeLine dnames tnames (S _ (N body)) = - withPrec Arg (prettyTerm dnames tnames body) -prettyTypeLine dnames tnames (S [< i] (Y body)) = +prettyTypeLine names (S _ (N body)) = + withPrec Arg (prettyTerm names body) +prettyTypeLine names (S [< i] (Y body)) = parens =<< do + let names' = extendDim i names i' <- prettyDBind i - ty' <- withPrec Outer $ prettyTerm (dnames :< i) tnames body + ty' <- withPrec Outer $ prettyTerm names' body pure $ sep [hsep [i', !darrowD], ty'] @@ -155,16 +160,16 @@ NameChunks : Type NameChunks = SnocList (NameSort, SnocList BindName) private -record SplitLams d n where +record SplitLams q d n where constructor MkSplitLams {0 dinner, ninner : Nat} dnames : BTelescope d dinner tnames : BTelescope n ninner chunks : NameChunks - body : Term dinner ninner + body : Term q dinner ninner private -splitLams : Term d n -> SplitLams d n +splitLams : {q : Nat} -> Term q d n -> SplitLams q d n splitLams s = go [<] [<] [<] (pushSubsts' s) where push : NameSort -> BindName -> NameChunks -> NameChunks @@ -175,7 +180,7 @@ where go : BTelescope d d' -> BTelescope n n' -> SnocList (NameSort, SnocList BindName) -> - Term d' n' -> SplitLams d n + Term q d' n' -> SplitLams q d n go dnames tnames chunks (Lam b _) = go dnames (tnames :< b.name) (push T b.name chunks) $ assert_smaller b $ pushSubsts' b.term @@ -187,28 +192,31 @@ where private -splitTuple : SnocList (Term d n) -> Term d n -> SnocList (Term d n) +splitTuple : {q : Nat} -> + SnocList (Term q d n) -> Term q d n -> SnocList (Term q d n) splitTuple ss p@(Pair t1 t2 _) = splitTuple (ss :< t1) $ assert_smaller p $ pushSubsts' t2 splitTuple ss t = ss :< t private -prettyTArg : {opts : _} -> BContext d -> BContext n -> - Term d n -> Eff Pretty (Doc opts) -prettyTArg dnames tnames s = - withPrec Arg $ assert_total prettyTerm dnames tnames s +prettyTArg : {opts : LayoutOpts} -> + NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts) +prettyTArg names s = + withPrec Arg $ assert_total prettyTerm names s private -prettyDArg : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts) -prettyDArg dnames p = [|atD <+> withPrec Arg (prettyDim dnames p)|] +prettyDArg : {opts : LayoutOpts} -> + NameContexts _ d _ -> Dim d -> Eff Pretty (Doc opts) +prettyDArg names p = [|atD <+> withPrec Arg (prettyDim names.dnames p)|] private -splitApps : Elim d n -> (Elim d n, List (Either (Dim d) (Term d n))) +splitApps : {q : Nat} -> + Elim q d n -> (Elim q d n, List (Either (Dim d) (Term q d n))) splitApps e = go [] (pushSubsts' e) where - go : List (Either (Dim d) (Term d n)) -> Elim d n -> - (Elim d n, List (Either (Dim d) (Term d n))) + go : List (Either (Dim d) (Term q d n)) -> Elim q d n -> + (Elim q d n, List (Either (Dim d) (Term q d n))) go xs e@(App f s _) = go (Right s :: xs) $ assert_smaller e $ pushSubsts' f go xs e@(DApp f p _) = @@ -216,49 +224,53 @@ where go xs s = (s, xs) private -prettyDTApps : {opts : _} -> - BContext d -> BContext n -> - Elim d n -> List (Either (Dim d) (Term d n)) -> +prettyDTApps : {opts : LayoutOpts} -> + NameContexts q d n -> + Elim q d n -> List (Either (Dim d) (Term q d n)) -> Eff Pretty (Doc opts) -prettyDTApps dnames tnames f xs = do - f <- withPrec Arg $ assert_total prettyElim dnames tnames f - xs <- for xs $ either (prettyDArg dnames) (prettyTArg dnames tnames) - parensIfM App =<< prettyAppD f xs +prettyDTApps names f xs = do + f <- withPrec Arg $ assert_total prettyElim names f + xs <- for xs $ either (prettyDArg names) (prettyTArg names) + prettyAppD f xs private -record CaseArm opts d n where +record CaseArm opts q d n where constructor MkCaseArm pat : Doc opts dbinds : BTelescope d dinner -- ๐Ÿด tbinds : BTelescope n ninner - body : Term dinner ninner - -parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n) - private - prettyCaseArm : CaseArm opts d n -> Eff Pretty (Doc opts) - prettyCaseArm (MkCaseArm pat dbinds tbinds body) = do - body <- withPrec Outer $ assert_total - prettyTerm (dnames . dbinds) (tnames . tbinds) body - header <- (pat <++>) <$> darrowD - pure $ ifMultiline (header <++> body) (vsep [header, !(indentD body)]) - - private - prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (List (Doc opts)) - prettyCaseBody xs = traverse prettyCaseArm xs + body : Term q dinner ninner private -prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts) +prettyCaseArm : {opts : LayoutOpts} -> + NameContexts q d n -> CaseArm opts q d n -> + Eff Pretty (Doc opts) +prettyCaseArm names (MkCaseArm pat dbinds tbinds body) = do + let names' = extendDimN' dbinds $ extendTermN' tbinds names + body <- withPrec Outer $ assert_total prettyTerm names' body + header <- (pat <++>) <$> darrowD + pure $ ifMultiline (header <++> body) (vsep [header, !(indentD body)]) + +private +prettyCaseBody : {opts : LayoutOpts} -> + NameContexts q d n -> List (CaseArm opts q d n) -> + Eff Pretty (List (Doc opts)) +prettyCaseBody names xs = traverse (prettyCaseArm names) xs + +private +prettyCompPat : {opts : LayoutOpts} -> + DimConst -> BindName -> Eff Pretty (Doc opts) prettyCompPat e x = [|prettyDimConst e <++> prettyDBind x|] private -prettyCompArm : {opts : _} -> BContext d -> BContext n -> - DimConst -> DScopeTerm d n -> Eff Pretty (Doc opts) -prettyCompArm dnames tnames e s = prettyCaseArm dnames tnames $ +prettyCompArm : {opts : LayoutOpts} -> NameContexts q d n -> + DimConst -> DScopeTerm q d n -> Eff Pretty (Doc opts) +prettyCompArm names e s = prettyCaseArm names $ MkCaseArm !(prettyCompPat e s.name) [< s.name] [<] s.term private -layoutComp : {opts : _} -> +layoutComp : {opts : LayoutOpts} -> (typq : List (Doc opts)) -> (val, r : Doc opts) -> (arms : List (Doc opts)) -> Eff Pretty (Doc opts) layoutComp typq val r arms = do @@ -273,32 +285,33 @@ layoutComp typq val r arms = do export -prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts) +prettyEnum : {opts : LayoutOpts} -> List String -> Eff Pretty (Doc opts) prettyEnum cases = tightBraces =<< fillSeparateTight !commaD <$> traverse (hl Constant . Doc.text . quoteTag) cases private -prettyCaseRet : {opts : _} -> - BContext d -> BContext n -> - ScopeTerm d n -> Eff Pretty (Doc opts) -prettyCaseRet dnames tnames body = withPrec Outer $ case body of - S _ (N tm) => assert_total prettyTerm dnames tnames tm +prettyCaseRet : {opts : LayoutOpts} -> + NameContexts q d n -> ScopeTerm q d n -> Eff Pretty (Doc opts) +prettyCaseRet names body = withPrec Outer $ case body of + S _ (N tm) => assert_total prettyTerm names tm S [< x] (Y tm) => do + let names' = extendTerm x names header <- [|prettyTBind x <++> darrowD|] - body <- assert_total prettyTerm dnames (tnames :< x) tm + body <- assert_total prettyTerm names' tm hangDSingle header body private -prettyCase_ : {opts : _} -> - BContext d -> BContext n -> - Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) -> +prettyCase_ : {opts : LayoutOpts} -> + NameContexts q d n -> + Doc opts -> Elim q d n -> ScopeTerm q d n -> + List (CaseArm opts q d n) -> Eff Pretty (Doc opts) -prettyCase_ dnames tnames intro head ret body = do - head <- withPrec Outer $ assert_total prettyElim dnames tnames head - ret <- prettyCaseRet dnames tnames ret - bodys <- prettyCaseBody dnames tnames body +prettyCase_ names intro head ret body = do + head <- withPrec Outer $ assert_total prettyElim names head + ret <- prettyCaseRet names ret + bodys <- prettyCaseBody names body return <- returnD; of_ <- ofD lb <- hl Delim "{"; rb <- hl Delim "}"; semi <- semiD ind <- askAt INDENT @@ -308,25 +321,27 @@ prettyCase_ dnames tnames intro head ret body = do indent ind $ vseparateTight semi bodys, rb]) private -prettyCase : {opts : _} -> - BContext d -> BContext n -> - Qty -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) -> +prettyCase : {opts : LayoutOpts} -> + NameContexts q d n -> + Qty q -> Elim q d n -> ScopeTerm q d n -> + List (CaseArm opts q d n) -> Eff Pretty (Doc opts) -prettyCase dnames tnames qty head ret body = - prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body +prettyCase names qty head ret body = + prettyCase_ names ![|caseD <+> prettyQty names qty|] head ret body private -LetBinder : Nat -> Nat -> Type -LetBinder d n = (Qty, BindName, Elim d n) +LetBinder : TermLike +LetBinder q d n = (Qty q, BindName, Elim q d n) private -LetExpr : Nat -> Nat -> Nat -> Type -LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n') +LetExpr : (q, d, n, n' : Nat) -> Type +LetExpr q d n n' = (Telescope (LetBinder q d) n n', Term q d n') -- [todo] factor out this and the untyped version somehow export -splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n) +splitLet : Telescope (LetBinder q d) n n' -> Term q d n' -> + Exists (LetExpr q d n) splitLet ys t@(Let qty rhs body _) = splitLet (ys :< (qty, body.name, rhs)) (assert_smaller t body.term) splitLet ys t = @@ -334,38 +349,40 @@ splitLet ys t = private covering prettyLets : {opts : LayoutOpts} -> - BContext d -> BContext a -> Telescope (LetBinder d) a b -> + NameContexts q d a -> Telescope (LetBinder q d) a b -> Eff Pretty (SnocList (Doc opts)) -prettyLets dnames xs lets = snd <$> go lets where - peelAnn : forall d, n. Elim d n -> Maybe (Term d n, Term d n) +prettyLets (MkNameContexts qnames dnames tnames) lets = snd <$> go lets where + peelAnn : forall d, n. Elim q d n -> Maybe (Term q d n, Term q d n) peelAnn (Ann tm ty _) = Just (tm, ty) peelAnn e = Nothing - letHeader : Qty -> BindName -> Eff Pretty (Doc opts) + letHeader : Qty q -> BindName -> Eff Pretty (Doc opts) letHeader qty x = do - lett <- [|letD <+> prettyQty qty|] + lett <- [|letD <+> prettyQty qnames qty|] x <- prettyTBind x pure $ lett <++> x letBody : forall n. BContext n -> - Doc opts -> Elim d n -> Eff Pretty (Doc opts) - letBody tnames hdr e = case peelAnn e of - Just (tm, ty) => do - ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty - tm <- withPrec Outer $ assert_total prettyTerm dnames tnames tm - colon <- colonD; eq <- cstD; d <- askAt INDENT - pure $ hangSingle d (hangSingle d hdr (colon <++> ty)) (eq <++> tm) - Nothing => do - e <- withPrec Outer $ assert_total prettyElim dnames tnames e - eq <- cstD; d <- askAt INDENT - inn <- inD - pure $ ifMultiline - (hsep [hdr, eq, e, inn]) - (vsep [hdr, indent d $ hsep [eq, e, inn]]) + Doc opts -> Elim q d n -> Eff Pretty (Doc opts) + letBody tnames hdr e = + let names = MkNameContexts' qnames dnames tnames in + case peelAnn e of + Just (tm, ty) => do + ty <- withPrec Outer $ assert_total prettyTerm names ty + tm <- withPrec Outer $ assert_total prettyTerm names tm + colon <- colonD; eq <- cstD; d <- askAt INDENT + pure $ hangSingle d (hangSingle d hdr (colon <++> ty)) (eq <++> tm) + Nothing => do + e <- withPrec Outer $ assert_total prettyElim names e + eq <- cstD; d <- askAt INDENT + inn <- inD + pure $ ifMultiline + (hsep [hdr, eq, e, inn]) + (vsep [hdr, indent d $ hsep [eq, e, inn]]) - go : forall b. Telescope (LetBinder d) a b -> + go : forall b. Telescope (LetBinder q d) a b -> Eff Pretty (BContext b, SnocList (Doc opts)) - go [<] = pure (xs, [<]) + go [<] = pure (tnames, [<]) go (lets :< (qty, x, rhs)) = do (ys, docs) <- go lets doc <- letBody ys !(letHeader qty x) rhs @@ -385,7 +402,7 @@ toTel [<] = [<] toTel (ctx :< x) = toTel ctx :< x private -prettyTyCasePat : {opts : _} -> +prettyTyCasePat : {opts : LayoutOpts} -> (k : TyConKind) -> BContext (arity k) -> Eff Pretty (Doc opts) prettyTyCasePat KTYPE [<] = typeD @@ -402,13 +419,14 @@ prettyTyCasePat KString [<] = stringD prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a -prettyLambda : {opts : _} -> BContext d -> BContext n -> - Term d n -> Eff Pretty (Doc opts) -prettyLambda dnames tnames s = - parensIfM Outer =<< do - let MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s - hangDSingle !(header chunks) - !(assert_total prettyTerm (dnames . ds) (tnames . ts) body) +prettyLambda : {opts : LayoutOpts} -> + NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts) +prettyLambda names s = + let Val q = names.qtyLen + MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s + names' = extendDimN' ds $ extendTermN' ts names in + parensIfM Outer =<< + hangDSingle !(header chunks) !(assert_total prettyTerm names' body) where introChar : NameSort -> Eff Pretty (Doc opts) introChar T = lamD @@ -426,198 +444,207 @@ where header cs = sep <$> traverse (\(s, xs) => header1 s (toList xs)) (toList cs) -prettyDisp : {opts : _} -> Universe -> Eff Pretty (Maybe (Doc opts)) +prettyDisp : {opts : LayoutOpts} -> Universe -> Eff Pretty (Maybe (Doc opts)) prettyDisp 0 = pure Nothing prettyDisp u = map Just $ hl Universe =<< ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u) -prettyTerm dnames tnames (TYPE l _) = do +prettyTerm names (TYPE l _) = do type <- hl Syntax . text =<< ifUnicode "โ˜…" "Type" level <- prettyDisp l pure $ maybe type (type <+>) level -prettyTerm dnames tnames (IOState _) = +prettyTerm _ (IOState _) = ioStateD -prettyTerm dnames tnames (Pi qty arg res _) = - parensIfM Outer =<< do - let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term - arr <- arrowD - lines <- map (<++> arr) <$> prettyPiBinds dnames tnames binds - let tnames = tnames . map pbname binds - cod <- withPrec Outer $ prettyTerm dnames tnames (assert_smaller res cod) - pure $ sepSingle $ toList $ lines :< cod +prettyTerm names (Pi qty arg res _) = do + let Val q = names.qtyLen + MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term + arr <- arrowD + lines <- map (<++> arr) <$> prettyPiBinds names binds + let names' = extendTermN' (map pbname binds) names + cod <- withPrec Outer $ prettyTerm names' (assert_smaller res cod) + parensIfM Outer $ sepSingle $ toList $ lines :< cod -prettyTerm dnames tnames s@(Lam {}) = - prettyLambda dnames tnames s +prettyTerm names s@(Lam {}) = + prettyLambda names s -prettyTerm dnames tnames (Sig fst snd _) = - parensIfM Times =<< do - let MkSplitSig {binds, last} = splitSig [< (snd.name, fst)] snd.term - times <- timesD - lines <- map (<++> times) <$> prettySigBinds dnames tnames binds - let tnames = tnames . map Builtin.fst binds - last <- withPrec InTimes $ - prettyTerm dnames tnames (assert_smaller snd last) - pure $ sepSingle $ toList $ lines :< last +prettyTerm names (Sig tfst tsnd _) = do + let Val q = names.qtyLen + MkSplitSig {binds, last} = splitSig [< (tsnd.name, tfst)] tsnd.term + times <- timesD + lines <- map (<++> times) <$> prettySigBinds names binds + let names' = extendTermN' (map fst binds) names + last <- withPrec InTimes $ prettyTerm names' (assert_smaller tsnd last) + parensIfM Times $ sepSingle $ toList $ lines :< last -prettyTerm dnames tnames p@(Pair fst snd _) = - parens =<< do - let elems = splitTuple [< fst] snd - lines <- for elems $ \t => - withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t - pure $ separateTight !commaD lines +prettyTerm names p@(Pair s t _) = do + let Val q = names.qtyLen + elems = splitTuple [< s] t + lines <- for elems $ \t => + withPrec Outer $ prettyTerm names $ assert_smaller p t + parens $ separateTight !commaD lines -prettyTerm dnames tnames (Enum cases _) = +prettyTerm _ (Enum cases _) = prettyEnum $ SortedSet.toList cases -prettyTerm dnames tnames (Tag tag _) = +prettyTerm _ (Tag tag _) = prettyTag tag -prettyTerm dnames tnames (Eq (S _ (N ty)) l r _) = - parensIfM Eq =<< do - l <- withPrec InEq $ prettyTerm dnames tnames l - r <- withPrec InEq $ prettyTerm dnames tnames r - ty <- withPrec InEq $ prettyTerm dnames tnames ty - pure $ sep [l <++> !eqndD, r <++> !colonD, ty] +prettyTerm names (Eq (S _ (N ty)) l r _) = do + l <- withPrec InEq $ prettyTerm names l + r <- withPrec InEq $ prettyTerm names r + ty <- withPrec InEq $ prettyTerm names ty + parensIfM Eq $ sep [l <++> !eqndD, r <++> !colonD, ty] -prettyTerm dnames tnames (Eq ty l r _) = - parensIfM App =<< do - ty <- prettyTypeLine dnames tnames ty - l <- withPrec Arg $ prettyTerm dnames tnames l - r <- withPrec Arg $ prettyTerm dnames tnames r - prettyAppD !eqD [ty, l, r] +prettyTerm names (Eq ty l r _) = do + ty <- prettyTypeLine names ty + l <- withPrec Arg $ prettyTerm names l + r <- withPrec Arg $ prettyTerm names r + prettyAppD !eqD [ty, l, r] -prettyTerm dnames tnames s@(DLam {}) = - prettyLambda dnames tnames s +prettyTerm names s@(DLam {}) = + prettyLambda names s -prettyTerm dnames tnames (NAT _) = natD -prettyTerm dnames tnames (Nat n _) = hl Syntax $ pshow n -prettyTerm dnames tnames (Succ p _) = - parensIfM App =<< - prettyAppD !succD [!(withPrec Arg $ prettyTerm dnames tnames p)] +prettyTerm _ (NAT _) = natD +prettyTerm _ (Nat n _) = hl Syntax $ pshow n +prettyTerm names (Succ p _) = + prettyAppD !succD [!(withPrec Arg $ prettyTerm names p)] -prettyTerm dnames tnames (STRING _) = stringD -prettyTerm dnames tnames (Str s _) = prettyStrLit s +prettyTerm _ (STRING _) = stringD +prettyTerm _ (Str s _) = prettyStrLit s -prettyTerm dnames tnames (BOX qty ty _) = +prettyTerm names (BOX qty ty _) = bracks . hcat =<< - sequence [prettyQty qty, dotD, - withPrec Outer $ prettyTerm dnames tnames ty] + sequence [prettyQty names qty, dotD, + withPrec Outer $ prettyTerm names ty] -prettyTerm dnames tnames (Box val _) = - bracks =<< withPrec Outer (prettyTerm dnames tnames val) +prettyTerm names (Box val _) = + bracks =<< withPrec Outer (prettyTerm names val) -prettyTerm dnames tnames (Let qty rhs body _) = do +prettyTerm names (Let qty rhs body _) = do let Evidence _ (lets, body) = splitLet [< (qty, body.name, rhs)] body.term - heads <- prettyLets dnames tnames lets - let tnames = tnames . map (\(_, x, _) => x) lets - body <- withPrec Outer $ assert_total prettyTerm dnames tnames body + heads <- prettyLets names lets + let names' = extendTermN' (map (fst . snd) lets) names + body <- withPrec Outer $ assert_total prettyTerm names' body let lines = toList $ heads :< body pure $ ifMultiline (hsep lines) (vsep lines) -prettyTerm dnames tnames (E e) = - case the (Elim d n) (pushSubsts' e) of - Ann tm _ _ => assert_total prettyTerm dnames tnames tm - _ => assert_total prettyElim dnames tnames e +prettyTerm names (E e) = do + -- [fixme] do this stuff somewhere else!!! + let Val q = names.qtyLen + case pushSubsts' e {tm = Elim} of + Ann tm _ _ => assert_total prettyTerm names tm + _ => assert_total prettyElim names e -prettyTerm dnames tnames t0@(CloT (Sub t ph)) = - prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' id ph t +prettyTerm names t0@(CloT (Sub t ph)) = do + let Val q = names.qtyLen + prettyTerm names $ assert_smaller t0 $ pushSubstsWith' id id ph t -prettyTerm dnames tnames t0@(DCloT (Sub t ph)) = - prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' ph id t +prettyTerm names t0@(DCloT (Sub t ph)) = do + let Val q = names.qtyLen + prettyTerm names $ assert_smaller t0 $ pushSubstsWith' id ph id t -prettyElim dnames tnames (F x u _) = do +prettyTerm names t0@(QCloT (SubR t ph)) = do + let Val q = names.qtyLen + prettyTerm names $ assert_smaller t0 $ pushSubstsWith' ph id id t + +prettyElim names (F x u _) = do x <- prettyFree x u <- prettyDisp u pure $ maybe x (x <+>) u -prettyElim dnames tnames (B i _) = - prettyTBind $ tnames !!! i +prettyElim names (B i _) = + prettyTBind $ names.tnames !!! i -prettyElim dnames tnames e@(App {}) = - let (f, xs) = splitApps e in - prettyDTApps dnames tnames f xs +prettyElim names e@(App {}) = do + let Val q = names.qtyLen + (f, xs) = splitApps e + prettyDTApps names f xs -prettyElim dnames tnames (CasePair qty pair ret body _) = do +prettyElim names (CasePair qty pair ret body _) = do let [< x, y] = body.names - pat <- parens . hsep =<< sequence - [[|prettyTBind x <+> commaD|], prettyTBind y] - prettyCase dnames tnames qty pair ret + pat <- parens $ !(prettyTBind x) <+> !commaD <++> !(prettyTBind y) + prettyCase names qty pair ret [MkCaseArm pat [<] [< x, y] body.term] -prettyElim dnames tnames (Fst pair _) = - parensIfM App =<< do - pair <- prettyTArg dnames tnames (E pair) - prettyAppD !fstD [pair] +prettyElim names (Fst pair _) = do + pair <- prettyTArg names (E pair) + prettyAppD !fstD [pair] -prettyElim dnames tnames (Snd pair _) = - parensIfM App =<< do - pair <- prettyTArg dnames tnames (E pair) - prettyAppD !sndD [pair] +prettyElim names (Snd pair _) = do + pair <- prettyTArg names (E pair) + prettyAppD !sndD [pair] -prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do +prettyElim names (CaseEnum qty tag ret arms _) = do arms <- for (SortedMap.toList arms) $ \(tag, body) => pure $ MkCaseArm !(prettyTag tag) [<] [<] body - prettyCase dnames tnames qty tag ret arms + prettyCase names qty tag ret arms -prettyElim dnames tnames (CaseNat qty qtyIH nat ret zero succ _) = do +prettyElim names (CaseNat qty qtyIH nat ret zero succ _) = do let zarm = MkCaseArm !zeroD [<] [<] zero [< p, ih] = succ.names spat0 <- [|succD <++> prettyTBind p|] - ihpat0 <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih] + ihpat0 <- map hcat $ sequence [prettyQty names qtyIH, dotD, prettyTBind ih] spat <- if ih.val == Unused then pure spat0 - else pure $ hsep [spat0 <+> !commaD, ihpat0] + else pure $ spat0 <+> !commaD <++> ihpat0 let sarm = MkCaseArm spat [<] [< p, ih] succ.term - prettyCase dnames tnames qty nat ret [zarm, sarm] + prettyCase names qty nat ret [zarm, sarm] -prettyElim dnames tnames (CaseBox qty box ret body _) = do +prettyElim names (CaseBox qty box ret body _) = do pat <- bracks =<< prettyTBind body.name let arm = MkCaseArm pat [<] [< body.name] body.term - prettyCase dnames tnames qty box ret [arm] + prettyCase names qty box ret [arm] -prettyElim dnames tnames e@(DApp {}) = - let (f, xs) = splitApps e in - prettyDTApps dnames tnames f xs +prettyElim names e@(DApp {}) = do + let Val q = names.qtyLen + (f, xs) = splitApps e + prettyDTApps names f xs -prettyElim dnames tnames (Ann tm ty _) = - case the (Term d n) (pushSubsts' tm) of - E e => assert_total prettyElim dnames tnames e +prettyElim names (Ann tm ty _) = do + -- [fixme] do this stuff somewhere else!!! + let Val q = names.qtyLen + case pushSubsts' tm {tm = Term} of + E e => assert_total prettyElim names e _ => do - tm <- withPrec AnnL $ assert_total prettyTerm dnames tnames tm - ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty + tm <- withPrec AnnL $ assert_total prettyTerm names tm + ty <- withPrec Outer $ assert_total prettyTerm names ty parensIfM Outer =<< hangDSingle (tm <++> !annD) ty -prettyElim dnames tnames (Coe ty p q val _) = - parensIfM App =<< do - ty <- prettyTypeLine dnames tnames ty - p <- prettyDArg dnames p - q <- prettyDArg dnames q - val <- prettyTArg dnames tnames val - prettyAppD !coeD [ty, sep [p, q], val] +prettyElim names (Coe ty p p' val _) = do + ty <- prettyTypeLine names ty + p <- prettyDArg names p + p' <- prettyDArg names p' + val <- prettyTArg names val + prettyAppD !coeD [ty, p <++> p', val] -prettyElim dnames tnames e@(Comp ty p q val r zero one _) = - parensIfM App =<< do - ty <- assert_total $ prettyTypeLine dnames tnames $ SN ty - pq <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q] - val <- prettyTArg dnames tnames val - r <- prettyDArg dnames r - arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|] - arm1 <- prettyCompArm dnames tnames One one - ind <- askAt INDENT - layoutComp [ty, pq] val r [arm0, arm1] +prettyElim names e@(Comp ty p p' val r zero one _) = do + ty <- assert_total $ prettyTypeLine names $ SN ty + pp <- [|prettyDArg names p <++> prettyDArg names p'|] + val <- prettyTArg names val + r <- prettyDArg names r + arm0 <- [|prettyCompArm names Zero zero <+> semiD|] + arm1 <- prettyCompArm names One one + ind <- askAt INDENT + parensIfM App =<< layoutComp [ty, pp] val r [arm0, arm1] -prettyElim dnames tnames (TypeCase ty ret arms def _) = do +prettyElim names (TypeCase ty ret arms def _) = do arms <- for (toList arms) $ \(k ** body) => do pat <- prettyTyCasePat k body.names pure $ MkCaseArm pat [<] (toTel body.names) body.term let darm = MkCaseArm !undD [<] [<] def - prettyCase_ dnames tnames !typecaseD ty (SN ret) $ arms ++ [darm] + prettyCase_ names !typecaseD ty (SN ret) $ arms ++ [darm] -prettyElim dnames tnames e0@(CloE (Sub e ph)) = - prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' id ph e +prettyElim names e0@(CloE (Sub e ph)) = do + let Val q = names.qtyLen + prettyElim names $ assert_smaller e0 $ pushSubstsWith' id id ph e -prettyElim dnames tnames e0@(DCloE (Sub e ph)) = - prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' ph id e +prettyElim names e0@(DCloE (Sub e ph)) = do + let Val q = names.qtyLen + prettyElim names $ assert_smaller e0 $ pushSubstsWith' id ph id e + +prettyElim names e0@(QCloE (SubR e ph)) = do + let Val q = names.qtyLen + prettyElim names $ assert_smaller e0 $ pushSubstsWith' ph id id e diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index bb13d38..da90850 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -6,10 +6,42 @@ import Data.SnocVect %default total +namespace CanQSubst + public export + interface CanQSubst (0 tm : TermLike) where + (//) : {q1, q2 : Nat} -> tm q1 d n -> Lazy (QSubst q1 q2) -> tm q2 d n + +||| does the minimal reasonable work: +||| - deletes the closure around an atomic constant like `TYPE` +||| - deletes an identity substitution +||| - composes (lazily) with an existing top-level dim-closure +||| - otherwise, wraps in a new closure +export +CanQSubst Term where + s // Shift SZ = s + TYPE l loc // _ = TYPE l loc + QCloT (SubR s ph) // th = QCloT $ SubR s $ ph .? th + s // th = QCloT $ SubR s th + +||| does the minimal reasonable work: +||| - deletes the closure around a term variable +||| - deletes an identity substitution +||| - composes (lazily) with an existing top-level dim-closure +||| - immediately looks up bound variables in a +||| top-level sequence of dimension applications +||| - otherwise, wraps in a new closure +export +CanQSubst Elim where + e // Shift SZ = e + F x u loc // _ = F x u loc -- [todo] q args + B i loc // _ = B i loc + QCloE (SubR e ph) // th = QCloE $ SubR e $ ph .? th + e // th = QCloE $ SubR e th + namespace CanDSubst public export interface CanDSubst (0 tm : TermLike) where - (//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n + (//) : tm q d1 n -> Lazy (DSubst d1 d2) -> tm q d2 n ||| does the minimal reasonable work: ||| - deletes the closure around an atomic constant like `TYPE` @@ -24,7 +56,7 @@ CanDSubst Term where s // th = DCloT $ Sub s th private -subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n +subDArgs : Elim q d1 n -> DSubst d1 d2 -> Elim q d2 n subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc subDArgs e th = DCloE $ Sub e th @@ -44,40 +76,54 @@ CanDSubst Elim where DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th e // th = DCloE $ Sub e th +namespace QSubst.ScopeTermN + export %inline + (//) : {q1, q2 : Nat} -> ScopeTermN s q1 d n -> Lazy (QSubst q1 q2) -> + ScopeTermN s q2 d n + S ns (Y body) // th = S ns $ Y $ body // th + S ns (N body) // th = S ns $ N $ body // th + namespace DSubst.ScopeTermN export %inline - (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) -> - ScopeTermN s d2 n + (//) : ScopeTermN s q d1 n -> Lazy (DSubst d1 d2) -> + ScopeTermN s q d2 n + S ns (Y body) // th = S ns $ Y $ body // th + S ns (N body) // th = S ns $ N $ body // th + +namespace QSubst.DScopeTermN + export %inline + (//) : {q1, q2 : Nat} -> DScopeTermN s q1 d n -> Lazy (QSubst q1 q2) -> + DScopeTermN s q2 d n S ns (Y body) // th = S ns $ Y $ body // th S ns (N body) // th = S ns $ N $ body // th namespace DSubst.DScopeTermN export %inline (//) : {s : Nat} -> - DScopeTermN s d1 n -> Lazy (DSubst d1 d2) -> - DScopeTermN s d2 n + DScopeTermN s q d1 n -> Lazy (DSubst d1 d2) -> + DScopeTermN s q d2 n S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th S ns (N body) // th = S ns $ N $ body // th export %inline -FromVarR (Elim d) where fromVarR = B +FromVarR (Elim q d) where fromVarR = B export %inline -FromVar (Elim d) where fromVar = B; fromVarSame _ _ = Refl +FromVar (Elim q d) where fromVar = B; fromVarSame _ _ = Refl export %inline -FromVarR (Term d) where fromVarR = E .: fromVarR +FromVarR (Term q d) where fromVarR = E .: fromVarR export %inline -FromVar (Term d) where fromVar = E .: fromVar; fromVarSame _ _ = Refl +FromVar (Term q d) where fromVar = E .: fromVar; fromVarSame _ _ = Refl export -CanSubstSelf (Elim d) +CanSubstSelf (Elim q d) private -tsubstElim : Elim d from -> Lazy (TSubst d from to) -> Elim d to +tsubstElim : Elim q d from -> Lazy (TSubst q d from to) -> Elim q d to tsubstElim (F x u loc) _ = F x u loc tsubstElim (B i loc) th = get th i loc tsubstElim (CloE (Sub e ph)) th = assert_total CloE $ Sub e $ ph . th @@ -92,15 +138,15 @@ tsubstElim e th = ||| - composes (lazily) with an existing top-level closure ||| - immediately looks up a bound variable ||| - otherwise, wraps in a new closure -CanSubstSelfR (Elim d) where (//?) = tsubstElim +CanSubstSelfR (Elim q d) where (//?) = tsubstElim export -CanSubstSelf (Elim d) where (//) = tsubstElim; substSame _ _ = Refl +CanSubstSelf (Elim q d) where (//) = tsubstElim; substSame _ _ = Refl namespace CanTSubst public export interface CanTSubst (0 tm : TermLike) where - (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2 + (//) : tm q d n1 -> Lazy (TSubst q d n1 n2) -> tm q d n2 ||| does the minimal reasonable work: ||| - deletes the closure around an atomic constant like `TYPE` @@ -120,69 +166,89 @@ CanTSubst Term where namespace ScopeTermN export %inline (//) : {s : Nat} -> - ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> - ScopeTermN s d n2 + ScopeTermN s q d n1 -> Lazy (TSubst q d n1 n2) -> + ScopeTermN s q d n2 S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th S ns (N body) // th = S ns $ N $ body // th namespace DScopeTermN export %inline (//) : {s : Nat} -> - DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2 + DScopeTermN s q d n1 -> Lazy (TSubst q d n1 n2) -> + DScopeTermN s q d n2 S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th S ns (N body) // th = S ns $ N $ body // th -export %inline CanShift (Term d) where s // by = s // Shift by -export %inline CanShift (Elim d) where e // by = e // Shift by +export %inline CanShift (Term q d) where s // by = s // Shift by +export %inline CanShift (Elim q d) where e // by = e // Shift by -export %inline CanShift (flip Term n) where s // by = s // Shift by -export %inline CanShift (flip Elim n) where e // by = e // Shift by +-- -- from is not accessible in this context +-- export %inline CanShift (\q => Term q d n) where s // by = s // Shift by +-- export %inline CanShift (\q => Elim q d n) where e // by = e // Shift by + +export %inline CanShift (\d => Term q d n) where s // by = s // Shift by +export %inline CanShift (\d => Elim q d n) where e // by = e // Shift by export %inline -{s : Nat} -> CanShift (ScopeTermN s d) where +{s : Nat} -> CanShift (ScopeTermN s q d) where b // by = b // Shift by export %inline -comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2 -comp th ps ph = map (// th) ps . ph +comp : {q1, q2 : Nat} -> + QSubst q1 q2 -> DSubst d1 d2 -> + TSubst q1 d1 n1 mid -> TSubst q2 d2 mid n2 -> TSubst q2 d2 n1 n2 +comp th ph ps ps' = map (\t => t // th // ph) ps . ps' + +-- export %inline +-- compD : DSubst d1 d2 -> TSubst q d1 n1 mid -> +-- TSubst q d2 mid n2 -> TSubst q d2 n1 n2 +-- compD th ps ph = map (// th) ps . ph + +-- export %inline +-- compQ : {q1, q2 : Nat} -> QSubst q1 q2 -> TSubst q1 d n1 mid -> +-- TSubst q2 d mid n2 -> TSubst q2 d n1 n2 +-- compQ th ps ph = map (// th) ps . ph public export %inline -dweakT : (by : Nat) -> Term d n -> Term (by + d) n +dweakT : (by : Nat) -> Term q d n -> Term q (by + d) n dweakT by t = t // shift by public export %inline -dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n +dweakS : (by : Nat) -> ScopeTermN s q d n -> ScopeTermN s q (by + d) n dweakS by t = t // shift by public export %inline dweakDS : {s : Nat} -> (by : Nat) -> - DScopeTermN s d n -> DScopeTermN s (by + d) n + DScopeTermN s q d n -> DScopeTermN s q (by + d) n dweakDS by t = t // shift by public export %inline -dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n +dweakE : (by : Nat) -> Elim q d n -> Elim q (by + d) n dweakE by t = t // shift by public export %inline -weakT : (by : Nat) -> Term d n -> Term d (by + n) +weakT : (by : Nat) -> Term q d n -> Term q d (by + n) weakT by t = t // shift by public export %inline -weakS : {s : Nat} -> (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n) +weakS : {s : Nat} -> (by : Nat) -> + ScopeTermN s q d n -> ScopeTermN s q d (by + n) weakS by t = t // shift by public export %inline weakDS : {s : Nat} -> (by : Nat) -> - DScopeTermN s d n -> DScopeTermN s d (by + n) + DScopeTermN s q d n -> DScopeTermN s q d (by + n) weakDS by t = t // shift by public export %inline -weakE : (by : Nat) -> Elim d n -> Elim d (by + n) +weakE : (by : Nat) -> Elim q d n -> Elim q d (by + n) weakE by t = t // shift by +-- no weakQ etc because no first-class binder to push under + parameters {auto _ : CanShift f} {s : Nat} export %inline @@ -206,69 +272,74 @@ namespace ScopeTermN t.term0 = getTerm0 t.body export %inline -subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n +subN : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n subN (S _ (Y body)) es = body // fromSnocVect es subN (S _ (N body)) _ = body export %inline -sub1 : ScopeTerm d n -> Elim d n -> Term d n +sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n sub1 t e = subN t [< e] export %inline -dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n +dsubN : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n dsubN (S _ (Y body)) ps = body // fromSnocVect ps dsubN (S _ (N body)) _ = body export %inline -dsub1 : DScopeTerm d n -> Dim d -> Term d n +dsub1 : DScopeTerm q d n -> Dim d -> Term q d n dsub1 t p = dsubN t [< p] public export %inline -(.zero) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n +(.zero) : (body : DScopeTerm q d n) -> {default body.loc loc : Loc} -> + Term q d n body.zero = dsub1 body $ K Zero loc public export %inline -(.one) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n +(.one) : (body : DScopeTerm q d n) -> {default body.loc loc : Loc} -> + Term q d n body.one = dsub1 body $ K One loc public export 0 CloTest : TermLike -> Type -CloTest tm = forall d, n. tm d n -> Bool +CloTest tm = forall q, d, n. tm q d n -> Bool public export interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where - pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 -> - tm d1 n1 -> Subset (tm d2 n2) (No . isClo) + pushSubstsWith : {q1, q2 : Nat} -> + QSubst q1 q2 -> DSubst d1 d2 -> TSubst q2 d2 n1 n2 -> + tm q1 d1 n1 -> Subset (tm q2 d2 n2) (No . isClo) public export -0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n) +0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm q d n) NotClo = No . isClo public export 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} -> PushSubsts tm isClo => TermLike -NonClo tm d n = Subset (tm d n) NotClo +NonClo tm q d n = Subset (tm q d n) NotClo public export %inline nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) => - (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n + (t : tm q d n) -> (0 nc : NotClo t) => NonClo tm q d n nclo t = Element t nc parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo} ||| if the input term has any top-level closures, push them under one layer of ||| syntax export %inline - pushSubsts : tm d n -> NonClo tm d n - pushSubsts s = pushSubstsWith id id s + pushSubsts : {q : Nat} -> tm q d n -> NonClo tm q d n + pushSubsts s = pushSubstsWith id id id s export %inline - pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2 - pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x + pushSubstsWith' : {q1, q2 : Nat} -> + QSubst q1 q2 -> DSubst d1 d2 -> TSubst q2 d2 n1 n2 -> + tm q1 d1 n1 -> tm q2 d2 n2 + pushSubstsWith' th ph ps x = fst $ pushSubstsWith th ph ps x export %inline - pushSubsts' : tm d n -> tm d n + pushSubsts' : {q : Nat} -> tm q d n -> tm q d n pushSubsts' s = fst $ pushSubsts s mutual @@ -276,6 +347,7 @@ mutual isCloT : CloTest Term isCloT (CloT {}) = True isCloT (DCloT {}) = True + isCloT (QCloT {}) = True isCloT (E e) = isCloE e isCloT _ = False @@ -283,92 +355,118 @@ mutual isCloE : CloTest Elim isCloE (CloE {}) = True isCloE (DCloE {}) = True + isCloE (QCloE {}) = True isCloE _ = False export PushSubsts Elim Subst.isCloE where - pushSubstsWith th ph (F x u loc) = + pushSubstsWith th ph ps (F x u loc) = nclo $ F x u loc - pushSubstsWith th ph (B i loc) = - let res = get ph i loc in + pushSubstsWith th ph ps (B i loc) = + let res = get ps i loc in case nchoose $ isCloE res of Left yes => assert_total pushSubsts res Right no => Element res no - pushSubstsWith th ph (App f s loc) = - nclo $ App (f // th // ph) (s // th // ph) loc - pushSubstsWith th ph (CasePair pi p r b loc) = - nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc - pushSubstsWith th ph (Fst pair loc) = - nclo $ Fst (pair // th // ph) loc - pushSubstsWith th ph (Snd pair loc) = - nclo $ Snd (pair // th // ph) loc - pushSubstsWith th ph (CaseEnum pi t r arms loc) = - nclo $ CaseEnum pi (t // th // ph) (r // th // ph) - (map (\b => b // th // ph) arms) loc - pushSubstsWith th ph (CaseNat pi pi' n r z s loc) = - nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph) - (z // th // ph) (s // th // ph) loc - pushSubstsWith th ph (CaseBox pi x r b loc) = - nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc - pushSubstsWith th ph (DApp f d loc) = - nclo $ DApp (f // th // ph) (d // th) loc - pushSubstsWith th ph (Ann s a loc) = - nclo $ Ann (s // th // ph) (a // th // ph) loc - pushSubstsWith th ph (Coe ty p q val loc) = - nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc - pushSubstsWith th ph (Comp ty p q val r zero one loc) = - nclo $ Comp (ty // th // ph) (p // th) (q // th) - (val // th // ph) (r // th) - (zero // th // ph) (one // th // ph) loc - pushSubstsWith th ph (TypeCase ty ret arms def loc) = - nclo $ TypeCase (ty // th // ph) (ret // th // ph) - (map (\t => t // th // ph) arms) (def // th // ph) loc - pushSubstsWith th ph (CloE (Sub e ps)) = - pushSubstsWith th (comp th ps ph) e - pushSubstsWith th ph (DCloE (Sub e ps)) = - pushSubstsWith (ps . th) ph e + pushSubstsWith th ph ps (App f s loc) = + nclo $ App (f // th // ph // ps) (s // th // ph // ps) loc + pushSubstsWith th ph ps (CasePair pi p r b loc) = + nclo $ CasePair (pi //? th) + (p // th // ph // ps) + (r // th // ph // ps) + (b // th // ph // ps) loc + pushSubstsWith th ph ps (Fst pair loc) = + nclo $ Fst (pair // th // ph // ps) loc + pushSubstsWith th ph ps (Snd pair loc) = + nclo $ Snd (pair // th // ph // ps) loc + pushSubstsWith th ph ps (CaseEnum pi t r arms loc) = + nclo $ CaseEnum (pi //? th) + (t // th // ph // ps) + (r // th // ph // ps) + (map (\b => b // th // ph // ps) arms) loc + pushSubstsWith th ph ps (CaseNat pi pi' n r z s loc) = + nclo $ CaseNat (pi //? th) (pi' //? th) + (n // th // ph // ps) + (r // th // ph // ps) + (z // th // ph // ps) + (s // th // ph // ps) loc + pushSubstsWith th ph ps (CaseBox pi x r b loc) = + nclo $ CaseBox (pi //? th) + (x // th // ph // ps) + (r // th // ph // ps) + (b // th // ph // ps) loc + pushSubstsWith th ph ps (DApp f d loc) = + nclo $ DApp (f // th // ph // ps) (d // ph) loc + pushSubstsWith th ph ps (Ann s a loc) = + nclo $ Ann (s // th // ph // ps) (a // th // ph // ps) loc + pushSubstsWith th ph ps (Coe ty p q val loc) = + nclo $ Coe + (ty // th // ph // ps) + (p // ph) (q // ph) + (val // th // ph // ps) loc + pushSubstsWith th ph ps (Comp ty p q val r zero one loc) = + nclo $ Comp (ty // th // ph // ps) (p // ph) (q // ph) + (val // th // ph // ps) (r // ph) + (zero // th // ph // ps) (one // th // ph // ps) loc + pushSubstsWith th ph ps (TypeCase ty ret arms def loc) = + nclo $ TypeCase (ty // th // ph // ps) (ret // th // ph // ps) + (map (\t => t // th // ph // ps) arms) (def // th // ph // ps) loc + pushSubstsWith th ph ps (CloE (Sub e ps')) = + pushSubstsWith th ph (comp th ph ps' ps) e + pushSubstsWith th ph ps (DCloE (Sub e ph')) = + pushSubstsWith th (ph' . ph) ps e + pushSubstsWith th ph ps (QCloE (SubR e th')) = + pushSubstsWith (th' .? th) ph ps e export PushSubsts Term Subst.isCloT where - pushSubstsWith th ph (TYPE l loc) = + pushSubstsWith th ph ps (TYPE l loc) = nclo $ TYPE l loc - pushSubstsWith th ph (IOState loc) = + pushSubstsWith _ _ _ (IOState loc) = nclo $ IOState loc - pushSubstsWith th ph (Pi qty a body loc) = - nclo $ Pi qty (a // th // ph) (body // th // ph) loc - pushSubstsWith th ph (Lam body loc) = - nclo $ Lam (body // th // ph) loc - pushSubstsWith th ph (Sig a b loc) = - nclo $ Sig (a // th // ph) (b // th // ph) loc - pushSubstsWith th ph (Pair s t loc) = - nclo $ Pair (s // th // ph) (t // th // ph) loc - pushSubstsWith th ph (Enum tags loc) = + pushSubstsWith th ph ps (Pi qty a body loc) = + nclo $ Pi (qty //? th) + (a // th // ph // ps) + (body // th // ph // ps) loc + pushSubstsWith th ph ps (Lam body loc) = + nclo $ Lam (body // th // ph // ps) loc + pushSubstsWith th ph ps (Sig a b loc) = + nclo $ Sig (a // th // ph // ps) (b // th // ph // ps) loc + pushSubstsWith th ph ps (Pair s t loc) = + nclo $ Pair (s // th // ph // ps) (t // th // ph // ps) loc + pushSubstsWith th ph ps (Enum tags loc) = nclo $ Enum tags loc - pushSubstsWith th ph (Tag tag loc) = + pushSubstsWith th ph ps (Tag tag loc) = nclo $ Tag tag loc - pushSubstsWith th ph (Eq ty l r loc) = - nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc - pushSubstsWith th ph (DLam body loc) = - nclo $ DLam (body // th // ph) loc - pushSubstsWith _ _ (NAT loc) = + pushSubstsWith th ph ps (Eq ty l r loc) = + nclo $ Eq + (ty // th // ph // ps) + (l // th // ph // ps) + (r // th // ph // ps) loc + pushSubstsWith th ph ps (DLam body loc) = + nclo $ DLam (body // th // ph // ps) loc + pushSubstsWith _ _ _ (NAT loc) = nclo $ NAT loc - pushSubstsWith _ _ (Nat n loc) = + pushSubstsWith _ _ _ (Nat n loc) = nclo $ Nat n loc - pushSubstsWith th ph (Succ n loc) = - nclo $ Succ (n // th // ph) loc - pushSubstsWith _ _ (STRING loc) = + pushSubstsWith th ph ps (Succ n loc) = + nclo $ Succ (n // th // ph // ps) loc + pushSubstsWith _ _ _ (STRING loc) = nclo $ STRING loc - pushSubstsWith _ _ (Str s loc) = + pushSubstsWith _ _ _ (Str s loc) = nclo $ Str s loc - pushSubstsWith th ph (BOX pi ty loc) = - nclo $ BOX pi (ty // th // ph) loc - pushSubstsWith th ph (Box val loc) = - nclo $ Box (val // th // ph) loc - pushSubstsWith th ph (E e) = - let Element e nc = pushSubstsWith th ph e in nclo $ E e - pushSubstsWith th ph (Let qty rhs body loc) = - nclo $ Let qty (rhs // th // ph) (body // th // ph) loc - pushSubstsWith th ph (CloT (Sub s ps)) = - pushSubstsWith th (comp th ps ph) s - pushSubstsWith th ph (DCloT (Sub s ps)) = - pushSubstsWith (ps . th) ph s + pushSubstsWith th ph ps (BOX pi ty loc) = + nclo $ BOX (pi //? th) (ty // th // ph // ps) loc + pushSubstsWith th ph ps (Box val loc) = + nclo $ Box (val // th // ph // ps) loc + pushSubstsWith th ph ps (E e) = + let Element e nc = pushSubstsWith th ph ps e in nclo $ E e + pushSubstsWith th ph ps (Let qty rhs body loc) = + nclo $ Let (qty //? th) + (rhs // th // ph // ps) + (body // th // ph // ps) loc + pushSubstsWith th ph ps (CloT (Sub s ps')) = + pushSubstsWith th ph (comp th ph ps' ps) s + pushSubstsWith th ph ps (DCloT (Sub s ph')) = + pushSubstsWith th (ph' . ph) ps s + pushSubstsWith th ph ps (QCloT (SubR s th')) = + pushSubstsWith (th' .? th) ph ps s diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 0709684..2244666 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -29,20 +29,20 @@ tightenDScope f p (S names (N body)) = S names . N <$> f p body mutual private - tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1) + tightenT : {q : Nat} -> OPE n1 n2 -> Term q d n2 -> Maybe (Term q d n1) tightenT p s = let Element s' _ = pushSubsts s in tightenT' p $ assert_smaller s s' private - tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1) + tightenE : {q : Nat} -> OPE n1 n2 -> Elim q d n2 -> Maybe (Elim q d n1) tightenE p e = let Element e' _ = pushSubsts e in tightenE' p $ assert_smaller e e' private - tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) => - Maybe (Term d n1) + tightenT' : {q : Nat} -> OPE n1 n2 -> (t : Term q d n2) -> (0 nt : NotClo t) => + Maybe (Term q d n1) tightenT' p (TYPE l loc) = pure $ TYPE l loc tightenT' p (IOState loc) = pure $ IOState loc tightenT' p (Pi qty arg res loc) = @@ -81,8 +81,9 @@ mutual E <$> assert_total tightenE p e private - tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) => - Maybe (Elim d n1) + tightenE' : {q : Nat} -> + OPE n1 n2 -> (e : Elim q d n2) -> (0 ne : NotClo e) => + Maybe (Elim q d n1) tightenE' p (F x u loc) = pure $ F x u loc tightenE' p (B i loc) = @@ -140,34 +141,35 @@ mutual <*> pure loc export - tightenS : {s : Nat} -> OPE m n -> - ScopeTermN s f n -> Maybe (ScopeTermN s f m) + tightenS : {q, s : Nat} -> OPE m n -> + ScopeTermN s q d n -> Maybe (ScopeTermN s q d m) tightenS = assert_total $ tightenScope tightenT export - tightenDS : OPE m n -> DScopeTermN s f n -> Maybe (DScopeTermN s f m) - tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term d n} + tightenDS : {q : Nat} -> + OPE m n -> DScopeTermN s q d n -> Maybe (DScopeTermN s q d m) + tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term q d n} -export Tighten (Elim d) where tighten p e = tightenE p e -export Tighten (Term d) where tighten p t = tightenT p t +export {q : Nat} -> Tighten (Elim q d) where tighten p e = tightenE p e +export {q : Nat} -> Tighten (Term q d) where tighten p t = tightenT p t mutual export - dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n) + dtightenT : {q : Nat} -> OPE d1 d2 -> Term q d2 n -> Maybe (Term q d1 n) dtightenT p s = let Element s' _ = pushSubsts s in dtightenT' p $ assert_smaller s s' export - dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n) + dtightenE : {q : Nat} -> OPE d1 d2 -> Elim q d2 n -> Maybe (Elim q d1 n) dtightenE p e = let Element e' _ = pushSubsts e in dtightenE' p $ assert_smaller e e' private - dtightenT' : OPE d1 d2 -> (t : Term d2 n) -> (0 nt : NotClo t) => - Maybe (Term d1 n) + dtightenT' : {q : Nat} -> OPE d1 d2 -> (t : Term q d2 n) -> (0 nt : NotClo t) => + Maybe (Term q d1 n) dtightenT' p (TYPE l loc) = pure $ TYPE l loc dtightenT' p (IOState loc) = @@ -208,8 +210,8 @@ mutual E <$> assert_total dtightenE p e export - dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) => - Maybe (Elim d1 n) + dtightenE' : {q : Nat} -> OPE d1 d2 -> (e : Elim q d2 n) -> (0 ne : NotClo e) => + Maybe (Elim q d1 n) dtightenE' p (F x u loc) = pure $ F x u loc dtightenE' p (B i loc) = @@ -258,17 +260,18 @@ mutual (traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|] export - dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n) - dtightenS = assert_total $ tightenDScope dtightenT {f = Term} + dtightenS : {q : Nat} -> OPE d1 d2 -> ScopeTermN s q d2 n -> + Maybe (ScopeTermN s q d1 n) + dtightenS = assert_total $ tightenDScope dtightenT {f = Term q} export - dtightenDS : {s : Nat} -> OPE d1 d2 -> - DScopeTermN s d2 n -> Maybe (DScopeTermN s d1 n) + dtightenDS : {q, s : Nat} -> OPE d1 d2 -> + DScopeTermN s q d2 n -> Maybe (DScopeTermN s q d1 n) dtightenDS = assert_total $ tightenScope dtightenT -export Tighten (\d => Term d n) where tighten p t = dtightenT p t -export Tighten (\d => Elim d n) where tighten p e = dtightenE p e +export {q : Nat} -> Tighten (\d => Term q d n) where tighten p t = dtightenT p t +export {q : Nat} -> Tighten (\d => Elim q d n) where tighten p e = dtightenE p e parameters {auto _ : Tighten f} {s : Nat} @@ -300,59 +303,64 @@ ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n ST names body = squeeze' $ SY names body public export %inline -DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n -DST names body = dsqueeze' {f = Term} $ SY names body +DST : {s, q : Nat} -> BContext s -> Term q (s + d) n -> DScopeTermN s q d n +DST names body = dsqueeze' {f = Term q} $ SY names body public export %inline -PiT : (qty : Qty) -> (x : BindName) -> - (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n +PiT : {q : Nat} -> (qty : Qty q) -> (x : BindName) -> + (arg : Term q d n) -> (res : Term q d (S n)) -> (loc : Loc) -> Term q d n PiT {qty, x, arg, res, loc} = Pi {qty, arg, res = ST [< x] res, loc} public export %inline -LamT : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n +LamT : {q : Nat} -> + (x : BindName) -> (body : Term q d (S n)) -> (loc : Loc) -> Term q d n LamT {x, body, loc} = Lam {body = ST [< x] body, loc} public export %inline -SigT : (x : BindName) -> (fst : Term d n) -> - (snd : Term d (S n)) -> (loc : Loc) -> Term d n +SigT : {q : Nat} -> (x : BindName) -> (fst : Term q d n) -> + (snd : Term q d (S n)) -> (loc : Loc) -> Term q d n SigT {x, fst, snd, loc} = Sig {fst, snd = ST [< x] snd, loc} public export %inline -EqT : (i : BindName) -> (ty : Term (S d) n) -> - (l, r : Term d n) -> (loc : Loc) -> Term d n +EqT : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) -> + (l, r : Term q d n) -> (loc : Loc) -> Term q d n EqT {i, ty, l, r, loc} = Eq {ty = DST [< i] ty, l, r, loc} public export %inline -DLamT : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n +DLamT : {q : Nat} -> + (i : BindName) -> (body : Term q (S d) n) -> (loc : Loc) -> Term q d n DLamT {i, body, loc} = DLam {body = DST [< i] body, loc} public export %inline -CoeT : (i : BindName) -> (ty : Term (S d) n) -> - (p, q : Dim d) -> (val : Term d n) -> (loc : Loc) -> Elim d n -CoeT {i, ty, p, q, val, loc} = Coe {ty = DST [< i] ty, p, q, val, loc} +CoeT : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) -> + (p, p' : Dim d) -> (val : Term q d n) -> (loc : Loc) -> Elim q d n +CoeT {i, ty, p, p', val, loc} = Coe {ty = DST [< i] ty, p, p', val, loc} public export %inline -typeCase1T : Elim d n -> Term d n -> - (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) -> +typeCase1T : {q : Nat} -> + Elim q d n -> Term q d n -> + (k : TyConKind) -> BContext (arity k) -> Term q d (arity k + n) -> (loc : Loc) -> - {default (NAT loc) def : Term d n} -> - Elim d n + {default (NAT loc) def : Term q d n} -> + Elim q d n typeCase1T ty ret k ns body loc {def} = typeCase ty ret [(k ** ST ns body)] def loc public export %inline -CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n -CompH' {ty, p, q, val, r, zero, one, loc} = +CompH' : {q : Nat} -> + (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> + (r : Dim d) -> (zero, one : DScopeTerm q d n) -> (loc : Loc) -> + Elim q d n +CompH' {ty, p, p', val, r, zero, one, loc} = let ty' = DST ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in Comp { - ty = dsub1 ty q, p, q, - val = E $ Coe ty p q val val.loc, r, + ty = dsub1 ty p', p, p', + val = E $ Coe ty p p' val val.loc, r, zero = DST zero.names $ E $ - Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc, + Coe ty' (B VZ zero.loc) (weakD 1 p') zero.term zero.loc, one = DST one.names $ E $ - Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc, + Coe ty' (B VZ one.loc) (weakD 1 p') one.term one.loc, loc } @@ -365,12 +373,12 @@ CompH' {ty, p, q, val, r, zero, one, loc} = ||| 1 j โ‡’ coe [i โ‡’ A] @j @q tโ‚ ||| } public export %inline -CompH : (i : BindName) -> (ty : Term (S d) n) -> - (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> - (j0 : BindName) -> (zero : Term (S d) n) -> - (j1 : BindName) -> (one : Term (S d) n) -> +CompH : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) -> + (p, p' : Dim d) -> (val : Term q d n) -> (r : Dim d) -> + (j0 : BindName) -> (zero : Term q (S d) n) -> + (j1 : BindName) -> (one : Term q (S d) n) -> (loc : Loc) -> - Elim d n -CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} = - CompH' {ty = DST [< i] ty, p, q, val, r, + Elim q d n +CompH {i, ty, p, p', val, r, j0, zero, j1, one, loc} = + CompH' {ty = DST [< i] ty, p, p', val, r, zero = DST [< j0] zero, one = DST [< j1] one, loc} diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 2ebed73..8885245 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -21,22 +21,22 @@ TTName = TT.Name public export -CheckResult' : Nat -> Type +CheckResult' : Nat -> Nat -> Type CheckResult' = QOutput public export -CheckResult : DimEq d -> Nat -> Type -CheckResult eqs n = IfConsistent eqs $ CheckResult' n +CheckResult : DimEq d -> Nat -> Nat -> Type +CheckResult eqs q n = IfConsistent eqs $ CheckResult' q n public export -record InferResult' d n where +record InferResult' q d n where constructor InfRes - type : Term d n - qout : QOutput n + type : Term q d n + qout : QOutput q n public export InferResult : DimEq d -> TermLike -InferResult eqs d n = IfConsistent eqs $ InferResult' d n +InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n export @@ -45,21 +45,22 @@ lookupFree x loc defs = maybe (throw $ NotInScope loc x) pure $ lookup x defs public export -substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n) +substCasePairRet : BContext 2 -> Term q d n -> ScopeTerm q d n -> + Term q d (2 + n) substCasePairRet [< x, y] dty retty = let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc arg = Ann tm (dty // fromNat 2) tm.loc in retty.term // (arg ::: shift 2) public export -substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n) +substCaseSuccRet : BContext 2 -> ScopeTerm q d n -> Term q d (2 + n) substCaseSuccRet [< p, ih] retty = let loc = p.loc `extendL` ih.loc arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) loc in retty.term // (arg ::: shift 2) public export -substCaseBoxRet : BindName -> Term d n -> ScopeTerm d n -> Term d (S n) +substCaseBoxRet : BindName -> Term q d n -> ScopeTerm q d n -> Term q d (S n) substCaseBoxRet x dty retty = let arg = Ann (Box (BVT 0 x.loc) x.loc) (weakT 1 dty) x.loc in retty.term // (arg ::: shift 1) @@ -68,15 +69,15 @@ substCaseBoxRet x dty retty = private 0 ExpectErrorConstructor : Type ExpectErrorConstructor = - forall d, n. Loc -> NameContexts d n -> Term d n -> Error + forall q, d, n. Loc -> NameContexts q d n -> Term q d n -> Error parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs, Has Log fs)} namespace TyContext - parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc) + parameters (ctx : TyContext q d n) (sg : SQty) (loc : Loc) export covering whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => - tm d n -> Eff fs (NonRedex tm d n defs (toWhnfContext ctx) sg) + tm q d n -> Eff fs (NonRedex tm q d n defs (toWhnfContext ctx) sg) whnf tm = do let Val n = ctx.termLen; Val d = ctx.dimLen res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm @@ -84,7 +85,7 @@ parameters (defs : Definitions) private covering %macro expect : ExpectErrorConstructor -> TTImp -> TTImp -> - Elab (Term d n -> Eff fs a) + Elab (Term q d n -> Eff fs a) expect err pat rhs = Prelude.do match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) pure $ \term => do @@ -92,54 +93,54 @@ parameters (defs : Definitions) maybe (throw $ err loc ctx.names term) pure $ match $ fst res export covering %inline - expectTYPE : Term d n -> Eff fs Universe + expectTYPE : Term q d n -> Eff fs Universe expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l) export covering %inline - expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n) + expectPi : Term q d n -> Eff fs (Qty q, Term q d n, ScopeTerm q d n) expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res)) export covering %inline - expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n) + expectSig : Term q d n -> Eff fs (Term q d n, ScopeTerm q d n) expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd)) export covering %inline - expectEnum : Term d n -> Eff fs (SortedSet TagVal) + expectEnum : Term q d n -> Eff fs (SortedSet TagVal) expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases) export covering %inline - expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n) + expectEq : Term q d n -> Eff fs (DScopeTerm q d n, Term q d n, Term q d n) expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r)) export covering %inline - expectNAT : Term d n -> Eff fs () + expectNAT : Term q d n -> Eff fs () expectNAT = expect ExpectedNAT `(NAT {}) `(()) export covering %inline - expectSTRING : Term d n -> Eff fs () + expectSTRING : Term q d n -> Eff fs () expectSTRING = expect ExpectedSTRING `(STRING {}) `(()) export covering %inline - expectBOX : Term d n -> Eff fs (Qty, Term d n) + expectBOX : Term q d n -> Eff fs (Qty q, Term q d n) expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty)) export covering %inline - expectIOState : Term d n -> Eff fs () + expectIOState : Term q d n -> Eff fs () expectIOState = expect ExpectedIOState `(IOState {}) `(()) namespace EqContext - parameters (ctx : EqContext n) (sg : SQty) (loc : Loc) + parameters (ctx : EqContext q n) (sg : SQty) (loc : Loc) export covering whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => - tm 0 n -> Eff fs (NonRedex tm 0 n defs (toWhnfContext ctx) sg) + tm q 0 n -> Eff fs (NonRedex tm q 0 n defs (toWhnfContext ctx) sg) whnf tm = do res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm rethrow res private covering %macro expect : ExpectErrorConstructor -> TTImp -> TTImp -> - Elab (Term 0 n -> Eff fs a) + Elab (Term q 0 n -> Eff fs a) expect err pat rhs = do match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) pure $ \term => do @@ -148,37 +149,37 @@ parameters (defs : Definitions) maybe (throw $ err loc ctx.names t0) pure $ match $ fst res export covering %inline - expectTYPE : Term 0 n -> Eff fs Universe + expectTYPE : Term q 0 n -> Eff fs Universe expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l) export covering %inline - expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n) + expectPi : Term q 0 n -> Eff fs (Qty q, Term q 0 n, ScopeTerm q 0 n) expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res)) export covering %inline - expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n) + expectSig : Term q 0 n -> Eff fs (Term q 0 n, ScopeTerm q 0 n) expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd)) export covering %inline - expectEnum : Term 0 n -> Eff fs (SortedSet TagVal) + expectEnum : Term q 0 n -> Eff fs (SortedSet TagVal) expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases) export covering %inline - expectEq : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n) + expectEq : Term q 0 n -> Eff fs (DScopeTerm q 0 n, Term q 0 n, Term q 0 n) expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r)) export covering %inline - expectNAT : Term 0 n -> Eff fs () + expectNAT : Term q 0 n -> Eff fs () expectNAT = expect ExpectedNAT `(NAT {}) `(()) export covering %inline - expectSTRING : Term 0 n -> Eff fs () + expectSTRING : Term q 0 n -> Eff fs () expectSTRING = expect ExpectedSTRING `(STRING {}) `(()) export covering %inline - expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n) + expectBOX : Term q 0 n -> Eff fs (Qty q, Term q 0 n) expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty)) export covering %inline - expectIOState : Term 0 n -> Eff fs () + expectIOState : Term q 0 n -> Eff fs () expectIOState = expect ExpectedIOState `(IOState {}) `(()) diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index d231694..11c51c6 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -3,7 +3,7 @@ module Quox.Typing.Context import Quox.Syntax import Quox.Context import Quox.Pretty -import public Data.Singleton +import public Quox.SingletonExtra import Derive.Prelude %default total @@ -11,48 +11,60 @@ import Derive.Prelude public export -QContext : Nat -> Type -QContext = Context' Qty +QContext : (q, n : Nat) -> Type +QContext q n = Context' (Qty q) n public export -record LocalVar d n where +record LocalVar q d n where constructor MkLocal - type : Term d n - term : Maybe (Term d n) -- if from a `let` -%runElab deriveIndexed "LocalVar" [Show] + type : Term q d n + term : Maybe (Term q d n) -- if from a `let` +-- %runElab deriveIndexed "LocalVar" [Show] + +export +[LocateVarType] Located (LocalVar q d n) where x.loc = x.type.loc namespace LocalVar export %inline - letVar : (type, term : Term d n) -> LocalVar d n + letVar : (type, term : Term q d n) -> LocalVar q d n letVar type term = MkLocal {type, term = Just term} export %inline - lamVar : (type : Term d n) -> LocalVar d n + lamVar : (type : Term q d n) -> LocalVar q d n lamVar type = MkLocal {type, term = Nothing} export %inline - mapVar : (Term d n -> Term d' n') -> LocalVar d n -> LocalVar d' n' + mapVar : (Term q d n -> Term q' d' n') -> LocalVar q d n -> LocalVar q' d' n' mapVar f = {type $= f, term $= map f} export %inline - subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n + subQ : {q1, q2 : Nat} -> QSubst q1 q2 -> LocalVar q1 d n -> LocalVar q2 d n + subQ th = mapVar (// th) + + export %inline + weakQ : {q : Nat} -> LocalVar q d n -> LocalVar (S q) d n + weakQ = subQ $ shift 1 + + export %inline + subD : DSubst d1 d2 -> LocalVar q d1 n -> LocalVar q d2 n subD th = mapVar (// th) export %inline - weakD : LocalVar d n -> LocalVar (S d) n + weakD : LocalVar q d n -> LocalVar q (S d) n weakD = subD $ shift 1 -export %inline CanShift (LocalVar d) where l // by = mapVar (// by) l -export %inline CanDSubst LocalVar where l // by = mapVar (// by) l -export %inline CanTSubst LocalVar where l // by = mapVar (// by) l +export %inline CanShift (LocalVar q d) where l // by = mapVar (// by) l +export %inline CanQSubst LocalVar where l // th = mapVar (// th) l +export %inline CanDSubst LocalVar where l // th = mapVar (// th) l +export %inline CanTSubst LocalVar where l // th = mapVar (// th) l public export TContext : TermLike -TContext d = Context (LocalVar d) +TContext q d = Context (LocalVar q d) public export -QOutput : Nat -> Type -QOutput = Context' Qty +QOutput : (q, n : Nat) -> Type +QOutput = QContext public export DimAssign : Nat -> Type @@ -60,48 +72,54 @@ DimAssign = Context' DimConst public export -record TyContext d n where +record TyContext q d n where constructor MkTyContext + {auto qtyLen : Singleton q} {auto dimLen : Singleton d} {auto termLen : Singleton n} + qnames : BContext q -- only used for printing dctx : DimEq d dnames : BContext d -- only used for printing - tctx : TContext d n + tctx : TContext q d n tnames : BContext n -- only used for printing - qtys : QContext n -- only used for printing + qtys : QContext q n -- only used for printing %name TyContext ctx -%runElab deriveIndexed "TyContext" [Show] +-- %runElab deriveIndexed "TyContext" [Show] public export -record EqContext n where +record EqContext q n where constructor MkEqContext + {auto qtyLen : Singleton q} {dimLen : Nat} {auto termLen : Singleton n} + qnames : BContext q -- only used for printing dassign : DimAssign dimLen -- only used for printing dnames : BContext dimLen -- only used for printing - tctx : TContext 0 n + tctx : TContext q 0 n tnames : BContext n -- only used for printing - qtys : QContext n -- only used for printing + qtys : QContext q n -- only used for printing %name EqContext ctx -%runElab deriveIndexed "EqContext" [Show] +-- %runElab deriveIndexed "EqContext" [Show] public export -record WhnfContext d n where +record WhnfContext q d n where constructor MkWhnfContext + {auto qtyLen : Singleton q} {auto dimLen : Singleton d} {auto termLen : Singleton n} + qnames : BContext q -- only used for printing dnames : BContext d tnames : BContext n - tctx : TContext d n + tctx : TContext q d n %name WhnfContext ctx -%runElab deriveIndexed "WhnfContext" [Show] +-- %runElab deriveIndexed "WhnfContext" [Show] namespace TContext export %inline - zeroFor : Context tm n -> QOutput n - zeroFor ctx = Zero <$ ctx + zeroFor : {q : Nat} -> Located1 tm => Context tm n -> QOutput q n + zeroFor = map $ \x => zero x.loc public export extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2 @@ -110,38 +128,40 @@ extendLen (tel :< _) x = [|S $ extendLen tel x|] public export -CtxExtension : Nat -> Nat -> Nat -> Type -CtxExtension d = Telescope ((Qty, BindName,) . Term d) +CtxExtension : (q, d, n1, n2 : Nat) -> Type +CtxExtension q d = Telescope $ \n => (Qty q, BindName, Term q d n) public export -CtxExtension0 : Nat -> Nat -> Nat -> Type -CtxExtension0 d = Telescope ((BindName,) . Term d) +CtxExtension0 : (q, d, n1, n2 : Nat) -> Type +CtxExtension0 q d = Telescope $ \n => (BindName, Term q d n) public export -CtxExtensionLet : Nat -> Nat -> Nat -> Type -CtxExtensionLet d = Telescope ((Qty, BindName,) . LocalVar d) +CtxExtensionLet : (q, d, n1, n2 : Nat) -> Type +CtxExtensionLet q d = Telescope $ \n => (Qty q, BindName, LocalVar q d n) public export -CtxExtensionLet0 : Nat -> Nat -> Nat -> Type -CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d) +CtxExtensionLet0 : (q, d, n1, n2 : Nat) -> Type +CtxExtensionLet0 q d = Telescope $ \n => (BindName, LocalVar q d n) namespace TyContext public export %inline - empty : TyContext 0 0 + empty : TyContext 0 0 0 empty = MkTyContext { - dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<] + qnames = [<], dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<] } public export %inline - null : TyContext d n -> Bool - null ctx = null ctx.dnames && null ctx.tnames + null : TyContext q d n -> Bool + null ctx = null ctx.qnames && null ctx.dnames && null ctx.tnames export %inline - extendTyLetN : CtxExtensionLet d n1 n2 -> TyContext d n1 -> TyContext d n2 - extendTyLetN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) = + extendTyLetN : CtxExtensionLet q d n1 n2 -> + TyContext q d n1 -> TyContext q d n2 + extendTyLetN xss + (MkTyContext {termLen, qnames, dctx, dnames, tctx, tnames, qtys}) = let (qs, xs, ls) = unzip3 xss in MkTyContext { - dctx, dnames, + qnames, dctx, dnames, termLen = extendLen xss termLen, tctx = tctx . ls, tnames = tnames . xs, @@ -149,63 +169,78 @@ namespace TyContext } export %inline - extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2 + extendTyN : CtxExtension q d n1 n2 -> TyContext q d n1 -> TyContext q d n2 extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s)) export %inline - extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2 - extendTyLetN0 xss = extendTyLetN (map (Zero,) xss) + extendTyLetN0 : CtxExtensionLet0 q d n1 n2 -> + TyContext q d n1 -> TyContext q d n2 + extendTyLetN0 xss ctx = + let Val q = ctx.qtyLen in + extendTyLetN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx export %inline - extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2 - extendTyN0 xss = extendTyN (map (Zero,) xss) + extendTyN0 : CtxExtension0 q d n1 n2 -> + TyContext q d n1 -> TyContext q d n2 + extendTyN0 xss ctx = + let Val q = ctx.qtyLen in + extendTyN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx export %inline - extendTyLet : Qty -> BindName -> Term d n -> Term d n -> - TyContext d n -> TyContext d (S n) + extendTyLet : Qty q -> BindName -> Term q d n -> Term q d n -> + TyContext q d n -> TyContext q d (S n) extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)] export %inline - extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n) + extendTy : Qty q -> BindName -> Term q d n -> + TyContext q d n -> TyContext q d (S n) extendTy q x s = extendTyN [< (q, x, s)] export %inline - extendTy0 : BindName -> Term d n -> TyContext d n -> TyContext d (S n) - extendTy0 = extendTy Zero + extendTy0 : BindName -> Term q d n -> + TyContext q d n -> TyContext q d (S n) + extendTy0 x t ctx = let Val q = ctx.qtyLen in extendTy (zero x.loc) x t ctx export %inline - extendDim : BindName -> TyContext d n -> TyContext (S d) n - extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) = + extendDim : BindName -> TyContext q d n -> TyContext q (S d) n + extendDim x (MkTyContext {dimLen, dctx, dnames, qnames, tctx, tnames, qtys}) = MkTyContext { dctx = dctx : Dim d -> TyContext d n -> TyContext d n - eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id} + eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n + eqDim p q = {dctx $= set p q} export - toWhnfContext : TyContext d n -> WhnfContext d n - toWhnfContext (MkTyContext {dnames, tnames, tctx, _}) = - MkWhnfContext {dnames, tnames, tctx} + toWhnfContext : TyContext q d n -> WhnfContext q d n + toWhnfContext (MkTyContext {qnames, dnames, tnames, tctx, _}) = + MkWhnfContext {qnames, dnames, tnames, tctx} + + public export + (.names) : TyContext q d n -> NameContexts q d n + (MkTyContext {qnames, dnames, tnames, _}).names = + MkNameContexts {qnames, dnames, tnames} namespace QOutput export %inline - (+) : QOutput n -> QOutput n -> QOutput n + (+) : QOutput q n -> QOutput q n -> QOutput q n (+) = zipWith (+) export %inline - (*) : Qty -> QOutput n -> QOutput n + (*) : Qty q -> QOutput q n -> QOutput q n (*) pi = map (pi *) export %inline - zeroFor : TyContext _ n -> QOutput n - zeroFor ctx = zeroFor ctx.tctx + zeroFor : TyContext q _ n -> QOutput q n + zeroFor ctx = + let Val q = ctx.qtyLen in + zeroFor ctx.tctx @{LocateVarType} export @@ -214,8 +249,10 @@ makeDAssign (Shift SZ) = [<] makeDAssign (K e _ ::: th) = makeDAssign th :< e export -makeEqContext' : {d : Nat} -> TyContext d n -> DSubst d 0 -> EqContext n +makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n makeEqContext' ctx th = MkEqContext { + qtyLen = ctx.qtyLen, + qnames = ctx.qnames, termLen = ctx.termLen, dassign = makeDAssign th, dnames = ctx.dnames, @@ -225,134 +262,160 @@ makeEqContext' ctx th = MkEqContext { } export -makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n +makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n makeEqContext ctx@(MkTyContext {dnames, _}) th = let Val d = lengthPrf0 dnames in makeEqContext' ctx th namespace EqContext public export %inline - empty : EqContext 0 + empty : EqContext 0 0 empty = MkEqContext { - dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<] + qnames = [<], dassign = [<], dnames = [<], + tctx = [<], tnames = [<], qtys = [<] } public export %inline - null : EqContext n -> Bool - null ctx = null ctx.dnames && null ctx.tnames + null : EqContext q n -> Bool + null ctx = null ctx.qnames && null ctx.dnames && null ctx.tnames export %inline - extendTyLetN : CtxExtensionLet 0 n1 n2 -> EqContext n1 -> EqContext n2 - extendTyLetN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) = + extendTyLetN : CtxExtensionLet q 0 n1 n2 -> EqContext q n1 -> EqContext q n2 + extendTyLetN xss + (MkEqContext {termLen, qnames, dassign, dnames, tctx, tnames, qtys}) = let (qs, xs, ls) = unzip3 xss in MkEqContext { termLen = extendLen xss termLen, tctx = tctx . ls, tnames = tnames . xs, qtys = qtys . qs, - dassign, dnames + dassign, dnames, qnames } export %inline - extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2 + extendTyN : CtxExtension q 0 n1 n2 -> EqContext q n1 -> EqContext q n2 extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s)) export %inline - extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2 - extendTyLetN0 xss = extendTyLetN (map (Zero,) xss) + extendTyLetN0 : CtxExtensionLet0 q 0 n1 n2 -> EqContext q n1 -> EqContext q n2 + extendTyLetN0 xss ctx = + let Val q = ctx.qtyLen in + extendTyLetN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx export %inline - extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2 - extendTyN0 xss = extendTyN (map (Zero,) xss) + extendTyN0 : CtxExtension0 q 0 n1 n2 -> EqContext q n1 -> EqContext q n2 + extendTyN0 xss ctx = + let Val q = ctx.qtyLen in + extendTyN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx export %inline - extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n -> - EqContext n -> EqContext (S n) + extendTyLet : Qty q -> BindName -> Term q 0 n -> Term q 0 n -> + EqContext q n -> EqContext q (S n) extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)] export %inline - extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n) + extendTy : Qty q -> BindName -> Term q 0 n -> + EqContext q n -> EqContext q (S n) extendTy q x s = extendTyN [< (q, x, s)] export %inline - extendTy0 : BindName -> Term 0 n -> EqContext n -> EqContext (S n) - extendTy0 = extendTy Zero + extendTy0 : BindName -> Term q 0 n -> EqContext q n -> EqContext q (S n) + extendTy0 x t ctx = let Val q = ctx.qtyLen in extendTy (zero x.loc) x t ctx export %inline - extendDim : BindName -> DimConst -> EqContext n -> EqContext n - extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) = + extendDim : BindName -> DimConst -> EqContext q n -> EqContext q n + extendDim x e (MkEqContext {dassign, dnames, qnames, tctx, tnames, qtys}) = MkEqContext {dassign = dassign :< e, dnames = dnames :< x, - tctx, tnames, qtys} + qnames, tctx, tnames, qtys} export - toTyContext : (e : EqContext n) -> TyContext e.dimLen n - toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) = + toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n + toTyContext + (MkEqContext {dimLen, dassign, dnames, qnames, tctx, tnames, qtys}) = MkTyContext { dctx = fromGround dnames dassign, tctx = map (subD $ shift0 dimLen) tctx, - dnames, tnames, qtys + dnames, qnames, tnames, qtys } export - toWhnfContext : (ectx : EqContext n) -> WhnfContext 0 n - toWhnfContext (MkEqContext {tnames, tctx, _}) = - MkWhnfContext {dnames = [<], tnames, tctx} + toWhnfContext : (ectx : EqContext q n) -> WhnfContext q 0 n + toWhnfContext (MkEqContext {qnames, tnames, tctx, _}) = + MkWhnfContext {dnames = [<], qnames, tnames, tctx} export - injElim : WhnfContext d n -> Elim 0 0 -> Elim d n + injElim : WhnfContext q d n -> Elim q 0 0 -> Elim q d n injElim ctx e = let Val d = ctx.dimLen; Val n = ctx.termLen in e // shift0 d // shift0 n + public export + (.names) : (e : EqContext q n) -> NameContexts q e.dimLen n + (MkEqContext {qnames, dnames, tnames, _}).names = + MkNameContexts {qnames, dnames, tnames} + + public export + (.names0) : EqContext q n -> NameContexts q 0 n + (MkEqContext {qnames, tnames, _}).names0 = + MkNameContexts {qnames, dnames = [<], tnames} + namespace WhnfContext public export %inline - empty : WhnfContext 0 0 - empty = MkWhnfContext [<] [<] [<] + empty : WhnfContext 0 0 0 + empty = MkWhnfContext [<] [<] [<] [<] export - extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n) - extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) = + extendTy' : BindName -> LocalVar q d n -> + WhnfContext q d n -> WhnfContext q d (S n) + extendTy' x var (MkWhnfContext {termLen, qnames, dnames, tnames, tctx}) = MkWhnfContext { - dnames, + dnames, qnames, termLen = [|S termLen|], tnames = tnames :< x, tctx = tctx :< var } export %inline - extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n) + extendTy : BindName -> Term q d n -> + WhnfContext q d n -> WhnfContext q d (S n) extendTy x ty ctx = extendTy' x (lamVar ty) ctx export %inline - extendTyLet : BindName -> (type, term : Term d n) -> - WhnfContext d n -> WhnfContext d (S n) + extendTyLet : BindName -> (type, term : Term q d n) -> + WhnfContext q d n -> WhnfContext q d (S n) extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx export - extendDimN : {s : Nat} -> BContext s -> WhnfContext d n -> - WhnfContext (s + d) n - extendDimN ns (MkWhnfContext {dnames, tnames, tctx, dimLen}) = + extendDimN : {s : Nat} -> BContext s -> WhnfContext q d n -> + WhnfContext q (s + d) n + extendDimN ns (MkWhnfContext {qnames, dnames, tnames, tctx, dimLen}) = MkWhnfContext { dimLen = [|Val s + dimLen|], dnames = dnames ++ toSnocVect' ns, tctx = map (subD $ shift s) tctx, - tnames + qnames, tnames } export - extendDim : BindName -> WhnfContext d n -> WhnfContext (S d) n + extendDim : BindName -> WhnfContext q d n -> WhnfContext q (S d) n extendDim i = extendDimN [< i] + public export + (.names) : WhnfContext q d n -> NameContexts q d n + (MkWhnfContext {qnames, dnames, tnames, _}).names = + MkNameContexts {qnames, dnames, tnames} + private prettyTContextElt : {opts : _} -> - BContext d -> BContext n -> - Doc opts -> BindName -> LocalVar d n -> + NameContexts q d n -> + Doc opts -> BindName -> LocalVar q d n -> Eff Pretty (Doc opts) -prettyTContextElt dnames tnames q x s = do +prettyTContextElt names q x s = do + let Val _ = lengthPrf0 names.qnames dot <- dotD x <- prettyTBind x; colon <- colonD - ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD - tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term + ty <- withPrec Outer $ prettyTerm names s.type; eq <- cstD + tm <- traverse (withPrec Outer . prettyTerm names) s.term d <- askAt INDENT let qx = hcat [q, dot, x] pure $ case tm of @@ -364,39 +427,37 @@ prettyTContextElt dnames tnames q x s = do private prettyTContext' : {opts : _} -> - BContext d -> Context' (Doc opts) n -> BContext n -> - TContext d n -> Eff Pretty (SnocList (Doc opts)) -prettyTContext' _ [<] [<] [<] = pure [<] -prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) = - [|prettyTContext' dnames qtys tnames tys :< - prettyTContextElt dnames tnames q x t|] + NameContexts q d n -> Context' (Doc opts) n -> + TContext q d n -> Eff Pretty (SnocList (Doc opts)) +prettyTContext' _ [<] [<] = pure [<] +prettyTContext' names (qtys :< q) (tys :< t) = + let names' = {tnames $= tail, termLen $= map pred} names in + [|prettyTContext' names' qtys tys :< + prettyTContextElt names' q (head names.tnames) t|] export prettyTContext : {opts : _} -> - BContext d -> QContext n -> BContext n -> - TContext d n -> Eff Pretty (Doc opts) -prettyTContext dnames qtys tnames tys = do - comma <- commaD - qtys <- traverse prettyQty qtys - sepSingle . exceptLast (<+> comma) . toList <$> - prettyTContext' dnames qtys tnames tys + NameContexts q d n -> QContext q n -> + TContext q d n -> Eff Pretty (Doc opts) +prettyTContext names qtys tys = do + qtys <- traverse (prettyQty names.qnames) qtys + sepSingleTight !commaD . toList <$> prettyTContext' names qtys tys export -prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts) -prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) = - case dctx of - C [<] => prettyTContext dnames qtys tnames tctx - _ => pure $ - sepSingle [!(prettyDimEq dnames dctx) <++> !pipeD, - !(prettyTContext dnames qtys tnames tctx)] +prettyTyContext : {opts : _} -> TyContext q d n -> Eff Pretty (Doc opts) +prettyTyContext ctx = case ctx.dctx of + C [<] => prettyTContext ctx.names ctx.qtys ctx.tctx + _ => pure $ + sepSingle [!(prettyDimEq ctx.dnames ctx.dctx) <++> !pipeD, + !(prettyTContext ctx.names ctx.qtys ctx.tctx)] export -prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts) +prettyEqContext : {opts : _} -> EqContext q n -> Eff Pretty (Doc opts) prettyEqContext ctx = prettyTyContext $ toTyContext ctx export -prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts) +prettyWhnfContext : {opts : _} -> WhnfContext q d n -> Eff Pretty (Doc opts) prettyWhnfContext ctx = let Val n = ctx.termLen in - sepSingle . exceptLast (<+> comma) . toList <$> - prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx + sepSingleTight !commaD . toList <$> + prettyTContext' ctx.names (replicate n "_") ctx.tctx diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 502757c..b34b041 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -17,108 +17,64 @@ import Derive.Prelude %default total -public export -record NameContexts d n where - constructor MkNameContexts - dnames : BContext d - tnames : BContext n -%runElab deriveIndexed "NameContexts" [Show] - -namespace NameContexts - export - empty : NameContexts 0 0 - empty = MkNameContexts [<] [<] - - export - extendDimN : BContext s -> NameContexts d n -> NameContexts (s + d) n - extendDimN xs = {dnames $= (++ toSnocVect' xs)} - - export - extendDim : BindName -> NameContexts d n -> NameContexts (S d) n - extendDim i = extendDimN [< i] - -namespace TyContext - public export - (.names) : TyContext d n -> NameContexts d n - (MkTyContext {dnames, tnames, _}).names = - MkNameContexts {dnames, tnames} - -namespace EqContext - public export - (.names) : (e : EqContext n) -> NameContexts e.dimLen n - (MkEqContext {dnames, tnames, _}).names = - MkNameContexts {dnames, tnames} - - public export - (.names0) : EqContext n -> NameContexts 0 n - (MkEqContext {tnames, _}).names0 = - MkNameContexts {dnames = [<], tnames} - -namespace WhnfContext - public export - (.names) : WhnfContext d n -> NameContexts d n - (MkWhnfContext {dnames, tnames, _}).names = - MkNameContexts {dnames, tnames} - - public export data Error -= ExpectedTYPE Loc (NameContexts d n) (Term d n) -| ExpectedPi Loc (NameContexts d n) (Term d n) -| ExpectedSig Loc (NameContexts d n) (Term d n) -| ExpectedEnum Loc (NameContexts d n) (Term d n) -| ExpectedEq Loc (NameContexts d n) (Term d n) -| ExpectedNAT Loc (NameContexts d n) (Term d n) -| ExpectedSTRING Loc (NameContexts d n) (Term d n) -| ExpectedBOX Loc (NameContexts d n) (Term d n) -| ExpectedIOState Loc (NameContexts d n) (Term d n) += ExpectedTYPE Loc (NameContexts q d n) (Term q d n) +| ExpectedPi Loc (NameContexts q d n) (Term q d n) +| ExpectedSig Loc (NameContexts q d n) (Term q d n) +| ExpectedEnum Loc (NameContexts q d n) (Term q d n) +| ExpectedEq Loc (NameContexts q d n) (Term q d n) +| ExpectedNAT Loc (NameContexts q d n) (Term q d n) +| ExpectedSTRING Loc (NameContexts q d n) (Term q d n) +| ExpectedBOX Loc (NameContexts q d n) (Term q d n) +| ExpectedIOState Loc (NameContexts q d n) (Term q d n) | BadUniverse Loc Universe Universe | TagNotIn Loc TagVal (SortedSet TagVal) | BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal) -| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n)) +| BadQtys Loc String (TyContext q d n) (List (QOutput q n, Term q d n)) -- first term arg of ClashT is the type -| ClashT Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n) -| ClashTy Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) -| ClashE Loc (EqContext n) EqMode (Elim 0 n) (Elim 0 n) +| ClashT Loc (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n) +| ClashTy Loc (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) +| ClashE Loc (EqContext q n) EqMode (Elim q 0 n) (Elim q 0 n) | ClashU Loc EqMode Universe Universe -| ClashQ Loc Qty Qty +| ClashQ Loc (BContext q) (Qty q) (Qty q) | NotInScope Loc Name -| NotType Loc (TyContext d n) (Term d n) -| WrongType Loc (EqContext n) (Term 0 n) (Term 0 n) +| NotType Loc (TyContext q d n) (Term q d n) +| WrongType Loc (EqContext q n) (Term q 0 n) (Term q 0 n) | WrongBuiltinType Builtin Error -| ExpectedSingleEnum Loc (NameContexts d n) (Term d n) +| ExpectedSingleEnum Loc (NameContexts q d n) (Term q d n) | MissingEnumArm Loc TagVal (List TagVal) -- extra context | WhileChecking - (TyContext d n) SQty - (Term d n) -- term - (Term d n) -- type + (TyContext q d n) SQty + (Term q d n) -- term + (Term q d n) -- type Error | WhileCheckingTy - (TyContext d n) - (Term d n) + (TyContext q d n) + (Term q d n) (Maybe Universe) Error | WhileInferring - (TyContext d n) SQty - (Elim d n) + (TyContext q d n) SQty + (Elim q d n) Error | WhileComparingT - (EqContext n) EqMode SQty - (Term 0 n) -- type - (Term 0 n) (Term 0 n) -- lhs/rhs + (EqContext q n) EqMode SQty + (Term q 0 n) -- type + (Term q 0 n) (Term q 0 n) -- lhs/rhs Error | WhileComparingE - (EqContext n) EqMode SQty - (Elim 0 n) (Elim 0 n) + (EqContext q n) EqMode SQty + (Elim q 0 n) (Elim q 0 n) Error %name Error err -%runElab derive "Error" [Show] +-- %runElab derive "Error" [Show] public export ErrorEff : Type -> Type @@ -144,7 +100,7 @@ Located Error where (ClashTy loc _ _ _ _).loc = loc (ClashE loc _ _ _ _).loc = loc (ClashU loc _ _ _).loc = loc - (ClashQ loc _ _).loc = loc + (ClashQ loc _ _ _).loc = loc (NotInScope loc _).loc = loc (NotType loc _ _).loc = loc (WrongType loc _ _ _).loc = loc @@ -192,14 +148,15 @@ expect : Has (Except e) fs => (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> Eff fs () expect err cmp x y = unless (x `cmp` y) $ throw $ err x y -parameters {auto _ : Has ErrorEff fs} (loc : Loc) +parameters {auto _ : Has ErrorEff fs} (loc : Loc) (ctx : BContext q) export %inline - expectEqualQ : Qty -> Qty -> Eff fs () - expectEqualQ = expect (ClashQ loc) (==) + expectEqualQ : Qty q -> Qty q -> Eff fs () + expectEqualQ = expect (ClashQ loc ctx) (==) + -- [fixme] probably replace (==) export %inline - expectCompatQ : Qty -> Qty -> Eff fs () - expectCompatQ = expect (ClashQ loc) compat + expectCompatQ : Qty q -> Qty q -> Eff fs () + expectCompatQ = expect (ClashQ loc ctx) compat export %inline expectModeU : EqMode -> Universe -> Universe -> Eff fs () @@ -225,8 +182,8 @@ isTypeInUniverse (Just k) = "is a type in universe \{show k}" private -filterSameQtys : BContext n -> List (QOutput n, z) -> - Exists $ \n' => (BContext n', List (QOutput n', z)) +filterSameQtys : BContext n -> List (QOutput q n, z) -> + Exists $ \n' => (BContext n', List (QOutput q n', z)) filterSameQtys [<] qts = Evidence 0 ([<], qts) filterSameQtys (ns :< n) qts = let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts @@ -236,27 +193,29 @@ filterSameQtys (ns :< n) qts = then Evidence l (ns, qts) else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs) where - allSame : List Qty -> Bool + allSame : List (Qty q) -> Bool allSame [] = True allSame (q :: qs) = all (== q) qs private -printCaseQtys : {opts : _} -> TyContext d n -> - BContext n' -> List (QOutput n', Term d n) -> +printCaseQtys : {opts : _} -> TyContext q d n -> + BContext n' -> List (QOutput q n', Term q d n) -> Eff Pretty (List (Doc opts)) printCaseQtys ctx ns qts = let Evidence _ (ns, qts) = filterSameQtys ns qts in traverse (line ns) qts where - line : BContext l -> (QOutput l, Term d n) -> Eff Pretty (Doc opts) - line ns (qs, t) = map (("-" <++>) . sep) $ sequence + line : BContext l -> (QOutput q l, Term q d n) -> Eff Pretty (Doc opts) + line ns (qs, t) = + let Val q = ctx.qtyLen; names = ctx.names in + map (("-" <++>) . sep) $ sequence [hangDSingle "the term" - !(prettyTerm ctx.dnames ctx.tnames t), + !(prettyTerm names t), hangDSingle "uses variables" $ separateTight !commaD $ toSnocList' !(traverse prettyTBind ns), hangDSingle "with quantities" $ - separateTight !commaD $ toSnocList' !(traverse prettyQty qs)] + separateTight !commaD $ toSnocList' !(traverse (prettyQty names) qs)] parameters {opts : LayoutOpts} (showContext : Bool) export @@ -268,11 +227,11 @@ parameters {opts : LayoutOpts} (showContext : Bool) else pure doc export %inline - inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts) + inTContext : TyContext q d n -> Doc opts -> Eff Pretty (Doc opts) inTContext ctx = inContext' (null ctx) ctx prettyTyContext export %inline - inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts) + inEContext : EqContext q n -> Doc opts -> Eff Pretty (Doc opts) inEContext ctx = inContext' (null ctx) ctx prettyEqContext export @@ -280,43 +239,43 @@ parameters {opts : LayoutOpts} (showContext : Bool) prettyErrorNoLoc err0 = case err0 of ExpectedTYPE _ ctx s => hangDSingle "expected a type universe, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedPi _ ctx s => hangDSingle "expected a function type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedSig _ ctx s => hangDSingle "expected a pair type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedEnum _ ctx s => hangDSingle "expected an enumeration type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedEq _ ctx s => hangDSingle "expected an equality type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedNAT _ ctx s => hangDSingle ("expected the type" <++> - !(prettyTerm [<] [<] $ NAT noLoc) <+> ", but got") - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx $ NAT noLoc) <+> ", but got") + !(prettyTerm ctx s) ExpectedSTRING _ ctx s => hangDSingle ("expected the type" <++> - !(prettyTerm [<] [<] $ STRING noLoc) <+> ", but got") - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx $ STRING noLoc) <+> ", but got") + !(prettyTerm ctx s) ExpectedBOX _ ctx s => hangDSingle "expected a box type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) ExpectedIOState _ ctx s => hangDSingle "expected IOState, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) BadUniverse _ k l => pure $ sep ["the universe level" <++> !(prettyUniverse k), @@ -324,57 +283,58 @@ parameters {opts : LayoutOpts} (showContext : Bool) TagNotIn _ tag set => hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"]) - !(prettyTerm [<] [<] $ Enum set noLoc) + !(prettyTerm empty $ Enum set noLoc) BadCaseEnum _ head body => sep <$> sequence [hangDSingle "case expression has head of type" - !(prettyTerm [<] [<] $ Enum head noLoc), + !(prettyTerm empty $ Enum head noLoc), hangDSingle "but cases for" - !(prettyTerm [<] [<] $ Enum body noLoc)] + !(prettyTerm empty $ Enum body noLoc)] BadQtys _ what ctx arms => hangDSingle (text "inconsistent variable usage in \{what}") $ sep !(printCaseQtys ctx ctx.tnames arms) ClashT _ ctx mode ty s t => + let names = ctx.names0 in inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames t), - hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)] + [hangDSingle "the term" !(prettyTerm names s), + hangDSingle (text "is not \{prettyMode mode}") !(prettyTerm names t), + hangDSingle "at type" !(prettyTerm names ty)] ClashTy _ ctx mode a b => + let names = ctx.names0 in inEContext ctx . sep =<< sequence - [hangDSingle "the type" !(prettyTerm [<] ctx.tnames a), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames b)] + [hangDSingle "the type" !(prettyTerm names a), + hangDSingle (text "is not \{prettyMode mode}") !(prettyTerm names b)] ClashE _ ctx mode e f => + let names = ctx.names0 in inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyElim [<] ctx.tnames e), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyElim [<] ctx.tnames f)] + [hangDSingle "the term" !(prettyElim names e), + hangDSingle (text "is not \{prettyMode mode}") !(prettyElim names f)] ClashU _ mode k l => pure $ sep ["the universe level" <++> !(prettyUniverse k), text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)] - ClashQ _ pi rh => pure $ - sep ["the quantity" <++> !(prettyQty pi), - "is not equal to" <++> !(prettyQty rh)] + ClashQ _ ctx pi rh => pure $ + sep ["the quantity" <++> !(prettyQty ctx pi), + "is not equal to" <++> !(prettyQty ctx rh)] NotInScope _ x => pure $ hsep [!(prettyFree x), "is not in scope"] NotType _ ctx s => inTContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s), + [hangDSingle "the term" !(prettyTerm ctx.names s), pure "is not a type"] WrongType _ ctx ty s => + let names = ctx.names0 in inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), - hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)] + [hangDSingle "the term" !(prettyTerm names s), + hangDSingle "cannot have type" !(prettyTerm names ty)] WrongBuiltinType b err => pure $ vappend @@ -384,24 +344,25 @@ parameters {opts : LayoutOpts} (showContext : Bool) ExpectedSingleEnum _ ctx s => hangDSingle "expected an enumeration type with one case, but got" - !(prettyTerm ctx.dnames ctx.tnames s) + !(prettyTerm ctx s) MissingEnumArm _ tag tags => pure $ sep [hsep ["the tag", !(prettyTag tag), "is not contained in"], - !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)] + !(prettyTerm empty $ Enum (fromList tags) noLoc)] WhileChecking ctx sg s a err => + let names = ctx.names in [|vappendBlank (inTContext ctx . sep =<< sequence - [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s), - hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a), - hangDSingle "with quantity" !(prettyQty sg.qty)]) + [hangDSingle "while checking" !(prettyTerm names s), + hangDSingle "has type" !(prettyTerm names a), + hangDSingle "with quantity" !(prettyQConst sg.qconst)]) (prettyErrorNoLoc err)|] WhileCheckingTy ctx a k err => [|vappendBlank (inTContext ctx . sep =<< sequence - [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a), + [hangDSingle "while checking" !(prettyTerm ctx.names a), pure $ text $ isTypeInUniverse k]) (prettyErrorNoLoc err)|] @@ -409,27 +370,27 @@ parameters {opts : LayoutOpts} (showContext : Bool) [|vappendBlank (inTContext ctx . sep =<< sequence [hangDSingle "while inferring the type of" - !(prettyElim ctx.dnames ctx.tnames e), - hangDSingle "with quantity" !(prettyQty sg.qty)]) + !(prettyElim ctx.names e), + hangDSingle "with quantity" !(prettyQConst sg.qconst)]) (prettyErrorNoLoc err)|] WhileComparingT ctx mode sg a s t err => + let names = ctx.names0 in [|vappendBlank (inEContext ctx . sep =<< sequence - [hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s), - hangDSingle (text "is \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames t), - hangDSingle "at type" !(prettyTerm [<] ctx.tnames a), - hangDSingle "with quantity" !(prettyQty sg.qty)]) + [hangDSingle "while checking that" !(prettyTerm names s), + hangDSingle (text "is \{prettyMode mode}") !(prettyTerm names t), + hangDSingle "at type" !(prettyTerm names a), + hangDSingle "with quantity" !(prettyQConst sg.qconst)]) (prettyErrorNoLoc err)|] WhileComparingE ctx mode sg e f err => + let names = ctx.names0 in [|vappendBlank (inEContext ctx . sep =<< sequence - [hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e), - hangDSingle (text "is \{prettyMode mode}") - !(prettyElim [<] ctx.tnames f), - hangDSingle "with quantity" !(prettyQty sg.qty)]) + [hangDSingle "while checking that" !(prettyElim names e), + hangDSingle (text "is \{prettyMode mode}") !(prettyElim names f), + hangDSingle "with quantity" !(prettyQConst sg.qconst)]) (prettyErrorNoLoc err)|] where diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr index 91d94d2..1e3f532 100644 --- a/lib/Quox/Whnf/Coercion.idr +++ b/lib/Quox/Whnf/Coercion.idr @@ -9,140 +9,147 @@ import Quox.Whnf.TypeCase private -coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc -> - ScopeTermN s d n -> ScopeTermN s d n -coeScoped ty p q loc (S names (N body)) = - S names $ N $ E $ Coe ty p q body loc -coeScoped ty p q loc (S names (Y body)) = - ST names $ E $ Coe (weakDS s ty) p q body loc +coeScoped : {s, q : Nat} -> DScopeTerm q d n -> Dim d -> Dim d -> Loc -> + ScopeTermN s q d n -> ScopeTermN s q d n +coeScoped ty p p' loc (S names (N body)) = + S names $ N $ E $ Coe ty p p' body loc +coeScoped ty p p' loc (S names (Y body)) = + ST names $ E $ Coe (weakDS s ty) p p' body loc where - weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n) + weakDS : (by : Nat) -> DScopeTerm q d n -> DScopeTerm q d (by + n) weakDS by (S names (Y body)) = S names $ Y $ weakT by body weakDS by (S names (N body)) = S names $ N $ weakT by body parameters {auto _ : CanWhnf Term Interface.isRedexT} {auto _ : CanWhnf Elim Interface.isRedexE} - (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty) - ||| reduce a function application `App (Coe ty p q val) s loc` + (defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty) + ||| reduce a function application `App (Coe ty p p' val) s loc` export covering - piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> - (val, s : Term d n) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - piCoe sty@(S [< i] ty) p q val s loc = do - -- (coe [i โ‡’ ฯ€.(x : A) โ†’ B] @p @q t) s โ‡ - -- coe [i โ‡’ B[๐’”โ€นiโ€บ/x] @p @q ((t โˆท (ฯ€.(x : A) โ†’ B)โ€นp/iโ€บ) ๐’”โ€นpโ€บ) - -- where ๐’”โ€นjโ€บ โ‰” coe [i โ‡’ A] @q @j s + piCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> + (val, s : Term q d n) -> Loc -> + Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + piCoe sty@(S [< i] ty) p p' val s loc = do + -- (coe [i โ‡’ ฯ€.(x : A) โ†’ B] @p @p' t) s โ‡ + -- coe [i โ‡’ B[๐’”โ€นiโ€บ/x] @p @p' ((t โˆท (ฯ€.(x : A) โ†’ B)โ€นp/iโ€บ) ๐’”โ€นpโ€บ) + -- where ๐’”โ€นjโ€บ โ‰” coe [i โ‡’ A] @p' @j s -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDim i ctx Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty (arg, res) <- tycasePi defs ctx1 ty - let s0 = CoeT i arg q p s s.loc - body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc - s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc) - (s // shift 1) s.loc - whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc + let Val q = ctx.qtyLen + s0 = CoeT i arg p' p s s.loc + body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc + s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) + (weakD 1 p') (BV 0 i.loc) + (s // shift 1) s.loc + whnf defs ctx sg $ CoeT i (sub1 res s1) p p' body loc - ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc` + ||| reduce a pair elimination `CasePair pi (Coe ty p p' val) ret body loc` export covering - sigCoe : (qty : Qty) -> - (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - sigCoe qty sty@(S [< i] ty) p q val ret body loc = do - -- caseฯ€ (coe [i โ‡’ (x : A) ร— B] @p @q s) return z โ‡’ C of { (a, b) โ‡’ e } + sigCoe : (qty : Qty q) -> + (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> + (ret : ScopeTerm q d n) -> (body : ScopeTermN 2 q d n) -> Loc -> + Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + sigCoe qty sty@(S [< i] ty) p p' val ret body loc = do + -- caseฯ€ (coe [i โ‡’ (x : A) ร— B] @p @p' s) return z โ‡’ C of { (a, b) โ‡’ e } -- โ‡ -- caseฯ€ s โˆท ((x : A) ร— B)โ€นp/iโ€บ return z โ‡’ C -- of { (a, b) โ‡’ - -- e[(coe [i โ‡’ A] @p @q a)/a, - -- (coe [i โ‡’ B[(coe [j โ‡’ Aโ€นj/iโ€บ] @p @i a)/x]] @p @q b)/b] } + -- e[(coe [i โ‡’ A] @p @p' a)/a, + -- (coe [i โ‡’ B[(coe [j โ‡’ Aโ€นj/iโ€บ] @p @i a)/x]] @p @p' b)/b] } -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDim i ctx Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty (tfst, tsnd) <- tycaseSig defs ctx1 ty - let [< x, y] = body.names - a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc + let Val q = ctx.qtyLen + [< x, y] = body.names + a' = CoeT i (weakT 2 tfst) p p' (BVT 1 x.loc) x.loc tsnd' = tsnd.term // (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2)) (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2) - b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc + b' = CoeT i tsnd' p p' (BVT 0 y.loc) y.loc whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc - ||| reduce a pair projection `Fst (Coe ty p q val) loc` + ||| reduce a pair projection `Fst (Coe ty p p' val) loc` export covering - fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - fstCoe sty@(S [< i] ty) p q val loc = do - -- fst (coe (๐‘– โ‡’ (x : A) ร— B) @p @q s) + fstCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> + Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + fstCoe sty@(S [< i] ty) p p' val loc = do + -- fst (coe (๐‘– โ‡’ (x : A) ร— B) @p @p' s) -- โ‡ - -- coe (๐‘– โ‡’ A) @p @q (fst (s โˆท (x : Aโ€นp/๐‘–โ€บ) ร— Bโ€นp/๐‘–โ€บ)) + -- coe (๐‘– โ‡’ A) @p @p' (fst (s โˆท (x : Aโ€นp/๐‘–โ€บ) ร— Bโ€นp/๐‘–โ€บ)) -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDim i ctx Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty (tfst, _) <- tycaseSig defs ctx1 ty + let Val q = ctx.qtyLen whnf defs ctx sg $ - Coe (ST [< i] tfst) p q + Coe (ST [< i] tfst) p p' (E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc ||| reduce a pair projection `Snd (Coe ty p q val) loc` export covering - sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - sndCoe sty@(S [< i] ty) p q val loc = do - -- snd (coe (๐‘– โ‡’ (x : A) ร— B) @p @q s) + sndCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> + Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + sndCoe sty@(S [< i] ty) p p' val loc = do + -- snd (coe (๐‘– โ‡’ (x : A) ร— B) @p @p' s) -- โ‡ - -- coe (๐‘– โ‡’ B[coe (๐‘— โ‡’ Aโ€น๐‘—/๐‘–โ€บ) @p @๐‘– (fst (s โˆท (x : A) ร— B))/x]) @p @q + -- coe (๐‘– โ‡’ B[coe (๐‘— โ‡’ Aโ€น๐‘—/๐‘–โ€บ) @p @๐‘– (fst (s โˆท (x : A) ร— B))/x]) @p @p' -- (snd (s โˆท (x : Aโ€นp/๐‘–โ€บ) ร— Bโ€นp/๐‘–โ€บ)) -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDim i ctx Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty (tfst, tsnd) <- tycaseSig defs ctx1 ty + let Val q = ctx.qtyLen whnf defs ctx sg $ Coe (ST [< i] $ sub1 tsnd $ Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2)) (weakD 1 p) (BV 0 loc) (E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc) - p q + p p' (E (Snd (Ann val (ty // one p) val.loc) val.loc)) loc ||| reduce a dimension application `DApp (Coe ty p q val) r loc` export covering - eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> + eqCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> (r : Dim d) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - eqCoe sty@(S [< j] ty) p q val r loc = do - -- (coe [j โ‡’ Eq [i โ‡’ A] L R] @p @q eq) @r + Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + eqCoe sty@(S [< j] ty) p p' val r loc = do + -- (coe [j โ‡’ Eq [i โ‡’ A] L R] @p @p' eq) @r -- โ‡ - -- comp [j โ‡’ Aโ€นr/iโ€บ] @p @q ((eq โˆท (Eq [i โ‡’ A] L R)โ€นp/jโ€บ) @r) + -- comp [j โ‡’ Aโ€นr/iโ€บ] @p @p' ((eq โˆท (Eq [i โ‡’ A] L R)โ€นp/jโ€บ) @r) -- @r { 0 j โ‡’ L; 1 j โ‡’ R } let ctx1 = extendDim j ctx Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty - let a' = dsub1 a (weakD 1 r) - val' = E $ DApp (Ann val (ty // one p) val.loc) r loc - whnf defs ctx sg $ CompH j a' p q val' r j s j t loc + let Val q = ctx.qtyLen + a' = dsub1 a (weakD 1 r) + val' = E $ DApp (Ann val (ty // one p) val.loc) r loc + whnf defs ctx sg $ CompH j a' p p' val' r j s j t loc ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body` export covering - boxCoe : (qty : Qty) -> - (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg)) - boxCoe qty sty@(S [< i] ty) p q val ret body loc = do - -- caseฯ€ (coe [i โ‡’ [ฯ. A]] @p @q s) return z โ‡’ C of { [a] โ‡’ e } + boxCoe : (qty : Qty q) -> + (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) -> + (ret : ScopeTerm q d n) -> (body : ScopeTerm q d n) -> Loc -> + Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg)) + boxCoe qty sty@(S [< i] ty) p p' val ret body loc = do + -- caseฯ€ (coe [i โ‡’ [ฯ. A]] @p @p' s) return z โ‡’ C of { [a] โ‡’ e } -- โ‡ - -- caseฯ€ s โˆท [ฯ. A]โ€นp/iโ€บ return z โ‡’ C of { [a] โ‡’ e[(coe [i โ‡’ A] p q a)/a] } - let ctx1 = extendDim i ctx + -- caseฯ€ s โˆท [ฯ. A]โ€นp/iโ€บ return z โ‡’ C of { [a] โ‡’ e[(coe [i โ‡’ A] p p' a)/a] } + let ctx1 = extendDim i ctx + Val q = ctx.qtyLen Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty ta <- tycaseBOX defs ctx1 ty let xloc = body.name.loc - let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc + let a' = CoeT i (weakT 1 ta) p p' (BVT 0 xloc) xloc whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret (ST body.names $ body.term // (a' ::: shift 1)) loc @@ -150,14 +157,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- new params block to call the above functions at different `n` parameters {auto _ : CanWhnf Term Interface.isRedexT} {auto _ : CanWhnf Elim Interface.isRedexE} - (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty) + (defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty) ||| pushes a coercion inside a whnf-ed term export covering pushCoe : BindName -> - (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc -> - (0 pc : So (canPushCoe sg ty s)) => - Eff Whnf (NonRedex Elim d n defs ctx sg) - pushCoe i ty p q s loc = + (ty : Term q (S d) n) -> (p, p' : Dim d) -> (s : Term q d n) -> + Loc -> (0 pc : So (canPushCoe sg ty s)) => + Eff Whnf (NonRedex Elim q d n defs ctx sg) + pushCoe i ty p p' s loc = case ty of -- (coe โ˜…แตข @_ @_ s) โ‡ (s โˆท โ˜…แตข) TYPE l tyLoc => @@ -169,40 +176,40 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- ฮท expand, then simplify the Coe/App in the body -- - -- (coe (๐‘– โ‡’ ฯ€.(x : A) โ†’ B) @p @q s) + -- (coe (๐‘– โ‡’ ฯ€.(x : A) โ†’ B) @p @p' s) -- โ‡ - -- (ฮป y โ‡’ (coe (๐‘– โ‡’ ฯ€.(x : A) โ†’ B) @p @q s) y) โˆท (ฯ€.(x : A) โ†’ B)โ€นq/๐‘–โ€บ - -- โ‡ โ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พ - -- (ฮป y โ‡’ โ‹ฏ) โˆท (ฯ€.(x : A) โ†’ B)โ€นq/๐‘–โ€บ -- see `piCoe` + -- (ฮป y โ‡’ (coe (๐‘– โ‡’ ฯ€.(x : A) โ†’ B) @p @p' s) y) โˆท (ฯ€.(x : A) โ†’ B)โ€นp'/๐‘–โ€บ + -- โ‡ โ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พ + -- (ฮป y โ‡’ โ‹ฏ) โˆท (ฯ€.(x : A) โ†’ B)โ€นp'/๐‘–โ€บ -- see `piCoe` -- -- do the piCoe step here because otherwise equality checking keeps -- doing the ฮท forever Pi {arg, res = S [< x] _, _} => do let ctx' = extendTy x (arg // one p) ctx body <- piCoe defs ctx' sg - (weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc + (weakDS 1 $ SY [< i] ty) p p' (weakT 1 s) (BVT 0 loc) loc whnf defs ctx sg $ - Ann (LamY x (E body.fst) loc) (ty // one q) loc + Ann (LamY x (E body.fst) loc) (ty // one p') loc - -- no ฮท!!! -- push into a pair constructor, otherwise still stuck -- -- sฬƒโ€น๐‘˜โ€บ โ‰” coe (๐‘— โ‡’ Aโ€น๐‘—/๐‘–โ€บ) @p @๐‘˜ s -- ----------------------------------------------- - -- (coe (๐‘– โ‡’ (x : A) ร— B) @p @q (s, t)) + -- (coe (๐‘– โ‡’ (x : A) ร— B) @p @p' (s, t)) -- โ‡ - -- (sฬƒโ€นqโ€บ, coe (๐‘– โ‡’ B[sฬƒโ€น๐‘–โ€บ/x]) @p @q t) - -- โˆท ((x : A) ร— B)โ€นq/๐‘–โ€บ + -- (sฬƒโ€นp'โ€บ, coe (๐‘– โ‡’ B[sฬƒโ€น๐‘–โ€บ/x]) @p @p' t) + -- โˆท ((x : A) ร— B)โ€นp'/๐‘–โ€บ Sig tfst tsnd tyLoc => do - let Pair fst snd sLoc = s - fst' = CoeT i tfst p q fst fst.loc + let Val q = ctx.qtyLen + Pair fst snd sLoc = s + fst' = CoeT i tfst p p' fst fst.loc fstInSnd = CoeT !(fresh i) (tfst // (BV 0 loc ::: shift 2)) (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc - snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc + snd' = CoeT i (sub1 tsnd fstInSnd) p p' snd snd.loc whnf defs ctx sg $ - Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc + Ann (Pair (E fst') (E snd') sLoc) (ty // one p') loc -- (coe {๐šฬ„} @_ @_ s) โ‡ (s โˆท {๐šฬ„}) Enum cases tyLoc => @@ -210,21 +217,21 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- ฮท expand/simplify, same as for ฮ  -- - -- (coe (๐‘– โ‡’ Eq (๐‘— โ‡’ A) l r) @p @q s) + -- (coe (๐‘– โ‡’ Eq (๐‘— โ‡’ A) l r) @p @p' s) -- โ‡ - -- (ฮด ๐‘˜ โ‡’ (coe (๐‘– โ‡’ Eq (๐‘— โ‡’ A) l r) @p @q s) @๐‘˜) โˆท (Eq (๐‘— โ‡’ A) l r)โ€นq/๐‘–โ€บ - -- โ‡ โ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พ - -- (ฮด ๐‘˜ โ‡’ โ‹ฏ) โˆท (Eq (๐‘— โ‡’ A) l r)โ€นq/๐‘–โ€บ -- see `eqCoe` + -- (ฮด ๐‘˜ โ‡’ (coe (๐‘– โ‡’ Eq (๐‘— โ‡’ A) l r) @p @p' s) @๐‘˜) โˆท (Eq (๐‘— โ‡’ A) l r)โ€นp'/๐‘–โ€บ + -- โ‡ โ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พโ€พ + -- (ฮด ๐‘˜ โ‡’ โ‹ฏ) โˆท (Eq (๐‘— โ‡’ A) l r)โ€นp'/๐‘–โ€บ -- see `eqCoe` -- -- do the eqCoe step here because otherwise equality checking keeps -- doing the ฮท forever Eq {ty = S [< j] _, _} => do let ctx' = extendDim j ctx body <- eqCoe defs ctx' sg - (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q) + (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 p') (dweakT 1 s) (BV 0 loc) loc whnf defs ctx sg $ - Ann (DLamY i (E body.fst) loc) (ty // one q) loc + Ann (DLamY i (E body.fst) loc) (ty // one p') loc -- (coe โ„• @_ @_ s) โ‡ (s โˆท โ„•) NAT tyLoc => @@ -236,17 +243,17 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- ฮท expand/simplify -- - -- (coe (๐‘– โ‡’ [ฯ€.A]) @p @q s) + -- (coe (๐‘– โ‡’ [ฯ€.A]) @p @p' s) -- โ‡ - -- [case coe (๐‘– โ‡’ [ฯ€.A]) @p @q s return Aโ€นq/๐‘–โ€บ of {[x] โ‡’ x}] + -- [case coe (๐‘– โ‡’ [ฯ€.A]) @p @p' s return Aโ€นp'/๐‘–โ€บ of {[x] โ‡’ x}] -- โ‡ - -- [case1 s โˆท [ฯ€.A]โ€นp/๐‘–โ€บ โ‹ฏ] โˆท [ฯ€.A]โ€นq/๐‘–โ€บ -- see `boxCoe` + -- [case1 s โˆท [ฯ€.A]โ€นp/๐‘–โ€บ โ‹ฏ] โˆท [ฯ€.A]โ€นp'/๐‘–โ€บ -- see `boxCoe` -- - -- do the eqCoe step here because otherwise equality checking keeps + -- do the boxCoe step here because otherwise equality checking keeps -- doing the ฮท forever BOX qty inner tyLoc => do body <- boxCoe defs ctx sg qty - (SY [< i] ty) p q s - (SN $ inner // one q) + (SY [< i] ty) p p' s + (SN $ inner // one p') (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc - whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc + whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one p') loc diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr index 3661c12..2994d69 100644 --- a/lib/Quox/Whnf/ComputeElimType.idr +++ b/lib/Quox/Whnf/ComputeElimType.idr @@ -15,46 +15,44 @@ export covering computeElimType : CanWhnf Term Interface.isRedexT => CanWhnf Elim Interface.isRedexE => - (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) -> - (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) => - Eff Whnf (Term d n) + (defs : Definitions) -> (ctx : WhnfContext q d n) -> (0 sg : SQty) -> + (e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) => + Eff Whnf (Term q d n) ||| computes a type and then reduces it to whnf export covering computeWhnfElimType0 : CanWhnf Term Interface.isRedexT => CanWhnf Elim Interface.isRedexE => - (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) -> - (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) => - Eff Whnf (Term d n) + (defs : Definitions) -> (ctx : WhnfContext q d n) -> (0 sg : SQty) -> + (e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) => + Eff Whnf (Term q d n) private covering computeElimTypeNoLog, computeWhnfElimType0NoLog : CanWhnf Term Interface.isRedexT => CanWhnf Elim Interface.isRedexE => - (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) -> - (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) => - Eff Whnf (Term d n) + (defs : Definitions) -> WhnfContext q d n -> (0 sg : SQty) -> + (e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) => + Eff Whnf (Term q d n) computeElimTypeNoLog defs ctx sg e = case e of F x u loc => do let Just def = lookup x defs | Nothing => throw $ NotInScope loc x - pure $ def.typeWithAt ctx.dimLen ctx.termLen u + let polyTy = def.typeWithAt ctx.dimLen ctx.termLen u + Val q = ctx.qtyLen + pure $ polyTy.type // ?freeQSubst - B i _ => - pure (ctx.tctx !! i).type + B i _ => pure (ctx.tctx !! i).type App f s loc => case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc ty => throw $ ExpectedPi loc ctx.names ty - CasePair {pair, ret, _} => - pure $ sub1 ret pair - Fst pair loc => case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of Sig {fst, _} => pure fst @@ -65,46 +63,34 @@ computeElimTypeNoLog defs ctx sg e = Sig {snd, _} => pure $ sub1 snd $ Fst pair loc ty => throw $ ExpectedSig loc ctx.names ty - CaseEnum {tag, ret, _} => - pure $ sub1 ret tag - - CaseNat {nat, ret, _} => - pure $ sub1 ret nat - - CaseBox {box, ret, _} => - pure $ sub1 ret box + CasePair {pair, ret, _} => pure $ sub1 ret pair + CaseEnum {tag, ret, _} => pure $ sub1 ret tag + CaseNat {nat, ret, _} => pure $ sub1 ret nat + CaseBox {box, ret, _} => pure $ sub1 ret box DApp {fun = f, arg = p, loc} => case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of Eq {ty, _} => pure $ dsub1 ty p t => throw $ ExpectedEq loc ctx.names t - Ann {ty, _} => - pure ty - - Coe {ty, q, _} => - pure $ dsub1 ty q - - Comp {ty, _} => - pure ty - - TypeCase {ret, _} => - pure ret + Ann {ty, _} => pure ty + Coe {ty, p', _} => pure $ dsub1 ty p' + Comp {ty, _} => pure ty + TypeCase {ret, _} => pure ret computeElimType defs ctx sg e {ne} = do let Val n = ctx.termLen sayMany "whnf" e.loc [90 :> "computeElimType", 95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx], - 90 :> hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]] + 90 :> hsep ["e =", runPretty $ prettyElim ctx.names e]] res <- computeElimTypeNoLog defs ctx sg e {ne} say "whnf" 91 e.loc $ - hsep ["computeElimType โ‡", - runPretty $ prettyTerm ctx.dnames ctx.tnames res] + hsep ["computeElimType โ‡", runPretty $ prettyTerm ctx.names res] pure res computeWhnfElimType0 defs ctx sg e = - computeElimType defs ctx sg e >>= whnf0 defs ctx SZero + whnf0 defs ctx SZero !(computeElimType defs ctx sg e) computeWhnfElimType0NoLog defs ctx sg e {ne} = - computeElimTypeNoLog defs ctx sg e {ne} >>= whnf0 defs ctx SZero + whnf0 defs ctx SZero !(computeElimTypeNoLog defs ctx sg e {ne}) diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr index e516f62..9632cc4 100644 --- a/lib/Quox/Whnf/Interface.idr +++ b/lib/Quox/Whnf/Interface.idr @@ -20,14 +20,15 @@ Whnf = [Except Error, NameGen, Log] public export 0 RedexTest : TermLike -> Type RedexTest tm = - {0 d, n : Nat} -> Definitions -> WhnfContext d n -> SQty -> tm d n -> Bool + {0 q, d, n : Nat} -> + Definitions -> WhnfContext q d n -> SQty -> tm q d n -> Bool public export interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm where whnf, whnfNoLog : - (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) -> - tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q)) + (defs : Definitions) -> (ctx : WhnfContext q d n) -> (sg : SQty) -> + tm q d n -> Eff Whnf (Subset (tm q d n) (No . isRedex defs ctx sg)) -- having isRedex be part of the class header, and needing to be explicitly -- quantified on every use since idris can't infer its type, is a little ugly. -- but none of the alternatives i've thought of so far work. e.g. in some @@ -36,26 +37,27 @@ where public export %inline whnf0, whnfNoLog0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => - Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n) + Definitions -> WhnfContext q d n -> SQty -> tm q d n -> Eff Whnf (tm q d n) whnf0 defs ctx q t = fst <$> whnf defs ctx q t whnfNoLog0 defs ctx q t = fst <$> whnfNoLog defs ctx q t public export 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex => - Definitions -> WhnfContext d n -> SQty -> Pred (tm d n) + Definitions -> WhnfContext q d n -> SQty -> + Pred (tm q d n) IsRedex defs ctx q = So . isRedex defs ctx q NotRedex defs ctx q = No . isRedex defs ctx q public export 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} -> - CanWhnf tm isRedex => (d, n : Nat) -> - Definitions -> WhnfContext d n -> SQty -> Type -NonRedex tm d n defs ctx q = Subset (tm d n) (NotRedex defs ctx q) + CanWhnf tm isRedex => (q, d, n : Nat) -> + Definitions -> WhnfContext q d n -> SQty -> Type +NonRedex tm q d n defs ctx sg = Subset (tm q d n) (NotRedex defs ctx sg) public export %inline nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) => - (t : tm d n) -> (0 nr : NotRedex defs ctx q t) => - NonRedex tm d n defs ctx q + (t : tm q d n) -> (0 nr : NotRedex defs ctx sg t) => + NonRedex tm q d n defs ctx sg nred t = Element t nr @@ -97,7 +99,7 @@ isNatHead _ = False ||| a natural constant, with or without an annotation public export %inline -isNatConst : Term d n -> Bool +isNatConst : Term {} -> Bool isNatConst (Nat {}) = True isNatConst (E (Ann (Nat {}) _ _)) = True isNatConst _ = False @@ -145,6 +147,7 @@ isTyCon (Let {}) = False isTyCon (E {}) = False isTyCon (CloT {}) = False isTyCon (DCloT {}) = False +isTyCon (QCloT {}) = False ||| a syntactic type, or a neutral public export %inline @@ -195,6 +198,7 @@ canPushCoe sg (Let {}) _ = False canPushCoe sg (E {}) _ = False canPushCoe sg (CloT {}) _ = False canPushCoe sg (DCloT {}) _ = False +canPushCoe sg (QCloT {}) _ = False mutual @@ -238,15 +242,16 @@ mutual isRedexE defs ctx sg (Ann {tm, ty, _}) = isE tm || isRedexT defs ctx sg tm || isRedexT defs ctx SZero ty isRedexE defs ctx sg (Coe {ty = S _ (N _), _}) = True - isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, q, val, _}) = + isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, p', val, _}) = isRedexT defs (extendDim i ctx) SZero ty || - canPushCoe sg ty val || isYes (p `decEqv` q) - isRedexE defs ctx sg (Comp {ty, p, q, r, _}) = - isYes (p `decEqv` q) || isK r + canPushCoe sg ty val || isYes (p `decEqv` p') + isRedexE defs ctx sg (Comp {ty, p, p', r, _}) = + isYes (p `decEqv` p') || isK r isRedexE defs ctx sg (TypeCase {ty, ret, _}) = isRedexE defs ctx sg ty || isRedexT defs ctx sg ret || isAnnTyCon ty isRedexE _ _ _ (CloE {}) = True isRedexE _ _ _ (DCloE {}) = True + isRedexE _ _ _ (QCloE {}) = True ||| a reducible term ||| @@ -260,6 +265,7 @@ mutual isRedexT : RedexTest Term isRedexT _ _ _ (CloT {}) = True isRedexT _ _ _ (DCloT {}) = True + isRedexT _ _ _ (QCloT {}) = True isRedexT _ _ _ (Let {}) = True isRedexT defs ctx sg (E {e, _}) = isAnn e || isRedexE defs ctx sg e isRedexT _ _ _ (Succ p {}) = isNatConst p diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr index 1c3bcc4..ee46712 100644 --- a/lib/Quox/Whnf/Main.idr +++ b/lib/Quox/Whnf/Main.idr @@ -19,19 +19,19 @@ export covering CanWhnf Elim Interface.isRedexE private %inline whnfDefault : {0 isRedex : RedexTest tm} -> - (CanWhnf tm isRedex, Located2 tm) => + (CanWhnf tm isRedex, Located3 tm) => String -> - (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) -> + (forall d, n. WhnfContext q d n -> tm q d n -> Eff Pretty LogDoc) -> (defs : Definitions) -> - (ctx : WhnfContext d n) -> + (ctx : WhnfContext q d n) -> (sg : SQty) -> - (s : tm d n) -> - Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg)) + (s : tm q d n) -> + Eff Whnf (Subset (tm q d n) (No . isRedex defs ctx sg)) whnfDefault name ppr defs ctx sg s = do sayMany "whnf" s.loc [10 :> "whnf", 95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx], - 95 :> hsep ["sg =", runPretty $ prettyQty sg.qty], + 95 :> hsep ["sg =", runPretty $ prettyQConst sg.qconst], 10 :> hsep [text name, "=", runPretty $ ppr ctx s]] res <- whnfNoLog defs ctx sg s say "whnf" 11 s.loc $ hsep ["whnf โ‡", runPretty $ ppr ctx res.fst] @@ -39,10 +39,10 @@ whnfDefault name ppr defs ctx sg s = do covering CanWhnf Elim Interface.isRedexE where - whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e + whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.names e whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq - _ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y + _ | Just y = whnf defs ctx sg $ setLoc loc $ ?whnfFreeQSubst _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah whnfNoLog defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1 @@ -186,8 +186,8 @@ CanWhnf Elim Interface.isRedexE where whnf defs ctx sg $ Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p) (dsub1 ty p) appLoc - Coe ty p' q' val _ => - eqCoe defs ctx sg ty p' q' val p appLoc + Coe ty r r' val _ => + eqCoe defs ctx sg ty r r' val p appLoc Right ndlh => case p of K e _ => do Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f @@ -206,36 +206,37 @@ CanWhnf Elim Interface.isRedexE where Element a anf <- whnf defs ctx SZero a pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf) - whnfNoLog defs ctx sg (Coe sty p q val coeLoc) = + whnfNoLog defs ctx sg (Coe sty p p' val coeLoc) = do -- ๐‘– โˆ‰ fv(A) -- ------------------------------- - -- coe (๐‘– โ‡’ A) @p @q s โ‡ s โˆท A + -- coe (๐‘– โ‡’ A) @p @p' s โ‡ s โˆท A -- -- [fixme] needs a real equality check between Aโ€น0/๐‘–โ€บ and Aโ€น1/๐‘–โ€บ - case dsqueeze sty {f = Term} of + let Val q = ctx.qtyLen + case dsqueeze sty {f = Term q} of ([< i], Left ty) => - case p `decEqv` q of + case p `decEqv` p' of -- coe (๐‘– โ‡’ A) @p @p s โ‡ (s โˆท Aโ€นp/๐‘–โ€บ) Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc No npq => do Element ty tynf <- whnf defs (extendDim i ctx) SZero ty case nchoose $ canPushCoe sg ty val of - Left pc => pushCoe defs ctx sg i ty p q val coeLoc - Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc) + Left pc => pushCoe defs ctx sg i ty p p' val coeLoc + Right npc => pure $ Element (Coe (SY [< i] ty) p p' val coeLoc) (tynf `orNo` npc `orNo` notYesNo npq) (_, Right ty) => whnf defs ctx sg $ Ann val ty coeLoc - whnfNoLog defs ctx sg (Comp ty p q val r zero one compLoc) = - case p `decEqv` q of + whnfNoLog defs ctx sg (Comp ty p p' val r zero one compLoc) = + case p `decEqv` p' of -- comp [A] @p @p s @r { โ‹ฏ } โ‡ s โˆท A Yes y => whnf defs ctx sg $ Ann val ty compLoc No npq => case r of - -- comp [A] @p @q s @0 { 0 ๐‘— โ‡’ tโ‚€; โ‹ฏ } โ‡ tโ‚€โ€นq/๐‘—โ€บ โˆท A - K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc - -- comp [A] @p @q s @1 { 1 ๐‘— โ‡’ tโ‚; โ‹ฏ } โ‡ tโ‚โ€นq/๐‘—โ€บ โˆท A - K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc - B {} => pure $ Element (Comp ty p q val r zero one compLoc) + -- comp [A] @p @p' s @0 { 0 ๐‘— โ‡’ tโ‚€; โ‹ฏ } โ‡ tโ‚€โ€นp'/๐‘—โ€บ โˆท A + K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero p') ty compLoc + -- comp [A] @p @p' s @1 { 1 ๐‘— โ‡’ tโ‚; โ‹ฏ } โ‡ tโ‚โ€นp'/๐‘—โ€บ โˆท A + K One _ => whnf defs ctx sg $ Ann (dsub1 one p') ty compLoc + B {} => pure $ Element (Comp ty p p' val r zero one compLoc) (notYesNo npq `orNo` Ah) whnfNoLog defs ctx sg (TypeCase ty ret arms def tcLoc) = @@ -248,17 +249,23 @@ CanWhnf Elim Interface.isRedexE where reduceTypeCase defs ctx ty u ret arms def tcLoc Right nt => pure $ Element (TypeCase ty ret arms def tcLoc) (tynf `orNo` retnf `orNo` nt) - No _ => - throw $ ClashQ tcLoc sg.qty Zero + No _ => do + let Val q = ctx.qtyLen + throw $ ClashQ tcLoc ctx.qnames (toQty tcLoc sg) (zero tcLoc) - whnfNoLog defs ctx sg (CloE (Sub el th)) = - whnfNoLog defs ctx sg $ pushSubstsWith' id th el - whnfNoLog defs ctx sg (DCloE (Sub el th)) = - whnfNoLog defs ctx sg $ pushSubstsWith' th id el + whnfNoLog defs ctx sg (CloE (Sub el th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' id id th el + whnfNoLog defs ctx sg (DCloE (Sub el th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' id th id el + whnfNoLog defs ctx sg (QCloE (SubR el th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' th id id el covering CanWhnf Term Interface.isRedexT where - whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.dnames ctx.tnames s + whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.names s whnfNoLog _ _ _ t@(TYPE {}) = pure $ nred t whnfNoLog _ _ _ t@(IOState {}) = pure $ nred t @@ -294,7 +301,14 @@ CanWhnf Term Interface.isRedexT where Left _ => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf Right na => pure $ Element (E e) $ na `orNo` enf - whnfNoLog defs ctx sg (CloT (Sub tm th)) = - whnfNoLog defs ctx sg $ pushSubstsWith' id th tm - whnfNoLog defs ctx sg (DCloT (Sub tm th)) = - whnfNoLog defs ctx sg $ pushSubstsWith' th id tm + whnfNoLog defs ctx sg (CloT (Sub tm th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' id id th tm + + whnfNoLog defs ctx sg (DCloT (Sub tm th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' id th id tm + + whnfNoLog defs ctx sg (QCloT (SubR tm th)) = do + let Val q = ctx.qtyLen + whnfNoLog defs ctx sg $ pushSubstsWith' th id id tm diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr index 9b3645f..e6a4de9 100644 --- a/lib/Quox/Whnf/TypeCase.idr +++ b/lib/Quox/Whnf/TypeCase.idr @@ -8,44 +8,45 @@ import Data.SnocVect private -tycaseRhs : (k : TyConKind) -> TypeCaseArms d n -> - Maybe (ScopeTermN (arity k) d n) +tycaseRhs : (k : TyConKind) -> TypeCaseArms q d n -> + Maybe (ScopeTermN (arity k) q d n) tycaseRhs k arms = lookupPrecise k arms private -tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n -> - ScopeTermN (arity k) d n +tycaseRhsDef : (def : Term q d n) -> (k : TyConKind) -> TypeCaseArms q d n -> + ScopeTermN (arity k) q d n tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms private -tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n -> - (0 eq : arity k = 0) => Maybe (Term d n) +tycaseRhs0 : (k : TyConKind) -> TypeCaseArms q d n -> + (0 eq : arity k = 0) => Maybe (Term q d n) tycaseRhs0 k arms = map (.term0) $ rewrite sym eq in tycaseRhs k arms private -tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n -> - (0 eq : arity k = 0) => Term d n +tycaseRhsDef0 : (def : Term q d n) -> (k : TyConKind) -> TypeCaseArms q d n -> + (0 eq : arity k = 0) => Term q d n tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms parameters {auto _ : CanWhnf Term Interface.isRedexT} {auto _ : CanWhnf Elim Interface.isRedexE} - (defs : Definitions) (ctx : WhnfContext d n) + (defs : Definitions) (ctx : WhnfContext q d n) ||| for ฯ€.(x : A) โ†’ B, returns (A, B); ||| for an elim returns a pair of type-cases that will reduce to that; ||| for other intro forms error export covering - tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => - Eff Whnf (Term d n, ScopeTerm d n) + tycasePi : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => + Eff Whnf (Term q d n, ScopeTerm q d n) tycasePi (Pi {arg, res, _}) = pure (arg, res) tycasePi (E e) {tnf} = do ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf} - let loc = e.loc - narg = mnb "Arg" loc; nret = mnb "Ret" loc - arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc - res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret] + let Val q = ctx.qtyLen + loc = e.loc + narg = mnb "Arg" loc; nret = mnb "Ret" loc + arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc + res' = typeCase1Y e (Arr (zero loc) arg ty loc) KPi [< !narg, !nret] (BVT 0 loc) loc - res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc + res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc pure (arg, res) tycasePi t = throw $ ExpectedPi t.loc ctx.names t @@ -53,17 +54,18 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} ||| for an elim returns a pair of type-cases that will reduce to that; ||| for other intro forms error export covering - tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => - Eff Whnf (Term d n, ScopeTerm d n) + tycaseSig : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => + Eff Whnf (Term q d n, ScopeTerm q d n) tycaseSig (Sig {fst, snd, _}) = pure (fst, snd) tycaseSig (E e) {tnf} = do ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf} - let loc = e.loc - nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc - fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc - snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd] + let Val q = ctx.qtyLen + loc = e.loc + nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc + fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc + snd' = typeCase1Y e (Arr (zero loc) fst ty loc) KSig [< !nfst, !nsnd] (BVT 0 loc) loc - snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc + snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc pure (fst, snd) tycaseSig t = throw $ ExpectedSig t.loc ctx.names t @@ -71,8 +73,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} ||| for an elim returns a type-case that will reduce to that; ||| for other intro forms error export covering - tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => - Eff Whnf (Term d n) + tycaseBOX : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => + Eff Whnf (Term q d n) tycaseBOX (BOX {ty, _}) = pure ty tycaseBOX (E e) {tnf} = do ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf} @@ -83,12 +85,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} ||| for an elim returns five type-cases that will reduce to that; ||| for other intro forms error export covering - tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => - Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n) + tycaseEq : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) => + Eff Whnf (Term q d n, Term q d n, DScopeTerm q d n, + Term q d n, Term q d n) tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r) tycaseEq (E e) {tnf} = do ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf} - let loc = e.loc + let Val q = ctx.qtyLen + loc = e.loc names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"] a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc @@ -104,10 +108,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} ||| `reduceTypeCase A i Q arms def _` reduces an expression ||| `type-case A โˆท โ˜…แตข return Q of { arms; _ โ‡’ def }` export covering - reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) -> - (arms : TypeCaseArms d n) -> (def : Term d n) -> + reduceTypeCase : (ty : Term q d n) -> (u : Universe) -> (ret : Term q d n) -> + (arms : TypeCaseArms q d n) -> (def : Term q d n) -> (0 _ : So (isTyCon ty)) => Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx SZero)) + Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx SZero)) reduceTypeCase ty u ret arms def loc = case ty of -- (type-case โ˜…แตข โˆท _ return Q of { โ˜… โ‡’ s; โ‹ฏ }) โ‡ s โˆท Q TYPE {} => @@ -120,9 +124,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- (type-case ฯ€.(x : A) โ†’ B โˆท โ˜…แตข return Q of { (a โ†’ b) โ‡’ s; โ‹ฏ }) โ‡ -- s[(A โˆท โ˜…แตข)/a, ((ฮป x โ‡’ B) โˆท 0.A โ†’ โ˜…แตข)/b] โˆท Q Pi {arg, res, loc = piLoc, _} => - let arg' = Ann arg (TYPE u arg.loc) arg.loc - res' = Ann (Lam res res.loc) - (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc + let Val q = ctx.qtyLen + arg' = Ann arg (TYPE u arg.loc) arg.loc + res' = Ann (Lam res res.loc) + (Arr (zero loc) arg (TYPE u arg.loc) arg.loc) res.loc in whnf defs ctx SZero $ Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc @@ -130,9 +135,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT} -- (type-case (x : A) ร— B โˆท โ˜…แตข return Q of { (a ร— b) โ‡’ s; โ‹ฏ }) โ‡ -- s[(A โˆท โ˜…แตข)/a, ((ฮป x โ‡’ B) โˆท 0.A โ†’ โ˜…แตข)/b] โˆท Q Sig {fst, snd, loc = sigLoc, _} => - let fst' = Ann fst (TYPE u fst.loc) fst.loc - snd' = Ann (Lam snd snd.loc) - (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc + let Val q = ctx.qtyLen + fst' = Ann fst (TYPE u fst.loc) fst.loc + snd' = Ann (Lam snd snd.loc) + (Arr (zero loc) fst (TYPE u fst.loc) fst.loc) snd.loc in whnf defs ctx SZero $ Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc diff --git a/tests/Tests/Qty.idr b/tests/Tests/Qty.idr new file mode 100644 index 0000000..73daccc --- /dev/null +++ b/tests/Tests/Qty.idr @@ -0,0 +1,8 @@ +module Tests.Qty + +import TAP +import Quox.Syntax.Qty +import PrettyExtra + + +