add locations and substitutions to untyped syntax
This commit is contained in:
parent
9cbd998d6f
commit
0b7bd0ef46
1 changed files with 109 additions and 46 deletions
|
|
@ -4,10 +4,12 @@ import Quox.Var
|
|||
import Quox.Context
|
||||
import Quox.Name
|
||||
import Quox.Pretty
|
||||
import Quox.Syntax.Subst
|
||||
|
||||
import Data.Vect
|
||||
import Data.DPair
|
||||
import Data.SortedMap
|
||||
import Data.SnocVect
|
||||
import Derive.Prelude
|
||||
%hide TT.Name
|
||||
|
||||
|
|
@ -15,40 +17,54 @@ import Derive.Prelude
|
|||
%language ElabReflection
|
||||
|
||||
|
||||
public export
|
||||
data Binder = Bind BaseName
|
||||
Eq Binder where _ == _ = True
|
||||
Ord Binder where compare _ _ = EQ
|
||||
%runElab derive "Binder" [Show]
|
||||
|
||||
public export
|
||||
data Term : Nat -> Type where
|
||||
F : (x : Name) -> Term n
|
||||
B : (i : Var n) -> Term n
|
||||
F : (x : Name) -> Loc -> Term n
|
||||
B : (i : Var n) -> Loc -> Term n
|
||||
|
||||
Lam : (x : Binder) -> (body : Term (S n)) -> Term n
|
||||
App : (fun, arg : Term n) -> Term n
|
||||
Lam : (x : BindName) -> (body : Term (S n)) -> Loc -> Term n
|
||||
App : (fun, arg : Term n) -> Loc -> Term n
|
||||
|
||||
Pair : (fst, snd : Term n) -> Term n
|
||||
Fst : (pair : Term n) -> Term n
|
||||
Snd : (pair : Term n) -> Term n
|
||||
Pair : (fst, snd : Term n) -> Loc -> Term n
|
||||
Fst : (pair : Term n) -> Loc -> Term n
|
||||
Snd : (pair : Term n) -> Loc -> Term n
|
||||
|
||||
Tag : (tag : String) -> Term n
|
||||
CaseEnum : (tag : Term n) -> (cases : List (String, Term n)) -> Term n
|
||||
Tag : (tag : String) -> Loc -> Term n
|
||||
CaseEnum : (tag : Term n) -> (cases : List (String, Term n)) -> Loc -> Term n
|
||||
||| empty match with an erased head
|
||||
Absurd : Loc -> Term n
|
||||
|
||||
Zero : Term n
|
||||
Succ : (nat : Term n) -> Term n
|
||||
Zero : Loc -> Term n
|
||||
Succ : (nat : Term n) -> Loc -> Term n
|
||||
CaseNat : (nat : Term n) ->
|
||||
(zer : Term n) ->
|
||||
(x, ih : Binder) -> (suc : Term (2 + n)) ->
|
||||
(x, ih : BindName) -> (suc : Term (2 + n)) ->
|
||||
Loc ->
|
||||
Term n
|
||||
|
||||
||| replacement for terms of type [0.A], for now
|
||||
ErasedBox : Term n
|
||||
Erased : Loc -> Term n
|
||||
%name Term s, t, u
|
||||
%runElab deriveIndexed "Term" [Eq, Ord, Show]
|
||||
|
||||
|
||||
export
|
||||
Located (Term n) where
|
||||
(F x loc).loc = loc
|
||||
(B i loc).loc = loc
|
||||
(Lam x body loc).loc = loc
|
||||
(App fun arg loc).loc = loc
|
||||
(Pair fst snd loc).loc = loc
|
||||
(Fst pair loc).loc = loc
|
||||
(Snd pair loc).loc = loc
|
||||
(Tag tag loc).loc = loc
|
||||
(CaseEnum tag cases loc).loc = loc
|
||||
(Absurd loc).loc = loc
|
||||
(Zero loc).loc = loc
|
||||
(Succ nat loc).loc = loc
|
||||
(CaseNat nat zer x ih suc loc).loc = loc
|
||||
(Erased loc).loc = loc
|
||||
|
||||
|
||||
public export
|
||||
0 Definitions : Type
|
||||
Definitions = SortedMap Name $ Term 0
|
||||
|
|
@ -56,37 +72,33 @@ Definitions = SortedMap Name $ Term 0
|
|||
|
||||
parameters {opts : LayoutOpts}
|
||||
export
|
||||
prettyBind : Binder -> Eff Pretty (Doc opts)
|
||||
prettyBind (Bind x) = hl TVar $ text $ baseStr x
|
||||
prettyTerm : BContext n -> Term n -> Eff Pretty (Doc opts)
|
||||
|
||||
export
|
||||
prettyTerm : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
|
||||
|
||||
export
|
||||
prettyArg : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyArg : BContext n -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
|
||||
|
||||
export
|
||||
prettyApp' : Context' Binder n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyApp' : Context' BindName n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyApp' xs fun arg =
|
||||
parensIfM App =<< do
|
||||
arg <- prettyArg xs arg
|
||||
pure $ sep [fun, arg]
|
||||
|
||||
export
|
||||
prettyApp : Context' Binder n -> Term n -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyApp : Context' BindName n -> Term n -> Term n -> Eff Pretty (Doc opts)
|
||||
prettyApp xs fun arg = prettyApp' xs !(prettyArg xs fun) arg
|
||||
|
||||
public export
|
||||
PrettyCaseArm : Nat -> Type
|
||||
PrettyCaseArm n = Exists $ \s => (Vect s Binder, Term (s + n))
|
||||
PrettyCaseArm n = Exists $ \s => (Vect s BindName, Term (s + n))
|
||||
|
||||
export %inline
|
||||
caseArm : Vect s Binder -> Term (s + n) -> PrettyCaseArm n
|
||||
caseArm : Vect s BindName -> Term (s + n) -> PrettyCaseArm n
|
||||
caseArm xs t = Evidence _ (xs, t)
|
||||
|
||||
export
|
||||
prettyCase : Context' Binder n ->
|
||||
prettyCase : Context' BindName n ->
|
||||
(a -> Eff Pretty (Doc opts)) ->
|
||||
Term n -> List (a, PrettyCaseArm n) ->
|
||||
Eff Pretty (Doc opts)
|
||||
|
|
@ -100,30 +112,81 @@ parameters {opts : LayoutOpts}
|
|||
body <- braces $ separateLoose !semiD cases
|
||||
pure $ sep [header, body]
|
||||
|
||||
prettyTerm _ (F x) = prettyFree x
|
||||
prettyTerm xs (B i) = prettyBind $ xs !!! i
|
||||
prettyTerm xs (Lam x body) =
|
||||
prettyTerm _ (F x _) = prettyFree x
|
||||
prettyTerm xs (B i _) = prettyTBind $ xs !!! i
|
||||
prettyTerm xs (Lam x body _) =
|
||||
parensIfM Outer =<< do
|
||||
header <- hsep <$> sequence [lamD, prettyBind x, darrowD]
|
||||
header <- hsep <$> sequence [lamD, prettyTBind x, darrowD]
|
||||
body <- withPrec Outer $ prettyTerm (xs :< x) body
|
||||
hangDSingle header body
|
||||
prettyTerm xs (App fun arg) = prettyApp xs fun arg
|
||||
prettyTerm xs (Pair fst snd) =
|
||||
prettyTerm xs (App fun arg _) = prettyApp xs fun arg
|
||||
prettyTerm xs (Pair fst snd _) =
|
||||
parens =<< separateTight !commaD <$>
|
||||
sequence {t = List} [prettyTerm xs fst, prettyTerm xs snd]
|
||||
prettyTerm xs (Fst pair) = prettyApp' xs !fstD pair
|
||||
prettyTerm xs (Snd pair) = prettyApp' xs !sndD pair
|
||||
prettyTerm xs (Tag tag) = prettyTag tag
|
||||
prettyTerm xs (CaseEnum tag cases) = assert_total
|
||||
prettyTerm xs (Fst pair _) = prettyApp' xs !fstD pair
|
||||
prettyTerm xs (Snd pair _) = prettyApp' xs !sndD pair
|
||||
prettyTerm xs (Tag tag _) = prettyTag tag
|
||||
prettyTerm xs (CaseEnum tag cases _) = assert_total
|
||||
prettyCase xs prettyTag tag $ map (mapSnd $ caseArm []) cases
|
||||
prettyTerm xs Zero = zeroD
|
||||
prettyTerm xs (Succ nat) = prettyApp' xs !succD nat
|
||||
prettyTerm xs (CaseNat nat zer x ih suc) = assert_total
|
||||
prettyTerm xs (Absurd _) = hl Syntax "absurd"
|
||||
prettyTerm xs (Zero _) = zeroD
|
||||
prettyTerm xs (Succ nat _) = prettyApp' xs !succD nat
|
||||
prettyTerm xs (CaseNat nat zer x ih suc _) = assert_total
|
||||
prettyCase xs pure nat
|
||||
[(!zeroD, caseArm [] zer),
|
||||
(!sucPat, caseArm [x, ih] suc)]
|
||||
where
|
||||
sucPat = separateTight {t = List} !commaD <$>
|
||||
sequence [[|succD <++> prettyBind x|], prettyBind ih]
|
||||
prettyTerm _ ErasedBox =
|
||||
sequence [[|succD <++> prettyTBind x|], prettyTBind ih]
|
||||
prettyTerm _ (Erased _) =
|
||||
hl Syntax =<< ifUnicode "⌷" "[]"
|
||||
|
||||
|
||||
public export
|
||||
USubst : Nat -> Nat -> Type
|
||||
USubst = Subst Term
|
||||
|
||||
|
||||
public export FromVar Term where fromVarLoc = B
|
||||
|
||||
|
||||
public export
|
||||
CanSubstSelf Term where
|
||||
s // th = case s of
|
||||
F x loc =>
|
||||
F x loc
|
||||
B i loc =>
|
||||
getLoc th i loc
|
||||
Lam x body loc =>
|
||||
Lam x (assert_total $ body // push th) loc
|
||||
App fun arg loc =>
|
||||
App (fun // th) (arg // th) loc
|
||||
Pair fst snd loc =>
|
||||
Pair (fst // th) (snd // th) loc
|
||||
Fst pair loc =>
|
||||
Fst (pair // th) loc
|
||||
Snd pair loc =>
|
||||
Snd (pair // th) loc
|
||||
Tag tag loc =>
|
||||
Tag tag loc
|
||||
CaseEnum tag cases loc =>
|
||||
CaseEnum (tag // th) (map (assert_total mapSnd (// th)) cases) loc
|
||||
Absurd loc =>
|
||||
Absurd loc
|
||||
Zero loc =>
|
||||
Zero loc
|
||||
Succ nat loc =>
|
||||
Succ (nat // th) loc
|
||||
CaseNat nat zer x ih suc loc =>
|
||||
CaseNat (nat // th) (zer // th)
|
||||
x ih (assert_total $ suc // pushN 2 th) loc
|
||||
Erased loc =>
|
||||
Erased loc
|
||||
|
||||
public export
|
||||
subN : SnocVect s (Term n) -> Term (s + n) -> Term n
|
||||
subN th t = t // fromSnocVect th
|
||||
|
||||
public export
|
||||
sub1 : Term n -> Term (S n) -> Term n
|
||||
sub1 e = subN [< e]
|
||||
|
|
|
|||
Loading…
Reference in a new issue