remove on-hold dir
This commit is contained in:
parent
dc076b636d
commit
4704dd0441
4 changed files with 0 additions and 673 deletions
|
|
@ -1,102 +0,0 @@
|
||||||
module Quox.Lexer
|
|
||||||
|
|
||||||
import public Quox.Token
|
|
||||||
|
|
||||||
import Data.String
|
|
||||||
import Data.String.Extra
|
|
||||||
import public Text.Lexer
|
|
||||||
import public Text.Lexer.Tokenizer
|
|
||||||
import Control.Monad.Either
|
|
||||||
import Generics.Derive
|
|
||||||
|
|
||||||
%default total
|
|
||||||
%language ElabReflection
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
record Error where
|
|
||||||
constructor Err
|
|
||||||
reason : StopReason
|
|
||||||
line, col : Int
|
|
||||||
char : Char
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
nameStart = pred $ \c => isAlpha c || c == '_'
|
|
||||||
nameCont = pred $ \c => isAlphaNum c || c == '_' || c == '\''
|
|
||||||
|
|
||||||
name = nameStart <+> many nameCont <+> reject nameCont
|
|
||||||
|
|
||||||
wild = is '_' <+> reject nameCont
|
|
||||||
|
|
||||||
%hide Text.Lexer.symbol
|
|
||||||
symbol = is '\'' <+> name
|
|
||||||
|
|
||||||
decimal = some digit <+> reject nameCont
|
|
||||||
|
|
||||||
|
|
||||||
natToNumber : Nat -> Number
|
|
||||||
natToNumber 0 = Zero
|
|
||||||
natToNumber 1 = One
|
|
||||||
natToNumber k = Other k
|
|
||||||
|
|
||||||
|
|
||||||
skip : Lexer -> Tokenizer (Maybe a)
|
|
||||||
skip lex = match lex $ const Nothing
|
|
||||||
|
|
||||||
simple : Char -> a -> Tokenizer (Maybe a)
|
|
||||||
simple ch = match (is ch) . const . Just
|
|
||||||
|
|
||||||
keyword : String -> Keyword -> Tokenizer (Maybe Token)
|
|
||||||
keyword str = match (exact str <+> reject nameCont) . const . Just . K
|
|
||||||
|
|
||||||
choice : (xs : List (Tokenizer a)) -> {auto 0 _ : NonEmpty xs} -> Tokenizer a
|
|
||||||
choice (t :: ts) = foldl (\a, b => a <|> b) t ts
|
|
||||||
|
|
||||||
match : Lexer -> (String -> a) -> Tokenizer (Maybe a)
|
|
||||||
match lex f = Tokenizer.match lex (Just . f)
|
|
||||||
%hide Tokenizer.match
|
|
||||||
|
|
||||||
|
|
||||||
tokens : Tokenizer (Maybe Token)
|
|
||||||
tokens = choice [
|
|
||||||
skip $ lineComment $ exact "--",
|
|
||||||
skip $ blockComment (exact "{-") (exact "-}"),
|
|
||||||
skip spaces,
|
|
||||||
|
|
||||||
simple '(' $ P LParen, simple ')' $ P RParen,
|
|
||||||
simple '[' $ P LSquare, simple ']' $ P RSquare,
|
|
||||||
simple '{' $ P LBrace, simple '}' $ P RBrace,
|
|
||||||
simple ',' $ P Comma,
|
|
||||||
simple '∷' $ P DblColon,
|
|
||||||
simple ':' $ P Colon, -- needs to be after '::'
|
|
||||||
simple '.' $ P Dot,
|
|
||||||
|
|
||||||
simple '→' $ P Arrow,
|
|
||||||
simple '⇒' $ P DblArrow,
|
|
||||||
simple '×' $ P Times,
|
|
||||||
simple '⊲' $ P Triangle,
|
|
||||||
match wild $ const $ P Wild,
|
|
||||||
|
|
||||||
keyword "λ" Lam,
|
|
||||||
keyword "let" Let, keyword "in" In,
|
|
||||||
keyword "case" Case, keyword "of" Of,
|
|
||||||
keyword "ω" Omega,
|
|
||||||
keyword "Π" Pi, keyword "Σ" Sigma, keyword "W" W,
|
|
||||||
|
|
||||||
match name $ Name,
|
|
||||||
match symbol $ Symbol . assert_total strTail,
|
|
||||||
|
|
||||||
match decimal $ N . natToNumber . cast,
|
|
||||||
match (is '★' <+> decimal) $ TYPE . cast . assert_total strTail
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
lex : String -> Either Error (List BToken)
|
|
||||||
lex str =
|
|
||||||
let (res, (reason, line, col, str)) = lex tokens str in
|
|
||||||
case reason of
|
|
||||||
EndInput => Right $ mapMaybe sequence res
|
|
||||||
_ => let char = assert_total strIndex str 0 in
|
|
||||||
Left $ Err {reason, line, col, char}
|
|
||||||
|
|
@ -1,159 +0,0 @@
|
||||||
module Quox.Parser
|
|
||||||
|
|
||||||
import Quox.Syntax
|
|
||||||
import Quox.Token
|
|
||||||
import Quox.Lexer
|
|
||||||
|
|
||||||
import Data.Maybe
|
|
||||||
import Data.SnocVect
|
|
||||||
import Data.SnocList
|
|
||||||
import Text.Parser
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
Vars : Nat -> Type
|
|
||||||
Vars n = SnocVect n String
|
|
||||||
|
|
||||||
public export
|
|
||||||
Grammar : Bool -> Type -> Type
|
|
||||||
Grammar = Core.Grammar () Token
|
|
||||||
%hide Core.Grammar
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Error
|
|
||||||
= Lex (Lexer.Error)
|
|
||||||
| Parse (List1 (ParsingError Token))
|
|
||||||
| Leftover (List BToken)
|
|
||||||
%hide Lexer.Error
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
parseAll : {c : Bool} -> Grammar c a -> List BToken -> Either Error a
|
|
||||||
parseAll grm input =
|
|
||||||
case parse grm input of
|
|
||||||
Right (x, []) => Right x
|
|
||||||
Right (x, rest) => Left $ Leftover rest
|
|
||||||
Left errs => Left $ Parse errs
|
|
||||||
|
|
||||||
public export
|
|
||||||
lexParseAll : {c : Bool} -> Grammar c a -> String -> Either Error a
|
|
||||||
lexParseAll grm = lex' >=> parseAll grm
|
|
||||||
where lex' : String -> Either Error (List BToken)
|
|
||||||
lex' = bimap Lex id . lex
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
punc : Punc -> Grammar True ()
|
|
||||||
punc p = terminal (show p) $ \case
|
|
||||||
P p' => if p == p' then Just () else Nothing
|
|
||||||
_ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
keyword : Keyword -> Grammar True ()
|
|
||||||
keyword k = terminal (show k) $ \case
|
|
||||||
K k' => if k == k' then Just () else Nothing
|
|
||||||
_ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
between : Punc -> Punc -> Grammar True a -> Grammar True a
|
|
||||||
between opener closer inner = punc opener *> inner <* punc closer
|
|
||||||
|
|
||||||
export
|
|
||||||
parens, squares, braces : Grammar True a -> Grammar True a
|
|
||||||
parens = between LParen RParen
|
|
||||||
squares = between LSquare RSquare
|
|
||||||
braces = between LBrace RBrace
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
number : Grammar True Nat
|
|
||||||
number = terminal "number" $ \case
|
|
||||||
N Zero => Just 0
|
|
||||||
N One => Just 1
|
|
||||||
N (Other k) => Just k
|
|
||||||
_ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
universe : Grammar True Nat
|
|
||||||
universe = terminal "universe" $ \case TYPE k => Just k; _ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
zero, one, omega : Grammar True ()
|
|
||||||
zero = terminal "0" $ \case N Zero => Just (); _ => Nothing
|
|
||||||
one = terminal "1" $ \case N One => Just (); _ => Nothing
|
|
||||||
omega = terminal "ω" $ \case K Omega => Just (); _ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
quantity : Grammar True Qty
|
|
||||||
quantity = Zero <$ zero <|> One <$ one <|> Any <$ omega
|
|
||||||
|
|
||||||
|
|
||||||
find1 : Eq a => SnocVect k a -> a -> Maybe (Var k)
|
|
||||||
find1 [<] y = Nothing
|
|
||||||
find1 (sx :< x) y = if x == y then Just VZ else VS <$> find1 sx y
|
|
||||||
|
|
||||||
find : Vars k -> Name -> Maybe (Var k)
|
|
||||||
find vs (MakeName [<] (UN y)) = find1 vs y
|
|
||||||
find _ _ = Nothing
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
checkAvoid1 : Vars n -> String -> Grammar False ()
|
|
||||||
checkAvoid1 avoid y =
|
|
||||||
when (isJust $ find1 avoid y) $
|
|
||||||
fail "wrong type of bound variable: \{show y}"
|
|
||||||
|
|
||||||
export
|
|
||||||
checkAvoid : Vars n -> Name -> Grammar False ()
|
|
||||||
checkAvoid avoid (MakeName [<] (UN y)) = checkAvoid1 avoid y
|
|
||||||
checkAvoid _ _ = pure ()
|
|
||||||
|
|
||||||
export
|
|
||||||
bound : (what : String) -> (bound : Vars k) -> (avoid : Vars n) ->
|
|
||||||
Grammar True (Var k)
|
|
||||||
bound what vs avoid = do
|
|
||||||
x <- terminal "bound \{what} variable" $ \case Name x => Just x; _ => Nothing
|
|
||||||
checkAvoid1 avoid x
|
|
||||||
maybe (fail "not in scope: \{x}") pure $ find1 vs x
|
|
||||||
|
|
||||||
export
|
|
||||||
sname : Grammar True String
|
|
||||||
sname = terminal "simple name" $ \case Name x => pure x; _ => Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
qname : Grammar True Name
|
|
||||||
qname = do
|
|
||||||
parts <- sepBy1 (punc Dot) sname
|
|
||||||
pure $ MakeName {mods = cast $ init parts, base = UN $ last parts}
|
|
||||||
|
|
||||||
export
|
|
||||||
nameWith : (bound : Vars k) -> (avoid : Vars n) ->
|
|
||||||
Grammar True (Either (Var k) Name)
|
|
||||||
nameWith bound avoid = do
|
|
||||||
y <- qname
|
|
||||||
checkAvoid avoid y
|
|
||||||
pure $ maybe (Right y) Left $ find bound y
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
dimension : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Dim d)
|
|
||||||
dimension dvars tvars =
|
|
||||||
K Zero <$ zero
|
|
||||||
<|> K One <$ one
|
|
||||||
<|> B <$> bound "dimension" {bound = dvars, avoid = tvars}
|
|
||||||
|
|
||||||
|
|
||||||
mutual
|
|
||||||
export
|
|
||||||
term : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Term d n)
|
|
||||||
term dvars tvars =
|
|
||||||
E <$> squares (elim {dvars, tvars})
|
|
||||||
<|> TYPE . U <$> universe
|
|
||||||
|
|
||||||
export
|
|
||||||
elim : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Elim d n)
|
|
||||||
elim dvars tvars =
|
|
||||||
either B F <$> nameWith {bound = tvars, avoid = dvars}
|
|
||||||
|
|
@ -1,363 +0,0 @@
|
||||||
module Quox.Syntax.DimEq
|
|
||||||
|
|
||||||
import public Quox.Syntax.Var
|
|
||||||
import public Quox.Syntax.Dim
|
|
||||||
import public Quox.Syntax.Subst
|
|
||||||
import public Quox.Context
|
|
||||||
|
|
||||||
import Data.Maybe
|
|
||||||
import Data.DPair
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
mutual
|
|
||||||
||| consistent (0≠1) set of constraints between dimension variables
|
|
||||||
public export
|
|
||||||
data DimEq' : Nat -> Type where
|
|
||||||
||| empty context
|
|
||||||
Nil : DimEq' 0
|
|
||||||
||| Ψ, 𝑖, 𝑖=ε
|
|
||||||
Const : (eqs : DimEq' d) -> (e : DimConst) -> DimEq' (S d)
|
|
||||||
||| Ψ, 𝑖, 𝑖=𝑗 (Ψ ⊢ 𝑗 and 𝑗 is unassigned)
|
|
||||||
Var : (eqs : DimEq' d) -> (i : Var d) -> (0 un : Unassigned eqs i) ->
|
|
||||||
DimEq' (S d)
|
|
||||||
||| Ψ, 𝑖 (𝑖 unassigned)
|
|
||||||
None : (eqs : DimEq' d) -> DimEq' (S d)
|
|
||||||
%name DimEq' eqs
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Unassigned : DimEq' d -> Var d -> Type where
|
|
||||||
UZ : Unassigned (None eqs) VZ
|
|
||||||
USK : Unassigned eqs i -> Unassigned (Const eqs e) (VS i)
|
|
||||||
USV : Unassigned eqs i -> Unassigned (Var eqs j un) (VS i)
|
|
||||||
USN : Unassigned eqs i -> Unassigned (None eqs ) (VS i)
|
|
||||||
%name Unassigned un
|
|
||||||
|
|
||||||
|
|
||||||
||| set of constraints that might be inconsistent
|
|
||||||
public export
|
|
||||||
data DimEq : Nat -> Type where
|
|
||||||
||| 0=1
|
|
||||||
ZeroIsOne : DimEq d
|
|
||||||
||| 0≠1, plus other constraints
|
|
||||||
C : (eqs : DimEq' d) -> DimEq d
|
|
||||||
%name DimEq eqs
|
|
||||||
|
|
||||||
|
|
||||||
||| contains a value iff the dim ctx is consistent
|
|
||||||
public export
|
|
||||||
data IfConsistent : DimEq d -> Type -> Type where
|
|
||||||
Nothing : IfConsistent ZeroIsOne a
|
|
||||||
Just : a -> IfConsistent (C eqs) a
|
|
||||||
|
|
||||||
export
|
|
||||||
Functor (IfConsistent eqs) where
|
|
||||||
map f Nothing = Nothing
|
|
||||||
map f (Just x) = Just (f x)
|
|
||||||
|
|
||||||
export
|
|
||||||
Foldable (IfConsistent eqs) where
|
|
||||||
foldr f z Nothing = z
|
|
||||||
foldr f z (Just x) = f x z
|
|
||||||
|
|
||||||
export
|
|
||||||
Traversable (IfConsistent eqs) where
|
|
||||||
traverse f Nothing = pure Nothing
|
|
||||||
traverse f (Just x) = Just <$> f x
|
|
||||||
|
|
||||||
||| performs an action if the dim ctx is consistent
|
|
||||||
public export
|
|
||||||
ifConsistent : Applicative f => (eqs : DimEq d) -> f a -> f (IfConsistent eqs a)
|
|
||||||
ifConsistent ZeroIsOne act = pure Nothing
|
|
||||||
ifConsistent (C _) act = Just <$> act
|
|
||||||
|
|
||||||
|
|
||||||
public export %inline
|
|
||||||
weakD : Dim d -> Dim (S d)
|
|
||||||
weakD p = p // SS SZ
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
tail' : DimEq' (S d) -> DimEq' d
|
|
||||||
tail' (Const eqs e) = eqs
|
|
||||||
tail' (Var eqs i un) = eqs
|
|
||||||
tail' (None eqs ) = eqs
|
|
||||||
|
|
||||||
public export
|
|
||||||
tail : DimEq (S d) -> DimEq d
|
|
||||||
tail ZeroIsOne = ZeroIsOne
|
|
||||||
tail (C eqs) = C $ tail' eqs
|
|
||||||
|
|
||||||
public export
|
|
||||||
head' : DimEq' (S d) -> Maybe (Dim d)
|
|
||||||
head' (Const _ e) = Just $ K e
|
|
||||||
head' (Var _ i _) = Just $ B i
|
|
||||||
head' (None _) = Nothing
|
|
||||||
|
|
||||||
export
|
|
||||||
tailU : Unassigned eqs (VS i) -> Unassigned (tail' eqs) i
|
|
||||||
tailU (USK un) = un
|
|
||||||
tailU (USV un) = un
|
|
||||||
tailU (USN un) = un
|
|
||||||
|
|
||||||
|
|
||||||
||| make a dim ctx where each variable has a constant assignment
|
|
||||||
public export
|
|
||||||
fromGround' : Context' DimConst d -> DimEq' d
|
|
||||||
fromGround' [<] = Nil
|
|
||||||
fromGround' (ctx :< e) = Const (fromGround' ctx) e
|
|
||||||
|
|
||||||
||| make a dim ctx where each variable has a constant assignment
|
|
||||||
public export
|
|
||||||
fromGround : Context' DimConst d -> DimEq d
|
|
||||||
fromGround = C . fromGround'
|
|
||||||
|
|
||||||
|
|
||||||
||| make a dim ctx where each variable is unassigned
|
|
||||||
public export
|
|
||||||
new' : (d : Nat) -> DimEq' d
|
|
||||||
new' 0 = Nil
|
|
||||||
new' (S d) = None (new' d)
|
|
||||||
|
|
||||||
||| make a dim ctx where each variable is unassigned
|
|
||||||
public export
|
|
||||||
new : (d : Nat) -> DimEq d
|
|
||||||
new d = C $ new' d
|
|
||||||
|
|
||||||
|
|
||||||
||| if the dim is a variable, then it is unassigned
|
|
||||||
public export
|
|
||||||
data UnassignedDim : DimEq' d -> Dim d -> Type where
|
|
||||||
UDK : UnassignedDim eqs (K e)
|
|
||||||
UDB : Unassigned eqs i -> UnassignedDim eqs (B i)
|
|
||||||
|
|
||||||
export
|
|
||||||
weakUD : {eqs : DimEq' (S d)} -> {p : Dim d} ->
|
|
||||||
UnassignedDim (tail' eqs) p -> UnassignedDim eqs (weakD p)
|
|
||||||
weakUD UDK = UDK
|
|
||||||
weakUD (UDB un) {eqs = Const eqs e} = UDB $ USK un
|
|
||||||
weakUD (UDB un) {eqs = Var eqs _ _} = UDB $ USV un
|
|
||||||
weakUD (UDB un) {eqs = None eqs} = UDB $ USN un
|
|
||||||
|
|
||||||
|
|
||||||
||| get the constraint on a variable 𝑖. if it is equal to another var 𝑗,
|
|
||||||
||| then 𝑗 is not further constrained
|
|
||||||
public export
|
|
||||||
getVarPrf : (eqs : DimEq' d) -> Var d -> Subset (Dim d) (UnassignedDim eqs)
|
|
||||||
getVarPrf (Const eqs e) VZ = Element (K e) UDK
|
|
||||||
getVarPrf (Var eqs i un) VZ = Element (B $ VS i) (UDB $ USV un)
|
|
||||||
getVarPrf (None eqs) VZ = Element (B VZ) (UDB UZ)
|
|
||||||
getVarPrf (Const eqs _) (VS i) = let p = getVarPrf eqs i in
|
|
||||||
Element (weakD p.fst) (weakUD p.snd)
|
|
||||||
getVarPrf (Var eqs _ _) (VS i) = let p = getVarPrf eqs i in
|
|
||||||
Element (weakD p.fst) (weakUD p.snd)
|
|
||||||
getVarPrf (None eqs) (VS i) = let p = getVarPrf eqs i in
|
|
||||||
Element (weakD p.fst) (weakUD p.snd)
|
|
||||||
|
|
||||||
public export
|
|
||||||
getVar : (eqs : DimEq' d) -> Var d -> Dim d
|
|
||||||
getVar eqs i = fst $ getVarPrf eqs i
|
|
||||||
|
|
||||||
public export
|
|
||||||
getPrf : (eqs : DimEq' d) -> Dim d -> Subset (Dim d) (UnassignedDim eqs)
|
|
||||||
getPrf eqs (K e) = Element (K e) UDK
|
|
||||||
getPrf eqs (B i) = getVarPrf eqs i
|
|
||||||
|
|
||||||
public export
|
|
||||||
get : DimEq' d -> Dim d -> Dim d
|
|
||||||
get eqs p = fst $ getPrf eqs p
|
|
||||||
|
|
||||||
|
|
||||||
-- version of `get` that only shifts once but is even more annoying to prove
|
|
||||||
-- anything about
|
|
||||||
private
|
|
||||||
getShift' : Shift d out -> DimEq' d -> Var d -> Maybe (Dim out)
|
|
||||||
getShift' by (Const eqs e) VZ = Just $ K e
|
|
||||||
getShift' by (Var eqs i un) VZ = Just $ B $ i // ssDown by
|
|
||||||
getShift' by (None eqs) VZ = Nothing
|
|
||||||
getShift' by eqs (VS i) = getShift' (ssDown by) (tail' eqs) i
|
|
||||||
|
|
||||||
private
|
|
||||||
getShift0' : DimEq' d -> Var d -> Maybe (Dim d)
|
|
||||||
getShift0' = getShift' SZ
|
|
||||||
|
|
||||||
private
|
|
||||||
get' : DimEq' d -> Dim d -> Dim d
|
|
||||||
get' eqs (K e) = K e
|
|
||||||
get' eqs (B i) = fromMaybe (B i) $ getShift0' eqs i
|
|
||||||
|
|
||||||
%transform "DimEq.get" get = get'
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
Equal' : DimEq' d -> Rel (Dim d)
|
|
||||||
Equal' eqs p q = get eqs p = get eqs q
|
|
||||||
|
|
||||||
||| whether two dimensions are equal under the current constraints
|
|
||||||
public export
|
|
||||||
data Equal : DimEq d -> Rel (Dim d) where
|
|
||||||
Eq01 : Equal ZeroIsOne p q
|
|
||||||
EqC : Equal' eqs p q -> Equal (C eqs) p q
|
|
||||||
%name DimEq.Equal prf
|
|
||||||
|
|
||||||
export
|
|
||||||
decEqual : (eqs : DimEq d) -> Dec2 (Equal eqs)
|
|
||||||
decEqual ZeroIsOne _ _ = Yes Eq01
|
|
||||||
decEqual (C eqs) p q = case get eqs p `decEq` get eqs q of
|
|
||||||
Yes y => Yes $ EqC y
|
|
||||||
No n => No $ \case EqC p => n p
|
|
||||||
|
|
||||||
export
|
|
||||||
equal : (eqs : DimEq d) -> Dim d -> Dim d -> Bool
|
|
||||||
equal eqs p q = isYes $ decEqual eqs p q
|
|
||||||
|
|
||||||
export
|
|
||||||
{eqs : DimEq d} -> Reflexive _ (Equal eqs) where
|
|
||||||
reflexive = case eqs of
|
|
||||||
ZeroIsOne => Eq01
|
|
||||||
C eqs => EqC Refl
|
|
||||||
|
|
||||||
export
|
|
||||||
Symmetric _ (Equal eqs) where
|
|
||||||
symmetric Eq01 = Eq01
|
|
||||||
symmetric (EqC eq) = EqC $ sym eq
|
|
||||||
|
|
||||||
export
|
|
||||||
Transitive _ (Equal eqs) where
|
|
||||||
transitive Eq01 Eq01 = Eq01
|
|
||||||
transitive (EqC p) (EqC q) = EqC $ p `trans` q
|
|
||||||
|
|
||||||
export {eqs : DimEq d} -> Equivalence _ (Equal eqs) where
|
|
||||||
|
|
||||||
|
|
||||||
||| extend the context with a new variable, possibly constrained
|
|
||||||
public export
|
|
||||||
(:<) : DimEq' d -> Maybe (Dim d) -> DimEq' (S d)
|
|
||||||
eqs :< Nothing = None eqs
|
|
||||||
eqs :< Just (K e) = Const eqs e
|
|
||||||
eqs :< Just (B i) with (getVarPrf eqs i)
|
|
||||||
_ | Element (K e) _ = Const eqs e
|
|
||||||
_ | Element (B j) un = Var eqs j $ let UDB un = un in un
|
|
||||||
|
|
||||||
infixl 7 :<?
|
|
||||||
||| extend the context with a new variable, possibly constrained
|
|
||||||
public export
|
|
||||||
(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
|
|
||||||
ZeroIsOne :<? p = ZeroIsOne
|
|
||||||
C eqs :<? p = C $ eqs :< p
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
checkConst : DimConst -> DimConst -> DimEq' d -> DimEq d
|
|
||||||
checkConst e f eqs = case decEq e f of Yes _ => C eqs; No _ => ZeroIsOne
|
|
||||||
|
|
||||||
public export
|
|
||||||
setConst : Var d -> DimConst -> DimEq' d -> DimEq d
|
|
||||||
setConst VZ e (Const eqs f) = checkConst e f $ eqs :< Just (K e)
|
|
||||||
setConst VZ e (Var eqs i un) = setConst i e eqs :<? Just (K e)
|
|
||||||
setConst VZ e (None eqs) = C $ Const eqs e
|
|
||||||
setConst (VS i) e (Const eqs f) = setConst i e eqs :<? Just (K f)
|
|
||||||
setConst (VS i) e (Var eqs j un) = setConst i e eqs :<? Just (B j)
|
|
||||||
setConst (VS i) e (None eqs) = setConst i e eqs :<? Nothing
|
|
||||||
|
|
||||||
public export
|
|
||||||
setVar : Var d -> Var d -> DimEq' d -> DimEq d
|
|
||||||
setVar VZ VZ eqs = C eqs
|
|
||||||
setVar VZ (VS j) (Const eqs e) = setConst j e eqs :<? Just (K e)
|
|
||||||
setVar VZ (VS j) (Var eqs k un) = setVar j k eqs :<? Just (B k)
|
|
||||||
setVar VZ (VS j) (None eqs) = C eqs :<? Just (B j)
|
|
||||||
setVar (VS i) VZ (Const eqs e) = setConst i e eqs :<? Just (K e)
|
|
||||||
setVar (VS i) VZ (Var eqs k un) = setVar i k eqs :<? Just (B k)
|
|
||||||
setVar (VS i) VZ (None eqs) = C eqs :<? Just (B i)
|
|
||||||
setVar (VS i) (VS j) (Const eqs e) = setVar i j eqs :<? Just (K e)
|
|
||||||
setVar (VS i) (VS j) (Var eqs k un) = setVar i j eqs :<? Just (B k)
|
|
||||||
setVar (VS i) (VS j) (None eqs) = setVar i j eqs :<? Nothing
|
|
||||||
|
|
||||||
public export
|
|
||||||
set : Dim d -> Dim d -> DimEq d -> DimEq d
|
|
||||||
set p q ZeroIsOne = ZeroIsOne
|
|
||||||
set (K e) (K f) (C eqs) = checkConst e f eqs
|
|
||||||
set (K e) (B j) (C eqs) = setConst j e eqs
|
|
||||||
set (B i) (K f) (C eqs) = setConst i f eqs
|
|
||||||
set (B i) (B j) (C eqs) = setVar i j eqs
|
|
||||||
|
|
||||||
|
|
||||||
private
|
|
||||||
splitV0 : (p : Dim (S d)) -> Either (p = B VZ) (q : Dim d ** p = weakD q)
|
|
||||||
splitV0 (K e) = Right (K e ** Refl)
|
|
||||||
splitV0 (B VZ) = Left Refl
|
|
||||||
splitV0 (B (VS i)) = Right (B i ** Refl)
|
|
||||||
|
|
||||||
|
|
||||||
export
|
|
||||||
0 getSnoc : (eqs : DimEq' d) -> (u : Maybe (Dim d)) -> (i : Var d) ->
|
|
||||||
getVar (eqs :< u) (VS i) = weakD (getVar eqs i)
|
|
||||||
getSnoc eqs Nothing i = Refl
|
|
||||||
getSnoc eqs (Just (K e)) i = Refl
|
|
||||||
getSnoc eqs (Just (B j)) i with (getVarPrf eqs j)
|
|
||||||
_ | Element (K _) _ = Refl
|
|
||||||
_ | Element (B _) _ = Refl
|
|
||||||
|
|
||||||
export
|
|
||||||
0 snocStrengthen : (p, q : Dim d) ->
|
|
||||||
Equal' (eqs :< u) (weakD p) (weakD q) -> Equal' eqs p q
|
|
||||||
snocStrengthen (K e) (K e) Refl = Refl
|
|
||||||
snocStrengthen (K e) (B i) prf =
|
|
||||||
shiftInj (SS SZ) _ _ $
|
|
||||||
rewrite sym $ getSnoc eqs u i in prf
|
|
||||||
snocStrengthen (B i) (K e) prf =
|
|
||||||
shiftInj (SS SZ) _ _ $
|
|
||||||
rewrite sym $ getSnoc eqs u i in prf
|
|
||||||
snocStrengthen (B i) (B j) prf =
|
|
||||||
shiftInj (SS SZ) _ _ $
|
|
||||||
rewrite sym $ getSnoc eqs u i in
|
|
||||||
rewrite sym $ getSnoc eqs u j in prf
|
|
||||||
|
|
||||||
export
|
|
||||||
0 snocStable : (eqs : DimEq d) -> (u : Maybe (Dim d)) -> (p, q : Dim d) ->
|
|
||||||
Equal eqs p q -> Equal (eqs :<? u) (weakD p) (weakD q)
|
|
||||||
snocStable ZeroIsOne u p q Eq01 = Eq01
|
|
||||||
snocStable (C eqs) u (K e) (K e) (EqC Refl) = reflexive
|
|
||||||
snocStable (C eqs) u (K e) (B i) (EqC prf) = EqC $
|
|
||||||
rewrite getSnoc eqs u i in rewrite sym prf in Refl
|
|
||||||
snocStable (C eqs) u (B i) (K e) (EqC prf) = EqC $
|
|
||||||
rewrite getSnoc eqs u i in rewrite prf in Refl
|
|
||||||
snocStable (C eqs) u (B i) (B j) (EqC prf) = EqC $
|
|
||||||
rewrite getSnoc eqs u i in
|
|
||||||
rewrite getSnoc eqs u j in
|
|
||||||
rewrite prf in Refl
|
|
||||||
|
|
||||||
export
|
|
||||||
0 checkConstStable : (eqs : DimEq' d) -> (e, f : DimConst) ->
|
|
||||||
(p, q : Dim d) -> Equal' eqs p q ->
|
|
||||||
Equal (checkConst e f eqs) p q
|
|
||||||
checkConstStable eqs e f p q prf with (decEq e f)
|
|
||||||
_ | Yes _ = EqC prf
|
|
||||||
_ | No _ = Eq01
|
|
||||||
|
|
||||||
export
|
|
||||||
0 setConstStable : (eqs : DimEq' d) -> (i : Var d) -> (e : DimConst) ->
|
|
||||||
(p, q : Dim d) -> Equal' eqs p q ->
|
|
||||||
Equal (setConst i e eqs) p q
|
|
||||||
setConstStable (Const eqs f) VZ e p q prf with (decEq e f)
|
|
||||||
_ | Yes _ = EqC prf
|
|
||||||
_ | No _ = Eq01
|
|
||||||
setConstStable (Const eqs f) (VS i) e p q prf = ?setConstStable_rhs_5
|
|
||||||
setConstStable (Var eqs j un) VZ e p q prf = ?setConstStable_rhs_6
|
|
||||||
setConstStable (Var eqs j un) (VS i) e p q prf = ?setConstStable_rhs_7
|
|
||||||
setConstStable (None eqs) VZ e p q prf = ?setConstStable_rhs_8
|
|
||||||
setConstStable (None eqs) (VS i) e p q prf = ?setConstStable_rhs_9
|
|
||||||
|
|
||||||
export
|
|
||||||
0 setVarStable : (eqs : DimEq' d) -> (i, j : Var d) ->
|
|
||||||
(p, q : Dim d) -> Equal' eqs p q ->
|
|
||||||
Equal (setVar i j eqs) p q
|
|
||||||
|
|
||||||
export
|
|
||||||
0 setStable : (eqs : DimEq d) -> (u, v, p, q : Dim d) ->
|
|
||||||
Equal eqs p q -> Equal (set u v eqs) p q
|
|
||||||
setStable ZeroIsOne p q u v Eq01 = Eq01
|
|
||||||
setStable (C eqs) (K e) (K f) p q (EqC prf) = checkConstStable eqs e f p q prf
|
|
||||||
setStable (C eqs) (K e) (B i) p q (EqC prf) = setConstStable eqs i e p q prf
|
|
||||||
setStable (C eqs) (B i) (K e) p q (EqC prf) = setConstStable eqs i e p q prf
|
|
||||||
setStable (C eqs) (B i) (B j) p q (EqC prf) = setVarStable eqs i j p q prf
|
|
||||||
|
|
@ -1,49 +0,0 @@
|
||||||
module Quox.Token
|
|
||||||
|
|
||||||
import Generics.Derive
|
|
||||||
import Text.Lexer
|
|
||||||
|
|
||||||
%default total
|
|
||||||
%language ElabReflection
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Punc
|
|
||||||
= LParen | RParen
|
|
||||||
| LSquare | RSquare
|
|
||||||
| LBrace | RBrace
|
|
||||||
| Comma
|
|
||||||
| Colon | DblColon
|
|
||||||
| Dot
|
|
||||||
| Arrow | DblArrow
|
|
||||||
| Times | Triangle
|
|
||||||
| Wild
|
|
||||||
%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Keyword
|
|
||||||
= Lam | Let | In | Case | Of | Omega
|
|
||||||
| Pi | Sigma | W
|
|
||||||
%runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
||||||
|
|
||||||
|
|
||||||
||| zero and one are separate because they are
|
|
||||||
||| quantity & dimension constants
|
|
||||||
public export
|
|
||||||
data Number = Zero | One | Other Nat
|
|
||||||
%runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
data Token
|
|
||||||
= P Punc
|
|
||||||
| K Keyword
|
|
||||||
| Name String | Symbol String
|
|
||||||
| N Number | TYPE Nat
|
|
||||||
%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
BToken : Type
|
|
||||||
BToken = WithBounds Token
|
|
||||||
Loading…
Reference in a new issue