add source locations to inner syntax
This commit is contained in:
parent
30fa93ab4e
commit
d5f4a012c5
35 changed files with 3210 additions and 2482 deletions
|
|
@ -40,6 +40,10 @@ public export
|
|||
NContext : Nat -> Type
|
||||
NContext = Context' BaseName
|
||||
|
||||
public export
|
||||
BContext : Nat -> Type
|
||||
BContext = Context' BindName
|
||||
|
||||
|
||||
public export
|
||||
unsnoc : Context tm (S n) -> (Context tm n, tm n)
|
||||
|
|
@ -183,6 +187,10 @@ parameters {auto _ : Applicative f}
|
|||
traverse f [<] = pure [<]
|
||||
traverse f (tel :< x) = [|traverse f tel :< f x|]
|
||||
|
||||
export %inline
|
||||
traverse' : (a -> f b) -> Telescope' a from to -> f (Telescope' b from to)
|
||||
traverse' f = traverse f
|
||||
|
||||
infixl 3 `app`
|
||||
||| like `(<*>)` but with effects
|
||||
export
|
||||
|
|
@ -197,6 +205,7 @@ parameters {auto _ : Applicative f}
|
|||
sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
|
||||
sequence = traverse id
|
||||
|
||||
|
||||
parameters {0 tm1, tm2 : Nat -> Type}
|
||||
(f : forall n. tm1 n -> tm2 n)
|
||||
export %inline
|
||||
|
|
@ -207,6 +216,8 @@ parameters {0 tm1, tm2 : Nat -> Type}
|
|||
(<$>) : Telescope tm1 from to -> Telescope tm2 from to
|
||||
(<$>) = map
|
||||
|
||||
|
||||
|
||||
export %inline
|
||||
(<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
|
||||
Telescope tm1 from to -> Telescope tm2 from to
|
||||
|
|
@ -311,3 +322,9 @@ export %inline
|
|||
export %inline
|
||||
(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
|
||||
prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
|
||||
|
||||
|
||||
namespace BContext
|
||||
export
|
||||
toNames : BContext n -> SnocList BaseName
|
||||
toNames = foldl (\xs, x => xs :< x.name) [<]
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@ module Quox.Definition
|
|||
import public Quox.No
|
||||
import public Quox.Syntax
|
||||
import public Data.SortedMap
|
||||
import public Quox.Loc
|
||||
import Control.Eff
|
||||
import Decidable.Decidable
|
||||
|
||||
|
|
@ -25,14 +26,18 @@ record Definition where
|
|||
qty : GQty
|
||||
type0 : Term 0 0
|
||||
body0 : DefBody
|
||||
loc_ : Loc
|
||||
|
||||
public export %inline
|
||||
mkPostulate : GQty -> (type0 : Term 0 0) -> Definition
|
||||
mkPostulate qty type0 = MkDef {qty, type0, body0 = Postulate}
|
||||
mkPostulate : GQty -> (type0 : Term 0 0) -> Loc -> Definition
|
||||
mkPostulate qty type0 loc_ = MkDef {qty, type0, body0 = Postulate, loc_}
|
||||
|
||||
public export %inline
|
||||
mkDef : GQty -> (type0, term0 : Term 0 0) -> Definition
|
||||
mkDef qty type0 term0 = MkDef {qty, type0, body0 = Concrete term0}
|
||||
mkDef : GQty -> (type0, term0 : Term 0 0) -> Loc -> Definition
|
||||
mkDef qty type0 term0 loc_ = MkDef {qty, type0, body0 = Concrete term0, loc_}
|
||||
|
||||
export Located Definition where def.loc = def.loc_
|
||||
export Relocatable Definition where setLoc loc = {loc_ := loc}
|
||||
|
||||
|
||||
parameters {d, n : Nat}
|
||||
|
|
@ -46,7 +51,7 @@ parameters {d, n : Nat}
|
|||
|
||||
public export %inline
|
||||
toElim : Definition -> Maybe $ Elim d n
|
||||
toElim def = pure $ !def.term :# def.type
|
||||
toElim def = pure $ Ann !def.term def.type def.loc
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
@ -62,9 +67,13 @@ Definitions : Type
|
|||
Definitions = SortedMap Name Definition
|
||||
|
||||
public export
|
||||
0 DefsReader : Type -> Type
|
||||
DefsReader : Type -> Type
|
||||
DefsReader = ReaderL DEFS Definitions
|
||||
|
||||
public export
|
||||
DefsState : Type -> Type
|
||||
DefsState = StateL DEFS Definitions
|
||||
|
||||
export
|
||||
defs : Has DefsReader fs => Eff fs Definitions
|
||||
defs = askAt DEFS
|
||||
|
|
|
|||
|
|
@ -9,20 +9,41 @@ import Quox.EffExtra
|
|||
|
||||
|
||||
public export
|
||||
0 EqModeState : Type -> Type
|
||||
EqModeState : Type -> Type
|
||||
EqModeState = State EqMode
|
||||
|
||||
public export
|
||||
0 EqualEff : List (Type -> Type)
|
||||
EqualEff = [ErrorEff, EqModeState]
|
||||
Equal : Type -> Type
|
||||
Equal = Eff [ErrorEff, DefsReader, NameGen]
|
||||
|
||||
public export
|
||||
0 Equal : Type -> Type
|
||||
Equal = Eff $ EqualEff
|
||||
Equal_ : Type -> Type
|
||||
Equal_ = Eff [ErrorEff, NameGen, EqModeState]
|
||||
|
||||
export
|
||||
runEqual : EqMode -> Equal a -> Either Error a
|
||||
runEqual mode = extract . runExcept . evalState mode
|
||||
runEqualWith_ : EqMode -> NameSuf -> Equal_ a -> (Either Error a, NameSuf)
|
||||
runEqualWith_ mode suf act =
|
||||
extract $
|
||||
runNameGenWith suf $
|
||||
runExcept $
|
||||
evalState mode act
|
||||
|
||||
export
|
||||
runEqual_ : EqMode -> Equal_ a -> Either Error a
|
||||
runEqual_ mode act = fst $ runEqualWith_ mode 0 act
|
||||
|
||||
|
||||
export
|
||||
runEqualWith : NameSuf -> Definitions -> Equal a -> (Either Error a, NameSuf)
|
||||
runEqualWith suf defs act =
|
||||
extract $
|
||||
runStateAt GEN suf $
|
||||
runReaderAt DEFS defs $
|
||||
runExcept act
|
||||
|
||||
export
|
||||
runEqual : Definitions -> Equal a -> Either Error a
|
||||
runEqual defs act = fst $ runEqualWith 0 defs act
|
||||
|
||||
|
||||
export %inline
|
||||
|
|
@ -30,22 +51,22 @@ mode : Has EqModeState fs => Eff fs EqMode
|
|||
mode = get
|
||||
|
||||
|
||||
parameters (ctx : EqContext n)
|
||||
parameters (loc : Loc) (ctx : EqContext n)
|
||||
private %inline
|
||||
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal a
|
||||
clashT ty s t = throw $ ClashT ctx !mode ty s t
|
||||
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal_ a
|
||||
clashT ty s t = throw $ ClashT loc ctx !mode ty s t
|
||||
|
||||
private %inline
|
||||
clashTy : Term 0 n -> Term 0 n -> Equal a
|
||||
clashTy s t = throw $ ClashTy ctx !mode s t
|
||||
clashTy : Term 0 n -> Term 0 n -> Equal_ a
|
||||
clashTy s t = throw $ ClashTy loc ctx !mode s t
|
||||
|
||||
private %inline
|
||||
clashE : Elim 0 n -> Elim 0 n -> Equal a
|
||||
clashE e f = throw $ ClashE ctx !mode e f
|
||||
clashE : Elim 0 n -> Elim 0 n -> Equal_ a
|
||||
clashE e f = throw $ ClashE loc ctx !mode e f
|
||||
|
||||
private %inline
|
||||
wrongType : Term 0 n -> Term 0 n -> Equal a
|
||||
wrongType ty s = throw $ WrongType ctx ty s
|
||||
wrongType : Term 0 n -> Term 0 n -> Equal_ a
|
||||
wrongType ty s = throw $ WrongType loc ctx ty s
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
@ -62,8 +83,8 @@ sameTyCon (Enum {}) (Enum {}) = True
|
|||
sameTyCon (Enum {}) _ = False
|
||||
sameTyCon (Eq {}) (Eq {}) = True
|
||||
sameTyCon (Eq {}) _ = False
|
||||
sameTyCon Nat Nat = True
|
||||
sameTyCon Nat _ = False
|
||||
sameTyCon (Nat {}) (Nat {}) = True
|
||||
sameTyCon (Nat {}) _ = False
|
||||
sameTyCon (BOX {}) (BOX {}) = True
|
||||
sameTyCon (BOX {}) _ = False
|
||||
sameTyCon (E {}) (E {}) = True
|
||||
|
|
@ -80,37 +101,39 @@ sameTyCon (E {}) _ = False
|
|||
||| * an enum type is a subsingleton if it has zero or one tags.
|
||||
||| * a box type is a subsingleton if its content is
|
||||
public export covering
|
||||
isSubSing : Has ErrorEff fs => {n : Nat} ->
|
||||
Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
|
||||
isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> Equal_ Bool
|
||||
isSubSing defs ctx ty0 = do
|
||||
Element ty0 nc <- whnf defs ctx ty0
|
||||
Element ty0 nc <- whnf defs ctx ty0.loc ty0
|
||||
case ty0 of
|
||||
TYPE _ => pure False
|
||||
Pi _ arg res => isSubSing defs (extendTy Zero res.name arg ctx) res.term
|
||||
Sig fst snd => isSubSing defs ctx fst `andM`
|
||||
isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
|
||||
Enum tags => pure $ length (SortedSet.toList tags) <= 1
|
||||
Eq {} => pure True
|
||||
Nat => pure False
|
||||
BOX _ ty => isSubSing defs ctx ty
|
||||
E (s :# _) => isSubSing defs ctx s
|
||||
E _ => pure False
|
||||
Lam _ => pure False
|
||||
Pair _ _ => pure False
|
||||
Tag _ => pure False
|
||||
DLam _ => pure False
|
||||
Zero => pure False
|
||||
Succ _ => pure False
|
||||
Box _ => pure False
|
||||
TYPE {} => pure False
|
||||
Pi {arg, res, _} =>
|
||||
isSubSing defs (extendTy Zero res.name arg ctx) res.term
|
||||
Sig {fst, snd, _} =>
|
||||
isSubSing defs ctx fst `andM`
|
||||
isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
|
||||
Enum {cases, _} =>
|
||||
pure $ length (SortedSet.toList cases) <= 1
|
||||
Eq {} => pure True
|
||||
Nat {} => pure False
|
||||
BOX {ty, _} => isSubSing defs ctx ty
|
||||
E (Ann {tm, _}) => isSubSing defs ctx tm
|
||||
E _ => pure False
|
||||
Lam {} => pure False
|
||||
Pair {} => pure False
|
||||
Tag {} => pure False
|
||||
DLam {} => pure False
|
||||
Zero {} => pure False
|
||||
Succ {} => pure False
|
||||
Box {} => pure False
|
||||
|
||||
|
||||
export
|
||||
ensureTyCon : Has ErrorEff fs =>
|
||||
(ctx : EqContext n) -> (t : Term 0 n) ->
|
||||
(loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
|
||||
Eff fs (So (isTyConE t))
|
||||
ensureTyCon ctx t = case nchoose $ isTyConE t of
|
||||
ensureTyCon loc ctx t = case nchoose $ isTyConE t of
|
||||
Left y => pure y
|
||||
Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
|
||||
Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)
|
||||
|
||||
||| performs the minimum work required to recompute the type of an elim.
|
||||
|||
|
||||
|
|
@ -118,10 +141,10 @@ ensureTyCon ctx t = case nchoose $ isTyConE t of
|
|||
private covering
|
||||
computeElimTypeE : (defs : Definitions) -> EqContext n ->
|
||||
(e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
|
||||
Equal (Term 0 n)
|
||||
Equal_ (Term 0 n)
|
||||
computeElimTypeE defs ectx e =
|
||||
let Val n = ectx.termLen in
|
||||
rethrow $ computeElimType defs (toWhnfContext ectx) e
|
||||
lift $ computeElimType defs (toWhnfContext ectx) e
|
||||
|
||||
parameters (defs : Definitions)
|
||||
mutual
|
||||
|
|
@ -131,55 +154,56 @@ parameters (defs : Definitions)
|
|||
|||
|
||||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
|
||||
export covering %inline
|
||||
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal ()
|
||||
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal_ ()
|
||||
compare0 ctx ty s t =
|
||||
wrapErr (WhileComparingT ctx !mode ty s t) $ do
|
||||
let Val n = ctx.termLen
|
||||
Element ty _ <- whnf defs ctx ty
|
||||
Element s _ <- whnf defs ctx s
|
||||
Element t _ <- whnf defs ctx t
|
||||
tty <- ensureTyCon ctx ty
|
||||
compare0' ctx ty s t
|
||||
Element ty' _ <- whnf defs ctx ty.loc ty
|
||||
Element s' _ <- whnf defs ctx s.loc s
|
||||
Element t' _ <- whnf defs ctx t.loc t
|
||||
tty <- ensureTyCon ty.loc ctx ty'
|
||||
compare0' ctx ty' s' t'
|
||||
|
||||
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
|
||||
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
|
||||
private %inline
|
||||
toLamBody : Elim d n -> Term d (S n)
|
||||
toLamBody e = E $ weakE 1 e :@ BVT 0
|
||||
toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
|
||||
|
||||
private covering
|
||||
compare0' : EqContext n ->
|
||||
(ty, s, t : Term 0 n) ->
|
||||
(0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
|
||||
(0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) =>
|
||||
Equal ()
|
||||
compare0' ctx (TYPE _) s t = compareType ctx s t
|
||||
Equal_ ()
|
||||
compare0' ctx (TYPE {}) s t = compareType ctx s t
|
||||
|
||||
compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local_ Equal $
|
||||
compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
|
||||
case (s, t) of
|
||||
-- Γ, x : A ⊢ s = t : B
|
||||
-- -------------------------------------------
|
||||
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
|
||||
(Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term
|
||||
(Lam b1 {}, Lam b2 {}) =>
|
||||
compare0 ctx' res.term b1.term b2.term
|
||||
|
||||
-- Γ, x : A ⊢ s = e x : B
|
||||
-- -----------------------------------
|
||||
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
|
||||
(E e, Lam b) => eta e b
|
||||
(Lam b, E e) => eta e b
|
||||
(E e, Lam b {}) => eta s.loc e b
|
||||
(Lam b {}, E e) => eta s.loc e b
|
||||
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
(Lam _, t) => wrongType ctx ty t
|
||||
(E _, t) => wrongType ctx ty t
|
||||
(s, _) => wrongType ctx ty s
|
||||
(Lam {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
where
|
||||
ctx' : EqContext (S n)
|
||||
ctx' = extendTy qty res.name arg ctx
|
||||
|
||||
eta : Elim 0 n -> ScopeTerm 0 n -> Equal ()
|
||||
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta e (S _ (N _)) = clashT ctx ty s t
|
||||
eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Equal_ ()
|
||||
eta _ e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta loc e (S _ (N _)) = clashT loc ctx ty s t
|
||||
|
||||
compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
|
|
@ -188,34 +212,35 @@ parameters (defs : Definitions)
|
|||
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
|
||||
--
|
||||
-- [todo] η for π ≥ 0 maybe
|
||||
(Pair sFst sSnd, Pair tFst tSnd) => do
|
||||
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
|
||||
compare0 ctx fst sFst tFst
|
||||
compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
|
||||
compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
|
||||
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
(Pair {}, E _) => clashT ctx ty s t
|
||||
(E _, Pair {}) => clashT ctx ty s t
|
||||
(Pair {}, E _) => clashT s.loc ctx ty s t
|
||||
(E _, Pair {}) => clashT s.loc ctx ty s t
|
||||
|
||||
(Pair {}, t) => wrongType ctx ty t
|
||||
(E _, t) => wrongType ctx ty t
|
||||
(s, _) => wrongType ctx ty s
|
||||
(Pair {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
|
||||
compare0' ctx ty@(Enum tags) s t = local_ Equal $
|
||||
compare0' ctx ty@(Enum {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- --------------------
|
||||
-- Γ ⊢ `t = `t : {ts}
|
||||
--
|
||||
-- t ∈ ts is in the typechecker, not here, ofc
|
||||
(Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
(Tag t1 {}, Tag t2 {}) =>
|
||||
unless (t1 == t2) $ clashT s.loc ctx ty s t
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
(Tag _, E _) => clashT ctx ty s t
|
||||
(E _, Tag _) => clashT ctx ty s t
|
||||
(Tag {}, E _) => clashT s.loc ctx ty s t
|
||||
(E _, Tag {}) => clashT s.loc ctx ty s t
|
||||
|
||||
(Tag _, t) => wrongType ctx ty t
|
||||
(E _, t) => wrongType ctx ty t
|
||||
(s, _) => wrongType ctx ty s
|
||||
(Tag {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
|
||||
compare0' _ (Eq {}) _ _ =
|
||||
-- ✨ uip ✨
|
||||
|
|
@ -224,84 +249,85 @@ parameters (defs : Definitions)
|
|||
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
|
||||
pure ()
|
||||
|
||||
compare0' ctx Nat s t = local_ Equal $
|
||||
compare0' ctx nat@(Nat {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- ---------------
|
||||
-- Γ ⊢ 0 = 0 : ℕ
|
||||
(Zero, Zero) => pure ()
|
||||
(Zero {}, Zero {}) => pure ()
|
||||
|
||||
-- Γ ⊢ m = n : ℕ
|
||||
-- Γ ⊢ s = t : ℕ
|
||||
-- -------------------------
|
||||
-- Γ ⊢ succ m = succ n : ℕ
|
||||
(Succ m, Succ n) => compare0 ctx Nat m n
|
||||
-- Γ ⊢ succ s = succ t : ℕ
|
||||
(Succ s' {}, Succ t' {}) => compare0 ctx nat s' t'
|
||||
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
(Zero, Succ _) => clashT ctx Nat s t
|
||||
(Zero, E _) => clashT ctx Nat s t
|
||||
(Succ _, Zero) => clashT ctx Nat s t
|
||||
(Succ _, E _) => clashT ctx Nat s t
|
||||
(E _, Zero) => clashT ctx Nat s t
|
||||
(E _, Succ _) => clashT ctx Nat s t
|
||||
(Zero {}, Succ {}) => clashT s.loc ctx nat s t
|
||||
(Zero {}, E _) => clashT s.loc ctx nat s t
|
||||
(Succ {}, Zero {}) => clashT s.loc ctx nat s t
|
||||
(Succ {}, E _) => clashT s.loc ctx nat s t
|
||||
(E _, Zero {}) => clashT s.loc ctx nat s t
|
||||
(E _, Succ {}) => clashT s.loc ctx nat s t
|
||||
|
||||
(Zero, t) => wrongType ctx Nat t
|
||||
(Succ _, t) => wrongType ctx Nat t
|
||||
(E _, t) => wrongType ctx Nat t
|
||||
(s, _) => wrongType ctx Nat s
|
||||
(Zero {}, t) => wrongType t.loc ctx nat t
|
||||
(Succ {}, t) => wrongType t.loc ctx nat t
|
||||
(E _, t) => wrongType t.loc ctx nat t
|
||||
(s, _) => wrongType s.loc ctx nat s
|
||||
|
||||
compare0' ctx ty@(BOX q ty') s t = local_ Equal $
|
||||
compare0' ctx ty@(BOX q ty' {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- Γ ⊢ s = t : A
|
||||
-- -----------------------
|
||||
-- Γ ⊢ [s] = [t] : [π.A]
|
||||
(Box s, Box t) => compare0 ctx ty' s t
|
||||
(Box s' {}, Box t' {}) => compare0 ctx ty' s' t'
|
||||
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
(Box _, t) => wrongType ctx ty t
|
||||
(E _, t) => wrongType ctx ty t
|
||||
(s, _) => wrongType ctx ty s
|
||||
(Box {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
|
||||
compare0' ctx ty@(E _) s t = do
|
||||
-- a neutral type can only be inhabited by neutral values
|
||||
-- e.g. an abstract value in an abstract type, bound variables, …
|
||||
E e <- pure s | _ => wrongType ctx ty s
|
||||
E f <- pure t | _ => wrongType ctx ty t
|
||||
let E e = s | _ => wrongType s.loc ctx ty s
|
||||
E f = t | _ => wrongType t.loc ctx ty t
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
||| compares two types, using the current variance `mode` for universes.
|
||||
||| fails if they are not types, even if they would happen to be equal.
|
||||
export covering %inline
|
||||
compareType : EqContext n -> (s, t : Term 0 n) -> Equal ()
|
||||
compareType : EqContext n -> (s, t : Term 0 n) -> Equal_ ()
|
||||
compareType ctx s t = do
|
||||
let Val n = ctx.termLen
|
||||
Element s _ <- whnf defs ctx s
|
||||
Element t _ <- whnf defs ctx t
|
||||
ts <- ensureTyCon ctx s
|
||||
tt <- ensureTyCon ctx t
|
||||
st <- either pure (const $ clashTy ctx s t) $ nchoose $ sameTyCon s t
|
||||
compareType' ctx s t
|
||||
Element s' _ <- whnf defs ctx s.loc s
|
||||
Element t' _ <- whnf defs ctx t.loc t
|
||||
ts <- ensureTyCon s.loc ctx s'
|
||||
tt <- ensureTyCon t.loc ctx t'
|
||||
st <- either pure (const $ clashTy s.loc ctx s' t') $
|
||||
nchoose $ sameTyCon s' t'
|
||||
compareType' ctx s' t'
|
||||
|
||||
private covering
|
||||
compareType' : EqContext n -> (s, t : Term 0 n) ->
|
||||
(0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
|
||||
(0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
|
||||
(0 _ : So (sameTyCon s t)) =>
|
||||
Equal ()
|
||||
Equal_ ()
|
||||
-- equality is the same as subtyping, except with the
|
||||
-- "≤" in the TYPE rule being replaced with "="
|
||||
compareType' ctx (TYPE k) (TYPE l) =
|
||||
compareType' ctx a@(TYPE k {}) (TYPE l {}) =
|
||||
-- 𝓀 ≤ ℓ
|
||||
-- ----------------------
|
||||
-- Γ ⊢ Type 𝓀 <: Type ℓ
|
||||
expectModeU !mode k l
|
||||
expectModeU a.loc !mode k l
|
||||
|
||||
compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _})
|
||||
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
||||
compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
|
||||
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
||||
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
|
||||
-- ----------------------------------------
|
||||
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
|
||||
expectEqualQ sQty tQty
|
||||
expectEqualQ a.loc sQty tQty
|
||||
local flip $ compareType ctx sArg tArg -- contra
|
||||
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
|
||||
|
||||
|
|
@ -325,21 +351,21 @@ parameters (defs : Definitions)
|
|||
Term.compare0 ctx sTy.zero sl tl
|
||||
Term.compare0 ctx sTy.one sr tr
|
||||
|
||||
compareType' ctx s@(Enum tags1) t@(Enum tags2) = do
|
||||
compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
|
||||
-- ------------------
|
||||
-- Γ ⊢ {ts} <: {ts}
|
||||
--
|
||||
-- no subtyping based on tag subsets, since that would need
|
||||
-- a runtime coercion
|
||||
unless (tags1 == tags2) $ clashTy ctx s t
|
||||
unless (tags1 == tags2) $ clashTy s.loc ctx s t
|
||||
|
||||
compareType' ctx Nat Nat =
|
||||
compareType' ctx (Nat {}) (Nat {}) =
|
||||
-- ------------
|
||||
-- Γ ⊢ ℕ <: ℕ
|
||||
pure ()
|
||||
|
||||
compareType' ctx (BOX pi a) (BOX rh b) = do
|
||||
expectEqualQ pi rh
|
||||
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
|
||||
expectEqualQ loc pi rh
|
||||
compareType ctx a b
|
||||
|
||||
compareType' ctx (E e) (E f) = do
|
||||
|
|
@ -347,13 +373,17 @@ parameters (defs : Definitions)
|
|||
-- has been inlined by whnf
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
-- Ψ | Γ ⊢₀ e ⇒ Eq [𝑖 ⇒ A] s t
|
||||
-- -----------------------------
|
||||
-- Ψ | Γ ⊢ e @0 = s ⇒ A[0/𝑖]
|
||||
-- Ψ | Γ ⊢ e @1 = s ⇒ A[1/𝑖]
|
||||
private covering
|
||||
replaceEnd : EqContext n ->
|
||||
(e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
|
||||
Equal (Elim 0 n)
|
||||
replaceEnd ctx e p ne = do
|
||||
(ty, l, r) <- expectEq defs ctx !(computeElimTypeE defs ctx e)
|
||||
pure $ ends l r p :# dsub1 ty (K p)
|
||||
(e : Elim 0 n) -> Loc -> DimConst -> Loc ->
|
||||
(0 ne : NotRedex defs e) -> Equal_ (Elim 0 n)
|
||||
replaceEnd ctx e eloc p ploc ne = do
|
||||
(ty, l, r) <- expectEq defs ctx eloc !(computeElimTypeE defs ctx e)
|
||||
pure $ Ann (ends l r p) (dsub1 ty (K p ploc)) eloc
|
||||
|
||||
namespace Elim
|
||||
-- [fixme] the following code ends up repeating a lot of work in the
|
||||
|
|
@ -364,133 +394,179 @@ parameters (defs : Definitions)
|
|||
||| ⚠ **assumes that they have both been typechecked, and have
|
||||
||| equal types.** ⚠
|
||||
export covering %inline
|
||||
compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal ()
|
||||
compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal_ ()
|
||||
compare0 ctx e f =
|
||||
wrapErr (WhileComparingE ctx !mode e f) $ do
|
||||
let Val n = ctx.termLen
|
||||
Element e ne <- whnf defs ctx e
|
||||
Element f nf <- whnf defs ctx f
|
||||
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
|
||||
unless !(isSubSing defs ctx !(computeElimTypeE defs ctx e)) $
|
||||
compare0' ctx e f ne nf
|
||||
Element e' ne <- whnf defs ctx e.loc e
|
||||
Element f' nf <- whnf defs ctx f.loc f
|
||||
unless !(isSubSing defs ctx =<< computeElimTypeE defs ctx e') $
|
||||
compare0' ctx e' f' ne nf
|
||||
|
||||
private covering
|
||||
compare0' : EqContext n ->
|
||||
(e, f : Elim 0 n) ->
|
||||
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
|
||||
Equal ()
|
||||
Equal_ ()
|
||||
-- replace applied equalities with the appropriate end first
|
||||
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
|
||||
--
|
||||
-- [todo] maybe have typed whnf and do this (and η???) there instead
|
||||
compare0' ctx (e :% K p) f ne nf =
|
||||
compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
|
||||
compare0' ctx e (f :% K q) ne nf =
|
||||
compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
|
||||
-- (see `replaceEnd`)
|
||||
compare0' ctx (DApp e (K p ploc) loc) f ne nf =
|
||||
compare0 ctx !(replaceEnd ctx e loc p ploc $ noOr1 ne) f
|
||||
compare0' ctx e (DApp f (K q qloc) loc) ne nf =
|
||||
compare0 ctx e !(replaceEnd ctx f loc q qloc $ noOr1 nf)
|
||||
|
||||
compare0' ctx e@(F x) f@(F y) _ _ = unless (x == y) $ clashE ctx e f
|
||||
compare0' ctx e@(F _) f _ _ = clashE ctx e f
|
||||
compare0' ctx e@(F x {}) f@(F y {}) _ _ =
|
||||
unless (x == y) $ clashE e.loc ctx e f
|
||||
compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE ctx e f
|
||||
compare0' ctx e@(B _) f _ _ = clashE ctx e f
|
||||
compare0' ctx e@(B i {}) f@(B j {}) _ _ =
|
||||
unless (i == j) $ clashE e.loc ctx e f
|
||||
compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (e :@ s) (f :@ t) ne nf =
|
||||
-- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
|
||||
-- Ψ | Γ ⊢ s = t ⇐ A
|
||||
-- -------------------------------
|
||||
-- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
|
||||
compare0' ctx (App e s eloc) (App f t floc) ne nf =
|
||||
local_ Equal $ do
|
||||
compare0 ctx e f
|
||||
(_, arg, _) <- expectPi defs ctx =<<
|
||||
(_, arg, _) <- expectPi defs ctx eloc =<<
|
||||
computeElimTypeE defs ctx e @{noOr1 ne}
|
||||
Term.compare0 ctx arg s t
|
||||
compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
|
||||
compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (CasePair epi e eret ebody)
|
||||
(CasePair fpi f fret fbody) ne nf =
|
||||
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
|
||||
-- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
|
||||
-- Ψ | Γ, x : A, y : B ⊢ s = t ⇐ Q[((x, y) ∷ (x : A) × B)/p]
|
||||
-- -----------------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
|
||||
-- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
|
||||
compare0' ctx (CasePair epi e eret ebody eloc)
|
||||
(CasePair fpi f fret fbody {}) ne nf =
|
||||
local_ Equal $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
||||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||||
(fst, snd) <- expectSig defs ctx ety
|
||||
(fst, snd) <- expectSig defs ctx eloc ety
|
||||
let [< x, y] = ebody.names
|
||||
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
|
||||
(substCasePairRet ety eret)
|
||||
(substCasePairRet ebody.names ety eret)
|
||||
ebody.term fbody.term
|
||||
expectEqualQ epi fpi
|
||||
compare0' ctx e@(CasePair {}) f _ _ = clashE ctx e f
|
||||
expectEqualQ e.loc epi fpi
|
||||
compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (CaseEnum epi e eret earms)
|
||||
(CaseEnum fpi f fret farms) ne nf =
|
||||
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
|
||||
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
|
||||
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
|
||||
-- --------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
|
||||
-- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
|
||||
compare0' ctx (CaseEnum epi e eret earms eloc)
|
||||
(CaseEnum fpi f fret farms floc) ne nf =
|
||||
local_ Equal $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
||||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||||
for_ !(expectEnum defs ctx ety) $ \t =>
|
||||
compare0 ctx (sub1 eret $ Tag t :# ety)
|
||||
!(lookupArm t earms) !(lookupArm t farms)
|
||||
expectEqualQ epi fpi
|
||||
for_ !(expectEnum defs ctx eloc ety) $ \t => do
|
||||
l <- lookupArm eloc t earms
|
||||
r <- lookupArm floc t farms
|
||||
compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
|
||||
expectEqualQ eloc epi fpi
|
||||
where
|
||||
lookupArm : TagVal -> CaseEnumArms d n -> Equal (Term d n)
|
||||
lookupArm t arms = case lookup t arms of
|
||||
lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
|
||||
lookupArm loc t arms = case lookup t arms of
|
||||
Just arm => pure arm
|
||||
Nothing => throw $ TagNotIn t (fromList $ keys arms)
|
||||
compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
|
||||
Nothing => throw $ TagNotIn loc t (fromList $ keys arms)
|
||||
compare0' ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (CaseNat epi epi' e eret ezer esuc)
|
||||
(CaseNat fpi fpi' f fret fzer fsuc) ne nf =
|
||||
-- Ψ | Γ ⊢ e = f ⇒ ℕ
|
||||
-- Ψ | Γ, x : ℕ ⊢ Q = R
|
||||
-- Ψ | Γ ⊢ s₀ = t₀ ⇐ Q[(0 ∷ ℕ)/x]
|
||||
-- Ψ | Γ, x : ℕ, y : Q ⊢ s₁ = t₁ ⇐ Q[(succ x ∷ ℕ)/x]
|
||||
-- -----------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
|
||||
-- = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
|
||||
-- ⇒ Q[e/x]
|
||||
compare0' ctx (CaseNat epi epi' e eret ezer esuc eloc)
|
||||
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
|
||||
local_ Equal $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
||||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||||
compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
|
||||
compare0 ctx
|
||||
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
|
||||
ezer fzer
|
||||
let [< p, ih] = esuc.names
|
||||
compare0 (extendTyN [< (epi, p, Nat), (epi', ih, eret.term)] ctx)
|
||||
(substCaseSuccRet eret)
|
||||
esuc.term fsuc.term
|
||||
expectEqualQ epi fpi
|
||||
expectEqualQ epi' fpi'
|
||||
compare0' ctx e@(CaseNat {}) f _ _ = clashE ctx e f
|
||||
compare0
|
||||
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
|
||||
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
|
||||
expectEqualQ e.loc epi fpi
|
||||
expectEqualQ e.loc epi' fpi'
|
||||
compare0' ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (CaseBox epi e eret ebody)
|
||||
(CaseBox fpi f fret fbody) ne nf =
|
||||
-- Ψ | Γ ⊢ e = f ⇒ [ρ. A]
|
||||
-- Ψ | Γ, x : [ρ. A] ⊢ Q = R
|
||||
-- Ψ | Γ, x : A ⊢ s = t ⇐ Q[([x] ∷ [ρ. A])/x]
|
||||
-- --------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
|
||||
-- = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
|
||||
compare0' ctx (CaseBox epi e eret ebody eloc)
|
||||
(CaseBox fpi f fret fbody floc) ne nf =
|
||||
local_ Equal $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
|
||||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||||
(q, ty) <- expectBOX defs ctx ety
|
||||
(q, ty) <- expectBOX defs ctx eloc ety
|
||||
compare0 (extendTy (epi * q) ebody.name ty ctx)
|
||||
(substCaseBoxRet ety eret)
|
||||
(substCaseBoxRet ebody.name ety eret)
|
||||
ebody.term fbody.term
|
||||
expectEqualQ epi fpi
|
||||
compare0' ctx e@(CaseBox {}) f _ _ = clashE ctx e f
|
||||
expectEqualQ eloc epi fpi
|
||||
compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (s :# a) (t :# b) _ _ =
|
||||
-- Ψ | Γ ⊢ s <: t : B
|
||||
-- --------------------------------
|
||||
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
|
||||
--
|
||||
-- and similar for :> and A
|
||||
compare0' ctx (Ann s a _) (Ann t b _) _ _ =
|
||||
let ty = case !mode of Super => a; _ => b in
|
||||
Term.compare0 ctx ty s t
|
||||
|
||||
compare0' ctx (Coe ty1 p1 q1 (E val1)) (Coe ty2 p2 q2 (E val2)) ne nf = do
|
||||
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
|
||||
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
|
||||
-- Ψ | Γ ⊢ e <: f ⇒ _
|
||||
-- (non-neutral forms have the coercion already pushed in)
|
||||
-- -----------------------------------------------------------
|
||||
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
|
||||
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
|
||||
compare0' ctx (Coe ty1 p1 q1 (E val1) _)
|
||||
(Coe ty2 p2 q2 (E val2) _) ne nf = do
|
||||
compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
|
||||
compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
|
||||
compare0 ctx val1 val2
|
||||
compare0' ctx e@(Coe {}) f _ _ = clashE ctx e f
|
||||
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (Comp _ _ _ _ (K _) _ _) _ ne _ = void $ absurd $ noOr2 ne
|
||||
compare0' ctx (Comp _ _ _ _ (B i) _ _) _ _ _ = absurd i
|
||||
compare0' ctx _ (Comp _ _ _ _ (K _) _ _) _ nf = void $ absurd $ noOr2 nf
|
||||
-- (no neutral compositions in a closed dctx)
|
||||
compare0' _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
|
||||
compare0' _ (Comp {r = B i _, _}) _ _ _ = absurd i
|
||||
compare0' _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
|
||||
|
||||
compare0' ctx (TypeCase ty1 ret1 arms1 def1)
|
||||
(TypeCase ty2 ret2 arms2 def2)
|
||||
ne _ =
|
||||
compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
|
||||
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
|
||||
local_ Equal $ do
|
||||
compare0 ctx ty1 ty2
|
||||
u <- expectTYPE defs ctx =<< computeElimTypeE defs ctx ty1 @{noOr1 ne}
|
||||
u <- expectTYPE defs ctx eloc =<<
|
||||
computeElimTypeE defs ctx ty1 @{noOr1 ne}
|
||||
compareType ctx ret1 ret2
|
||||
compareType ctx def1 def2
|
||||
for_ allKinds $ \k =>
|
||||
compareArm ctx k ret1 u
|
||||
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
|
||||
compare0' ctx e@(TypeCase {}) f _ _ = clashE ctx e f
|
||||
compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
|
||||
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
|
||||
compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f
|
||||
compare0' ctx (Ann s a _) f _ _ = Term.compare0 ctx a s (E f)
|
||||
compare0' ctx e (Ann t b _) _ _ = Term.compare0 ctx b (E e) t
|
||||
compare0' ctx e@(Ann {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
||| compare two type-case branches, which came from the arms of the given
|
||||
||| kind. `ret` is the return type of the case expression, and `u` is the
|
||||
|
|
@ -500,7 +576,7 @@ parameters (defs : Definitions)
|
|||
(ret : Term 0 n) -> (u : Universe) ->
|
||||
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
|
||||
(def : Term 0 n) ->
|
||||
Equal ()
|
||||
Equal_ ()
|
||||
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
|
||||
compareArm ctx k ret u b1 b2 def =
|
||||
let def = SN def in
|
||||
|
|
@ -510,22 +586,22 @@ parameters (defs : Definitions)
|
|||
compareArm_ : EqContext n -> (k : TyConKind) ->
|
||||
(ret : Term 0 n) -> (u : Universe) ->
|
||||
(b1, b2 : TypeCaseArmBody k 0 n) ->
|
||||
Equal ()
|
||||
Equal_ ()
|
||||
compareArm_ ctx KTYPE ret u b1 b2 =
|
||||
compare0 ctx ret b1.term b2.term
|
||||
|
||||
compareArm_ ctx KPi ret u b1 b2 = do
|
||||
let [< a, b] = b1.names
|
||||
ctx = extendTyN
|
||||
[< (Zero, a, TYPE u),
|
||||
(Zero, b, Arr Zero (BVT 0) (TYPE u))] ctx
|
||||
[< (Zero, a, TYPE u a.loc),
|
||||
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
|
||||
compare0 ctx (weakT 2 ret) b1.term b2.term
|
||||
|
||||
compareArm_ ctx KSig ret u b1 b2 = do
|
||||
let [< a, b] = b1.names
|
||||
ctx = extendTyN
|
||||
[< (Zero, a, TYPE u),
|
||||
(Zero, b, Arr Zero (BVT 0) (TYPE u))] ctx
|
||||
[< (Zero, a, TYPE u a.loc),
|
||||
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
|
||||
compare0 ctx (weakT 2 ret) b1.term b2.term
|
||||
|
||||
compareArm_ ctx KEnum ret u b1 b2 =
|
||||
|
|
@ -534,70 +610,76 @@ parameters (defs : Definitions)
|
|||
compareArm_ ctx KEq ret u b1 b2 = do
|
||||
let [< a0, a1, a, l, r] = b1.names
|
||||
ctx = extendTyN
|
||||
[< (Zero, a0, TYPE u),
|
||||
(Zero, a1, TYPE u),
|
||||
(Zero, a, Eq0 (TYPE u) (BVT 1) (BVT 0)),
|
||||
(Zero, l, BVT 2),
|
||||
(Zero, r, BVT 2)] ctx
|
||||
[< (Zero, a0, TYPE u a0.loc),
|
||||
(Zero, a1, TYPE u a1.loc),
|
||||
(Zero, a, Eq0 (TYPE u a.loc)
|
||||
(BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
|
||||
(Zero, l, BVT 2 a0.loc),
|
||||
(Zero, r, BVT 2 a1.loc)] ctx
|
||||
compare0 ctx (weakT 5 ret) b1.term b2.term
|
||||
|
||||
compareArm_ ctx KNat ret u b1 b2 =
|
||||
compare0 ctx ret b1.term b2.term
|
||||
|
||||
compareArm_ ctx KBOX ret u b1 b2 = do
|
||||
let ctx = extendTy Zero b1.name (TYPE u) ctx
|
||||
let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx
|
||||
compare0 ctx (weakT 1 ret) b1.term b1.term
|
||||
|
||||
|
||||
parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
|
||||
parameters (loc : Loc) (ctx : TyContext d n)
|
||||
-- [todo] only split on the dvars that are actually used anywhere in
|
||||
-- the calls to `splits`
|
||||
|
||||
parameters (mode : EqMode)
|
||||
private
|
||||
fromEqual_ : Equal_ a -> Equal a
|
||||
fromEqual_ act = lift $ evalState mode act
|
||||
|
||||
private
|
||||
eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f ()
|
||||
eachFace act =
|
||||
for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th
|
||||
|
||||
private
|
||||
runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
|
||||
Equal ()
|
||||
runCompare act = fromEqual_ $ eachFace $ act !defs
|
||||
|
||||
namespace Term
|
||||
export covering
|
||||
compare : (ty, s, t : Term d n) -> Eff fs ()
|
||||
compare ty s t =
|
||||
map fst $ runState @{Z} mode $
|
||||
for_ (splits ctx.dctx) $ \th =>
|
||||
let ectx = makeEqContext ctx th in
|
||||
lift $ compare0 !defs ectx (ty // th) (s // th) (t // th)
|
||||
compare : (ty, s, t : Term d n) -> Equal ()
|
||||
compare ty s t = runCompare $ \defs, ectx, th =>
|
||||
compare0 defs ectx (ty // th) (s // th) (t // th)
|
||||
|
||||
export covering
|
||||
compareType : (s, t : Term d n) -> Eff fs ()
|
||||
compareType s t =
|
||||
map fst $ runState @{Z} mode $
|
||||
for_ (splits ctx.dctx) $ \th =>
|
||||
let ectx = makeEqContext ctx th in
|
||||
lift $ compareType !defs ectx (s // th) (t // th)
|
||||
compareType : (s, t : Term d n) -> Equal ()
|
||||
compareType s t = runCompare $ \defs, ectx, th =>
|
||||
compareType defs ectx (s // th) (t // th)
|
||||
|
||||
namespace Elim
|
||||
||| you don't have to pass the type in but the arguments must still be
|
||||
||| of the same type!!
|
||||
export covering %inline
|
||||
compare : (e, f : Elim d n) -> Eff fs ()
|
||||
compare e f =
|
||||
map fst $ runState @{Z} mode $
|
||||
for_ (splits ctx.dctx) $ \th =>
|
||||
let ectx = makeEqContext ctx th in
|
||||
lift $ compare0 !defs ectx (e // th) (f // th)
|
||||
export covering
|
||||
compare : (e, f : Elim d n) -> Equal ()
|
||||
compare e f = runCompare $ \defs, ectx, th =>
|
||||
compare0 defs ectx (e // th) (f // th)
|
||||
|
||||
namespace Term
|
||||
export covering %inline
|
||||
equal, sub, super : (ty, s, t : Term d n) -> Eff fs ()
|
||||
equal, sub, super : (ty, s, t : Term d n) -> Equal ()
|
||||
equal = compare Equal
|
||||
sub = compare Sub
|
||||
super = compare Super
|
||||
|
||||
export covering %inline
|
||||
equalType, subtype, supertype : (s, t : Term d n) -> Eff fs ()
|
||||
equalType, subtype, supertype : (s, t : Term d n) -> Equal ()
|
||||
equalType = compareType Equal
|
||||
subtype = compareType Sub
|
||||
supertype = compareType Super
|
||||
|
||||
namespace Elim
|
||||
export covering %inline
|
||||
equal, sub, super : (e, f : Elim d n) -> Eff fs ()
|
||||
equal, sub, super : (e, f : Elim d n) -> Equal ()
|
||||
equal = compare Equal
|
||||
sub = compare Sub
|
||||
super = compare Super
|
||||
|
|
|
|||
108
lib/Quox/Loc.idr
108
lib/Quox/Loc.idr
|
|
@ -1,7 +1,8 @@
|
|||
||| file locations
|
||||
module Quox.Loc
|
||||
|
||||
import Text.Bounded
|
||||
import public Text.Bounded
|
||||
import Data.SortedMap
|
||||
import Derive.Prelude
|
||||
|
||||
%default total
|
||||
|
|
@ -11,53 +12,110 @@ public export
|
|||
FileName : Type
|
||||
FileName = String
|
||||
|
||||
%runElab derive "Bounds" [Ord]
|
||||
|
||||
public export
|
||||
record Loc' where
|
||||
data Loc_ = NoLoc | YesLoc FileName Bounds
|
||||
%name Loc_ loc
|
||||
%runElab derive "Loc_" [Eq, Ord, Show]
|
||||
|
||||
|
||||
||| a wrapper for locations which are always considered equal
|
||||
public export
|
||||
record Loc where
|
||||
constructor L
|
||||
fname : FileName
|
||||
startLine, startCol, endLine, endCol : Int
|
||||
%name Loc' loc
|
||||
%runElab derive "Loc'" [Eq, Ord, Show]
|
||||
val : Loc_
|
||||
%name Loc loc
|
||||
%runElab derive "Loc" [Show]
|
||||
|
||||
public export
|
||||
Loc : Type
|
||||
Loc = Maybe Loc'
|
||||
export %inline Eq Loc where _ == _ = True
|
||||
export %inline Ord Loc where compare _ _ = EQ
|
||||
|
||||
export
|
||||
public export %inline
|
||||
noLoc : Loc
|
||||
noLoc = L NoLoc
|
||||
|
||||
public export %inline
|
||||
makeLoc : FileName -> Bounds -> Loc
|
||||
makeLoc fname (MkBounds {startLine, startCol, endLine, endCol}) =
|
||||
Just $ L {fname, startLine, startCol, endLine, endCol}
|
||||
makeLoc = L .: YesLoc
|
||||
|
||||
|
||||
export
|
||||
onlyStart_ : Loc_ -> Loc_
|
||||
onlyStart_ NoLoc = NoLoc
|
||||
onlyStart_ (YesLoc fname (MkBounds sl sc _ _)) =
|
||||
YesLoc fname $ MkBounds sl sc sl sc
|
||||
|
||||
export %inline
|
||||
onlyStart : Loc -> Loc
|
||||
onlyStart Nothing = Nothing
|
||||
onlyStart (Just (L fname sl sc _ _)) = Just $ L fname sl sc sl sc
|
||||
onlyStart = {val $= onlyStart_}
|
||||
|
||||
export
|
||||
onlyEnd_ : Loc_ -> Loc_
|
||||
onlyEnd_ NoLoc = NoLoc
|
||||
onlyEnd_ (YesLoc fname (MkBounds _ _ el ec)) =
|
||||
YesLoc fname $ MkBounds el ec el ec
|
||||
|
||||
export %inline
|
||||
onlyEnd : Loc -> Loc
|
||||
onlyEnd Nothing = Nothing
|
||||
onlyEnd (Just (L fname _ _ el ec)) = Just $ L fname el ec el ec
|
||||
onlyEnd = {val $= onlyEnd_}
|
||||
|
||||
|
||||
export
|
||||
extend : Loc -> Bounds -> Loc
|
||||
extend Nothing _ = Nothing
|
||||
extend (Just (L fname sl1 sc1 el1 ec1)) (MkBounds sl2 sc2 el2 ec2) =
|
||||
extend_ : Loc_ -> Bounds -> Loc_
|
||||
extend_ NoLoc _ = NoLoc
|
||||
extend_ (YesLoc fname (MkBounds sl1 sc1 el1 ec1)) (MkBounds sl2 sc2 el2 ec2) =
|
||||
let (sl, sc) = (sl1, sc1) `min` (sl2, sc2)
|
||||
(el, ec) = (el1, ec1) `max` (el2, ec2)
|
||||
in
|
||||
Just $ L fname sl sc el ec
|
||||
YesLoc fname $ MkBounds sl sc el ec
|
||||
|
||||
export
|
||||
extend : Loc -> Bounds -> Loc
|
||||
extend l b = L $ extend_ l.val b
|
||||
|
||||
export
|
||||
extend' : Loc -> Maybe Bounds -> Loc
|
||||
extend' l b = maybe l (extend l) b
|
||||
|
||||
|
||||
namespace Loc_
|
||||
export
|
||||
(.bounds) : Loc_ -> Maybe Bounds
|
||||
(YesLoc _ b).bounds = Just b
|
||||
(NoLoc).bounds = Nothing
|
||||
|
||||
namespace Loc
|
||||
export
|
||||
(.bounds) : Loc -> Maybe Bounds
|
||||
l.bounds = l.val.bounds
|
||||
|
||||
export %inline
|
||||
extendL : Loc -> Loc -> Loc
|
||||
extendL l1 l2 = l1 `extend'` l2.bounds
|
||||
|
||||
|
||||
infixr 1 `or_`, `or`
|
||||
export %inline
|
||||
or_ : Loc_ -> Loc_ -> Loc_
|
||||
or_ l1@(YesLoc {}) _ = l1
|
||||
or_ NoLoc l2 = l2
|
||||
|
||||
export %inline
|
||||
or : Loc -> Loc -> Loc
|
||||
or (L l1) (L l2) = L $ l1 `or_` l2
|
||||
|
||||
|
||||
public export
|
||||
interface Located a where (.loc) : a -> Loc
|
||||
|
||||
export
|
||||
(.bounds) : Loc -> Maybe Bounds
|
||||
(Just (L {fname, startLine, startCol, endLine, endCol})).bounds =
|
||||
Just $ MkBounds {startLine, startCol, endLine, endCol}
|
||||
(Nothing).bounds = Nothing
|
||||
public export
|
||||
0 Located1 : (a -> Type) -> Type
|
||||
Located1 f = forall x. Located (f x)
|
||||
|
||||
public export
|
||||
interface Located a => Relocatable a where setLoc : Loc -> a -> a
|
||||
|
||||
public export
|
||||
0 Relocatable1 : (a -> Type) -> Type
|
||||
Relocatable1 f = forall x. Relocatable (f x)
|
||||
|
|
|
|||
|
|
@ -1,8 +1,10 @@
|
|||
module Quox.Name
|
||||
|
||||
import Quox.Loc
|
||||
import Quox.CharExtra
|
||||
import public Data.SnocList
|
||||
import Data.List
|
||||
import Control.Eff
|
||||
import Text.Lexer
|
||||
import Derive.Prelude
|
||||
|
||||
|
|
@ -12,16 +14,22 @@ import Derive.Prelude
|
|||
%language ElabReflection
|
||||
|
||||
|
||||
public export
|
||||
NameSuf : Type
|
||||
NameSuf = Nat
|
||||
|
||||
public export
|
||||
data BaseName
|
||||
= UN String -- user-given name
|
||||
| Unused -- "_"
|
||||
= UN String -- user-given name
|
||||
| MN String NameSuf -- machine-generated name
|
||||
| Unused -- "_"
|
||||
%runElab derive "BaseName" [Eq, Ord]
|
||||
|
||||
export
|
||||
baseStr : BaseName -> String
|
||||
baseStr (UN x) = x
|
||||
baseStr Unused = "_"
|
||||
baseStr (UN x) = x
|
||||
baseStr (MN x i) = "\{x}#\{show i}"
|
||||
baseStr Unused = "_"
|
||||
|
||||
export Show BaseName where show = baseStr
|
||||
export FromString BaseName where fromString = UN
|
||||
|
|
@ -83,6 +91,17 @@ export FromString PName where fromString = MakePName [<]
|
|||
export FromString Name where fromString = fromPBaseName
|
||||
|
||||
|
||||
public export
|
||||
record BindName where
|
||||
constructor BN
|
||||
name : BaseName
|
||||
loc_ : Loc
|
||||
%runElab derive "BindName" [Eq, Ord, Show]
|
||||
|
||||
export Located BindName where n.loc = n.loc_
|
||||
export Relocatable BindName where setLoc loc (BN x _) = BN x loc
|
||||
|
||||
|
||||
export
|
||||
toDotsP : PName -> String
|
||||
toDotsP x = fastConcat $ cast $ map (<+> ".") x.mods :< x.base
|
||||
|
|
@ -140,3 +159,41 @@ isName str =
|
|||
case scan name [] (unpack str) of
|
||||
Just (_, []) => True
|
||||
_ => False
|
||||
|
||||
|
||||
public export
|
||||
data GenTag = GEN
|
||||
|
||||
public export
|
||||
NameGen : Type -> Type
|
||||
NameGen = StateL GEN NameSuf
|
||||
|
||||
export
|
||||
runNameGenWith : Has NameGen fs =>
|
||||
NameSuf -> Eff fs a -> Eff (fs - NameGen) (a, NameSuf)
|
||||
runNameGenWith = runStateAt GEN
|
||||
|
||||
export
|
||||
runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
|
||||
runNameGen = map fst . runNameGenWith 0
|
||||
|
||||
||| generate a fresh name with the given base
|
||||
export
|
||||
mn : Has NameGen fs => PBaseName -> Eff fs BaseName
|
||||
mn base = do
|
||||
i <- getAt GEN
|
||||
modifyAt GEN S
|
||||
pure $ MN base i
|
||||
|
||||
||| generate a fresh binding name with the given base and
|
||||
||| (optionally) location `loc`
|
||||
export
|
||||
mnb : Has NameGen fs =>
|
||||
PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName
|
||||
mnb base = pure $ BN !(mn base) loc
|
||||
|
||||
export
|
||||
fresh : Has NameGen fs => BindName -> Eff fs BindName
|
||||
fresh (BN (UN str) loc) = mnb str {loc}
|
||||
fresh (BN (MN str k) loc) = mnb str {loc}
|
||||
fresh (BN Unused loc) = mnb "x" {loc}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
||| take freshly-parsed input, translate it to core, and check it
|
||||
||| take freshly-parsed input, scope check, type check, add to env
|
||||
module Quox.Parser.FromParser
|
||||
|
||||
import Quox.Parser.Syntax
|
||||
|
|
@ -41,19 +41,19 @@ data StateTag = NS | SEEN
|
|||
public export
|
||||
FromParserPure : List (Type -> Type)
|
||||
FromParserPure =
|
||||
[Except Error, StateL DEFS Definitions, StateL NS Mods]
|
||||
[Except Error, DefsState, StateL NS Mods, NameGen]
|
||||
|
||||
public export
|
||||
FromParserEff : List (Type -> Type)
|
||||
FromParserEff =
|
||||
[Except Error, StateL DEFS Definitions, StateL NS Mods,
|
||||
Reader IncludePath, StateL SEEN SeenFiles, IO]
|
||||
LoadFile' : List (Type -> Type)
|
||||
LoadFile' = [IO, StateL SEEN SeenFiles, Reader IncludePath]
|
||||
|
||||
public export
|
||||
FromParser : Type -> Type
|
||||
FromParser = Eff FromParserEff
|
||||
LoadFile : List (Type -> Type)
|
||||
LoadFile = LoadFile' ++ [Except Error]
|
||||
|
||||
-- [todo] put the locs in the core ast, obv
|
||||
public export
|
||||
FromParserIO : List (Type -> Type)
|
||||
FromParserIO = FromParserPure ++ LoadFile'
|
||||
|
||||
|
||||
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
|
||||
|
|
@ -70,31 +70,32 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
|
|||
export
|
||||
fromPDimWith : Has (Except Error) fs =>
|
||||
Context' PatVar d -> PDim -> Eff fs (Dim d)
|
||||
fromPDimWith ds (K e _) = pure $ K e
|
||||
fromPDimWith ds (V i _) =
|
||||
fromBaseName (pure . B) (const $ throw $ DimNotInScope i) ds i
|
||||
fromPDimWith ds (K e loc) = pure $ K e loc
|
||||
fromPDimWith ds (V i loc) =
|
||||
fromBaseName (\i => pure $ B i loc)
|
||||
(const $ throw $ DimNotInScope loc i) ds i
|
||||
|
||||
private
|
||||
avoidDim : Has (Except Error) fs =>
|
||||
Context' PatVar d -> PName -> Eff fs Name
|
||||
avoidDim ds x =
|
||||
fromName (const $ throw $ DimNameInTerm x.base) (pure . fromPName) ds x
|
||||
Context' PatVar d -> Loc -> PName -> Eff fs Name
|
||||
avoidDim ds loc x =
|
||||
fromName (const $ throw $ DimNameInTerm loc x.base) (pure . fromPName) ds x
|
||||
|
||||
private
|
||||
resolveName : Mods -> Name -> Eff FromParserPure (Term d n)
|
||||
resolveName ns x =
|
||||
resolveName : Mods -> Loc -> Name -> Eff FromParserPure (Term d n)
|
||||
resolveName ns loc x =
|
||||
let here = addMods ns x in
|
||||
if isJust $ lookup here !(getAt DEFS) then
|
||||
pure $ FT here
|
||||
pure $ FT here loc
|
||||
else do
|
||||
let ns :< _ = ns
|
||||
| _ => throw $ TermNotInScope x
|
||||
resolveName ns x
|
||||
| _ => throw $ TermNotInScope loc x
|
||||
resolveName ns loc x
|
||||
|
||||
export
|
||||
fromPatVar : PatVar -> BaseName
|
||||
fromPatVar (Unused _) = Unused
|
||||
fromPatVar (PV x _) = UN x
|
||||
fromPatVar : PatVar -> BindName
|
||||
fromPatVar (Unused loc) = BN Unused loc
|
||||
fromPatVar (PV x loc) = BN (UN x) loc
|
||||
|
||||
export
|
||||
fromPQty : PQty -> Qty
|
||||
|
|
@ -110,93 +111,112 @@ mutual
|
|||
fromPTermWith : Context' PatVar d -> Context' PatVar n ->
|
||||
PTerm -> Eff FromParserPure (Term d n)
|
||||
fromPTermWith ds ns t0 = case t0 of
|
||||
TYPE k _ =>
|
||||
pure $ TYPE k
|
||||
TYPE k loc =>
|
||||
pure $ TYPE k loc
|
||||
|
||||
Pi pi x s t _ =>
|
||||
Pi pi x s t loc =>
|
||||
Pi (fromPQty pi)
|
||||
<$> fromPTermWith ds ns s
|
||||
<*> fromPTermTScope ds ns [< x] t
|
||||
<*> pure loc
|
||||
|
||||
Lam x s _ =>
|
||||
Lam <$> fromPTermTScope ds ns [< x] s
|
||||
Lam x s loc =>
|
||||
Lam <$> fromPTermTScope ds ns [< x] s <*> pure loc
|
||||
|
||||
App s t _ =>
|
||||
map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
|
||||
App s t loc =>
|
||||
map E $ App
|
||||
<$> fromPTermElim ds ns s
|
||||
<*> fromPTermWith ds ns t
|
||||
<*> pure loc
|
||||
|
||||
Sig x s t _ =>
|
||||
Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [< x] t
|
||||
Sig x s t loc =>
|
||||
Sig <$> fromPTermWith ds ns s
|
||||
<*> fromPTermTScope ds ns [< x] t
|
||||
<*> pure loc
|
||||
|
||||
Pair s t _ =>
|
||||
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
|
||||
Pair s t loc =>
|
||||
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure loc
|
||||
|
||||
Case pi pair (r, ret) (CasePair (x, y) body _) _ =>
|
||||
Case pi pair (r, ret) (CasePair (x, y) body _) loc =>
|
||||
map E $ CasePair (fromPQty pi)
|
||||
<$> fromPTermElim ds ns pair
|
||||
<*> fromPTermTScope ds ns [< r] ret
|
||||
<*> fromPTermTScope ds ns [< x, y] body
|
||||
<*> pure loc
|
||||
|
||||
Case pi tag (r, ret) (CaseEnum arms _) _ =>
|
||||
Case pi tag (r, ret) (CaseEnum arms _) loc =>
|
||||
map E $ CaseEnum (fromPQty pi)
|
||||
<$> fromPTermElim ds ns tag
|
||||
<*> fromPTermTScope ds ns [< r] ret
|
||||
<*> assert_total fromPTermEnumArms ds ns arms
|
||||
<*> pure loc
|
||||
|
||||
Nat _ => pure Nat
|
||||
Zero _ => pure Zero
|
||||
Succ n _ => [|Succ $ fromPTermWith ds ns n|]
|
||||
Nat loc => pure $ Nat loc
|
||||
Zero loc => pure $ Zero loc
|
||||
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
|
||||
|
||||
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) _ =>
|
||||
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) loc =>
|
||||
map E $ CaseNat (fromPQty pi) (fromPQty pi')
|
||||
<$> fromPTermElim ds ns nat
|
||||
<*> fromPTermTScope ds ns [< r] ret
|
||||
<*> fromPTermWith ds ns zer
|
||||
<*> fromPTermTScope ds ns [< s, ih] suc
|
||||
<*> pure loc
|
||||
|
||||
Enum strs _ =>
|
||||
Enum strs loc =>
|
||||
let set = SortedSet.fromList strs in
|
||||
if length strs == length (SortedSet.toList set) then
|
||||
pure $ Enum set
|
||||
pure $ Enum set loc
|
||||
else
|
||||
throw $ DuplicatesInEnum strs
|
||||
throw $ DuplicatesInEnum loc strs
|
||||
|
||||
Tag str _ => pure $ Tag str
|
||||
Tag str loc => pure $ Tag str loc
|
||||
|
||||
Eq (i, ty) s t _ =>
|
||||
Eq (i, ty) s t loc =>
|
||||
Eq <$> fromPTermDScope ds ns [< i] ty
|
||||
<*> fromPTermWith ds ns s
|
||||
<*> fromPTermWith ds ns t
|
||||
<*> pure loc
|
||||
|
||||
DLam i s _ =>
|
||||
DLam <$> fromPTermDScope ds ns [< i] s
|
||||
DLam i s loc =>
|
||||
DLam <$> fromPTermDScope ds ns [< i] s <*> pure loc
|
||||
|
||||
DApp s p _ =>
|
||||
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
|
||||
DApp s p loc =>
|
||||
map E $ DApp
|
||||
<$> fromPTermElim ds ns s
|
||||
<*> fromPDimWith ds p
|
||||
<*> pure loc
|
||||
|
||||
BOX q ty _ => BOX (fromPQty q) <$> fromPTermWith ds ns ty
|
||||
BOX q ty loc => BOX (fromPQty q) <$> fromPTermWith ds ns ty <*> pure loc
|
||||
|
||||
Box val _ => Box <$> fromPTermWith ds ns val
|
||||
Box val loc => Box <$> fromPTermWith ds ns val <*> pure loc
|
||||
|
||||
Case pi box (r, ret) (CaseBox b body _) _ =>
|
||||
Case pi box (r, ret) (CaseBox b body _) loc =>
|
||||
map E $ CaseBox (fromPQty pi)
|
||||
<$> fromPTermElim ds ns box
|
||||
<*> fromPTermTScope ds ns [< r] ret
|
||||
<*> fromPTermTScope ds ns [< b] body
|
||||
<*> pure loc
|
||||
|
||||
V x _ =>
|
||||
fromName (pure . E . B) (resolveName !(getAt NS) <=< avoidDim ds) ns x
|
||||
V x loc =>
|
||||
fromName (\i => pure $ E $ B i loc)
|
||||
(resolveName !(getAt NS) loc <=< avoidDim ds loc) ns x
|
||||
|
||||
Ann s a _ =>
|
||||
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
|
||||
Ann s a loc =>
|
||||
map E $ Ann
|
||||
<$> fromPTermWith ds ns s
|
||||
<*> fromPTermWith ds ns a
|
||||
<*> pure loc
|
||||
|
||||
Coe (i, ty) p q val _ =>
|
||||
Coe (i, ty) p q val loc =>
|
||||
map E $ Coe
|
||||
<$> fromPTermDScope ds ns [< i] ty
|
||||
<*> fromPDimWith ds p
|
||||
<*> fromPDimWith ds q
|
||||
<*> fromPTermWith ds ns val
|
||||
<*> pure loc
|
||||
|
||||
Comp (i, ty) p q val r (j0, val0) (j1, val1) _ =>
|
||||
Comp (i, ty) p q val r (j0, val0) (j1, val1) loc =>
|
||||
map E $ CompH'
|
||||
<$> fromPTermDScope ds ns [< i] ty
|
||||
<*> fromPDimWith ds p
|
||||
|
|
@ -205,6 +225,7 @@ mutual
|
|||
<*> fromPDimWith ds r
|
||||
<*> fromPTermDScope ds ns [< j0] val0
|
||||
<*> fromPTermDScope ds ns [< j1] val1
|
||||
<*> pure loc
|
||||
|
||||
private
|
||||
fromPTermEnumArms : Context' PatVar d -> Context' PatVar n ->
|
||||
|
|
@ -221,7 +242,7 @@ mutual
|
|||
case !(fromPTermWith ds ns e) of
|
||||
E e => pure e
|
||||
t => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in
|
||||
throw $ AnnotationNeeded ctx t
|
||||
throw $ AnnotationNeeded t.loc ctx t
|
||||
|
||||
-- [todo] use SN if the var is named but still unused
|
||||
private
|
||||
|
|
@ -251,10 +272,10 @@ fromPTerm = fromPTermWith [<] [<]
|
|||
|
||||
|
||||
export
|
||||
globalPQty : (q : Qty) -> Eff [Except Error] (So $ isGlobal q)
|
||||
globalPQty pi = case choose $ isGlobal pi of
|
||||
globalPQty : Loc -> (q : Qty) -> Eff [Except Error] (So $ isGlobal q)
|
||||
globalPQty loc pi = case choose $ isGlobal pi of
|
||||
Left y => pure y
|
||||
Right _ => throw $ QtyNotGlobal pi
|
||||
Right _ => throw $ QtyNotGlobal loc pi
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -262,30 +283,31 @@ fromPBaseNameNS : PBaseName -> Eff [StateL NS Mods] Name
|
|||
fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name
|
||||
|
||||
private
|
||||
injTC : TC a -> Eff FromParserPure a
|
||||
injTC act = rethrow $ mapFst WrapTypeError $ runTC !(getAt DEFS) act
|
||||
liftTC : TC a -> Eff FromParserPure a
|
||||
liftTC act = do
|
||||
res <- lift $ runExcept $ runReaderAt DEFS !(getAt DEFS) act
|
||||
rethrow $ mapFst WrapTypeError res
|
||||
|
||||
export covering
|
||||
fromPDef : PDefinition -> Eff FromParserPure NDefinition
|
||||
fromPDef (MkPDef qty pname ptype pterm _) = do
|
||||
fromPDef (MkPDef qty pname ptype pterm defLoc) = do
|
||||
name <- lift $ fromPBaseNameNS pname
|
||||
let qty = fromPQty qty
|
||||
qtyGlobal <- lift $ globalPQty qty
|
||||
let gqty = Element qty qtyGlobal
|
||||
let sqty = globalToSubj gqty
|
||||
qtyGlobal <- lift $ globalPQty qty.loc qty.val
|
||||
let gqty = Element qty.val qtyGlobal
|
||||
sqty = globalToSubj gqty
|
||||
type <- lift $ traverse fromPTerm ptype
|
||||
term <- lift $ fromPTerm pterm
|
||||
case type of
|
||||
Just type => do
|
||||
injTC $ checkTypeC empty type Nothing
|
||||
injTC $ ignore $ checkC empty sqty term type
|
||||
let def = mkDef gqty type term
|
||||
liftTC $ checkTypeC empty type Nothing
|
||||
liftTC $ ignore $ checkC empty sqty term type
|
||||
let def = mkDef gqty type term defLoc
|
||||
modifyAt DEFS $ insert name def
|
||||
pure (name, def)
|
||||
Nothing => do
|
||||
let E elim = term | t => throw $ AnnotationNeeded empty t
|
||||
res <- injTC $ inferC empty sqty elim
|
||||
let def = mkDef gqty res.type term
|
||||
let E elim = term | _ => throw $ AnnotationNeeded term.loc empty term
|
||||
res <- liftTC $ inferC empty sqty elim
|
||||
let def = mkDef gqty res.type term defLoc
|
||||
modifyAt DEFS $ insert name def
|
||||
pure (name, def)
|
||||
|
||||
|
|
@ -296,27 +318,23 @@ fromPDecl (PNs ns) =
|
|||
localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
|
||||
|
||||
|
||||
public export
|
||||
LoadFile : List (Type -> Type)
|
||||
LoadFile = [IO, StateL SEEN SeenFiles, Reader IncludePath, Except Error]
|
||||
|
||||
export covering
|
||||
loadFile : String -> Eff LoadFile (Maybe String)
|
||||
loadFile file =
|
||||
loadFile : Loc -> String -> Eff LoadFile (Maybe String)
|
||||
loadFile loc file =
|
||||
if contains file !(getAt SEEN) then
|
||||
pure Nothing
|
||||
else do
|
||||
Just ifile <- firstExists (map (</> file) !ask)
|
||||
| Nothing => throw $ LoadError file FileNotFound
|
||||
| Nothing => throw $ LoadError loc file FileNotFound
|
||||
case !(readFile ifile) of
|
||||
Right res => modifyAt SEEN (insert file) $> Just res
|
||||
Left err => throw $ LoadError ifile err
|
||||
Left err => throw $ LoadError loc ifile err
|
||||
|
||||
mutual
|
||||
export covering
|
||||
loadProcessFile : String -> FromParser (List NDefinition)
|
||||
loadProcessFile file =
|
||||
case !(lift $ loadFile file) of
|
||||
loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
|
||||
loadProcessFile loc file =
|
||||
case !(lift $ loadFile loc file) of
|
||||
Just inp => do
|
||||
tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp
|
||||
concat <$> traverse fromPTopLevel tl
|
||||
|
|
@ -324,26 +342,29 @@ mutual
|
|||
|
||||
||| populates the `defs` field of the state
|
||||
export covering
|
||||
fromPTopLevel : PTopLevel -> FromParser (List NDefinition)
|
||||
fromPTopLevel (PD decl) = lift $ fromPDecl decl
|
||||
fromPTopLevel (PLoad file _) = loadProcessFile file
|
||||
fromPTopLevel : PTopLevel -> Eff FromParserIO (List NDefinition)
|
||||
fromPTopLevel (PD decl) = lift $ fromPDecl decl
|
||||
fromPTopLevel (PLoad file loc) = loadProcessFile loc file
|
||||
|
||||
export
|
||||
fromParserPure : Definitions ->
|
||||
fromParserPure : NameSuf -> Definitions ->
|
||||
Eff FromParserPure a ->
|
||||
Either Error (a, Definitions)
|
||||
fromParserPure defs act =
|
||||
(Either Error (a, Definitions), NameSuf)
|
||||
fromParserPure suf defs act =
|
||||
extract $
|
||||
runStateAt GEN suf $
|
||||
runExcept $
|
||||
evalStateAt NS [<] $
|
||||
runStateAt DEFS defs act
|
||||
|
||||
export
|
||||
fromParserIO : (MonadRec io, HasIO io) =>
|
||||
IncludePath -> IORef SeenFiles -> IORef Definitions ->
|
||||
FromParser a -> io (Either Error a)
|
||||
fromParserIO inc seen defs act =
|
||||
IncludePath ->
|
||||
IORef SeenFiles -> IORef NameSuf -> IORef Definitions ->
|
||||
Eff FromParserIO a -> io (Either Error a)
|
||||
fromParserIO inc seen suf defs act =
|
||||
runIO $
|
||||
runStateIORefAt GEN suf $
|
||||
runExcept $
|
||||
evalStateAt NS [<] $
|
||||
runStateIORefAt SEEN seen $
|
||||
|
|
|
|||
|
|
@ -18,33 +18,24 @@ ParseError = Parser.Error
|
|||
|
||||
public export
|
||||
data Error =
|
||||
AnnotationNeeded (NameContexts d n) (Term d n)
|
||||
| DuplicatesInEnum (List TagVal)
|
||||
| TermNotInScope Name
|
||||
| DimNotInScope PBaseName
|
||||
| QtyNotGlobal Qty
|
||||
| DimNameInTerm PBaseName
|
||||
AnnotationNeeded Loc (NameContexts d n) (Term d n)
|
||||
| DuplicatesInEnum Loc (List TagVal)
|
||||
| TermNotInScope Loc Name
|
||||
| DimNotInScope Loc PBaseName
|
||||
| QtyNotGlobal Loc Qty
|
||||
| DimNameInTerm Loc PBaseName
|
||||
| WrapTypeError TypeError
|
||||
| LoadError String FileError
|
||||
| LoadError Loc String FileError
|
||||
| WrapParseError String ParseError
|
||||
|
||||
|
||||
parameters (unicode, showContext : Bool)
|
||||
export
|
||||
prettyBounds : String -> Bounds -> Doc HL
|
||||
prettyBounds file (MkBounds l1 c1 l2 c2) =
|
||||
hcat [hl Free $ pretty file, hl Delim ":",
|
||||
hl TVar $ pretty l1, hl Delim ":",
|
||||
hl DVar $ pretty c1, hl Delim "-",
|
||||
hl TVar $ pretty l2, hl Delim ":",
|
||||
hl DVar $ pretty c2]
|
||||
|
||||
export
|
||||
prettyParseError1 : String -> ParsingError _ -> Doc HL
|
||||
prettyParseError1 file (Error msg Nothing) =
|
||||
pretty msg
|
||||
prettyParseError1 file (Error msg (Just bounds)) =
|
||||
asep [prettyBounds file bounds <+> hl Delim ":", pretty msg]
|
||||
hsep [prettyLoc $ makeLoc file bounds, pretty msg]
|
||||
|
||||
export
|
||||
prettyParseError : String -> ParseError -> Doc HL
|
||||
|
|
@ -56,33 +47,38 @@ parameters (unicode, showContext : Bool)
|
|||
|
||||
export
|
||||
prettyError : Error -> Doc HL
|
||||
prettyError (AnnotationNeeded ctx tm) =
|
||||
sep ["the term", prettyTerm unicode ctx.dnames ctx.tnames tm,
|
||||
prettyError (AnnotationNeeded loc ctx tm) =
|
||||
sep [prettyLoc loc <++> "the term",
|
||||
prettyTerm unicode ctx.dnames ctx.tnames tm,
|
||||
"needs a type annotation"]
|
||||
-- [todo] print the original PTerm instead
|
||||
|
||||
prettyError (DuplicatesInEnum tags) =
|
||||
sep ["duplicate tags in enum type", braces $ fillSep $ map pretty tags]
|
||||
prettyError (DuplicatesInEnum loc tags) =
|
||||
sep [prettyLoc loc <++> "duplicate tags in enum type",
|
||||
braces $ fillSep $ map pretty tags]
|
||||
|
||||
prettyError (DimNotInScope i) =
|
||||
sep ["dimension", pretty0 unicode $ DV $ fromString i, "not in scope"]
|
||||
prettyError (DimNotInScope loc i) =
|
||||
sep [prettyLoc loc <++> "dimension",
|
||||
pretty0 unicode $ DV $ fromString i, "not in scope"]
|
||||
|
||||
prettyError (TermNotInScope x) =
|
||||
sep ["term variable", pretty0 unicode $ F x {d = 0, n = 0}, "not in scope"]
|
||||
prettyError (TermNotInScope loc x) =
|
||||
sep [prettyLoc loc <++> "term variable",
|
||||
hl Free $ pretty0 unicode x, "not in scope"]
|
||||
|
||||
prettyError (QtyNotGlobal pi) =
|
||||
sep ["quantity", pretty0 unicode pi,
|
||||
prettyError (QtyNotGlobal loc pi) =
|
||||
sep [prettyLoc loc <++> "quantity", pretty0 unicode pi,
|
||||
"can't be used on a top level declaration"]
|
||||
|
||||
prettyError (DimNameInTerm i) =
|
||||
sep ["dimension variable", pretty0 unicode $ DV $ fromString i,
|
||||
"used in a term context"]
|
||||
prettyError (DimNameInTerm loc i) =
|
||||
sep [prettyLoc loc <++> "dimension variable",
|
||||
pretty0 unicode $ DV $ fromString i, "used in a term context"]
|
||||
|
||||
prettyError (WrapTypeError err) =
|
||||
Typing.prettyError unicode showContext $ trimContext 2 err
|
||||
|
||||
prettyError (LoadError str err) =
|
||||
vsep [hsep ["couldn't load file", pretty str], fromString $ show err]
|
||||
prettyError (LoadError loc str err) =
|
||||
vsep [hsep [prettyLoc loc, "couldn't load file", pretty str],
|
||||
fromString $ show err]
|
||||
|
||||
prettyError (WrapParseError file err) =
|
||||
prettyParseError file err
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ lexParseWith grm input = do
|
|||
export
|
||||
withLoc : {c : Bool} -> FileName -> (Grammar c (Loc -> a)) -> Grammar c a
|
||||
withLoc fname act = bounds act <&> \res =>
|
||||
if res.isIrrelevant then res.val Nothing
|
||||
if res.isIrrelevant then res.val noLoc
|
||||
else res.val $ makeLoc fname res.bounds
|
||||
|
||||
export
|
||||
|
|
@ -241,40 +241,40 @@ casePat fname = withLoc fname $
|
|||
<|> delim "[" "]" [|PBox (patVar fname)|]
|
||||
<|> fatalError "invalid pattern"
|
||||
|
||||
export covering
|
||||
export
|
||||
term : FileName -> Grammar True PTerm
|
||||
-- defined after all the subterm parsers
|
||||
|
||||
export covering
|
||||
export
|
||||
typeLine : FileName -> Grammar True (PatVar, PTerm)
|
||||
typeLine fname = do
|
||||
resC "["
|
||||
mustWork $ do
|
||||
i <- patVar fname <* resC "⇒" <|> unused fname
|
||||
t <- term fname <* needRes "]"
|
||||
t <- assert_total term fname <* needRes "]"
|
||||
pure (i, t)
|
||||
|
||||
||| box term `[t]` or type `[π.A]`
|
||||
export covering
|
||||
export
|
||||
boxTerm : FileName -> Grammar True PTerm
|
||||
boxTerm fname = withLoc fname $ do
|
||||
res "["; commit
|
||||
q <- optional $ qty fname <* res "."
|
||||
t <- mustWork $ term fname <* needRes "]"
|
||||
q <- optional $ qty fname <* res "."
|
||||
t <- mustWork $ assert_total term fname <* needRes "]"
|
||||
pure $ maybe (Box t) (\q => BOX q t) q
|
||||
|
||||
||| tuple term like `(a, b)`, or parenthesised single term.
|
||||
||| allows terminating comma. more than two elements are nested on the right:
|
||||
||| `(a, b, c, d) = (a, (b, (c, d)))`.
|
||||
export covering
|
||||
export
|
||||
tupleTerm : FileName -> Grammar True PTerm
|
||||
tupleTerm fname = withLoc fname $ do
|
||||
terms <- delimSep1 "(" ")" "," $ term fname
|
||||
terms <- delimSep1 "(" ")" "," $ assert_total term fname
|
||||
pure $ \loc => foldr1 (\s, t => Pair s t loc) terms
|
||||
|
||||
||| argument/atomic term: single-token terms, or those with delimiters e.g.
|
||||
||| `[t]`
|
||||
export covering
|
||||
export
|
||||
termArg : FileName -> Grammar True PTerm
|
||||
termArg fname = withLoc fname $
|
||||
[|TYPE universe1|]
|
||||
|
|
@ -287,7 +287,7 @@ termArg fname = withLoc fname $
|
|||
<|> [|V qname|]
|
||||
<|> const <$> tupleTerm fname
|
||||
|
||||
export covering
|
||||
export
|
||||
coeTerm : FileName -> Grammar True PTerm
|
||||
coeTerm fname = withLoc fname $ do
|
||||
resC "coe"
|
||||
|
|
@ -298,9 +298,11 @@ public export
|
|||
CompBranch : Type
|
||||
CompBranch = (DimConst, PatVar, PTerm)
|
||||
|
||||
export covering
|
||||
export
|
||||
compBranch : FileName -> Grammar True CompBranch
|
||||
compBranch fname = [|(,,) dimConst (patVar fname) (needRes "⇒" *> term fname)|]
|
||||
compBranch fname =
|
||||
[|(,,) dimConst (patVar fname)
|
||||
(needRes "⇒" *> assert_total term fname)|]
|
||||
|
||||
private
|
||||
checkCompTermBody : (PatVar, PTerm) -> PDim -> PDim -> PTerm -> PDim ->
|
||||
|
|
@ -313,7 +315,7 @@ checkCompTermBody a p q s r (e0, s0) (e1, s1) bounds =
|
|||
(_, _) =>
|
||||
fatalLoc bounds "body of 'comp' needs one 0 case and one 1 case"
|
||||
|
||||
export covering
|
||||
export
|
||||
compTerm : FileName -> Grammar True PTerm
|
||||
compTerm fname = withLoc fname $ do
|
||||
resC "comp"
|
||||
|
|
@ -328,27 +330,27 @@ compTerm fname = withLoc fname $ do
|
|||
let body = bounds $ mergeBounds bodyStart bodyEnd
|
||||
checkCompTermBody a p q s r s0 s1 body
|
||||
|
||||
export covering
|
||||
export
|
||||
splitUniverseTerm : FileName -> Grammar True PTerm
|
||||
splitUniverseTerm fname = withLoc fname $ resC "★" *> mustWork [|TYPE nat|]
|
||||
|
||||
export covering
|
||||
export
|
||||
eqTerm : FileName -> Grammar True PTerm
|
||||
eqTerm fname = withLoc fname $
|
||||
resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
|
||||
|
||||
export covering
|
||||
export
|
||||
succTerm : FileName -> Grammar True PTerm
|
||||
succTerm fname = withLoc fname $
|
||||
resC "succ" *> mustWork [|Succ (termArg fname)|]
|
||||
|
||||
||| a dimension argument with an `@` prefix, or
|
||||
||| a term argument with no prefix
|
||||
export covering
|
||||
export
|
||||
anyArg : FileName -> Grammar True (Either PDim PTerm)
|
||||
anyArg fname = dimArg fname <||> termArg fname
|
||||
|
||||
export covering
|
||||
export
|
||||
normalAppTerm : FileName -> Grammar True PTerm
|
||||
normalAppTerm fname = withLoc fname $ do
|
||||
head <- termArg fname
|
||||
|
|
@ -360,7 +362,7 @@ where ap : Loc -> PTerm -> Either PDim PTerm -> PTerm
|
|||
|
||||
||| application term `f x @y z`, or other terms that look like application
|
||||
||| like `succ` or `coe`.
|
||||
export covering
|
||||
export
|
||||
appTerm : FileName -> Grammar True PTerm
|
||||
appTerm fname =
|
||||
coeTerm fname
|
||||
|
|
@ -370,53 +372,55 @@ appTerm fname =
|
|||
<|> succTerm fname
|
||||
<|> normalAppTerm fname
|
||||
|
||||
export covering
|
||||
export
|
||||
infixEqTerm : FileName -> Grammar True PTerm
|
||||
infixEqTerm fname = withLoc fname $ do
|
||||
l <- appTerm fname; commit
|
||||
rest <- optional $
|
||||
res "≡" *> [|(,) (term fname) (needRes ":" *> appTerm fname)|]
|
||||
rest <- optional $ res "≡" *>
|
||||
[|(,) (assert_total term fname) (needRes ":" *> appTerm fname)|]
|
||||
let u = Unused $ onlyStart l.loc
|
||||
pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest
|
||||
|
||||
export covering
|
||||
export
|
||||
annTerm : FileName -> Grammar True PTerm
|
||||
annTerm fname = withLoc fname $ do
|
||||
tm <- infixEqTerm fname; commit
|
||||
ty <- optional $ res "∷" *> term fname
|
||||
ty <- optional $ res "∷" *> assert_total term fname
|
||||
pure $ \loc => maybe tm (\ty => Ann tm ty loc) ty
|
||||
|
||||
export covering
|
||||
export
|
||||
lamTerm : FileName -> Grammar True PTerm
|
||||
lamTerm fname = withLoc fname $ do
|
||||
k <- DLam <$ res "δ" <|> Lam <$ res "λ"
|
||||
mustWork $ do
|
||||
xs <- some $ patVar fname; needRes "⇒"
|
||||
body <- term fname; commit
|
||||
xs <- some $ patVar fname; needRes "⇒"
|
||||
body <- assert_total term fname; commit
|
||||
pure $ \loc => foldr (\x, s => k x s loc) body xs
|
||||
|
||||
-- [todo] fix the backtracking in e.g. (F x y z × B)
|
||||
export covering
|
||||
export
|
||||
properBinders : FileName -> Grammar True (List1 PatVar, PTerm)
|
||||
properBinders fname = do
|
||||
properBinders fname = assert_total $ do
|
||||
-- putting assert_total directly on `term`, in this one function,
|
||||
-- doesn't work. i cannot tell why
|
||||
res "("
|
||||
xs <- some $ patVar fname; resC ":"
|
||||
t <- term fname; needRes ")"
|
||||
pure (xs, t)
|
||||
|
||||
export covering
|
||||
export
|
||||
piTerm : FileName -> Grammar True PTerm
|
||||
piTerm fname = withLoc fname $ do
|
||||
q <- qty fname; resC "."
|
||||
dom <- piBinder; needRes "→"
|
||||
cod <- term fname; commit
|
||||
q <- qty fname; resC "."
|
||||
dom <- piBinder; needRes "→"
|
||||
cod <- assert_total term fname; commit
|
||||
pure $ \loc => foldr (\x, t => Pi q x (snd dom) t loc) cod (fst dom)
|
||||
where
|
||||
piBinder : Grammar True (List1 PatVar, PTerm)
|
||||
piBinder = properBinders fname
|
||||
<|> [|(,) [|singleton $ unused fname|] (termArg fname)|]
|
||||
|
||||
export covering
|
||||
export
|
||||
sigmaTerm : FileName -> Grammar True PTerm
|
||||
sigmaTerm fname =
|
||||
(properBinders fname >>= continueDep)
|
||||
|
|
@ -440,9 +444,10 @@ public export
|
|||
PCaseArm : Type
|
||||
PCaseArm = (PCasePat, PTerm)
|
||||
|
||||
export covering
|
||||
export
|
||||
caseArm : FileName -> Grammar True PCaseArm
|
||||
caseArm fname = [|(,) (casePat fname) (needRes "⇒" *> term fname)|]
|
||||
caseArm fname =
|
||||
[|(,) (casePat fname) (needRes "⇒" *> assert_total term fname)|]
|
||||
|
||||
export
|
||||
checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody
|
||||
|
|
@ -468,30 +473,30 @@ checkCaseArms loc ((PBox x _, rhs) :: rest) =
|
|||
if null rest then pure $ CaseBox x rhs loc
|
||||
else fatalError "unexpected pattern after box"
|
||||
|
||||
export covering
|
||||
export
|
||||
caseBody : FileName -> Grammar True PCaseBody
|
||||
caseBody fname = do
|
||||
body <- bounds $ delimSep "{" "}" ";" $ caseArm fname
|
||||
let loc = makeLoc fname body.bounds
|
||||
checkCaseArms loc body.val
|
||||
|
||||
export covering
|
||||
export
|
||||
caseReturn : FileName -> Grammar True (PatVar, PTerm)
|
||||
caseReturn fname = do
|
||||
x <- patVar fname <* resC "⇒" <|> unused fname
|
||||
ret <- term fname
|
||||
ret <- assert_total term fname
|
||||
pure (x, ret)
|
||||
|
||||
export covering
|
||||
export
|
||||
caseTerm : FileName -> Grammar True PTerm
|
||||
caseTerm fname = withLoc fname $ do
|
||||
qty <- caseIntro fname; commit
|
||||
head <- mustWork $ term fname; needRes "return"
|
||||
ret <- mustWork $ caseReturn fname; needRes "of"
|
||||
qty <- caseIntro fname; commit
|
||||
head <- mustWork $ assert_total term fname; needRes "return"
|
||||
ret <- mustWork $ caseReturn fname; needRes "of"
|
||||
body <- mustWork $ caseBody fname
|
||||
pure $ Case qty head ret body
|
||||
|
||||
-- export covering
|
||||
-- export
|
||||
-- term : FileName -> Grammar True PTerm
|
||||
term fname = lamTerm fname
|
||||
<|> caseTerm fname
|
||||
|
|
@ -499,7 +504,7 @@ term fname = lamTerm fname
|
|||
<|> sigmaTerm fname
|
||||
|
||||
|
||||
export covering
|
||||
export
|
||||
decl : FileName -> Grammar True PDecl
|
||||
|
||||
||| `def` alone means `defω`
|
||||
|
|
@ -512,7 +517,7 @@ defIntro fname =
|
|||
let any = PQ Any $ makeLoc fname pos.bounds
|
||||
option any $ qty fname <* needRes "."
|
||||
|
||||
export covering
|
||||
export
|
||||
definition : FileName -> Grammar True PDefinition
|
||||
definition fname = withLoc fname $ do
|
||||
qty <- defIntro fname
|
||||
|
|
@ -522,7 +527,7 @@ definition fname = withLoc fname $ do
|
|||
optRes ";"
|
||||
pure $ MkPDef qty name type term
|
||||
|
||||
export covering
|
||||
export
|
||||
namespace_ : FileName -> Grammar True PNamespace
|
||||
namespace_ fname = withLoc fname $ do
|
||||
ns <- resC "namespace" *> qname; needRes "{"
|
||||
|
|
@ -531,28 +536,28 @@ namespace_ fname = withLoc fname $ do
|
|||
where
|
||||
nsInner : Grammar True (List PDecl)
|
||||
nsInner = [] <$ resC "}"
|
||||
<|> [|(decl fname <* commit) :: nsInner|]
|
||||
<|> [|(assert_total decl fname <* commit) :: assert_total nsInner|]
|
||||
|
||||
decl fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
|
||||
|
||||
export covering
|
||||
export
|
||||
load : FileName -> Grammar True PTopLevel
|
||||
load fname = withLoc fname $
|
||||
resC "load" *> mustWork [|PLoad strLit|] <* optRes ";"
|
||||
|
||||
export covering
|
||||
export
|
||||
topLevel : FileName -> Grammar True PTopLevel
|
||||
topLevel fname = load fname <|> [|PD $ decl fname|]
|
||||
|
||||
export covering
|
||||
export
|
||||
input : FileName -> Grammar False (List PTopLevel)
|
||||
input fname = [] <$ eof
|
||||
<|> [|(topLevel fname <* commit) :: input fname|]
|
||||
<|> [|(topLevel fname <* commit) :: assert_total input fname|]
|
||||
|
||||
export covering
|
||||
export
|
||||
lexParseTerm : FileName -> String -> Either Error PTerm
|
||||
lexParseTerm = lexParseWith . term
|
||||
|
||||
export covering
|
||||
export
|
||||
lexParseInput : FileName -> String -> Either Error (List PTopLevel)
|
||||
lexParseInput = lexParseWith . input
|
||||
|
|
|
|||
|
|
@ -33,11 +33,14 @@ isUnused _ = False
|
|||
|
||||
|
||||
public export
|
||||
data PQty = PQ Qty Loc
|
||||
record PQty where
|
||||
constructor PQ
|
||||
val : Qty
|
||||
loc_ : Loc
|
||||
%name PQty qty
|
||||
%runElab derive "PQty" [Eq, Ord, Show]
|
||||
|
||||
export Located PQty where (PQ _ loc).loc = loc
|
||||
export Located PQty where q.loc = q.loc_
|
||||
|
||||
namespace PDim
|
||||
public export
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
module Quox.Pretty
|
||||
|
||||
import Quox.Loc
|
||||
import Quox.Name
|
||||
|
||||
import public Text.PrettyPrint.Prettyprinter.Doc
|
||||
|
|
@ -200,6 +201,7 @@ pretty0 unicode = pretty0With unicode [<] [<]
|
|||
|
||||
export PrettyHL BaseName where prettyM = pure . pretty . baseStr
|
||||
export PrettyHL Name where prettyM = pure . pretty . toDots
|
||||
export PrettyHL BindName where prettyM = prettyM . name
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -278,3 +280,14 @@ epretty @{p} x = Evidence a (p, x)
|
|||
|
||||
public export data Lit = L (Doc HL)
|
||||
export PrettyHL Lit where prettyM (L doc) = pure doc
|
||||
|
||||
|
||||
export
|
||||
prettyLoc : Loc -> Doc HL
|
||||
prettyLoc (L NoLoc) = hl TVarErr "no location" <+> hl Delim ":"
|
||||
prettyLoc (L (YesLoc file (MkBounds l1 c1 l2 c2))) =
|
||||
hcat [hl Free $ pretty file, hl Delim ":",
|
||||
hl TVar $ pretty l1, hl Delim ":",
|
||||
hl DVar $ pretty c1, hl Delim "-",
|
||||
hl TVar $ pretty l2, hl Delim ":",
|
||||
hl DVar $ pretty c2, hl Delim ":"]
|
||||
|
|
|
|||
1118
lib/Quox/Reduce.idr
1118
lib/Quox/Reduce.idr
File diff suppressed because it is too large
Load diff
|
|
@ -1,5 +1,6 @@
|
|||
module Quox.Syntax.Dim
|
||||
|
||||
import Quox.Loc
|
||||
import Quox.Name
|
||||
import Quox.Syntax.Var
|
||||
import Quox.Syntax.Subst
|
||||
|
|
@ -17,7 +18,6 @@ import Derive.Prelude
|
|||
public export
|
||||
data DimConst = Zero | One
|
||||
%name DimConst e
|
||||
|
||||
%runElab derive "DimConst" [Eq, Ord, Show]
|
||||
|
||||
||| `ends l r e` returns `l` if `e` is `Zero`, or `r` if it is `One`.
|
||||
|
|
@ -26,23 +26,42 @@ ends : Lazy a -> Lazy a -> DimConst -> a
|
|||
ends l r Zero = l
|
||||
ends l r One = r
|
||||
|
||||
export Uninhabited (Zero = One) where uninhabited _ impossible
|
||||
export Uninhabited (One = Zero) where uninhabited _ impossible
|
||||
|
||||
public export
|
||||
DecEq DimConst where
|
||||
decEq Zero Zero = Yes Refl
|
||||
decEq Zero One = No absurd
|
||||
decEq One Zero = No absurd
|
||||
decEq One One = Yes Refl
|
||||
|
||||
|
||||
public export
|
||||
data Dim : Nat -> Type where
|
||||
K : DimConst -> Dim d
|
||||
B : Var d -> Dim d
|
||||
K : DimConst -> Loc -> Dim d
|
||||
B : Var d -> Loc -> Dim d
|
||||
%name Dim.Dim p, q
|
||||
|
||||
%runElab deriveIndexed "Dim" [Eq, Ord, Show]
|
||||
|
||||
export
|
||||
Located (Dim d) where
|
||||
(K _ loc).loc = loc
|
||||
(B _ loc).loc = loc
|
||||
|
||||
export
|
||||
Relocatable (Dim d) where
|
||||
setLoc loc (K e _) = K e loc
|
||||
setLoc loc (B i _) = B i loc
|
||||
|
||||
export
|
||||
PrettyHL DimConst where
|
||||
prettyM = pure . hl Dim . ends "0" "1"
|
||||
|
||||
export
|
||||
PrettyHL (Dim n) where
|
||||
prettyM (K e) = prettyM e
|
||||
prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
|
||||
prettyM (K e _) = prettyM e
|
||||
prettyM (B i _) = prettyVar DVar DVarErr (!ask).dnames i
|
||||
|
||||
export
|
||||
prettyDim : (dnames : NContext d) -> Dim d -> Doc HL
|
||||
|
|
@ -60,13 +79,13 @@ prettyDim dnames p =
|
|||
||| - `x` otherwise.
|
||||
public export
|
||||
endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
|
||||
endsOr l r x (K e) = ends l r e
|
||||
endsOr l r x (B _) = x
|
||||
endsOr l r x (K e _) = ends l r e
|
||||
endsOr l r x (B _ _) = x
|
||||
|
||||
|
||||
public export %inline
|
||||
toConst : Dim 0 -> DimConst
|
||||
toConst (K e) = e
|
||||
toConst (K e _) = e
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -81,52 +100,55 @@ prettyDSubst th =
|
|||
!(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
|
||||
|
||||
|
||||
public export FromVar Dim where fromVar = B
|
||||
public export FromVar Dim where fromVarLoc = B
|
||||
|
||||
|
||||
export
|
||||
CanShift Dim where
|
||||
K e // _ = K e
|
||||
B i // by = B (i // by)
|
||||
K e loc // _ = K e loc
|
||||
B i loc // by = B (i // by) loc
|
||||
|
||||
export
|
||||
CanSubstSelf Dim where
|
||||
K e // _ = K e
|
||||
B i // th = th !! i
|
||||
K e loc // _ = K e loc
|
||||
B i loc // th = getLoc th i loc
|
||||
|
||||
|
||||
export Uninhabited (Zero = One) where uninhabited _ impossible
|
||||
export Uninhabited (One = Zero) where uninhabited _ impossible
|
||||
|
||||
export Uninhabited (B i = K e) where uninhabited _ impossible
|
||||
export Uninhabited (K e = B i) where uninhabited _ impossible
|
||||
|
||||
public export %inline Injective Dim.B where injective Refl = Refl
|
||||
public export %inline Injective Dim.K where injective Refl = Refl
|
||||
export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible
|
||||
export Uninhabited (K e loc1 = B i loc2) where uninhabited _ impossible
|
||||
|
||||
public export
|
||||
DecEq DimConst where
|
||||
decEq Zero Zero = Yes Refl
|
||||
decEq Zero One = No absurd
|
||||
decEq One Zero = No absurd
|
||||
decEq One One = Yes Refl
|
||||
data Eqv : Dim d1 -> Dim d2 -> Type where
|
||||
EK : K e _ `Eqv` K e _
|
||||
EB : i `Eqv` j -> B i _ `Eqv` B j _
|
||||
|
||||
export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
|
||||
export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
|
||||
|
||||
export
|
||||
injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
|
||||
injectiveB (EB e) = e
|
||||
|
||||
export
|
||||
injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
|
||||
injectiveK EK = Refl
|
||||
|
||||
public export
|
||||
DecEq (Dim d) where
|
||||
decEq (K e) (K f) with (decEq e f)
|
||||
_ | Yes prf = Yes $ cong K prf
|
||||
_ | No contra = No $ contra . injective
|
||||
decEq (K e) (B j) = No absurd
|
||||
decEq (B i) (K f) = No absurd
|
||||
decEq (B i) (B j) with (decEq i j)
|
||||
_ | Yes prf = Yes $ cong B prf
|
||||
_ | No contra = No $ contra . injective
|
||||
decEqv : Dec2 Dim.Eqv
|
||||
decEqv (K e _) (K f _) = case decEq e f of
|
||||
Yes Refl => Yes EK
|
||||
No n => No $ n . injectiveK
|
||||
decEqv (B i _) (B j _) = case decEqv i j of
|
||||
Yes y => Yes $ EB y
|
||||
No n => No $ \(EB y) => n y
|
||||
decEqv (B _ _) (K _ _) = No absurd
|
||||
decEqv (K _ _) (B _ _) = No absurd
|
||||
|
||||
||| 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 d) => Dim d
|
||||
BV i = B $ V i
|
||||
BV : (i : Nat) -> (0 _ : LT i d) => (loc : Loc) -> Dim d
|
||||
BV i loc = B (V i) loc
|
||||
|
||||
|
||||
export
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ toMaybe (Just x) = Just x
|
|||
export
|
||||
fromGround' : Context' DimConst d -> DimEq' d
|
||||
fromGround' [<] = [<]
|
||||
fromGround' (ctx :< e) = fromGround' ctx :< Just (K e)
|
||||
fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
|
||||
|
||||
export
|
||||
fromGround : Context' DimConst d -> DimEq d
|
||||
|
|
@ -98,8 +98,8 @@ get' : DimEq' d -> Var d -> Maybe (Dim d)
|
|||
get' = getWith $ \p, by => map (// by) p
|
||||
|
||||
public export %inline
|
||||
getVar : DimEq' d -> Var d -> Dim d
|
||||
getVar eqs i = fromMaybe (B i) $ get' eqs i
|
||||
getVar : DimEq' d -> Var d -> Loc -> Dim d
|
||||
getVar eqs i loc = fromMaybe (B i loc) $ get' eqs i
|
||||
|
||||
public export %inline
|
||||
getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
|
||||
|
|
@ -107,8 +107,8 @@ getShift' = getShiftWith $ \p, by => map (// by) p
|
|||
|
||||
public export %inline
|
||||
get : DimEq' d -> Dim d -> Dim d
|
||||
get _ (K e) = K e
|
||||
get eqs (B i) = getVar eqs i
|
||||
get _ (K e loc) = K e loc
|
||||
get eqs (B i loc) = getVar eqs i loc
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
@ -126,7 +126,7 @@ C eqs :<? d = C $ eqs :< map (get eqs) d
|
|||
|
||||
private %inline
|
||||
ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
|
||||
ifVar i p = map $ \q => if q == B i then p else q
|
||||
ifVar i p = map $ \q => if q == B i noLoc then p else q
|
||||
|
||||
-- (using decEq instead of (==) because of the proofs below)
|
||||
private %inline
|
||||
|
|
@ -135,39 +135,43 @@ checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
|
|||
|
||||
|
||||
export
|
||||
setConst : Var d -> DimConst -> DimEq' d -> DimEq d
|
||||
setConst VZ e (eqs :< Nothing) = C $ eqs :< Just (K e)
|
||||
setConst VZ e (eqs :< Just (K f)) = checkConst e f $ eqs :< Just (K f)
|
||||
setConst VZ e (eqs :< Just (B i)) = setConst i e eqs :<? Just (K e)
|
||||
setConst (VS i) e (eqs :< p) = setConst i e eqs :<? ifVar i (K e) p
|
||||
setConst : Var d -> DimConst -> Loc -> DimEq' d -> DimEq d
|
||||
setConst VZ e loc (eqs :< Nothing) =
|
||||
C $ eqs :< Just (K e loc)
|
||||
setConst VZ e _ (eqs :< Just (K f loc)) =
|
||||
checkConst e f $ eqs :< Just (K f loc)
|
||||
setConst VZ e loc (eqs :< Just (B i _)) =
|
||||
setConst i e loc eqs :<? Just (K e loc)
|
||||
setConst (VS i) e loc (eqs :< p) =
|
||||
setConst i e loc eqs :<? ifVar i (K e loc) p
|
||||
|
||||
mutual
|
||||
private
|
||||
setVar' : (i, j : Var d) -> (0 _ : i `LT` j) -> DimEq' d -> DimEq d
|
||||
setVar' VZ (VS i) LTZ (eqs :< Nothing) =
|
||||
C eqs :<? Just (B i)
|
||||
setVar' VZ (VS i) LTZ (eqs :< Just (K e)) =
|
||||
setConst i e eqs :<? Just (K e)
|
||||
setVar' VZ (VS i) LTZ (eqs :< Just (B j)) =
|
||||
setVar i j eqs :<? Just (B (max i j))
|
||||
setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
|
||||
setVar' i j lt eqs :<? ifVar i (B j) p
|
||||
setVar' : (i, j : Var d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
|
||||
setVar' VZ (VS i) LTZ loc (eqs :< Nothing) =
|
||||
C eqs :<? Just (B i loc)
|
||||
setVar' VZ (VS i) LTZ loc (eqs :< Just (K e eloc)) =
|
||||
setConst i e loc eqs :<? Just (K e eloc)
|
||||
setVar' VZ (VS i) LTZ loc (eqs :< Just (B j jloc)) =
|
||||
setVar i j loc jloc eqs :<? Just (if j > i then B j jloc else B i loc)
|
||||
setVar' (VS i) (VS j) (LTS lt) loc (eqs :< p) =
|
||||
setVar' i j lt loc eqs :<? ifVar i (B j loc) p
|
||||
|
||||
export %inline
|
||||
setVar : (i, j : Var d) -> DimEq' d -> DimEq d
|
||||
setVar i j eqs with (compareP i j) | (compare i.nat j.nat)
|
||||
setVar i j eqs | IsLT lt | LT = setVar' i j lt eqs
|
||||
setVar i i eqs | IsEQ | EQ = C eqs
|
||||
setVar i j eqs | IsGT gt | GT = setVar' j i gt eqs
|
||||
setVar : (i, j : Var d) -> Loc -> Loc -> DimEq' d -> DimEq d
|
||||
setVar i j li lj eqs with (compareP i j) | (compare i.nat j.nat)
|
||||
setVar i j li lj eqs | IsLT lt | LT = setVar' i j lt lj eqs
|
||||
setVar i i li lj eqs | IsEQ | EQ = C eqs
|
||||
setVar i j li lj eqs | IsGT gt | GT = setVar' j i gt li eqs
|
||||
|
||||
|
||||
export %inline
|
||||
set : (p, q : Dim d) -> DimEq d -> DimEq d
|
||||
set _ _ ZeroIsOne = ZeroIsOne
|
||||
set (K e) (K f) (C eqs) = checkConst e f eqs
|
||||
set (K e) (B i) (C eqs) = setConst i e eqs
|
||||
set (B i) (K e) (C eqs) = setConst i e eqs
|
||||
set (B i) (B j) (C eqs) = setVar i j eqs
|
||||
set (K e eloc) (K f floc) (C eqs) = checkConst e f eqs
|
||||
set (K e eloc) (B i iloc) (C eqs) = setConst i e eloc eqs
|
||||
set (B i iloc) (K e eloc) (C eqs) = setConst i e eloc eqs
|
||||
set (B i iloc) (B j jloc) (C eqs) = setVar i j iloc jloc eqs
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
@ -175,25 +179,26 @@ Split : Nat -> Type
|
|||
Split d = (DimEq' d, DSubst (S d) d)
|
||||
|
||||
export %inline
|
||||
split1 : DimConst -> DimEq' (S d) -> Maybe (Split d)
|
||||
split1 e eqs = case setConst VZ e eqs of
|
||||
split1 : DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
|
||||
split1 e loc eqs = case setConst VZ e loc eqs of
|
||||
ZeroIsOne => Nothing
|
||||
C (eqs :< _) => Just (eqs, K e ::: id)
|
||||
C (eqs :< _) => Just (eqs, K e loc ::: id)
|
||||
|
||||
export %inline
|
||||
split : DimEq' (S d) -> List (Split d)
|
||||
split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
|
||||
|
||||
split : Loc -> DimEq' (S d) -> List (Split d)
|
||||
split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs)
|
||||
|
||||
export
|
||||
splits' : DimEq' d -> List (DSubst d 0)
|
||||
splits' [<] = [id]
|
||||
splits' eqs@(_ :< _) = [th . ph | (eqs', th) <- split eqs, ph <- splits' eqs']
|
||||
splits' : Loc -> DimEq' d -> List (DSubst d 0)
|
||||
splits' _ [<] = [id]
|
||||
splits' loc eqs@(_ :< _) =
|
||||
[th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs']
|
||||
|
||||
||| the Loc is put into each of the DimConsts
|
||||
export %inline
|
||||
splits : DimEq d -> List (DSubst d 0)
|
||||
splits ZeroIsOne = []
|
||||
splits (C eqs) = splits' eqs
|
||||
splits : Loc -> DimEq d -> List (DSubst d 0)
|
||||
splits _ ZeroIsOne = []
|
||||
splits loc (C eqs) = splits' loc eqs
|
||||
|
||||
|
||||
private
|
||||
|
|
@ -208,16 +213,16 @@ newGet' d i = newGetShift d i SZ
|
|||
|
||||
export
|
||||
0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
|
||||
newGet d (K e) = Refl
|
||||
newGet d (B i) = rewrite newGet' d i in Refl
|
||||
newGet d (K e _) = Refl
|
||||
newGet d (B i _) = rewrite newGet' d i in Refl
|
||||
|
||||
|
||||
export
|
||||
0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
|
||||
setSelf p ZeroIsOne = Refl
|
||||
setSelf (K Zero) (C eqs) = Refl
|
||||
setSelf (K One) (C eqs) = Refl
|
||||
setSelf (B i) (C eqs) with (compareP i i) | (compare i.nat i.nat)
|
||||
setSelf (K Zero _) (C eqs) = Refl
|
||||
setSelf (K One _) (C eqs) = Refl
|
||||
setSelf (B i _) (C eqs) with (compareP i i) | (compare i.nat i.nat)
|
||||
_ | IsLT lt | LT = absurd lt
|
||||
_ | IsEQ | EQ = Refl
|
||||
_ | IsGT gt | GT = absurd gt
|
||||
|
|
@ -250,7 +255,7 @@ PrettyHL (DimEq' d) where
|
|||
go [<] = pure [<]
|
||||
go (eqs :< Nothing) = local {dnames $= tail} $ go eqs
|
||||
go (eqs :< Just p) = do
|
||||
eq <- prettyCst (BV {d = 1} 0) (weakD 1 p)
|
||||
eq <- prettyCst (BV {d = 1} 0 noLoc) (weakD 1 p)
|
||||
eqs <- local {dnames $= tail} $ go eqs
|
||||
pure $ eqs :< eq
|
||||
|
||||
|
|
@ -262,16 +267,16 @@ PrettyHL (DimEq d) where
|
|||
prettyM (C eqs) = prettyM eqs
|
||||
|
||||
export
|
||||
prettyDimEq : NContext d -> DimEq d -> Doc HL
|
||||
prettyDimEq ds = pretty0With False (toSnocList' ds) [<]
|
||||
prettyDimEq : BContext d -> DimEq d -> Doc HL
|
||||
prettyDimEq ds = pretty0With False (toNames ds) [<]
|
||||
|
||||
|
||||
public export
|
||||
wf' : DimEq' d -> Bool
|
||||
wf' [<] = True
|
||||
wf' (eqs :< Nothing) = wf' eqs
|
||||
wf' (eqs :< Just (K e)) = wf' eqs
|
||||
wf' (eqs :< Just (B i)) = isNothing (get' eqs i) && wf' eqs
|
||||
wf' [<] = True
|
||||
wf' (eqs :< Nothing) = wf' eqs
|
||||
wf' (eqs :< Just (K e _)) = wf' eqs
|
||||
wf' (eqs :< Just (B i _)) = isNothing (get' eqs i) && wf' eqs
|
||||
|
||||
public export
|
||||
wf : DimEq d -> Bool
|
||||
|
|
|
|||
|
|
@ -35,27 +35,28 @@ public export
|
|||
data Eqv : Shift from1 to1 -> Shift from2 to2 -> Type where
|
||||
EqSZ : SZ `Eqv` SZ
|
||||
EqSS : by `Eqv` bz -> SS by `Eqv` SS bz
|
||||
%name Eqv e
|
||||
%name Shift.Eqv e
|
||||
|
||||
||| two equivalent shifts are equal if they have the same indices.
|
||||
export
|
||||
0 fromEqv : by `Eqv` bz -> by = bz
|
||||
fromEqv EqSZ = Refl
|
||||
fromEqv (EqSS e) = cong SS $ fromEqv e
|
||||
using (by : Shift from to, bz : Shift from to)
|
||||
||| two equivalent shifts are equal if they have the same indices.
|
||||
export
|
||||
0 fromEqv : by `Eqv` bz -> by = bz
|
||||
fromEqv EqSZ = Refl
|
||||
fromEqv (EqSS e) = cong SS $ fromEqv e
|
||||
|
||||
||| two equal shifts are equivalent.
|
||||
export
|
||||
0 toEqv : by = bz -> by `Eqv` bz
|
||||
toEqv Refl {by = SZ} = EqSZ
|
||||
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl
|
||||
||| two equal shifts are equivalent.
|
||||
export
|
||||
0 toEqv : by = bz -> by `Eqv` bz
|
||||
toEqv Refl {by = SZ} = EqSZ
|
||||
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl
|
||||
|
||||
|
||||
export
|
||||
eqLen : Shift from1 to -> Shift from2 to -> Maybe (from1 = from2)
|
||||
eqLen SZ SZ = Just Refl
|
||||
eqLen SZ (SS by) = Nothing
|
||||
eqLen (SS by) SZ = Nothing
|
||||
eqLen (SS by) (SS bz) = eqLen by bz
|
||||
cmpLen : Shift from1 to -> Shift from2 to -> Either Ordering (from1 = from2)
|
||||
cmpLen SZ SZ = Right Refl
|
||||
cmpLen SZ (SS by) = Left LT
|
||||
cmpLen (SS by) SZ = Left GT
|
||||
cmpLen (SS by) (SS bz) = cmpLen by bz
|
||||
|
||||
export
|
||||
0 shiftDiff : (by : Shift from to) -> to = by.nat + from
|
||||
|
|
|
|||
|
|
@ -48,12 +48,16 @@ interface FromVar term => CanSubstSelf term where
|
|||
(//) : term from -> Lazy (Subst term from to) -> term to
|
||||
|
||||
|
||||
infixl 8 !!
|
||||
public export
|
||||
(!!) : FromVar term => Subst term from to -> Var from -> term to
|
||||
(Shift by) !! i = fromVar $ shift by i
|
||||
(t ::: th) !! VZ = t
|
||||
(t ::: th) !! (VS i) = th !! i
|
||||
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
|
||||
getLoc (Shift by) i loc = fromVarLoc (shift by i) loc
|
||||
getLoc (t ::: th) VZ _ = t
|
||||
getLoc (t ::: th) (VS i) loc = getLoc th i loc
|
||||
|
||||
-- infixl 8 !!
|
||||
-- public export
|
||||
-- (!!) : FromVar term => Subst term from to -> Var from -> term to
|
||||
-- th !! i = getLoc th i noLoc
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -160,12 +164,16 @@ PrettyHL (f to) => PrettyHL (Subst f from to) where
|
|||
prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
|
||||
|
||||
|
||||
||| whether two substitutions with the same codomain have the same shape
|
||||
||| (the same number of terms and the same shift at the end). if so, they
|
||||
||| also have the same domain
|
||||
export
|
||||
eqShape : Subst env from1 to -> Subst env from2 to -> Maybe (from1 = from2)
|
||||
eqShape (Shift by) (Shift bz) = eqLen by bz
|
||||
eqShape (Shift by) (t ::: th) = Nothing
|
||||
eqShape (t ::: th) (Shift by) = Nothing
|
||||
eqShape (t ::: th) (x ::: ph) = cong S <$> eqShape th ph
|
||||
cmpShape : Subst env from1 to -> Subst env from2 to ->
|
||||
Either Ordering (from1 = from2)
|
||||
cmpShape (Shift by) (Shift bz) = cmpLen by bz
|
||||
cmpShape (Shift _) (_ ::: _) = Left LT
|
||||
cmpShape (_ ::: _) (Shift _) = Left GT
|
||||
cmpShape (_ ::: th) (_ ::: ph) = cong S <$> cmpShape th ph
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -175,13 +183,20 @@ record WithSubst tm env n where
|
|||
subst : Lazy (Subst env from n)
|
||||
|
||||
export
|
||||
(forall n. Eq (tm n), Eq (env n)) => Eq (WithSubst tm env n) where
|
||||
(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubst tm env n) where
|
||||
Sub t1 s1 == Sub t2 s2 =
|
||||
case eqShape s1 s2 of
|
||||
Just Refl => t1 == t2 && s1 == s2
|
||||
Nothing => False
|
||||
case cmpShape s1 s2 of
|
||||
Left _ => False
|
||||
Right Refl => t1 == t2 && s1 == s2
|
||||
|
||||
export
|
||||
(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubst tm env n) where
|
||||
Sub t1 s1 `compare` Sub t2 s2 =
|
||||
case cmpShape s1 s2 of
|
||||
Left o => o
|
||||
Right Refl => compare (t1, s1) (t2, s2)
|
||||
|
||||
export %hint
|
||||
ShowWithSubst : (forall n. Show (tm n), Show (env n)) =>
|
||||
ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
|
||||
Show (WithSubst tm env n)
|
||||
ShowWithSubst = deriveShow
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import public Quox.Syntax.Qty
|
|||
import public Quox.Syntax.Dim
|
||||
import public Quox.Syntax.Term.TyConKind
|
||||
import public Quox.Name
|
||||
import public Quox.Loc
|
||||
import public Quox.Context
|
||||
|
||||
import Quox.Pretty
|
||||
|
|
@ -63,7 +64,7 @@ ShowScopedBody = deriveShow
|
|||
public export
|
||||
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
|
||||
constructor S
|
||||
names : NContext s
|
||||
names : BContext s
|
||||
body : ScopedBody s f n
|
||||
%name Scoped body
|
||||
|
||||
|
|
@ -88,38 +89,38 @@ mutual
|
|||
public export
|
||||
data Term : (d, n : Nat) -> Type where
|
||||
||| type of types
|
||||
TYPE : (l : Universe) -> Term d n
|
||||
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| function type
|
||||
Pi : (qty : Qty) -> (arg : Term d n) ->
|
||||
(res : ScopeTerm d n) -> Term d n
|
||||
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
||||
||| function term
|
||||
Lam : (body : ScopeTerm d n) -> Term d n
|
||||
Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| pair type
|
||||
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> Term d n
|
||||
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
||||
||| pair value
|
||||
Pair : (fst, snd : Term d n) -> Term d n
|
||||
Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| enumeration type
|
||||
Enum : (cases : SortedSet TagVal) -> Term d n
|
||||
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
|
||||
||| enumeration value
|
||||
Tag : (tag : TagVal) -> Term d n
|
||||
Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| equality type
|
||||
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> Term d n
|
||||
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
|
||||
||| equality term
|
||||
DLam : (body : DScopeTerm d n) -> Term d n
|
||||
DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| natural numbers (temporary until 𝐖 gets added)
|
||||
Nat : Term d n
|
||||
Nat : (loc : Loc) -> Term d n
|
||||
-- [todo] can these be elims?
|
||||
Zero : Term d n
|
||||
Succ : (p : Term d n) -> Term d n
|
||||
Zero : (loc : Loc) -> Term d n
|
||||
Succ : (p : Term d n) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| "box" (package a value up with a certain quantity)
|
||||
BOX : (qty : Qty) -> (ty : Term d n) -> Term d n
|
||||
Box : (val : Term d n) -> Term d n
|
||||
BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
|
||||
Box : (val : Term d n) -> (loc : Loc) -> Term d n
|
||||
|
||||
||| elimination
|
||||
E : (e : Elim d n) -> Term d n
|
||||
|
|
@ -134,12 +135,12 @@ mutual
|
|||
public export
|
||||
data Elim : (d, n : Nat) -> Type where
|
||||
||| free variable
|
||||
F : (x : Name) -> Elim d n
|
||||
F : (x : Name) -> (loc : Loc) -> Elim d n
|
||||
||| bound variable
|
||||
B : (i : Var n) -> Elim d n
|
||||
B : (i : Var n) -> (loc : Loc) -> Elim d n
|
||||
|
||||
||| term application
|
||||
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
|
||||
App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
|
||||
|
||||
||| pair destruction
|
||||
|||
|
||||
|
|
@ -148,12 +149,14 @@ mutual
|
|||
CasePair : (qty : Qty) -> (pair : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(body : ScopeTermN 2 d n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| enum matching
|
||||
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(arms : CaseEnumArms d n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| nat matching
|
||||
|
|
@ -161,33 +164,36 @@ mutual
|
|||
(ret : ScopeTerm d n) ->
|
||||
(zero : Term d n) ->
|
||||
(succ : ScopeTermN 2 d n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| unboxing
|
||||
CaseBox : (qty : Qty) -> (box : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
(body : ScopeTerm d n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| dim application
|
||||
(:%) : (fun : Elim d n) -> (arg : Dim d) -> Elim d n
|
||||
DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
|
||||
|
||||
||| type-annotated term
|
||||
(:#) : (tm, ty : Term d n) -> Elim d n
|
||||
Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim 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) -> Elim d n
|
||||
(val : Term d n) -> (loc : Loc) -> Elim 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) -> Elim d n
|
||||
(zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim 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) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| term closure/suspended substitution
|
||||
|
|
@ -244,88 +250,211 @@ mutual
|
|||
||| scope which ignores all its binders
|
||||
public export %inline
|
||||
SN : {s : Nat} -> f n -> Scoped s f n
|
||||
SN = S (replicate s Unused) . N
|
||||
SN = S (replicate s $ BN Unused noLoc) . N
|
||||
|
||||
||| scope which uses its binders
|
||||
public export %inline
|
||||
SY : NContext s -> f (s + n) -> Scoped s f n
|
||||
SY : BContext s -> f (s + n) -> Scoped s f n
|
||||
SY ns = S ns . Y
|
||||
|
||||
public export %inline
|
||||
name : Scoped 1 f n -> BaseName
|
||||
name : Scoped 1 f n -> BindName
|
||||
name (S [< x] _) = x
|
||||
|
||||
public export %inline
|
||||
(.name) : Scoped 1 f n -> BaseName
|
||||
(.name) : Scoped 1 f n -> BindName
|
||||
s.name = name s
|
||||
|
||||
||| more convenient Pi
|
||||
public export %inline
|
||||
PiY : (qty : Qty) -> (x : BaseName) ->
|
||||
(arg : Term d n) -> (res : Term d (S n)) -> Term d n
|
||||
PiY {qty, x, arg, res} = Pi {qty, arg, res = SY [< x] res}
|
||||
PiY : (qty : Qty) -> (x : BindName) ->
|
||||
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term 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, body, loc} = Lam {body = SY [< x] body, loc}
|
||||
|
||||
public export %inline
|
||||
LamN : (body : Term d n) -> (loc : Loc) -> Term 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) -> Term d n
|
||||
Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
|
||||
Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
|
||||
Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
|
||||
|
||||
||| more convenient Sig
|
||||
public export %inline
|
||||
SigY : (x : BaseName) -> (fst : Term d n) ->
|
||||
(snd : Term d (S n)) -> Term d n
|
||||
SigY {x, fst, snd} = Sig {fst, snd = SY [< x] snd}
|
||||
SigY : (x : BindName) -> (fst : Term d n) ->
|
||||
(snd : Term d (S n)) -> (loc : Loc) -> Term 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) -> Term d n
|
||||
And {fst, snd} = Sig {fst, snd = SN snd}
|
||||
And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
|
||||
And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
|
||||
|
||||
||| more convenient Eq
|
||||
public export %inline
|
||||
EqY : (i : BaseName) -> (ty : Term (S d) n) ->
|
||||
(l, r : Term d n) -> Term d n
|
||||
EqY {i, ty, l, r} = Eq {ty = SY [< i] ty, l, r}
|
||||
EqY : (i : BindName) -> (ty : Term (S d) n) ->
|
||||
(l, r : Term d n) -> (loc : Loc) -> Term 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, body, loc} = DLam {body = SY [< i] body, loc}
|
||||
|
||||
public export %inline
|
||||
DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
|
||||
DLamN {body, loc} = DLam {body = SN body, loc}
|
||||
|
||||
||| non dependent equality type
|
||||
public export %inline
|
||||
Eq0 : (ty, l, r : Term d n) -> Term d n
|
||||
Eq0 {ty, l, r} = Eq {ty = SN ty, l, r}
|
||||
Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term 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 -> Term d n
|
||||
FT = E . F
|
||||
FT : Name -> (loc : Loc) -> Term d n
|
||||
FT x loc = E $ F x 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) => Elim d n
|
||||
BV i = B $ V i
|
||||
BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim 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) => Term d n
|
||||
BVT i = E $ BV i
|
||||
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
|
||||
BVT i loc = E $ BV i loc
|
||||
|
||||
public export
|
||||
makeNat : Nat -> Term d n
|
||||
makeNat 0 = Zero
|
||||
makeNat (S k) = Succ $ makeNat k
|
||||
makeNat : Nat -> Loc -> Term d n
|
||||
makeNat 0 loc = Zero loc
|
||||
makeNat (S k) loc = Succ (makeNat k loc) loc
|
||||
|
||||
public export %inline
|
||||
enum : List TagVal -> Term d n
|
||||
enum = Enum . SortedSet.fromList
|
||||
enum : List TagVal -> Loc -> Term 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 -> Elim d n
|
||||
typeCase ty ret arms def = TypeCase ty ret (fromList arms) def
|
||||
List (TypeCaseArm d n) -> Term d n -> Loc -> Elim 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) -> NContext (arity k) -> Term d (arity k + n) ->
|
||||
{default Nat def : Term d n} ->
|
||||
(k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
|
||||
(loc : Loc) ->
|
||||
{default (Nat loc) def : Term d n} ->
|
||||
Elim d n
|
||||
typeCase1Y ty ret k ns body {def} =
|
||||
typeCase ty ret [(k ** SY ns body)] def
|
||||
typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
|
||||
|
||||
|
||||
export
|
||||
Located (Elim d n) where
|
||||
(F _ loc).loc = loc
|
||||
(B _ loc).loc = loc
|
||||
(App _ _ loc).loc = loc
|
||||
(CasePair _ _ _ _ loc).loc = loc
|
||||
(CaseEnum _ _ _ _ loc).loc = loc
|
||||
(CaseNat _ _ _ _ _ _ loc).loc = loc
|
||||
(CaseBox _ _ _ _ loc).loc = loc
|
||||
(DApp _ _ loc).loc = loc
|
||||
(Ann _ _ loc).loc = loc
|
||||
(Coe _ _ _ _ loc).loc = loc
|
||||
(Comp _ _ _ _ _ _ _ loc).loc = loc
|
||||
(TypeCase _ _ _ _ loc).loc = loc
|
||||
(CloE (Sub e _)).loc = e.loc
|
||||
(DCloE (Sub e _)).loc = e.loc
|
||||
|
||||
export
|
||||
Located (Term d n) where
|
||||
(TYPE _ 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
|
||||
(Zero loc).loc = loc
|
||||
(Succ _ loc).loc = loc
|
||||
(BOX _ _ loc).loc = loc
|
||||
(Box _ loc).loc = loc
|
||||
(E e).loc = e.loc
|
||||
(CloT (Sub t _)).loc = t.loc
|
||||
(DCloT (Sub t _)).loc = t.loc
|
||||
|
||||
export
|
||||
Located1 f => Located (ScopedBody s f n) where
|
||||
(Y t).loc = t.loc
|
||||
(N t).loc = t.loc
|
||||
|
||||
export
|
||||
Located1 f => Located (Scoped s f n) where
|
||||
t.loc = t.body.loc
|
||||
|
||||
|
||||
export
|
||||
Relocatable (Elim d n) where
|
||||
setLoc loc (F x _) = F x loc
|
||||
setLoc loc (B i _) = B i loc
|
||||
setLoc loc (App fun arg _) = App fun arg loc
|
||||
setLoc loc (CasePair qty pair ret body _) =
|
||||
CasePair qty pair ret body loc
|
||||
setLoc loc (CaseEnum qty tag ret arms _) =
|
||||
CaseEnum qty tag ret arms loc
|
||||
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
|
||||
CaseNat qty qtyIH nat ret zero succ loc
|
||||
setLoc loc (CaseBox qty box ret body _) =
|
||||
CaseBox qty box ret body loc
|
||||
setLoc loc (DApp fun arg _) =
|
||||
DApp fun arg loc
|
||||
setLoc loc (Ann tm ty _) =
|
||||
Ann tm ty loc
|
||||
setLoc loc (Coe ty p q val _) =
|
||||
Coe ty p q val loc
|
||||
setLoc loc (Comp ty p q val r zero one _) =
|
||||
Comp ty p q val r zero one loc
|
||||
setLoc loc (TypeCase ty ret arms def _) =
|
||||
TypeCase ty ret arms def loc
|
||||
setLoc loc (CloE (Sub term subst)) =
|
||||
CloE $ Sub (setLoc loc term) subst
|
||||
setLoc loc (DCloE (Sub term subst)) =
|
||||
DCloE $ Sub (setLoc loc term) subst
|
||||
|
||||
export
|
||||
Relocatable (Term d n) where
|
||||
setLoc loc (TYPE l _) = TYPE l loc
|
||||
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
|
||||
setLoc loc (Lam body _) = Lam body loc
|
||||
setLoc loc (Sig fst snd _) = Sig fst snd loc
|
||||
setLoc loc (Pair fst snd _) = Pair fst snd loc
|
||||
setLoc loc (Enum cases _) = Enum cases loc
|
||||
setLoc loc (Tag tag _) = Tag tag loc
|
||||
setLoc loc (Eq ty l r _) = Eq ty l r loc
|
||||
setLoc loc (DLam body _) = DLam body loc
|
||||
setLoc loc (Nat _) = Nat loc
|
||||
setLoc loc (Zero _) = Zero loc
|
||||
setLoc loc (Succ p _) = Succ p loc
|
||||
setLoc loc (BOX qty ty _) = BOX qty ty loc
|
||||
setLoc loc (Box val _) = Box val loc
|
||||
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
|
||||
|
||||
export
|
||||
Relocatable1 f => Relocatable (ScopedBody s f n) where
|
||||
setLoc loc (Y body) = Y $ setLoc loc body
|
||||
setLoc loc (N body) = N $ setLoc loc body
|
||||
|
||||
export
|
||||
Relocatable1 f => Relocatable (Scoped s f n) where
|
||||
setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)
|
||||
|
|
|
|||
|
|
@ -82,8 +82,8 @@ PrettyHL a => PrettyHL (Binder a) where
|
|||
export
|
||||
prettyBindType : PrettyHL a => PrettyHL b =>
|
||||
Pretty.HasEnv m =>
|
||||
Maybe Qty -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
|
||||
prettyBindType q x s arr t = do
|
||||
Maybe Qty -> BindName -> a -> Doc HL -> b -> m (Doc HL)
|
||||
prettyBindType q (BN x _) s arr t = do
|
||||
bind <- case q of
|
||||
Nothing => pretty0M $ MkBinder x s
|
||||
Just q => pretty0M $ MkWithQty q $ MkBinder x s
|
||||
|
|
@ -92,14 +92,15 @@ prettyBindType q x s arr t = do
|
|||
|
||||
export
|
||||
prettyArm : PrettyHL a => Pretty.HasEnv m =>
|
||||
BinderSort -> SnocList BaseName -> Doc HL -> a -> m (Doc HL)
|
||||
BinderSort -> SnocList BindName -> Doc HL -> a -> m (Doc HL)
|
||||
prettyArm sort xs pat body = do
|
||||
let xs = map name xs
|
||||
body <- withPrec Outer $ unders sort xs $ prettyM body
|
||||
pure $ hang 2 $ sep [pat <++> !darrowD, body]
|
||||
|
||||
export
|
||||
prettyLams : PrettyHL a => Pretty.HasEnv m =>
|
||||
Maybe (Doc HL) -> BinderSort -> SnocList BaseName -> a ->
|
||||
Maybe (Doc HL) -> BinderSort -> SnocList BindName -> a ->
|
||||
m (Doc HL)
|
||||
prettyLams lam sort names body = do
|
||||
let var = case sort of T => TVar; D => DVar
|
||||
|
|
@ -109,14 +110,15 @@ prettyLams lam sort names body = do
|
|||
|
||||
|
||||
public export
|
||||
data TypeLine a = MkTypeLine BaseName a
|
||||
data TypeLine a = MkTypeLine BindName a
|
||||
|
||||
export
|
||||
PrettyHL a => PrettyHL (TypeLine a) where
|
||||
prettyM (MkTypeLine Unused ty) =
|
||||
bracks <$> pretty0M ty
|
||||
prettyM (MkTypeLine i ty) =
|
||||
map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
|
||||
if i.name == Unused then
|
||||
bracks <$> pretty0M ty
|
||||
else
|
||||
map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -142,28 +144,28 @@ prettyTuple = map (parens . align . separate commaD) . traverse prettyM
|
|||
|
||||
export
|
||||
prettyArms : PrettyHL a => Pretty.HasEnv m =>
|
||||
BinderSort -> List (SnocList BaseName, Doc HL, a) -> m (Doc HL)
|
||||
BinderSort -> List (SnocList BindName, Doc HL, a) -> m (Doc HL)
|
||||
prettyArms s =
|
||||
map (braces . aseparate semiD) .
|
||||
traverse (\(xs, l, r) => prettyArm s xs l r)
|
||||
|
||||
export
|
||||
prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
|
||||
Doc HL -> a -> BaseName -> b ->
|
||||
List (SnocList BaseName, Doc HL, c) ->
|
||||
Doc HL -> a -> BindName -> b ->
|
||||
List (SnocList BindName, Doc HL, c) ->
|
||||
m (Doc HL)
|
||||
prettyCase' intro elim r ret arms = do
|
||||
elim <- pretty0M elim
|
||||
ret <- case r of
|
||||
Unused => under T r $ pretty0M ret
|
||||
ret <- case r.name of
|
||||
Unused => under T r.name $ pretty0M ret
|
||||
_ => prettyLams Nothing T [< r] ret
|
||||
arms <- prettyArms T arms
|
||||
pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
|
||||
|
||||
export
|
||||
prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
|
||||
Qty -> a -> BaseName -> b ->
|
||||
List (SnocList BaseName, Doc HL, c) ->
|
||||
Qty -> a -> BindName -> b ->
|
||||
List (SnocList BindName, Doc HL, c) ->
|
||||
m (Doc HL)
|
||||
prettyCase pi elim r ret arms = do
|
||||
caseq <- (caseD <+>) <$> prettySuffix pi
|
||||
|
|
@ -197,14 +199,14 @@ prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
|
|||
prettyBoxVal val = bracks <$> pretty0M val
|
||||
|
||||
export
|
||||
prettyCompPat : Pretty.HasEnv m => DimConst -> BaseName -> m (Doc HL)
|
||||
prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j]
|
||||
prettyCompPat : Pretty.HasEnv m => DimConst -> BindName -> m (Doc HL)
|
||||
prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j.name]
|
||||
|
||||
export
|
||||
toNatLit : Term d n -> Maybe Nat
|
||||
toNatLit Zero = Just 0
|
||||
toNatLit (Succ n) = [|S $ toNatLit n|]
|
||||
toNatLit _ = Nothing
|
||||
toNatLit (Zero _) = Just 0
|
||||
toNatLit (Succ n _) = [|S $ toNatLit n|]
|
||||
toNatLit _ = Nothing
|
||||
|
||||
private
|
||||
eterm : Term d n -> Exists (Term d)
|
||||
|
|
@ -216,69 +218,69 @@ parameters (showSubsts : Bool)
|
|||
export covering
|
||||
[TermSubst] PrettyHL (Term d n) using ElimSubst
|
||||
where
|
||||
prettyM (TYPE l) =
|
||||
prettyM (TYPE l _) =
|
||||
pure $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
|
||||
|
||||
prettyM (Pi qty s (S _ (N t))) = do
|
||||
prettyM (Pi qty s (S _ (N t)) _) = do
|
||||
dom <- pretty0M $ MkWithQty qty s
|
||||
cod <- withPrec AnnR $ prettyM t
|
||||
parensIfM AnnR $ asep [dom <++> !arrowD, cod]
|
||||
|
||||
prettyM (Pi qty s (S [< x] (Y t))) =
|
||||
prettyM (Pi qty s (S [< x] (Y t)) _) =
|
||||
prettyBindType (Just qty) x s !arrowD t
|
||||
|
||||
prettyM (Lam (S x t)) =
|
||||
prettyM (Lam (S x t) _) =
|
||||
let GotLams {names, body, _} = getLams' x t.term Refl in
|
||||
prettyLams (Just !lamD) T (toSnocList' names) body
|
||||
|
||||
prettyM (Sig s (S _ (N t))) = do
|
||||
prettyM (Sig s (S _ (N t)) _) = do
|
||||
s <- withPrec InTimes $ prettyM s
|
||||
t <- withPrec Times $ prettyM t
|
||||
parensIfM Times $ asep [s <++> !timesD, t]
|
||||
|
||||
prettyM (Sig s (S [< x] (Y t))) =
|
||||
prettyM (Sig s (S [< x] (Y t)) _) =
|
||||
prettyBindType Nothing x s !timesD t
|
||||
|
||||
prettyM (Pair s t) =
|
||||
prettyM (Pair s t _) =
|
||||
let GotPairs {init, last, _} = getPairs' [< s] t in
|
||||
prettyTuple $ toList $ init :< last
|
||||
|
||||
prettyM (Enum tags) =
|
||||
prettyM (Enum tags _) =
|
||||
pure $ delims "{" "}" . aseparate comma $ map prettyTagBare $
|
||||
Prelude.toList tags
|
||||
|
||||
prettyM (Tag t) =
|
||||
prettyM (Tag t _) =
|
||||
pure $ prettyTag t
|
||||
|
||||
prettyM (Eq (S _ (N ty)) l r) = do
|
||||
prettyM (Eq (S _ (N ty)) l r _) = do
|
||||
l <- withPrec InEq $ prettyM l
|
||||
r <- withPrec InEq $ prettyM r
|
||||
ty <- withPrec InEq $ prettyM ty
|
||||
parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
|
||||
|
||||
prettyM (Eq (S [< i] (Y ty)) l r) = do
|
||||
prettyM (Eq (S [< i] (Y ty)) l r _) = do
|
||||
prettyApps Nothing (L eqD)
|
||||
[epretty $ MkTypeLine i ty, epretty l, epretty r]
|
||||
|
||||
prettyM (DLam (S i t)) =
|
||||
prettyM (DLam (S i t) _) =
|
||||
let GotDLams {names, body, _} = getDLams' i t.term Refl in
|
||||
prettyLams (Just !dlamD) D (toSnocList' names) body
|
||||
|
||||
prettyM Nat = natD
|
||||
prettyM (Nat _) = natD
|
||||
|
||||
prettyM Zero = pure $ hl Syntax "0"
|
||||
prettyM (Zero _) = pure $ hl Syntax "0"
|
||||
|
||||
prettyM (Succ n) =
|
||||
prettyM (Succ n _) =
|
||||
case toNatLit n of
|
||||
Just n => pure $ hl Syntax $ pretty $ S n
|
||||
Nothing => prettyApps Nothing (L succD) [n]
|
||||
|
||||
prettyM (BOX pi ty) = do
|
||||
prettyM (BOX pi ty _) = do
|
||||
pi <- pretty0M pi
|
||||
ty <- pretty0M ty
|
||||
pure $ bracks $ hcat [pi, dotD, align ty]
|
||||
|
||||
prettyM (Box val) = prettyBoxVal val
|
||||
prettyM (Box val _) = prettyBoxVal val
|
||||
|
||||
prettyM (E e) = prettyM e
|
||||
|
||||
|
|
@ -299,49 +301,49 @@ parameters (showSubsts : Bool)
|
|||
export covering
|
||||
[ElimSubst] PrettyHL (Elim d n) using TermSubst
|
||||
where
|
||||
prettyM (F x) =
|
||||
prettyM (F x _) =
|
||||
hl' Free <$> prettyM x
|
||||
|
||||
prettyM (B i) =
|
||||
prettyM (B i _) =
|
||||
prettyVar TVar TVarErr (!ask).tnames i
|
||||
|
||||
prettyM (e :@ s) =
|
||||
prettyM (App e s _) =
|
||||
let GotArgs {fun, args, _} = getArgs' e [s] in
|
||||
prettyApps Nothing fun args
|
||||
|
||||
prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body)) = do
|
||||
prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body) _) = do
|
||||
pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
|
||||
prettyCase pi p r ret.term [([< x, y], pat, body.term)]
|
||||
|
||||
prettyM (CaseEnum pi t (S [< r] ret) arms) =
|
||||
prettyM (CaseEnum pi t (S [< r] ret) arms _) =
|
||||
prettyCase pi t r ret.term
|
||||
[([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
|
||||
|
||||
prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc)) =
|
||||
prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc) _) =
|
||||
prettyCase pi nat r ret.term
|
||||
[([<], zeroD, eterm zer),
|
||||
([< s, ih], !succPat, eterm suc.term)]
|
||||
where
|
||||
succPat : m (Doc HL)
|
||||
succPat = case (ih, pi') of
|
||||
(Unused, Zero) => pure $ succD <++> !(pretty0M s)
|
||||
(BN Unused _, Zero) => pure $ succD <++> !(pretty0M s)
|
||||
_ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
|
||||
!(pretty0M $ MkWithQty pi' ih)]
|
||||
|
||||
prettyM (CaseBox pi box (S [< r] ret) (S [< u] body)) =
|
||||
prettyM (CaseBox pi box (S [< r] ret) (S [< u] body) _) =
|
||||
prettyCase pi box r ret.term
|
||||
[([< u], !(prettyBoxVal $ TV u), body.term)]
|
||||
[([< u], !(prettyBoxVal $ TV u.name), body.term)]
|
||||
|
||||
prettyM (e :% d) =
|
||||
prettyM (DApp e d _) =
|
||||
let GotDArgs {fun, args, _} = getDArgs' e [d] in
|
||||
prettyApps (Just "@") fun args
|
||||
|
||||
prettyM (s :# a) = do
|
||||
prettyM (Ann s a _) = do
|
||||
s <- withPrec AnnL $ prettyM s
|
||||
a <- withPrec AnnR $ prettyM a
|
||||
parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
|
||||
|
||||
prettyM (Coe (S [< i] ty) p q val) =
|
||||
prettyM (Coe (S [< i] ty) p q val _) =
|
||||
let ty = case ty of
|
||||
Y ty => epretty $ MkTypeLine i ty
|
||||
N ty => epretty ty
|
||||
|
|
@ -352,9 +354,9 @@ parameters (showSubsts : Bool)
|
|||
(Just "@", epretty q),
|
||||
(Nothing, epretty val)]
|
||||
|
||||
prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one)) = do
|
||||
prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one) _) = do
|
||||
apps <- prettyApps' (L compD)
|
||||
[(Nothing, epretty $ MkTypeLine Unused ty),
|
||||
[(Nothing, epretty $ MkTypeLine (BN Unused noLoc) ty),
|
||||
(Just "@", epretty p),
|
||||
(Just "@", epretty q),
|
||||
(Nothing, epretty val),
|
||||
|
|
@ -364,29 +366,30 @@ parameters (showSubsts : Bool)
|
|||
([< o], !(prettyCompPat One o), one.term)]
|
||||
pure $ apps <++> arms
|
||||
|
||||
prettyM (TypeCase ty ret arms def) = do
|
||||
prettyM (TypeCase ty ret arms def _) = do
|
||||
arms <- traverse fromArm (toList arms)
|
||||
prettyCase' typecaseD ty Unused ret $
|
||||
prettyCase' typecaseD ty (BN Unused noLoc) ret $
|
||||
arms ++ [([<], hl Syntax "_", eterm def)]
|
||||
where
|
||||
v : BaseName -> Doc HL
|
||||
v = pretty0 True . TV
|
||||
v : BindName -> Doc HL
|
||||
v = pretty0 True . TV . name
|
||||
|
||||
tyCasePat : (k : TyConKind) -> NContext (arity k) -> m (Doc HL)
|
||||
tyCasePat : (k : TyConKind) -> BContext (arity k) -> m (Doc HL)
|
||||
tyCasePat KTYPE [<] = typeD
|
||||
tyCasePat KPi [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
|
||||
tyCasePat KSig [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
|
||||
tyCasePat KEnum [<] = pure $ hl Syntax "{}"
|
||||
tyCasePat KEq vars = prettyApps Nothing (L eqD) $ map TV $ toList' vars
|
||||
tyCasePat KNat [<] = natD
|
||||
tyCasePat KBOX [< a] = pure $ bracks $ v a
|
||||
tyCasePat KEq vars =
|
||||
prettyApps Nothing (L eqD) $ map (TV . name) $ toList' vars
|
||||
|
||||
fromArm : TypeCaseArm d n ->
|
||||
m (SnocList BaseName, Doc HL, Exists (Term d))
|
||||
m (SnocList BindName, Doc HL, Exists (Term d))
|
||||
fromArm (k ** S ns t) =
|
||||
pure (toSnocList' ns, !(tyCasePat k ns), eterm t.term)
|
||||
|
||||
prettyM (CloE (Sub e th)) =
|
||||
prettyM (CloE (Sub e th)) =
|
||||
if showSubsts then
|
||||
parensIfM SApp . hang 2 =<<
|
||||
[|withPrec SApp (prettyM e) <%> prettyTSubst th|]
|
||||
|
|
@ -414,7 +417,7 @@ PrettyHL (Elim d n) where prettyM = prettyM @{ElimSubst False}
|
|||
|
||||
export covering
|
||||
prettyTerm : (unicode : Bool) ->
|
||||
(dnames : NContext d) -> (tnames : NContext n) ->
|
||||
(dnames : BContext d) -> (tnames : BContext n) ->
|
||||
Term d n -> Doc HL
|
||||
prettyTerm unicode dnames tnames term =
|
||||
pretty0With unicode (toSnocList' dnames) (toSnocList' tnames) term
|
||||
pretty0With unicode (toNames dnames) (toNames tnames) term
|
||||
|
|
|
|||
|
|
@ -13,8 +13,8 @@ import public Data.Vect
|
|||
|
||||
public export %inline
|
||||
isLam : Term {} -> Bool
|
||||
isLam (Lam _) = True
|
||||
isLam _ = False
|
||||
isLam (Lam {}) = True
|
||||
isLam _ = False
|
||||
|
||||
public export
|
||||
0 NotLam : Pred $ Term {}
|
||||
|
|
@ -23,8 +23,8 @@ NotLam = No . isLam
|
|||
|
||||
public export %inline
|
||||
isDLam : Term {} -> Bool
|
||||
isDLam (DLam _) = True
|
||||
isDLam _ = False
|
||||
isDLam (DLam {}) = True
|
||||
isDLam _ = False
|
||||
|
||||
public export
|
||||
0 NotDLam : Pred $ Term {}
|
||||
|
|
@ -43,7 +43,7 @@ NotPair = No . isPair
|
|||
|
||||
public export %inline
|
||||
isApp : Elim {} -> Bool
|
||||
isApp (_ :@ _) = True
|
||||
isApp (App {}) = True
|
||||
isApp _ = False
|
||||
|
||||
public export
|
||||
|
|
@ -53,19 +53,21 @@ NotApp = No . isApp
|
|||
|
||||
public export %inline
|
||||
isDApp : Elim {} -> Bool
|
||||
isDApp (_ :% _) = True
|
||||
isDApp _ = False
|
||||
isDApp (DApp {}) = True
|
||||
isDApp _ = False
|
||||
|
||||
public export
|
||||
0 NotDApp : Pred $ Elim {}
|
||||
NotDApp = No . isDApp
|
||||
|
||||
|
||||
infixl 9 :@@
|
||||
||| apply multiple arguments at once
|
||||
public export %inline
|
||||
(:@@) : Elim d n -> List (Term d n) -> Elim d n
|
||||
f :@@ ss = foldl (:@) f ss
|
||||
-- infixl 9 :@@
|
||||
-- ||| apply multiple arguments at once
|
||||
-- public export %inline
|
||||
-- (:@@) : Elim d n -> List (Term d n) -> Elim d n
|
||||
-- f :@@ ss = foldl app f ss where
|
||||
-- app : Elim d n -> Term d n -> Elim d n
|
||||
-- app f s = App f s (f.loc `extend'` s.loc.bounds)
|
||||
|
||||
public export
|
||||
record GetArgs d n where
|
||||
|
|
@ -85,7 +87,7 @@ mutual
|
|||
getArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
|
||||
List (Term d n) -> GetArgs d n
|
||||
getArgsNc fun args = case nchoose $ isApp fun of
|
||||
Left y => let f :@ a = fun in getArgs' f (a :: args)
|
||||
Left y => let App f a _ = fun in getArgs' f (a :: args)
|
||||
Right n => GotArgs {fun, args, notApp = n}
|
||||
|
||||
||| splits an application into its head and arguments. if it's not an
|
||||
|
|
@ -96,11 +98,13 @@ getArgs : Elim d n -> GetArgs d n
|
|||
getArgs e = getArgs' e []
|
||||
|
||||
|
||||
infixl 9 :%%
|
||||
||| apply multiple dimension arguments at once
|
||||
public export %inline
|
||||
(:%%) : Elim d n -> List (Dim d) -> Elim d n
|
||||
f :%% ss = foldl (:%) f ss
|
||||
-- infixl 9 :%%
|
||||
-- ||| apply multiple dimension arguments at once
|
||||
-- public export %inline
|
||||
-- (:%%) : Elim d n -> List (Dim d) -> Elim d n
|
||||
-- f :%% ss = foldl dapp f ss where
|
||||
-- dapp : Elim d n -> Dim d -> Elim d n
|
||||
-- dapp f p = DApp f p (f.loc `extend'` p.loc.bounds)
|
||||
|
||||
public export
|
||||
record GetDArgs d n where
|
||||
|
|
@ -120,7 +124,7 @@ mutual
|
|||
getDArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
|
||||
List (Dim d) -> GetDArgs d n
|
||||
getDArgsNc fun args = case nchoose $ isDApp fun of
|
||||
Left y => let f :% d = fun in getDArgs' f (d :: args)
|
||||
Left y => let DApp f d _ = fun in getDArgs' f (d :: args)
|
||||
Right n => GotDArgs {fun, args, notDApp = n}
|
||||
|
||||
||| splits a dimension application into its head and arguments. if it's not an
|
||||
|
|
@ -130,33 +134,33 @@ getDArgs : Elim d n -> GetDArgs d n
|
|||
getDArgs e = getDArgs' e []
|
||||
|
||||
|
||||
infixr 1 :\\
|
||||
public export
|
||||
absN : NContext m -> Term d (m + n) -> Term d n
|
||||
absN [<] s = s
|
||||
absN (xs :< x) s = absN xs $ Lam $ ST [< x] s
|
||||
-- infixr 1 :\\
|
||||
-- public export
|
||||
-- absN : BContext m -> Term d (m + n) -> Term d n
|
||||
-- absN [<] s = s
|
||||
-- absN (xs :< x) s = absN xs $ Lam (ST [< x] s) ?absloc
|
||||
|
||||
public export %inline
|
||||
(:\\) : NContext m -> Term d (m + n) -> Term d n
|
||||
(:\\) = absN
|
||||
-- public export %inline
|
||||
-- (:\\) : BContext m -> Term d (m + n) -> Term d n
|
||||
-- (:\\) = absN
|
||||
|
||||
|
||||
infixr 1 :\\%
|
||||
public export
|
||||
dabsN : NContext m -> Term (m + d) n -> Term d n
|
||||
dabsN [<] s = s
|
||||
dabsN (xs :< x) s = dabsN xs $ DLam $ DST [< x] s
|
||||
-- infixr 1 :\\%
|
||||
-- public export
|
||||
-- dabsN : BContext m -> Term (m + d) n -> Term d n
|
||||
-- dabsN [<] s = s
|
||||
-- dabsN (xs :< x) s = dabsN xs $ DLam (DST [< x] s) ?dabsLoc
|
||||
|
||||
public export %inline
|
||||
(:\\%) : NContext m -> Term (m + d) n -> Term d n
|
||||
(:\\%) = dabsN
|
||||
-- public export %inline
|
||||
-- (:\\%) : BContext m -> Term (m + d) n -> Term d n
|
||||
-- (:\\%) = dabsN
|
||||
|
||||
|
||||
public export
|
||||
record GetLams d n where
|
||||
constructor GotLams
|
||||
{0 lams, rest : Nat}
|
||||
names : NContext lams
|
||||
names : BContext lams
|
||||
body : Term d rest
|
||||
0 eq : lams + n = rest
|
||||
0 notLam : NotLam body
|
||||
|
|
@ -164,7 +168,7 @@ record GetLams d n where
|
|||
mutual
|
||||
export %inline
|
||||
getLams' : forall lams, rest.
|
||||
NContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
|
||||
BContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
|
||||
GetLams d n
|
||||
getLams' xs s0 eq =
|
||||
let Element s nc = pushSubsts s0 in
|
||||
|
|
@ -172,12 +176,12 @@ mutual
|
|||
|
||||
private
|
||||
getLamsNc : forall lams, rest.
|
||||
NContext lams ->
|
||||
BContext lams ->
|
||||
(t : Term d rest) -> (0 nc : NotClo t) =>
|
||||
(0 eq : lams + n = rest) ->
|
||||
GetLams d n
|
||||
getLamsNc xs s Refl = case nchoose $ isLam s of
|
||||
Left y => let Lam (S [< x] body) = s in
|
||||
Left y => let Lam (S [< x] body) _ = s in
|
||||
getLams' (xs :< x) (assert_smaller s body.term) Refl
|
||||
Right n => GotLams xs s Refl n
|
||||
|
||||
|
|
@ -190,7 +194,7 @@ public export
|
|||
record GetDLams d n where
|
||||
constructor GotDLams
|
||||
{0 lams, rest : Nat}
|
||||
names : NContext lams
|
||||
names : BContext lams
|
||||
body : Term rest n
|
||||
0 eq : lams + d = rest
|
||||
0 notDLam : NotDLam body
|
||||
|
|
@ -198,7 +202,7 @@ record GetDLams d n where
|
|||
mutual
|
||||
export %inline
|
||||
getDLams' : forall lams, rest.
|
||||
NContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
|
||||
BContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
|
||||
GetDLams d n
|
||||
getDLams' xs s0 eq =
|
||||
let Element s nc = pushSubsts s0 in
|
||||
|
|
@ -206,12 +210,12 @@ mutual
|
|||
|
||||
private
|
||||
getDLamsNc : forall lams, rest.
|
||||
NContext lams ->
|
||||
BContext lams ->
|
||||
(t : Term rest n) -> (0 nc : NotClo t) =>
|
||||
(0 eq : lams + d = rest) ->
|
||||
GetDLams d n
|
||||
getDLamsNc is s Refl = case nchoose $ isDLam s of
|
||||
Left y => let DLam (S [< i] body) = s in
|
||||
Left y => let DLam (S [< i] body) _ = s in
|
||||
getDLams' (is :< i) (assert_smaller s body.term) Refl
|
||||
Right n => GotDLams is s Refl n
|
||||
|
||||
|
|
@ -238,7 +242,7 @@ mutual
|
|||
(t : Term d n) -> (0 nc : NotClo t) =>
|
||||
GetPairs d n
|
||||
getPairsNc ss t = case nchoose $ isPair t of
|
||||
Left y => let Pair s t = t in
|
||||
Left y => let Pair s t _ = t in
|
||||
getPairs' (ss :< s) t
|
||||
Right n => GotPairs ss t n
|
||||
|
||||
|
|
|
|||
|
|
@ -20,14 +20,14 @@ namespace CanDSubst
|
|||
export
|
||||
CanDSubst Term where
|
||||
s // Shift SZ = s
|
||||
TYPE l // _ = TYPE l
|
||||
TYPE l loc // _ = TYPE l loc
|
||||
DCloT (Sub s ph) // th = DCloT $ Sub s $ ph . th
|
||||
s // th = DCloT $ Sub s th
|
||||
|
||||
private
|
||||
subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
|
||||
subDArgs (f :% d) th = subDArgs f th :% (d // th)
|
||||
subDArgs e th = DCloE $ Sub e th
|
||||
subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
|
||||
subDArgs e th = DCloE $ Sub e th
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
||| - deletes the closure around a term variable
|
||||
|
|
@ -39,9 +39,9 @@ subDArgs e th = DCloE $ Sub e th
|
|||
export
|
||||
CanDSubst Elim where
|
||||
e // Shift SZ = e
|
||||
F x // _ = F x
|
||||
B i // _ = B i
|
||||
f :% d // th = subDArgs (f :% d) th
|
||||
F x loc // _ = F x loc
|
||||
B i loc // _ = B i loc
|
||||
e@(DApp {}) // th = subDArgs e th
|
||||
DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th
|
||||
e // th = DCloE $ Sub e th
|
||||
|
||||
|
|
@ -61,8 +61,8 @@ namespace DSubst.DScopeTermN
|
|||
S ns (N body) // th = S ns $ N $ body // th
|
||||
|
||||
|
||||
export %inline FromVar (Elim d) where fromVar = B
|
||||
export %inline FromVar (Term d) where fromVar = E . fromVar
|
||||
export %inline FromVar (Elim d) where fromVarLoc = B
|
||||
export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
|
||||
|
||||
|
||||
||| does the minimal reasonable work:
|
||||
|
|
@ -73,8 +73,8 @@ export %inline FromVar (Term d) where fromVar = E . fromVar
|
|||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanSubstSelf (Elim d) where
|
||||
F x // _ = F x
|
||||
B i // th = th !! i
|
||||
F x loc // _ = F x loc
|
||||
B i loc // th = getLoc th i loc
|
||||
CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
|
||||
e // th = case force th of
|
||||
Shift SZ => e
|
||||
|
|
@ -93,7 +93,7 @@ namespace CanTSubst
|
|||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanTSubst Term where
|
||||
TYPE l // _ = TYPE l
|
||||
TYPE l loc // _ = TYPE l loc
|
||||
E e // th = E $ e // th
|
||||
CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
|
||||
s // th = case force th of
|
||||
|
|
@ -192,12 +192,12 @@ dsub1 t p = dsubN t [< p]
|
|||
|
||||
|
||||
public export %inline
|
||||
(.zero) : DScopeTerm d n -> Term d n
|
||||
body.zero = dsub1 body $ K Zero
|
||||
(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
|
||||
body.zero = dsub1 body $ K Zero loc
|
||||
|
||||
public export %inline
|
||||
(.one) : DScopeTerm d n -> Term d n
|
||||
body.one = dsub1 body $ K One
|
||||
(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
|
||||
body.one = dsub1 body $ K One loc
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -251,29 +251,34 @@ mutual
|
|||
mutual
|
||||
export
|
||||
PushSubsts Term Subst.isCloT where
|
||||
pushSubstsWith th ph (TYPE l) =
|
||||
nclo $ TYPE l
|
||||
pushSubstsWith th ph (Pi qty a body) =
|
||||
nclo $ Pi qty (a // th // ph) (body // th // ph)
|
||||
pushSubstsWith th ph (Lam body) =
|
||||
nclo $ Lam (body // th // ph)
|
||||
pushSubstsWith th ph (Sig a b) =
|
||||
nclo $ Sig (a // th // ph) (b // th // ph)
|
||||
pushSubstsWith th ph (Pair s t) =
|
||||
nclo $ Pair (s // th // ph) (t // th // ph)
|
||||
pushSubstsWith th ph (Enum tags) =
|
||||
nclo $ Enum tags
|
||||
pushSubstsWith th ph (Tag tag) =
|
||||
nclo $ Tag tag
|
||||
pushSubstsWith th ph (Eq ty l r) =
|
||||
nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph)
|
||||
pushSubstsWith th ph (DLam body) =
|
||||
nclo $ DLam (body // th // ph)
|
||||
pushSubstsWith _ _ Nat = nclo Nat
|
||||
pushSubstsWith _ _ Zero = nclo Zero
|
||||
pushSubstsWith th ph (Succ n) = nclo $ Succ $ n // th // ph
|
||||
pushSubstsWith th ph (BOX pi ty) = nclo $ BOX pi $ ty // th // ph
|
||||
pushSubstsWith th ph (Box val) = nclo $ Box $ val // th // ph
|
||||
pushSubstsWith th ph (TYPE l loc) =
|
||||
nclo $ TYPE l 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) =
|
||||
nclo $ Enum tags loc
|
||||
pushSubstsWith th ph (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) =
|
||||
nclo $ Nat loc
|
||||
pushSubstsWith _ _ (Zero loc) =
|
||||
nclo $ Zero loc
|
||||
pushSubstsWith th ph (Succ n loc) =
|
||||
nclo $ Succ (n // th // ph) 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 (CloT (Sub s ps)) =
|
||||
|
|
@ -283,38 +288,38 @@ mutual
|
|||
|
||||
export
|
||||
PushSubsts Elim Subst.isCloE where
|
||||
pushSubstsWith th ph (F x) =
|
||||
nclo $ F x
|
||||
pushSubstsWith th ph (B i) =
|
||||
let res = ph !! i in
|
||||
pushSubstsWith th ph (F x loc) =
|
||||
nclo $ F x loc
|
||||
pushSubstsWith th ph (B i loc) =
|
||||
let res = getLoc ph i loc in
|
||||
case nchoose $ isCloE res of
|
||||
Left yes => assert_total pushSubsts res
|
||||
Right no => Element res no
|
||||
pushSubstsWith th ph (f :@ s) =
|
||||
nclo $ (f // th // ph) :@ (s // th // ph)
|
||||
pushSubstsWith th ph (CasePair pi p r b) =
|
||||
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph)
|
||||
pushSubstsWith th ph (CaseEnum pi t r arms) =
|
||||
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 (CaseEnum pi t r arms loc) =
|
||||
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
|
||||
(map (\b => b // th // ph) arms)
|
||||
pushSubstsWith th ph (CaseNat pi pi' n r z s) =
|
||||
(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)
|
||||
pushSubstsWith th ph (CaseBox pi x r b) =
|
||||
nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph)
|
||||
pushSubstsWith th ph (f :% d) =
|
||||
nclo $ (f // th // ph) :% (d // th)
|
||||
pushSubstsWith th ph (s :# a) =
|
||||
nclo $ (s // th // ph) :# (a // th // ph)
|
||||
pushSubstsWith th ph (Coe ty p q val) =
|
||||
nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph)
|
||||
pushSubstsWith th ph (Comp ty p q val r zero one) =
|
||||
(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)
|
||||
pushSubstsWith th ph (TypeCase ty ret arms def) =
|
||||
(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)
|
||||
(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)) =
|
||||
|
|
@ -323,14 +328,19 @@ mutual
|
|||
|
||||
private %inline
|
||||
CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(r : Dim d) -> (zero, one : DScopeTerm d n) -> Elim d n
|
||||
CompHY {ty, p, q, val, r, zero, one} =
|
||||
let ty' = SY ty.names $ ty.term // (B VZ ::: shift 2) in
|
||||
(r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
|
||||
CompHY {ty, p, q, val, r, zero, one, loc} =
|
||||
-- [fixme] maintain location of existing B VZ
|
||||
let ty' = SY ty.names $ ty.term // (B VZ noLoc ::: shift 2) in
|
||||
Comp {
|
||||
ty = dsub1 ty q, p, q,
|
||||
val = E $ Coe ty p q val, r,
|
||||
zero = SY zero.names $ E $ Coe ty' (B VZ) (weakD 1 q) zero.term,
|
||||
one = SY one.names $ E $ Coe ty' (B VZ) (weakD 1 q) one.term
|
||||
val = E $ Coe ty p q val val.loc, r,
|
||||
-- [fixme] better locations for these vars?
|
||||
zero = SY zero.names $ E $
|
||||
Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
|
||||
one = SY one.names $ E $
|
||||
Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
|
||||
loc
|
||||
}
|
||||
|
||||
public export %inline
|
||||
|
|
@ -338,26 +348,28 @@ CompH' : (ty : DScopeTerm d n) ->
|
|||
(p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
|
||||
(zero : DScopeTerm d n) ->
|
||||
(one : DScopeTerm d n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
CompH' {ty, p, q, val, r, zero, one} =
|
||||
CompH' {ty, p, q, val, r, zero, one, loc} =
|
||||
case dsqueeze ty of
|
||||
S _ (N ty) => Comp {ty, p, q, val, r, zero, one}
|
||||
S _ (Y _) => CompHY {ty, p, q, val, r, zero, one}
|
||||
S _ (N ty) => Comp {ty, p, q, val, r, zero, one, loc}
|
||||
S _ (Y _) => CompHY {ty, p, q, val, r, zero, one, loc}
|
||||
|
||||
||| heterogeneous composition, using Comp and Coe (and subst)
|
||||
|||
|
||||
||| comp [i ⇒ A] @p @q s { (r=0) j ⇒ t₀; (r=1) j ⇒ t₁ }
|
||||
||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
|
||||
||| ≔
|
||||
||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) {
|
||||
||| (r=0) j ⇒ coe [i ⇒ A] @j @q t₀;
|
||||
||| (r=1) j ⇒ coe [i ⇒ A] @j @q t₁
|
||||
||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
|
||||
||| 0 j ⇒ coe [i ⇒ A] @j @q t₀;
|
||||
||| 1 j ⇒ coe [i ⇒ A] @j @q t₁
|
||||
||| }
|
||||
public export %inline
|
||||
CompH : (i : BaseName) -> (ty : Term (S d) n) ->
|
||||
CompH : (i : BindName) -> (ty : Term (S d) n) ->
|
||||
(p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
|
||||
(j0 : BaseName) -> (zero : Term (S d) n) ->
|
||||
(j1 : BaseName) -> (one : Term (S d) n) ->
|
||||
(j0 : BindName) -> (zero : Term (S d) n) ->
|
||||
(j1 : BindName) -> (one : Term (S d) n) ->
|
||||
(loc : Loc) ->
|
||||
Elim d n
|
||||
CompH {i, ty, p, q, val, r, j0, zero, j1, one} =
|
||||
CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
|
||||
CompH' {ty = SY [< i] ty, p, q, val, r,
|
||||
zero = SY [< j0] zero, one = SY [< j0] one}
|
||||
zero = SY [< j0] zero, one = SY [< j0] one, loc}
|
||||
|
|
|
|||
|
|
@ -18,6 +18,12 @@ Tighten (Shift from) where
|
|||
tighten (Keep p) (SS by) = [|SS $ tighten p by|]
|
||||
|
||||
|
||||
export
|
||||
Tighten Dim where
|
||||
tighten p (K e loc) = pure $ K e loc
|
||||
tighten p (B i loc) = B <$> tighten p i <*> pure loc
|
||||
|
||||
|
||||
export
|
||||
tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
|
||||
OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
|
||||
|
|
@ -46,23 +52,35 @@ 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 p (TYPE l) = pure $ TYPE l
|
||||
tightenT p (Pi qty arg res) =
|
||||
Pi qty <$> tightenT p arg <*> tightenS p res
|
||||
tightenT p (Lam body) = Lam <$> tightenS p body
|
||||
tightenT p (Sig fst snd) = Sig <$> tightenT p fst <*> tightenS p snd
|
||||
tightenT p (Pair fst snd) = Pair <$> tightenT p fst <*> tightenT p snd
|
||||
tightenT p (Enum cases) = pure $ Enum cases
|
||||
tightenT p (Tag tag) = pure $ Tag tag
|
||||
tightenT p (Eq ty l r) =
|
||||
Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r
|
||||
tightenT p (DLam body) = DLam <$> tightenDS p body
|
||||
tightenT p Nat = pure Nat
|
||||
tightenT p Zero = pure Zero
|
||||
tightenT p (Succ s) = Succ <$> tightenT p s
|
||||
tightenT p (BOX qty ty) = BOX qty <$> tightenT p ty
|
||||
tightenT p (Box val) = Box <$> tightenT p val
|
||||
tightenT p (E e) = assert_total $ E <$> tightenE p e
|
||||
tightenT p (TYPE l loc) = pure $ TYPE l loc
|
||||
tightenT p (Pi qty arg res loc) =
|
||||
Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc
|
||||
tightenT p (Lam body loc) =
|
||||
Lam <$> tightenS p body <*> pure loc
|
||||
tightenT p (Sig fst snd loc) =
|
||||
Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
|
||||
tightenT p (Pair fst snd loc) =
|
||||
Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc
|
||||
tightenT p (Enum cases loc) =
|
||||
pure $ Enum cases loc
|
||||
tightenT p (Tag tag loc) =
|
||||
pure $ Tag tag loc
|
||||
tightenT p (Eq ty l r loc) =
|
||||
Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc
|
||||
tightenT p (DLam body loc) =
|
||||
DLam <$> tightenDS p body <*> pure loc
|
||||
tightenT p (Nat loc) =
|
||||
pure $ Nat loc
|
||||
tightenT p (Zero loc) =
|
||||
pure $ Zero loc
|
||||
tightenT p (Succ s loc) =
|
||||
Succ <$> tightenT p s <*> pure loc
|
||||
tightenT p (BOX qty ty loc) =
|
||||
BOX qty <$> tightenT p ty <*> pure loc
|
||||
tightenT p (Box val loc) =
|
||||
Box <$> tightenT p val <*> pure loc
|
||||
tightenT p (E e) =
|
||||
assert_total $ E <$> tightenE p e
|
||||
tightenT p (CloT (Sub tm th)) = do
|
||||
th <- assert_total $ tightenSub tightenE p th
|
||||
pure $ CloT $ Sub tm th
|
||||
|
|
@ -72,45 +90,57 @@ mutual
|
|||
|
||||
private
|
||||
tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
|
||||
tightenE p (F x) = pure $ F x
|
||||
tightenE p (B i) = [|B $ tighten p i|]
|
||||
tightenE p (fun :@ arg) = [|tightenE p fun :@ tightenT p arg|]
|
||||
tightenE p (CasePair qty pair ret body) =
|
||||
tightenE p (F x loc) =
|
||||
pure $ F x loc
|
||||
tightenE p (B i loc) =
|
||||
B <$> tighten p i <*> pure loc
|
||||
tightenE p (App fun arg loc) =
|
||||
App <$> tightenE p fun <*> tightenT p arg <*> pure loc
|
||||
tightenE p (CasePair qty pair ret body loc) =
|
||||
CasePair qty <$> tightenE p pair
|
||||
<*> tightenS p ret
|
||||
<*> tightenS p body
|
||||
tightenE p (CaseEnum qty tag ret arms) =
|
||||
<*> pure loc
|
||||
tightenE p (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty <$> tightenE p tag
|
||||
<*> tightenS p ret
|
||||
<*> traverse (tightenT p) arms
|
||||
tightenE p (CaseNat qty qtyIH nat ret zero succ) =
|
||||
<*> pure loc
|
||||
tightenE p (CaseNat qty qtyIH nat ret zero succ loc) =
|
||||
CaseNat qty qtyIH
|
||||
<$> tightenE p nat
|
||||
<*> tightenS p ret
|
||||
<*> tightenT p zero
|
||||
<*> tightenS p succ
|
||||
tightenE p (CaseBox qty box ret body) =
|
||||
<*> pure loc
|
||||
tightenE p (CaseBox qty box ret body loc) =
|
||||
CaseBox qty <$> tightenE p box
|
||||
<*> tightenS p ret
|
||||
<*> tightenS p body
|
||||
tightenE p (fun :% arg) = (:% arg) <$> tightenE p fun
|
||||
tightenE p (tm :# ty) = [|tightenT p tm :# tightenT p ty|]
|
||||
tightenE p (Coe ty q0 q1 val) =
|
||||
<*> pure loc
|
||||
tightenE p (DApp fun arg loc) =
|
||||
DApp <$> tightenE p fun <*> pure arg <*> pure loc
|
||||
tightenE p (Ann tm ty loc) =
|
||||
Ann <$> tightenT p tm <*> tightenT p ty <*> pure loc
|
||||
tightenE p (Coe ty q0 q1 val loc) =
|
||||
Coe <$> tightenDS p ty
|
||||
<*> pure q0 <*> pure q1
|
||||
<*> tightenT p val
|
||||
tightenE p (Comp ty q0 q1 val r zero one) =
|
||||
<*> pure loc
|
||||
tightenE p (Comp ty q0 q1 val r zero one loc) =
|
||||
Comp <$> tightenT p ty
|
||||
<*> pure q0 <*> pure q1
|
||||
<*> tightenT p val
|
||||
<*> pure r
|
||||
<*> tightenDS p zero
|
||||
<*> tightenDS p one
|
||||
tightenE p (TypeCase ty ret arms def) =
|
||||
<*> pure loc
|
||||
tightenE p (TypeCase ty ret arms def loc) =
|
||||
TypeCase <$> tightenE p ty
|
||||
<*> tightenT p ret
|
||||
<*> traverse (tightenS p) arms
|
||||
<*> tightenT p def
|
||||
<*> pure loc
|
||||
tightenE p (CloE (Sub el th)) = do
|
||||
th <- assert_total $ tightenSub tightenE p th
|
||||
pure $ CloE $ Sub el th
|
||||
|
|
@ -130,35 +160,40 @@ mutual
|
|||
export Tighten (Elim d) where tighten p e = tightenE p e
|
||||
export Tighten (Term d) where tighten p t = tightenT p t
|
||||
|
||||
export
|
||||
Tighten Dim where
|
||||
tighten p (K e) = pure $ K e
|
||||
tighten p (B i) = B <$> tighten p i
|
||||
|
||||
|
||||
mutual
|
||||
export
|
||||
dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n)
|
||||
dtightenT p (TYPE l) = pure $ TYPE l
|
||||
dtightenT p (Pi qty arg res) =
|
||||
Pi qty <$> dtightenT p arg <*> dtightenS p res
|
||||
dtightenT p (Lam body) =
|
||||
Lam <$> dtightenS p body
|
||||
dtightenT p (Sig fst snd) =
|
||||
Sig <$> dtightenT p fst <*> dtightenS p snd
|
||||
dtightenT p (Pair fst snd) =
|
||||
Pair <$> dtightenT p fst <*> dtightenT p snd
|
||||
dtightenT p (Enum cases) = pure $ Enum cases
|
||||
dtightenT p (Tag tag) = pure $ Tag tag
|
||||
dtightenT p (Eq ty l r) =
|
||||
Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r
|
||||
dtightenT p (DLam body) = DLam <$> dtightenDS p body
|
||||
dtightenT p Nat = pure Nat
|
||||
dtightenT p Zero = pure Zero
|
||||
dtightenT p (Succ s) = Succ <$> dtightenT p s
|
||||
dtightenT p (BOX qty ty) = BOX qty <$> dtightenT p ty
|
||||
dtightenT p (Box val) = Box <$> dtightenT p val
|
||||
dtightenT p (E e) = assert_total $ E <$> dtightenE p e
|
||||
dtightenT p (TYPE l loc) =
|
||||
pure $ TYPE l loc
|
||||
dtightenT p (Pi qty arg res loc) =
|
||||
Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc
|
||||
dtightenT p (Lam body loc) =
|
||||
Lam <$> dtightenS p body <*> pure loc
|
||||
dtightenT p (Sig fst snd loc) =
|
||||
Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
|
||||
dtightenT p (Pair fst snd loc) =
|
||||
Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc
|
||||
dtightenT p (Enum cases loc) =
|
||||
pure $ Enum cases loc
|
||||
dtightenT p (Tag tag loc) =
|
||||
pure $ Tag tag loc
|
||||
dtightenT p (Eq ty l r loc) =
|
||||
Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc
|
||||
dtightenT p (DLam body loc) =
|
||||
DLam <$> dtightenDS p body <*> pure loc
|
||||
dtightenT p (Nat loc) =
|
||||
pure $ Nat loc
|
||||
dtightenT p (Zero loc) =
|
||||
pure $ Zero loc
|
||||
dtightenT p (Succ s loc) =
|
||||
Succ <$> dtightenT p s <*> pure loc
|
||||
dtightenT p (BOX qty ty loc) =
|
||||
BOX qty <$> dtightenT p ty <*> pure loc
|
||||
dtightenT p (Box val loc) =
|
||||
Box <$> dtightenT p val <*> pure loc
|
||||
dtightenT p (E e) =
|
||||
assert_total $ E <$> dtightenE p e
|
||||
dtightenT p (CloT (Sub tm th)) = do
|
||||
tm <- dtightenT p tm
|
||||
th <- assert_total $ traverse (dtightenE p) th
|
||||
|
|
@ -169,38 +204,48 @@ mutual
|
|||
|
||||
export
|
||||
dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
|
||||
dtightenE p (F x) = pure $ F x
|
||||
dtightenE p (B i) = pure $ B i
|
||||
dtightenE p (fun :@ arg) = [|dtightenE p fun :@ dtightenT p arg|]
|
||||
dtightenE p (CasePair qty pair ret body) =
|
||||
dtightenE p (F x loc) =
|
||||
pure $ F x loc
|
||||
dtightenE p (B i loc) =
|
||||
pure $ B i loc
|
||||
dtightenE p (App fun arg loc) =
|
||||
App <$> dtightenE p fun <*> dtightenT p arg <*> pure loc
|
||||
dtightenE p (CasePair qty pair ret body loc) =
|
||||
CasePair qty <$> dtightenE p pair
|
||||
<*> dtightenS p ret
|
||||
<*> dtightenS p body
|
||||
dtightenE p (CaseEnum qty tag ret arms) =
|
||||
<*> pure loc
|
||||
dtightenE p (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty <$> dtightenE p tag
|
||||
<*> dtightenS p ret
|
||||
<*> traverse (dtightenT p) arms
|
||||
dtightenE p (CaseNat qty qtyIH nat ret zero succ) =
|
||||
<*> pure loc
|
||||
dtightenE p (CaseNat qty qtyIH nat ret zero succ loc) =
|
||||
CaseNat qty qtyIH
|
||||
<$> dtightenE p nat
|
||||
<*> dtightenS p ret
|
||||
<*> dtightenT p zero
|
||||
<*> dtightenS p succ
|
||||
dtightenE p (CaseBox qty box ret body) =
|
||||
<*> pure loc
|
||||
dtightenE p (CaseBox qty box ret body loc) =
|
||||
CaseBox qty <$> dtightenE p box
|
||||
<*> dtightenS p ret
|
||||
<*> dtightenS p body
|
||||
dtightenE p (fun :% arg) = [|dtightenE p fun :% tighten p arg|]
|
||||
dtightenE p (tm :# ty) = [|dtightenT p tm :# dtightenT p ty|]
|
||||
dtightenE p (Coe ty q0 q1 val) =
|
||||
[|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val)|]
|
||||
dtightenE p (Comp ty q0 q1 val r zero one) =
|
||||
<*> pure loc
|
||||
dtightenE p (DApp fun arg loc) =
|
||||
DApp <$> dtightenE p fun <*> tighten p arg <*> pure loc
|
||||
dtightenE p (Ann tm ty loc) =
|
||||
Ann <$> dtightenT p tm <*> dtightenT p ty <*> pure loc
|
||||
dtightenE p (Coe ty q0 q1 val loc) =
|
||||
[|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val)
|
||||
(pure loc)|]
|
||||
dtightenE p (Comp ty q0 q1 val r zero one loc) =
|
||||
[|Comp (dtightenT p ty) (tighten p q0) (tighten p q1)
|
||||
(dtightenT p val) (tighten p r)
|
||||
(dtightenDS p zero) (dtightenDS p one)|]
|
||||
dtightenE p (TypeCase ty ret arms def) =
|
||||
(dtightenDS p zero) (dtightenDS p one) (pure loc)|]
|
||||
dtightenE p (TypeCase ty ret arms def loc) =
|
||||
[|TypeCase (dtightenE p ty) (dtightenT p ret)
|
||||
(traverse (dtightenS p) arms) (dtightenT p def)|]
|
||||
(traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|]
|
||||
dtightenE p (CloE (Sub el th)) = do
|
||||
el <- dtightenE p el
|
||||
th <- assert_total $ traverse (dtightenE p) th
|
||||
|
|
@ -226,46 +271,55 @@ export [ElimD] Tighten (\d => Elim d n) where tighten p e = dtightenE p e
|
|||
-- versions of SY, etc, that try to tighten and use SN automatically
|
||||
|
||||
public export
|
||||
ST : Tighten f => {s : Nat} -> NContext s -> f (s + n) -> Scoped s f n
|
||||
ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
|
||||
ST names body =
|
||||
case tightenN s body of
|
||||
Just body => S names $ N body
|
||||
Nothing => S names $ Y body
|
||||
|
||||
public export
|
||||
DST : {s : Nat} -> NContext s -> Term (s + d) n -> DScopeTermN s d n
|
||||
DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
|
||||
DST names body =
|
||||
case tightenN @{TermD} s body of
|
||||
Just body => S names $ N body
|
||||
Nothing => S names $ Y body
|
||||
|
||||
public export %inline
|
||||
PiT : (qty : Qty) -> (x : BaseName) ->
|
||||
(arg : Term d n) -> (res : Term d (S n)) -> Term d n
|
||||
PiT {qty, x, arg, res} = Pi {qty, arg, res = ST [< x] res}
|
||||
PiT : (qty : Qty) -> (x : BindName) ->
|
||||
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
|
||||
PiT {qty, x, arg, res, loc} = Pi {qty, arg, res = ST [< x] res, loc}
|
||||
|
||||
public export %inline
|
||||
SigT : (x : BaseName) -> (fst : Term d n) ->
|
||||
(snd : Term d (S n)) -> Term d n
|
||||
SigT {x, fst, snd} = Sig {fst, snd = ST [< x] snd}
|
||||
LamT : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
|
||||
LamT {x, body, loc} = Lam {body = ST [< x] body, loc}
|
||||
|
||||
public export %inline
|
||||
EqT : (i : BaseName) -> (ty : Term (S d) n) ->
|
||||
(l, r : Term d n) -> Term d n
|
||||
EqT {i, ty, l, r} = Eq {ty = DST [< i] ty, l, r}
|
||||
SigT : (x : BindName) -> (fst : Term d n) ->
|
||||
(snd : Term d (S n)) -> (loc : Loc) -> Term d n
|
||||
SigT {x, fst, snd, loc} = Sig {fst, snd = ST [< x] snd, loc}
|
||||
|
||||
public export %inline
|
||||
CoeT : (i : BaseName) -> (ty : Term (S d) n) ->
|
||||
(p, q : Dim d) -> (val : Term d n) -> Elim d n
|
||||
CoeT {i, ty, p, q, val} = Coe {ty = DST [< i] ty, p, q, val}
|
||||
EqT : (i : BindName) -> (ty : Term (S d) n) ->
|
||||
(l, r : Term d n) -> (loc : Loc) -> Term 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 {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}
|
||||
|
||||
public export %inline
|
||||
typeCase1T : Elim d n -> Term d n ->
|
||||
(k : TyConKind) -> NContext (arity k) -> Term d (arity k + n) ->
|
||||
{default Nat def : Term d n} ->
|
||||
(k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
|
||||
(loc : Loc) ->
|
||||
{default (Nat loc) def : Term d n} ->
|
||||
Elim d n
|
||||
typeCase1T ty ret k ns body {def} =
|
||||
typeCase ty ret [(k ** ST ns body)] def
|
||||
typeCase1T ty ret k ns body loc {def} =
|
||||
typeCase ty ret [(k ** ST ns body)] def loc
|
||||
|
||||
|
||||
export
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
module Quox.Syntax.Var
|
||||
|
||||
import Quox.Name
|
||||
import public Quox.Loc
|
||||
import public Quox.Name
|
||||
import Quox.Pretty
|
||||
import Quox.OPE
|
||||
|
||||
|
|
@ -42,6 +43,23 @@ export Uninhabited (VZ = VS i) where uninhabited _ impossible
|
|||
export Uninhabited (VS i = VZ) where uninhabited _ impossible
|
||||
|
||||
|
||||
public export
|
||||
data Eqv : Var m -> Var n -> Type where
|
||||
EZ : VZ `Eqv` VZ
|
||||
ES : i `Eqv` j -> VS i `Eqv` VS j
|
||||
%name Var.Eqv e
|
||||
|
||||
export
|
||||
decEqv : Dec2 Eqv
|
||||
decEqv VZ VZ = Yes EZ
|
||||
decEqv VZ (VS i) = No $ \case _ impossible
|
||||
decEqv (VS i) VZ = No $ \case _ impossible
|
||||
decEqv (VS i) (VS j) =
|
||||
case decEqv i j of
|
||||
Yes y => Yes $ ES y
|
||||
No n => No $ \(ES y) => n y
|
||||
|
||||
|
||||
private
|
||||
lookupS : Nat -> SnocList a -> Maybe a
|
||||
lookupS _ [<] = Nothing
|
||||
|
|
@ -148,9 +166,13 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
|
|||
|
||||
|
||||
public export
|
||||
interface FromVar f where %inline fromVar : Var n -> f n
|
||||
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
|
||||
|
||||
public export FromVar Var where fromVar = id
|
||||
public export %inline
|
||||
fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
|
||||
fromVar x = fromVarLoc x loc
|
||||
|
||||
public export FromVar Var where fromVarLoc x _ = x
|
||||
|
||||
export
|
||||
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
|
||||
|
|
|
|||
|
|
@ -13,26 +13,30 @@ import Quox.EffExtra
|
|||
|
||||
public export
|
||||
0 TCEff : List (Type -> Type)
|
||||
TCEff = [ErrorEff, DefsReader]
|
||||
TCEff = [ErrorEff, DefsReader, NameGen]
|
||||
|
||||
public export
|
||||
0 TC : Type -> Type
|
||||
TC = Eff TCEff
|
||||
|
||||
export
|
||||
runTC : Definitions -> TC a -> Either Error a
|
||||
runTC defs =
|
||||
extract . runExcept . runReaderAt DEFS defs
|
||||
|
||||
runTCWith : NameSuf -> Definitions -> TC a -> (Either Error a, NameSuf)
|
||||
runTCWith = runEqualWith
|
||||
|
||||
export
|
||||
popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) -> Eff fs (QOutput n)
|
||||
popQs [<] qout = pure qout
|
||||
popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
|
||||
runTC : Definitions -> TC a -> Either Error a
|
||||
runTC = runEqual
|
||||
|
||||
export %inline
|
||||
popQ : Has ErrorEff fs => Qty -> QOutput (S n) -> Eff fs (QOutput n)
|
||||
popQ pi = popQs [< pi]
|
||||
|
||||
parameters (loc : Loc)
|
||||
export
|
||||
popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) -> Eff fs (QOutput n)
|
||||
popQs [<] qout = pure qout
|
||||
popQs (pis :< pi) (qout :< rh) = do expectCompatQ loc rh pi; popQs pis qout
|
||||
|
||||
export %inline
|
||||
popQ : Has ErrorEff fs => Qty -> QOutput (S n) -> Eff fs (QOutput n)
|
||||
popQ pi = popQs [< pi]
|
||||
|
||||
export
|
||||
lubs1 : List1 (QOutput n) -> Maybe (QOutput n)
|
||||
|
|
@ -47,29 +51,32 @@ lubs ctx [] = Just $ zeroFor ctx
|
|||
lubs ctx (x :: xs) = lubs1 $ x ::: xs
|
||||
|
||||
|
||||
||| context extension with no names or quantities
|
||||
private
|
||||
CtxExtension0' : Nat -> Nat -> Nat -> Type
|
||||
CtxExtension0' s d n = Context (Term d . (+ n)) s
|
||||
|
||||
private
|
||||
addNames0 : Context (Term d . (+ n)) s -> NContext s -> CtxExtension d n (s + n)
|
||||
addNames0 [<] [<] = [<]
|
||||
addNames0 (ts :< t) (xs :< x) = addNames0 ts xs :< (Zero, x, t)
|
||||
|
||||
export
|
||||
typecaseTel : (k : TyConKind) -> Universe -> CtxExtension0' (arity k) d n
|
||||
typecaseTel k u = case k of
|
||||
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
|
||||
CtxExtension d n (arity k + n)
|
||||
typecaseTel k xs u = case k of
|
||||
KTYPE => [<]
|
||||
-- A : ★ᵤ, B : 0.A → ★ᵤ
|
||||
KPi => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
|
||||
KSig => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
|
||||
KPi =>
|
||||
let [< a, b] = xs in
|
||||
[< (Zero, a, TYPE u a.loc),
|
||||
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
|
||||
KSig =>
|
||||
let [< a, b] = xs in
|
||||
[< (Zero, a, TYPE u a.loc),
|
||||
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
|
||||
KEnum => [<]
|
||||
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
|
||||
KEq => [< TYPE u, TYPE u, Eq0 (TYPE u) (BVT 1) (BVT 0), BVT 2, BVT 2]
|
||||
KEq =>
|
||||
let [< a0, a1, a, l, r] = xs in
|
||||
[< (Zero, a0, TYPE u a0.loc),
|
||||
(Zero, a1, TYPE u a1.loc),
|
||||
(Zero, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
|
||||
(Zero, l, BVT 2 l.loc),
|
||||
(Zero, r, BVT 2 r.loc)]
|
||||
KNat => [<]
|
||||
-- A : ★ᵤ
|
||||
KBOX => [< TYPE u]
|
||||
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
|
||||
|
||||
|
||||
mutual
|
||||
|
|
@ -149,8 +156,8 @@ mutual
|
|||
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
|
||||
TC (CheckResult' n)
|
||||
toCheckType ctx sg t ty = do
|
||||
u <- expectTYPE !defs ctx ty
|
||||
expectEqualQ Zero sg.fst
|
||||
u <- expectTYPE !defs ctx ty.loc ty
|
||||
expectEqualQ t.loc Zero sg.fst
|
||||
checkTypeNoWrap ctx t (Just u)
|
||||
pure $ zeroFor ctx
|
||||
|
||||
|
|
@ -159,70 +166,70 @@ mutual
|
|||
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
|
||||
TC (CheckResult' n)
|
||||
|
||||
check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
|
||||
check' ctx sg t@(TYPE {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Lam body) ty = do
|
||||
(qty, arg, res) <- expectPi !defs ctx ty
|
||||
check' ctx sg (Lam body loc) ty = do
|
||||
(qty, arg, res) <- expectPi !defs ctx ty.loc ty
|
||||
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
|
||||
-- with ρ ≤ σπ
|
||||
let qty' = sg.fst * qty
|
||||
qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
|
||||
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
|
||||
popQ qty' qout
|
||||
popQ loc qty' qout
|
||||
|
||||
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Pair fst snd) ty = do
|
||||
(tfst, tsnd) <- expectSig !defs ctx ty
|
||||
check' ctx sg (Pair fst snd loc) ty = do
|
||||
(tfst, tsnd) <- expectSig !defs ctx ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
|
||||
qfst <- checkC ctx sg fst tfst
|
||||
let tsnd = sub1 tsnd (fst :# tfst)
|
||||
let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
|
||||
-- if Ψ | Γ ⊢ σ · t ⇐ B[s] ⊳ Σ₂
|
||||
qsnd <- checkC ctx sg snd tsnd
|
||||
-- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
|
||||
pure $ qfst + qsnd
|
||||
|
||||
check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty
|
||||
check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Tag t) ty = do
|
||||
tags <- expectEnum !defs ctx ty
|
||||
check' ctx sg (Tag t loc) ty = do
|
||||
tags <- expectEnum !defs ctx ty.loc ty
|
||||
-- if t ∈ ts
|
||||
unless (t `elem` tags) $ throw $ TagNotIn t tags
|
||||
unless (t `elem` tags) $ throw $ TagNotIn loc t tags
|
||||
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
|
||||
pure $ zeroFor ctx
|
||||
|
||||
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (DLam body) ty = do
|
||||
(ty, l, r) <- expectEq !defs ctx ty
|
||||
check' ctx sg (DLam body loc) ty = do
|
||||
(ty, l, r) <- expectEq !defs ctx ty.loc ty
|
||||
let ctx' = extendDim body.name ctx
|
||||
ty = ty.term
|
||||
body = body.term
|
||||
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
|
||||
qout <- checkC ctx' sg body ty
|
||||
-- if Ψ, i, i = 0 | Γ ⊢ t = l : A
|
||||
equal (eqDim (BV 0) (K Zero) ctx') ty body (dweakT 1 l)
|
||||
lift $ equal loc (eqDim (B VZ loc) (K Zero loc) ctx') ty body (dweakT 1 l)
|
||||
-- if Ψ, i, i = 1 | Γ ⊢ t = r : A
|
||||
equal (eqDim (BV 0) (K One) ctx') ty body (dweakT 1 r)
|
||||
lift $ equal loc (eqDim (B VZ loc) (K One loc) ctx') ty body (dweakT 1 r)
|
||||
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
|
||||
pure qout
|
||||
|
||||
check' ctx sg Nat ty = toCheckType ctx sg Nat ty
|
||||
check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg Zero ty = do
|
||||
expectNat !defs ctx ty
|
||||
check' ctx sg (Zero {}) ty = do
|
||||
expectNat !defs ctx ty.loc ty
|
||||
pure $ zeroFor ctx
|
||||
|
||||
check' ctx sg (Succ n) ty = do
|
||||
expectNat !defs ctx ty
|
||||
checkC ctx sg n Nat
|
||||
check' ctx sg (Succ n {}) ty = do
|
||||
expectNat !defs ctx ty.loc ty
|
||||
checkC ctx sg n ty
|
||||
|
||||
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Box val) ty = do
|
||||
(q, ty) <- expectBOX !defs ctx ty
|
||||
check' ctx sg (Box val loc) ty = do
|
||||
(q, ty) <- expectBOX !defs ctx ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
|
||||
valout <- checkC ctx sg val ty
|
||||
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
|
||||
|
|
@ -232,7 +239,7 @@ mutual
|
|||
-- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
|
||||
infres <- inferC ctx sg e
|
||||
-- if Ψ | Γ ⊢ A' <: A
|
||||
subtype ctx infres.type ty
|
||||
lift $ subtype e.loc ctx infres.type ty
|
||||
-- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
|
||||
pure infres.qout
|
||||
|
||||
|
|
@ -241,13 +248,13 @@ mutual
|
|||
(subj : Term d n) -> (0 nc : NotClo subj) =>
|
||||
Maybe Universe -> TC ()
|
||||
|
||||
checkType' ctx (TYPE k) u = do
|
||||
checkType' ctx (TYPE k loc) u = do
|
||||
-- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
|
||||
case u of
|
||||
Just l => unless (k < l) $ throw $ BadUniverse k l
|
||||
Just l => unless (k < l) $ throw $ BadUniverse loc k l
|
||||
Nothing => pure ()
|
||||
|
||||
checkType' ctx (Pi qty arg res) u = do
|
||||
checkType' ctx (Pi qty arg res _) u = do
|
||||
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
|
||||
checkTypeC ctx arg u
|
||||
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
|
||||
|
|
@ -255,9 +262,9 @@ mutual
|
|||
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
|
||||
|
||||
checkType' ctx t@(Lam {}) u =
|
||||
throw $ NotType ctx t
|
||||
throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx (Sig fst snd) u = do
|
||||
checkType' ctx (Sig fst snd _) u = do
|
||||
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
|
||||
checkTypeC ctx fst u
|
||||
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
|
||||
|
|
@ -265,15 +272,15 @@ mutual
|
|||
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
|
||||
|
||||
checkType' ctx t@(Pair {}) u =
|
||||
throw $ NotType ctx t
|
||||
throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx (Enum _) u = pure ()
|
||||
checkType' ctx (Enum {}) u = pure ()
|
||||
-- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
|
||||
|
||||
checkType' ctx t@(Tag {}) u =
|
||||
throw $ NotType ctx t
|
||||
throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx (Eq t l r) u = do
|
||||
checkType' ctx (Eq t l r _) u = do
|
||||
-- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
|
||||
case t.body of
|
||||
Y t' => checkTypeC (extendDim t.name ctx) t' u
|
||||
|
|
@ -285,50 +292,31 @@ mutual
|
|||
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
|
||||
|
||||
checkType' ctx t@(DLam {}) u =
|
||||
throw $ NotType ctx t
|
||||
throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx Nat u = pure ()
|
||||
checkType' ctx Zero u = throw $ NotType ctx Zero
|
||||
checkType' ctx t@(Succ _) u = throw $ NotType ctx t
|
||||
checkType' ctx (Nat {}) u = pure ()
|
||||
checkType' ctx t@(Zero {}) u = throw $ NotType t.loc ctx t
|
||||
checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx (BOX q ty) u = checkType ctx ty u
|
||||
checkType' ctx t@(Box _) u = throw $ NotType ctx t
|
||||
checkType' ctx (BOX q ty _) u = checkType ctx ty u
|
||||
checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t
|
||||
|
||||
checkType' ctx (E e) u = do
|
||||
-- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
|
||||
infres <- inferC ctx szero e
|
||||
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
|
||||
case u of
|
||||
Just u => subtype ctx infres.type (TYPE u)
|
||||
Nothing => ignore $
|
||||
expectTYPE !defs ctx infres.type
|
||||
Just u => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
|
||||
Nothing => ignore $ expectTYPE !defs ctx e.loc infres.type
|
||||
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
|
||||
|
||||
private covering
|
||||
check0ScopeN : {s : Nat} ->
|
||||
TyContext d n -> CtxExtension0' s d n ->
|
||||
ScopeTermN s d n -> Term d n -> TC ()
|
||||
check0ScopeN ctx ext (S _ (N body)) ty = check0 ctx body ty
|
||||
check0ScopeN ctx ext (S names (Y body)) ty =
|
||||
check0 (extendTyN (addNames0 ext names) ctx) body (weakT s ty)
|
||||
|
||||
private covering
|
||||
check0Scope : TyContext d n -> Term d n ->
|
||||
ScopeTerm d n -> Term d n -> TC ()
|
||||
check0Scope ctx t = check0ScopeN ctx [< t]
|
||||
|
||||
|
||||
private covering
|
||||
checkTypeScopeN : TyContext d n -> CtxExtension0' s d n ->
|
||||
ScopeTermN s d n -> Maybe Universe -> TC ()
|
||||
checkTypeScopeN ctx ext (S _ (N body)) u = checkType ctx body u
|
||||
checkTypeScopeN ctx ext (S names (Y body)) u =
|
||||
checkType (extendTyN (addNames0 ext names) ctx) body u
|
||||
|
||||
private covering
|
||||
checkTypeScope : TyContext d n -> Term d n ->
|
||||
ScopeTerm d n -> Maybe Universe -> TC ()
|
||||
checkTypeScope ctx s = checkTypeScopeN ctx [< s]
|
||||
checkTypeScope ctx s (S _ (N body)) u = checkType ctx body u
|
||||
checkTypeScope ctx s (S [< x] (Y body)) u =
|
||||
checkType (extendTy Zero x s ctx) body u
|
||||
|
||||
|
||||
private covering
|
||||
|
|
@ -336,20 +324,20 @@ mutual
|
|||
(subj : Elim d n) -> (0 nc : NotClo subj) =>
|
||||
TC (InferResult' d n)
|
||||
|
||||
infer' ctx sg (F x) = do
|
||||
infer' ctx sg (F x loc) = do
|
||||
-- if π·x : A {≔ s} in global context
|
||||
g <- lookupFree x !defs
|
||||
g <- lookupFree x loc !defs
|
||||
-- if σ ≤ π
|
||||
expectCompatQ sg.fst g.qty.fst
|
||||
expectCompatQ loc sg.fst g.qty.fst
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
|
||||
let Val d = ctx.dimLen; Val n = ctx.termLen
|
||||
pure $ InfRes {type = g.type, qout = zeroFor ctx}
|
||||
|
||||
infer' ctx sg (B i) =
|
||||
infer' ctx sg (B i _) =
|
||||
-- if x : A ∈ Γ
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
|
||||
pure $ lookupBound sg.fst i ctx.tctx
|
||||
where
|
||||
where
|
||||
lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
|
||||
lookupBound pi VZ (ctx :< type) =
|
||||
InfRes {type = weakT 1 type, qout = zeroFor ctx :< pi}
|
||||
|
|
@ -357,19 +345,19 @@ mutual
|
|||
let InfRes {type, qout} = lookupBound pi i ctx in
|
||||
InfRes {type = weakT 1 type, qout = qout :< Zero}
|
||||
|
||||
infer' ctx sg (fun :@ arg) = do
|
||||
infer' ctx sg (App fun arg loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
|
||||
funres <- inferC ctx sg fun
|
||||
(qty, argty, res) <- expectPi !defs ctx funres.type
|
||||
(qty, argty, res) <- expectPi !defs ctx fun.loc funres.type
|
||||
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
|
||||
argout <- checkC ctx (subjMult sg qty) arg argty
|
||||
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
|
||||
pure $ InfRes {
|
||||
type = sub1 res $ arg :# argty,
|
||||
type = sub1 res $ Ann arg argty arg.loc,
|
||||
qout = funres.qout + qty * argout
|
||||
}
|
||||
|
||||
infer' ctx sg (CasePair pi pair ret body) = do
|
||||
infer' ctx sg (CasePair pi pair ret body loc) = do
|
||||
-- no check for 1 ≤ π, since pairs have a single constructor.
|
||||
-- e.g. at 0 the components are also 0 in the body
|
||||
--
|
||||
|
|
@ -377,27 +365,28 @@ mutual
|
|||
pairres <- inferC ctx sg pair
|
||||
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
|
||||
(tfst, tsnd) <- expectSig !defs ctx pairres.type
|
||||
(tfst, tsnd) <- expectSig !defs ctx pair.loc pairres.type
|
||||
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
|
||||
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
|
||||
-- with ρ₁, ρ₂ ≤ πσ
|
||||
let [< x, y] = body.names
|
||||
pisg = pi * sg.fst
|
||||
bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
|
||||
bodyty = substCasePairRet pairres.type ret
|
||||
bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pisg, pisg]
|
||||
bodyty = substCasePairRet body.names pairres.type ret
|
||||
bodyout <- checkC bodyctx sg body.term bodyty >>=
|
||||
popQs loc [< pisg, pisg]
|
||||
-- then Ψ | Γ ⊢ σ · caseπ ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
|
||||
pure $ InfRes {
|
||||
type = sub1 ret pair,
|
||||
qout = pi * pairres.qout + bodyout
|
||||
}
|
||||
|
||||
infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
|
||||
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
|
||||
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
|
||||
tres <- inferC ctx sg t
|
||||
ttags <- expectEnum !defs ctx tres.type
|
||||
ttags <- expectEnum !defs ctx t.loc tres.type
|
||||
-- if 1 ≤ π, OR there is only zero or one option
|
||||
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ One pi
|
||||
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
|
||||
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name tres.type ctx) ret.term Nothing
|
||||
-- if for each "a ⇒ s" in arms,
|
||||
|
|
@ -405,109 +394,109 @@ mutual
|
|||
-- with Σ₂ = lubs Σᵢ
|
||||
let arms = SortedMap.toList arms
|
||||
let armTags = SortedSet.fromList $ map fst arms
|
||||
unless (ttags == armTags) $ throw $ BadCaseEnum ttags armTags
|
||||
unless (ttags == armTags) $ throw $ BadCaseEnum loc ttags armTags
|
||||
armres <- for arms $ \(a, s) =>
|
||||
checkC ctx sg s (sub1 ret (Tag a :# tres.type))
|
||||
checkC ctx sg s $ sub1 ret $ Ann (Tag a s.loc) tres.type s.loc
|
||||
let Just armout = lubs ctx armres
|
||||
| _ => throw $ BadQtys "case arms" ctx $
|
||||
zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
|
||||
| _ => throw $ BadQtys loc "case arms" ctx $
|
||||
zipWith (\qs, (t, rhs) => (qs, Tag t noLoc)) armres arms
|
||||
pure $ InfRes {
|
||||
type = sub1 ret t,
|
||||
qout = pi * tres.qout + armout
|
||||
}
|
||||
|
||||
infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
|
||||
infer' ctx sg (CaseNat pi pi' n ret zer suc loc) = do
|
||||
-- if 1 ≤ π
|
||||
expectCompatQ One pi
|
||||
expectCompatQ loc One pi
|
||||
-- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
|
||||
nres <- inferC ctx sg n
|
||||
expectNat !defs ctx nres.type
|
||||
let nat = nres.type
|
||||
expectNat !defs ctx n.loc nat
|
||||
-- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name Nat ctx) ret.term Nothing
|
||||
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
|
||||
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
|
||||
zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
|
||||
zerout <- checkC ctx sg zer $ sub1 ret $ Ann (Zero zer.loc) nat zer.loc
|
||||
-- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
|
||||
-- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
|
||||
let [< p, ih] = suc.names
|
||||
pisg = pi * sg.fst
|
||||
sucCtx = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
|
||||
sucType = substCaseSuccRet ret
|
||||
sucCtx = extendTyN [< (pisg, p, Nat p.loc), (pi', ih, ret.term)] ctx
|
||||
sucType = substCaseSuccRet suc.names ret
|
||||
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
|
||||
expectCompatQ qih (pi' * sg.fst)
|
||||
expectCompatQ loc qih (pi' * sg.fst)
|
||||
-- [fixme] better error here
|
||||
expectCompatQ (qp + qih) pisg
|
||||
expectCompatQ loc (qp + qih) pisg
|
||||
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
|
||||
pure $ InfRes {
|
||||
type = sub1 ret n,
|
||||
qout = pi * nres.qout + zerout + Any * sucout
|
||||
}
|
||||
|
||||
infer' ctx sg (CaseBox pi box ret body) = do
|
||||
infer' ctx sg (CaseBox pi box ret body loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
|
||||
boxres <- inferC ctx sg box
|
||||
(q, ty) <- expectBOX !defs ctx boxres.type
|
||||
(q, ty) <- expectBOX !defs ctx box.loc boxres.type
|
||||
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
|
||||
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
|
||||
-- with ς ≤ ρπσ
|
||||
let qpisg = q * pi * sg.fst
|
||||
bodyCtx = extendTy qpisg body.name ty ctx
|
||||
bodyType = substCaseBoxRet ty ret
|
||||
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
|
||||
bodyType = substCaseBoxRet body.name ty ret
|
||||
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc qpisg
|
||||
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
|
||||
pure $ InfRes {
|
||||
type = sub1 ret box,
|
||||
qout = boxres.qout + bodyout
|
||||
}
|
||||
|
||||
infer' ctx sg (fun :% dim) = do
|
||||
infer' ctx sg (DApp fun dim loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
|
||||
InfRes {type, qout} <- inferC ctx sg fun
|
||||
ty <- fst <$> expectEq !defs ctx type
|
||||
ty <- fst <$> expectEq !defs ctx fun.loc type
|
||||
-- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
|
||||
pure $ InfRes {type = dsub1 ty dim, qout}
|
||||
|
||||
infer' ctx sg (Coe (S [< i] ty) p q val) = do
|
||||
let ty = ty.term
|
||||
checkType (extendDim i ctx) ty Nothing
|
||||
qout <- checkC ctx sg val (ty // one p)
|
||||
pure $ InfRes {type = ty // one q, qout}
|
||||
infer' ctx sg (Coe ty p q val loc) = do
|
||||
checkType (extendDim ty.name ctx) ty.term Nothing
|
||||
qout <- checkC ctx sg val $ dsub1 ty p
|
||||
pure $ InfRes {type = dsub1 ty q, qout}
|
||||
|
||||
infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1)) = do
|
||||
infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
|
||||
checkType ctx ty Nothing
|
||||
qout <- checkC ctx sg val ty
|
||||
let ty' = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
|
||||
ctx0 = extendDim j0 $ eqDim r (K Zero) ctx
|
||||
ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
|
||||
val0 = val0.term
|
||||
qout0 <- check ctx0 sg val0 ty'
|
||||
equal (eqDim (BV 0) p' ctx0) ty' val0 val'
|
||||
let ctx1 = extendDim j0 $ eqDim r (K One) ctx
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) ty' val0 val'
|
||||
let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
|
||||
val1 = val1.term
|
||||
qout1 <- check ctx1 sg val1 ty'
|
||||
equal (eqDim (BV 0) p' ctx1) ty' val1 val'
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) ty' val1 val'
|
||||
let qout0' = toMaybe $ map (, val0 // one p) qout0
|
||||
qout1' = toMaybe $ map (, val1 // one p) qout1
|
||||
qouts = (qout, val) :: catMaybes [qout0', qout1']
|
||||
let Just qout = lubs ctx $ map fst qouts
|
||||
| Nothing => throw $ BadQtys "composition" ctx qouts
|
||||
| Nothing => throw $ BadQtys loc "composition" ctx qouts
|
||||
pure $ InfRes {type = ty, qout}
|
||||
|
||||
infer' ctx sg (TypeCase ty ret arms def) = do
|
||||
infer' ctx sg (TypeCase ty ret arms def loc) = do
|
||||
-- if σ = 0
|
||||
expectEqualQ Zero sg.fst
|
||||
expectEqualQ loc Zero sg.fst
|
||||
-- if Ψ, Γ ⊢₀ e ⇒ Type u
|
||||
u <- expectTYPE !defs ctx . type =<< inferC ctx szero ty
|
||||
u <- expectTYPE !defs ctx ty.loc . type =<< inferC ctx szero ty
|
||||
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
|
||||
checkTypeC ctx ret Nothing
|
||||
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
|
||||
for_ allKinds $ \k =>
|
||||
for_ (lookupPrecise k arms) $ \(S names t) =>
|
||||
check0 (extendTyN (addNames0 (typecaseTel k u) names) ctx)
|
||||
check0 (extendTyN (typecaseTel k names u) ctx)
|
||||
t.term (weakT (arity k) ret)
|
||||
-- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
|
||||
pure $ InfRes {type = ret, qout = zeroFor ctx}
|
||||
|
||||
infer' ctx sg (term :# type) = do
|
||||
infer' ctx sg (Ann term type loc) = do
|
||||
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
|
||||
checkTypeC ctx type Nothing
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
|
||||
|
|
|
|||
|
|
@ -39,111 +39,122 @@ InferResult eqs d n = IfConsistent eqs $ InferResult' d n
|
|||
|
||||
|
||||
export
|
||||
lookupFree : Has ErrorEff fs => Name -> Definitions -> Eff fs Definition
|
||||
lookupFree x defs = maybe (throw $ NotInScope x) pure $ lookup x defs
|
||||
lookupFree : Has ErrorEff fs => Name -> Loc -> Definitions -> Eff fs Definition
|
||||
lookupFree x loc defs = maybe (throw $ NotInScope loc x) pure $ lookup x defs
|
||||
|
||||
|
||||
public export
|
||||
substCasePairRet : Term d n -> ScopeTerm d n -> Term d (2 + n)
|
||||
substCasePairRet dty retty =
|
||||
let arg = Pair (BVT 1) (BVT 0) :# (dty // fromNat 2) in
|
||||
substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term 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 : ScopeTerm d n -> Term d (2 + n)
|
||||
substCaseSuccRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
|
||||
substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
|
||||
substCaseSuccRet [< p, ih] retty =
|
||||
let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat noLoc) $ p.loc `extendL` ih.loc
|
||||
in
|
||||
retty.term // (arg ::: shift 2)
|
||||
|
||||
public export
|
||||
substCaseBoxRet : Term d n -> ScopeTerm d n -> Term d (S n)
|
||||
substCaseBoxRet dty retty =
|
||||
retty.term // (Box (BVT 0) :# weakT 1 dty ::: shift 1)
|
||||
substCaseBoxRet : BindName -> Term d n -> ScopeTerm d n -> Term 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)
|
||||
|
||||
|
||||
parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
|
||||
parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
|
||||
namespace TyContext
|
||||
parameters (ctx : TyContext d n)
|
||||
parameters (ctx : TyContext d n) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
tm d n -> Eff fs (NonRedex tm d n defs)
|
||||
whnf = let Val n = ctx.termLen; Val d = ctx.dimLen in
|
||||
rethrow . whnf defs (toWhnfContext ctx)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen; Val d = ctx.dimLen
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
|
||||
rethrow res
|
||||
|
||||
private covering %macro
|
||||
expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
|
||||
expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
|
||||
TTImp -> TTImp -> Elab (Term d n -> Eff fs a)
|
||||
expect k l r = do
|
||||
f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
|
||||
pure $ \t => maybe (throw $ k ctx.names t) pure . f . fst =<< whnf t
|
||||
pure $ \t => maybe (throw $ k loc ctx.names t) pure . f . fst =<< whnf t
|
||||
|
||||
export covering %inline
|
||||
expectTYPE : Term d n -> Eff fs Universe
|
||||
expectTYPE = expect ExpectedTYPE `(TYPE l) `(l)
|
||||
expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
|
||||
|
||||
export covering %inline
|
||||
expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
|
||||
expectPi = expect ExpectedPi `(Pi {qty, arg, res}) `((qty, arg, res))
|
||||
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 = expect ExpectedSig `(Sig {fst, snd}) `((fst, snd))
|
||||
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
|
||||
|
||||
export covering %inline
|
||||
expectEnum : Term d n -> Eff fs (SortedSet TagVal)
|
||||
expectEnum = expect ExpectedEnum `(Enum ts) `(ts)
|
||||
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 = expect ExpectedEq `(Eq {ty, l, r}) `((ty, l, r))
|
||||
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
|
||||
|
||||
export covering %inline
|
||||
expectNat : Term d n -> Eff fs ()
|
||||
expectNat = expect ExpectedNat `(Nat) `(())
|
||||
expectNat = expect ExpectedNat `(Nat {}) `(())
|
||||
|
||||
export covering %inline
|
||||
expectBOX : Term d n -> Eff fs (Qty, Term d n)
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty}) `((qty, ty))
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
|
||||
|
||||
|
||||
namespace EqContext
|
||||
parameters (ctx : EqContext n)
|
||||
parameters (ctx : EqContext n) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
tm 0 n -> Eff fs (NonRedex tm 0 n defs)
|
||||
whnf = let Val n = ctx.termLen in rethrow . whnf defs (toWhnfContext ctx)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
|
||||
rethrow res
|
||||
|
||||
private covering %macro
|
||||
expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
|
||||
expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
|
||||
TTImp -> TTImp -> Elab (Term 0 n -> Eff fs a)
|
||||
expect k l r = do
|
||||
f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
|
||||
pure $ \t =>
|
||||
let err = throw $ k ctx.names (t // shift0 ctx.dimLen) in
|
||||
let err = throw $ k loc ctx.names (t // shift0 ctx.dimLen) in
|
||||
maybe err pure . f . fst =<< whnf t
|
||||
|
||||
export covering %inline
|
||||
expectTYPE : Term 0 n -> Eff fs Universe
|
||||
expectTYPE = expect ExpectedTYPE `(TYPE l) `(l)
|
||||
expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
|
||||
|
||||
export covering %inline
|
||||
expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
|
||||
expectPi = expect ExpectedPi `(Pi {qty, arg, res}) `((qty, arg, res))
|
||||
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 = expect ExpectedSig `(Sig {fst, snd}) `((fst, snd))
|
||||
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
|
||||
|
||||
export covering %inline
|
||||
expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
|
||||
expectEnum = expect ExpectedEnum `(Enum ts) `(ts)
|
||||
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 = expect ExpectedEq `(Eq {ty, l, r}) `((ty, l, r))
|
||||
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
|
||||
|
||||
export covering %inline
|
||||
expectNat : Term 0 n -> Eff fs ()
|
||||
expectNat = expect ExpectedNat `(Nat) `(())
|
||||
expectNat = expect ExpectedNat `(Nat {}) `(())
|
||||
|
||||
export covering %inline
|
||||
expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty}) `((qty, ty))
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
|
||||
|
|
|
|||
|
|
@ -31,9 +31,9 @@ record TyContext d n where
|
|||
{auto dimLen : Singleton d}
|
||||
{auto termLen : Singleton n}
|
||||
dctx : DimEq d
|
||||
dnames : NContext d
|
||||
dnames : BContext d
|
||||
tctx : TContext d n
|
||||
tnames : NContext n
|
||||
tnames : BContext n
|
||||
qtys : QContext n -- only used for printing
|
||||
%name TyContext ctx
|
||||
|
||||
|
|
@ -44,9 +44,9 @@ record EqContext n where
|
|||
{dimLen : Nat}
|
||||
{auto termLen : Singleton n}
|
||||
dassign : DimAssign dimLen -- only used for printing
|
||||
dnames : NContext dimLen -- only used for printing
|
||||
dnames : BContext dimLen -- only used for printing
|
||||
tctx : TContext 0 n
|
||||
tnames : NContext n
|
||||
tnames : BContext n
|
||||
qtys : QContext n -- only used for printing
|
||||
%name EqContext ctx
|
||||
|
||||
|
|
@ -54,8 +54,8 @@ record EqContext n where
|
|||
public export
|
||||
record WhnfContext d n where
|
||||
constructor MkWhnfContext
|
||||
dnames : NContext d
|
||||
tnames : NContext n
|
||||
dnames : BContext d
|
||||
tnames : BContext n
|
||||
tctx : TContext d n
|
||||
%name WhnfContext ctx
|
||||
|
||||
|
|
@ -76,7 +76,7 @@ extendLen (tel :< _) x = [|S $ extendLen tel x|]
|
|||
|
||||
public export
|
||||
CtxExtension : Nat -> Nat -> Nat -> Type
|
||||
CtxExtension d = Telescope ((Qty, BaseName,) . Term d)
|
||||
CtxExtension d = Telescope ((Qty, BindName,) . Term d)
|
||||
|
||||
namespace TyContext
|
||||
public export %inline
|
||||
|
|
@ -101,11 +101,11 @@ namespace TyContext
|
|||
}
|
||||
|
||||
export %inline
|
||||
extendTy : Qty -> BaseName -> Term d n -> TyContext d n -> TyContext d (S n)
|
||||
extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
|
||||
extendTy q x s = extendTyN [< (q, x, s)]
|
||||
|
||||
export %inline
|
||||
extendDim : BaseName -> TyContext d n -> TyContext (S d) n
|
||||
extendDim : BindName -> TyContext d n -> TyContext (S d) n
|
||||
extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
|
||||
MkTyContext {
|
||||
dctx = dctx :<? Nothing,
|
||||
|
|
@ -141,8 +141,8 @@ namespace QOutput
|
|||
|
||||
export
|
||||
makeDAssign : DSubst d 0 -> DimAssign d
|
||||
makeDAssign (Shift SZ) = [<]
|
||||
makeDAssign (K e ::: th) = makeDAssign th :< e
|
||||
makeDAssign (Shift SZ) = [<]
|
||||
makeDAssign (K e _ ::: th) = makeDAssign th :< e
|
||||
|
||||
export
|
||||
makeEqContext' : {d : Nat} -> TyContext d n -> DSubst d 0 -> EqContext n
|
||||
|
|
@ -172,8 +172,7 @@ namespace EqContext
|
|||
null ctx = null ctx.dnames && null ctx.tnames
|
||||
|
||||
export %inline
|
||||
extendTyN : Telescope (\n => (Qty, BaseName, Term 0 n)) from to ->
|
||||
EqContext from -> EqContext to
|
||||
extendTyN : CtxExtension 0 from to -> EqContext from -> EqContext to
|
||||
extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
|
||||
let (qs, xs, ss) = unzip3 xss in
|
||||
MkEqContext {
|
||||
|
|
@ -185,11 +184,11 @@ namespace EqContext
|
|||
}
|
||||
|
||||
export %inline
|
||||
extendTy : Qty -> BaseName -> Term 0 n -> EqContext n -> EqContext (S n)
|
||||
extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
|
||||
extendTy q x s = extendTyN [< (q, x, s)]
|
||||
|
||||
export %inline
|
||||
extendDim : BaseName -> DimConst -> EqContext n -> EqContext n
|
||||
extendDim : BindName -> DimConst -> EqContext n -> EqContext n
|
||||
extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
|
||||
MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
|
||||
tctx, tnames, qtys}
|
||||
|
|
@ -214,7 +213,7 @@ namespace WhnfContext
|
|||
empty = MkWhnfContext [<] [<] [<]
|
||||
|
||||
export
|
||||
extendDimN : {s : Nat} -> NContext s -> WhnfContext d n ->
|
||||
extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
|
||||
WhnfContext (s + d) n
|
||||
extendDimN ns (MkWhnfContext {dnames, tnames, tctx}) =
|
||||
MkWhnfContext {
|
||||
|
|
@ -224,16 +223,16 @@ namespace WhnfContext
|
|||
}
|
||||
|
||||
export
|
||||
extendDim : BaseName -> WhnfContext d n -> WhnfContext (S d) n
|
||||
extendDim : BindName -> WhnfContext d n -> WhnfContext (S d) n
|
||||
extendDim i = extendDimN [< i]
|
||||
|
||||
|
||||
private
|
||||
data CtxBinder a = MkCtxBinder BaseName a
|
||||
data CtxBinder a = MkCtxBinder BindName a
|
||||
|
||||
PrettyHL a => PrettyHL (CtxBinder a) where
|
||||
prettyM (MkCtxBinder x t) = pure $
|
||||
sep [hsep [!(pretty0M $ TV x), colonD], !(pretty0M t)]
|
||||
sep [hsep [!(pretty0M $ TV x.name), colonD], !(pretty0M t)]
|
||||
|
||||
parameters (unicode : Bool)
|
||||
private
|
||||
|
|
@ -241,16 +240,16 @@ parameters (unicode : Bool)
|
|||
pipeD = hl Syntax "|"
|
||||
|
||||
export covering
|
||||
prettyTContext : NContext d ->
|
||||
QContext n -> NContext n ->
|
||||
prettyTContext : BContext d ->
|
||||
QContext n -> BContext n ->
|
||||
TContext d n -> Doc HL
|
||||
prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
|
||||
go : QContext m -> NContext m -> TContext d m -> SnocList (Doc HL)
|
||||
go : QContext m -> BContext m -> TContext d m -> SnocList (Doc HL)
|
||||
go [<] [<] [<] = [<]
|
||||
go (qs :< q) (xs :< x) (ctx :< t) =
|
||||
let bind = MkWithQty q $ MkCtxBinder x t in
|
||||
go qs xs ctx :<
|
||||
runPrettyWith unicode (toSnocList' ds) (toSnocList' xs) (pretty0M bind)
|
||||
runPrettyWith unicode (toNames ds) (toNames xs) (pretty0M bind)
|
||||
|
||||
export covering
|
||||
prettyTyContext : TyContext d n -> Doc HL
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
module Quox.Typing.Error
|
||||
|
||||
import Quox.Loc
|
||||
import Quox.Syntax
|
||||
import Quox.Typing.Context
|
||||
import Quox.Typing.EqMode
|
||||
|
|
@ -12,8 +13,8 @@ import Control.Eff
|
|||
public export
|
||||
record NameContexts d n where
|
||||
constructor MkNameContexts
|
||||
dnames : NContext d
|
||||
tnames : NContext n
|
||||
dnames : BContext d
|
||||
tnames : BContext n
|
||||
|
||||
namespace NameContexts
|
||||
export
|
||||
|
|
@ -21,11 +22,11 @@ namespace NameContexts
|
|||
empty = MkNameContexts [<] [<]
|
||||
|
||||
export
|
||||
extendDimN : NContext s -> NameContexts d n -> NameContexts (s + d) n
|
||||
extendDimN : BContext s -> NameContexts d n -> NameContexts (s + d) n
|
||||
extendDimN xs = {dnames $= (++ toSnocVect' xs)}
|
||||
|
||||
export
|
||||
extendDim : BaseName -> NameContexts d n -> NameContexts (S d) n
|
||||
extendDim : BindName -> NameContexts d n -> NameContexts (S d) n
|
||||
extendDim i = extendDimN [< i]
|
||||
|
||||
namespace TyContext
|
||||
|
|
@ -54,30 +55,30 @@ namespace WhnfContext
|
|||
|
||||
public export
|
||||
data Error
|
||||
= ExpectedTYPE (NameContexts d n) (Term d n)
|
||||
| ExpectedPi (NameContexts d n) (Term d n)
|
||||
| ExpectedSig (NameContexts d n) (Term d n)
|
||||
| ExpectedEnum (NameContexts d n) (Term d n)
|
||||
| ExpectedEq (NameContexts d n) (Term d n)
|
||||
| ExpectedNat (NameContexts d n) (Term d n)
|
||||
| ExpectedBOX (NameContexts d n) (Term d n)
|
||||
| BadUniverse Universe Universe
|
||||
| TagNotIn TagVal (SortedSet TagVal)
|
||||
| BadCaseEnum (SortedSet TagVal) (SortedSet TagVal)
|
||||
| BadQtys String (TyContext d n) (List (QOutput n, Term d n))
|
||||
= 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)
|
||||
| ExpectedBOX Loc (NameContexts d n) (Term 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))
|
||||
|
||||
-- first term arg of ClashT is the type
|
||||
| ClashT (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
|
||||
| ClashTy (EqContext n) EqMode (Term 0 n) (Term 0 n)
|
||||
| ClashE (EqContext n) EqMode (Elim 0 n) (Elim 0 n)
|
||||
| ClashU EqMode Universe Universe
|
||||
| ClashQ Qty Qty
|
||||
| NotInScope Name
|
||||
| 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)
|
||||
| ClashU Loc EqMode Universe Universe
|
||||
| ClashQ Loc Qty Qty
|
||||
| NotInScope Loc Name
|
||||
|
||||
| NotType (TyContext d n) (Term d n)
|
||||
| WrongType (EqContext n) (Term 0 n) (Term 0 n)
|
||||
| NotType Loc (TyContext d n) (Term d n)
|
||||
| WrongType Loc (EqContext n) (Term 0 n) (Term 0 n)
|
||||
|
||||
| MissingEnumArm TagVal (List TagVal)
|
||||
| MissingEnumArm Loc TagVal (List TagVal)
|
||||
|
||||
-- extra context
|
||||
| WhileChecking
|
||||
|
|
@ -166,18 +167,18 @@ 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}
|
||||
parameters {auto _ : Has ErrorEff fs} (loc : Loc)
|
||||
export %inline
|
||||
expectEqualQ : Qty -> Qty -> Eff fs ()
|
||||
expectEqualQ = expect ClashQ (==)
|
||||
expectEqualQ = expect (ClashQ loc) (==)
|
||||
|
||||
export %inline
|
||||
expectCompatQ : Qty -> Qty -> Eff fs ()
|
||||
expectCompatQ = expect ClashQ compat
|
||||
expectCompatQ = expect (ClashQ loc) compat
|
||||
|
||||
export %inline
|
||||
expectModeU : EqMode -> Universe -> Universe -> Eff fs ()
|
||||
expectModeU mode = expect (ClashU mode) $ ucmp mode
|
||||
expectModeU mode = expect (ClashU loc mode) $ ucmp mode
|
||||
|
||||
|
||||
private
|
||||
|
|
@ -207,8 +208,8 @@ parameters (unicode : Bool)
|
|||
dstermn ctx (S i t) = termn (extendDimN i ctx) t.term
|
||||
|
||||
private
|
||||
filterSameQtys : NContext n -> List (QOutput n, z) ->
|
||||
Exists $ \n' => (NContext n', List (QOutput n', z))
|
||||
filterSameQtys : BContext n -> List (QOutput n, z) ->
|
||||
Exists $ \n' => (BContext n', List (QOutput n', z))
|
||||
filterSameQtys [<] qts = Evidence 0 ([<], qts)
|
||||
filterSameQtys (ns :< n) qts =
|
||||
let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
|
||||
|
|
@ -224,7 +225,7 @@ parameters (unicode : Bool)
|
|||
|
||||
private
|
||||
printCaseQtys : TyContext d n ->
|
||||
NContext n' -> List (QOutput n', Term d n) ->
|
||||
BContext n' -> List (QOutput n', Term d n) ->
|
||||
List (Doc HL)
|
||||
printCaseQtys ctx ns qts =
|
||||
let Evidence l (ns, qts) = filterSameQtys ns qts in
|
||||
|
|
@ -233,94 +234,97 @@ parameters (unicode : Bool)
|
|||
commaList : PrettyHL a => Context' a l -> Doc HL
|
||||
commaList = hseparate comma . map (pretty0 unicode) . toList'
|
||||
|
||||
line : NContext l -> (QOutput l, Term d n) -> Doc HL
|
||||
line : BContext l -> (QOutput l, Term d n) -> Doc HL
|
||||
line ns (qs, t) =
|
||||
"-" <++> asep ["the term", termn ctx.names t,
|
||||
"uses variables", commaList $ TV <$> ns,
|
||||
"uses variables", commaList $ (TV . name) <$> ns,
|
||||
"with quantities", commaList qs]
|
||||
|
||||
-- [todo] only show some contexts, probably
|
||||
export
|
||||
prettyError : (showContext : Bool) -> Error -> Doc HL
|
||||
prettyError showContext = \case
|
||||
ExpectedTYPE ctx s =>
|
||||
sep ["expected a type universe, but got", termn ctx s]
|
||||
ExpectedTYPE loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected a type universe, but got", termn ctx s]
|
||||
|
||||
ExpectedPi ctx s =>
|
||||
sep ["expected a function type, but got", termn ctx s]
|
||||
ExpectedPi loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected a function type, but got", termn ctx s]
|
||||
|
||||
ExpectedSig ctx s =>
|
||||
sep ["expected a pair type, but got", termn ctx s]
|
||||
ExpectedSig loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected a pair type, but got", termn ctx s]
|
||||
|
||||
ExpectedEnum ctx s =>
|
||||
sep ["expected an enumeration type, but got", termn ctx s]
|
||||
ExpectedEnum loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected an enumeration type, but got",
|
||||
termn ctx s]
|
||||
|
||||
ExpectedEq ctx s =>
|
||||
sep ["expected an equality type, but got", termn ctx s]
|
||||
ExpectedEq loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected an equality type, but got", termn ctx s]
|
||||
|
||||
ExpectedNat ctx s {d, n} =>
|
||||
sep ["expected the type", pretty0 unicode $ Nat {d, n},
|
||||
"but got", termn ctx s]
|
||||
ExpectedNat loc ctx s {d, n} =>
|
||||
sep [prettyLoc loc <++> "expected the type",
|
||||
pretty0 unicode $ Nat noLoc {d, n}, "but got", termn ctx s]
|
||||
|
||||
ExpectedBOX ctx s =>
|
||||
sep ["expected a box type, but got", termn ctx s]
|
||||
ExpectedBOX loc ctx s =>
|
||||
sep [prettyLoc loc <++> "expected a box type, but got", termn ctx s]
|
||||
|
||||
BadUniverse k l =>
|
||||
sep ["the universe level", prettyUniverse k,
|
||||
BadUniverse loc k l =>
|
||||
sep [prettyLoc loc <++> "the universe level", prettyUniverse k,
|
||||
"is not strictly less than", prettyUniverse l]
|
||||
|
||||
TagNotIn tag set =>
|
||||
sep [sep ["tag", prettyTag tag, "is not contained in"],
|
||||
termn empty (Enum set)]
|
||||
TagNotIn loc tag set =>
|
||||
sep [hsep [prettyLoc loc, "tag", prettyTag tag, "is not contained in"],
|
||||
termn empty (Enum set noLoc)]
|
||||
|
||||
BadCaseEnum type arms =>
|
||||
sep ["case expression has head of type", termn empty (Enum type),
|
||||
"but cases for", termn empty (Enum arms)]
|
||||
BadCaseEnum loc type arms =>
|
||||
sep [prettyLoc loc <++> "case expression has head of type",
|
||||
termn empty (Enum type noLoc),
|
||||
"but cases for", termn empty (Enum arms noLoc)]
|
||||
|
||||
BadQtys what ctx arms =>
|
||||
BadQtys loc what ctx arms =>
|
||||
hang 4 $ sep $
|
||||
("inconsistent variable usage in" <++> fromString what) ::
|
||||
printCaseQtys ctx ctx.tnames arms
|
||||
hsep [prettyLoc loc, "inconsistent variable usage in", fromString what]
|
||||
:: printCaseQtys ctx ctx.tnames arms
|
||||
|
||||
ClashT ctx mode ty s t =>
|
||||
ClashT loc ctx mode ty s t =>
|
||||
inEContext ctx $
|
||||
sep ["the term", termn ctx.names0 s,
|
||||
sep [prettyLoc loc <++> "the term", termn ctx.names0 s,
|
||||
hsep ["is not", prettyMode mode], termn ctx.names0 t,
|
||||
"at type", termn ctx.names0 ty]
|
||||
|
||||
ClashTy ctx mode a b =>
|
||||
ClashTy loc ctx mode a b =>
|
||||
inEContext ctx $
|
||||
sep ["the type", termn ctx.names0 a,
|
||||
sep [prettyLoc loc <++> "the type", termn ctx.names0 a,
|
||||
hsep ["is not", prettyMode mode], termn ctx.names0 b]
|
||||
|
||||
ClashE ctx mode e f =>
|
||||
ClashE loc ctx mode e f =>
|
||||
inEContext ctx $
|
||||
sep ["the term", termn ctx.names0 $ E e,
|
||||
sep [prettyLoc loc <++> "the term", termn ctx.names0 $ E e,
|
||||
hsep ["is not", prettyMode mode], termn ctx.names0 $ E f]
|
||||
|
||||
ClashU mode k l =>
|
||||
sep ["the universe level", prettyUniverse k,
|
||||
ClashU loc mode k l =>
|
||||
sep [prettyLoc loc <++> "the universe level", prettyUniverse k,
|
||||
hsep ["is not", prettyMode mode], prettyUniverse l]
|
||||
|
||||
ClashQ pi rh =>
|
||||
sep ["the quantity", pretty0 unicode pi,
|
||||
ClashQ loc pi rh =>
|
||||
sep [prettyLoc loc <++> "the quantity", pretty0 unicode pi,
|
||||
"is not equal to", pretty0 unicode rh]
|
||||
|
||||
NotInScope x =>
|
||||
hsep [hl' Free $ pretty0 unicode x, "is not in scope"]
|
||||
NotInScope loc x =>
|
||||
hsep [prettyLoc loc, hl' Free $ pretty0 unicode x, "is not in scope"]
|
||||
|
||||
NotType ctx s =>
|
||||
NotType loc ctx s =>
|
||||
inTContext ctx $
|
||||
sep ["the term", termn ctx.names s, "is not a type"]
|
||||
sep [prettyLoc loc <++> "the term", termn ctx.names s, "is not a type"]
|
||||
|
||||
WrongType ctx ty s =>
|
||||
WrongType loc ctx ty s =>
|
||||
inEContext ctx $
|
||||
sep ["the term", termn ctx.names0 s,
|
||||
sep [prettyLoc loc <++> "the term", termn ctx.names0 s,
|
||||
"cannot have type", termn ctx.names0 ty]
|
||||
|
||||
MissingEnumArm tag tags =>
|
||||
sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"],
|
||||
termn empty $ Enum $ fromList tags]
|
||||
MissingEnumArm loc tag tags =>
|
||||
sep [hsep [prettyLoc loc, "the tag", hl Tag $ pretty tag,
|
||||
"is not contained in"],
|
||||
termn empty $ Enum (fromList tags) noLoc]
|
||||
|
||||
WhileChecking ctx pi s a err =>
|
||||
vsep [inTContext ctx $
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue