diff --git a/lib/on-hold/Quox/Lexer.idr b/lib/on-hold/Quox/Lexer.idr deleted file mode 100644 index 3a299dd..0000000 --- a/lib/on-hold/Quox/Lexer.idr +++ /dev/null @@ -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} diff --git a/lib/on-hold/Quox/Parser.idr b/lib/on-hold/Quox/Parser.idr deleted file mode 100644 index f9f4b09..0000000 --- a/lib/on-hold/Quox/Parser.idr +++ /dev/null @@ -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} diff --git a/lib/on-hold/Quox/Syntax/DimEq.idr b/lib/on-hold/Quox/Syntax/DimEq.idr deleted file mode 100644 index 4730b35..0000000 --- a/lib/on-hold/Quox/Syntax/DimEq.idr +++ /dev/null @@ -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 : Maybe (Dim d) -> DimEq (S d) -ZeroIsOne : 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 : Var d -> DimEq' d -> DimEq d -setVar VZ VZ eqs = C eqs -setVar VZ (VS j) (Const eqs e) = setConst j e eqs : 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 : (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 diff --git a/lib/on-hold/Quox/Token.idr b/lib/on-hold/Quox/Token.idr deleted file mode 100644 index 432dd22..0000000 --- a/lib/on-hold/Quox/Token.idr +++ /dev/null @@ -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