diff options
Diffstat (limited to 'src/Obs')
| -rw-r--r-- | src/Obs/Abstract.idr | 24 | ||||
| -rw-r--r-- | src/Obs/NormalForm.idr | 39 | ||||
| -rw-r--r-- | src/Obs/NormalForm/Normalise.idr | 132 | ||||
| -rw-r--r-- | src/Obs/Parser.idr | 64 | ||||
| -rw-r--r-- | src/Obs/Sort.idr | 2 | ||||
| -rw-r--r-- | src/Obs/Syntax.idr | 35 | ||||
| -rw-r--r-- | src/Obs/Term.idr | 35 | ||||
| -rw-r--r-- | src/Obs/Typing.idr | 92 | ||||
| -rw-r--r-- | src/Obs/Typing/Conversion.idr | 8 |
9 files changed, 424 insertions, 7 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index 03367dc..48709c1 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -68,6 +68,30 @@ abstractSyntax ctx (Case t s b f g) = do f <- abstractSyntaxBounds ctx f g <- abstractSyntaxBounds ctx g pure (Case t s b f g) +abstractSyntax ctx (Container a s s') = do + a <- abstractSyntaxBounds ctx a + s <- abstractSyntaxBounds ctx s + s' <- abstractSyntaxBounds ctx s' + pure (Container a s s') +abstractSyntax ctx (MkContainer t p f) = do + t <- abstractSyntaxBounds ctx t + p <- abstractSyntaxBounds ctx p + f <- abstractSyntaxBounds ctx f + pure (MkContainer t p f) +abstractSyntax ctx (Tag t) = do + t <- abstractSyntaxBounds ctx t + pure (Tag t) +abstractSyntax ctx (Position t) = do + t <- abstractSyntaxBounds ctx t + pure (Position t) +abstractSyntax ctx (Next t) = do + t <- abstractSyntaxBounds ctx t + pure (Next t) +abstractSyntax ctx (Sem s a t) = do + s <- abstractSyntaxBounds ctx s + a <- abstractSyntaxBounds ctx a + t <- abstractSyntaxBounds ctx t + pure (Sem s a t) abstractSyntax ctx Top = pure Top abstractSyntax ctx Point = pure Point abstractSyntax ctx Bottom = pure Bottom diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr index 71b554c..cf5bb61 100644 --- a/src/Obs/NormalForm.idr +++ b/src/Obs/NormalForm.idr @@ -26,6 +26,8 @@ data Constructor : Nat -> Type where Sum : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n Left : NormalForm n -> Constructor n Right : NormalForm n -> Constructor n + Container : Sort -> NormalForm n -> Sort -> Sort -> Constructor n + MkContainer : NormalForm n -> NormalForm n -> NormalForm n -> Constructor n Top : Constructor n Bottom : Constructor n @@ -36,6 +38,9 @@ data Neutral : Nat -> Type where Fst : Neutral n -> Neutral n Snd : Neutral n -> Neutral n Case : Neutral n -> NormalForm n -> NormalForm n -> Neutral n + Tag : Neutral n -> Neutral n + Position : Neutral n -> Neutral n + Next : Neutral n -> Neutral n Absurd : Neutral n Equal : Neutral n -> NormalForm n -> NormalForm n -> Neutral n EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n @@ -79,6 +84,8 @@ eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u' eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b' eqCnstr (Left t) (Left t') = eqWhnf t t' eqCnstr (Right t) (Right t') = eqWhnf t t' +eqCnstr (Container s a s' s'') (Container l a' l' l'') = s == l && eqWhnf a a' && s' == l' && s'' == l'' +eqCnstr (MkContainer t p f) (MkContainer t' p' f') = eqWhnf t t' && eqWhnf p p' && eqWhnf f f' eqCnstr Top Top = True eqCnstr Bottom Bottom = True eqCnstr _ _ = False @@ -88,6 +95,9 @@ eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u' eqNtrl (Fst t) (Fst t') = eqNtrl t t' eqNtrl (Snd t) (Snd t') = eqNtrl t t' eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g' +eqNtrl (Tag t) (Tag t') = eqNtrl t t' +eqNtrl (Position t) (Position t') = eqNtrl t t' +eqNtrl (Next t) (Next t') = eqNtrl t t' eqNtrl Absurd Absurd = True eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u' eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u' @@ -164,6 +174,18 @@ prettyPrecCnstr d (Right t) = parenthesise (d >= App) $ group $ fillSep [pretty "Right", prettyPrecWhnf App t] +prettyPrecCnstr d (Container s a s' s'') = + parenthesise (d >= App) $ + group $ + fillSep [pretty "Container", prettyPrecWhnf App a, prettyPrec App s', prettyPrec App s''] +prettyPrecCnstr d (MkContainer t p f) = + parenthesise (d >= User 0) $ + group $ + fillSep + [ prettyPrecWhnf (User 0) t <++> pretty "<|" + , prettyPrecWhnf (User 0) p <++> pretty "/" + , prettyPrecWhnf (User 0) f + ] prettyPrecCnstr d Top = pretty "()" prettyPrecCnstr d Bottom = pretty "Void" @@ -184,6 +206,18 @@ prettyPrecNtrl d (Case t f g) = parenthesise (d >= App) $ group $ fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g] +prettyPrecNtrl d (Tag t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "tag", prettyPrecNtrl App t] +prettyPrecNtrl d (Position t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "position", prettyPrecNtrl App t] +prettyPrecNtrl d (Next t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "next", prettyPrecNtrl App t] prettyPrecNtrl d Absurd = pretty "absurd" prettyPrecNtrl d (Equal _ t u) = parenthesise (d >= Equal) $ @@ -258,6 +292,8 @@ renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f) renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f) renameCnstr (Left t) f = Left (renameWhnf t f) renameCnstr (Right t) f = Right (renameWhnf t f) +renameCnstr (Container s a s' s'') f = Container s (renameWhnf a f) s' s'' +renameCnstr (MkContainer t p u) f = MkContainer (renameWhnf t f) (renameWhnf p f) (renameWhnf u f) renameCnstr Top f = Top renameCnstr Bottom f = Bottom @@ -266,6 +302,9 @@ renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f) renameNtrl (Fst t) f = Fst (renameNtrl t f) renameNtrl (Snd t) f = Snd (renameNtrl t f) renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f) +renameNtrl (Tag t) f = Tag (renameNtrl t f) +renameNtrl (Position t) f = Position (renameNtrl t f) +renameNtrl (Next t) f = Next (renameNtrl t f) renameNtrl Absurd f = Absurd renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f) renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f) diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr index 919067e..b50b520 100644 --- a/src/Obs/NormalForm/Normalise.idr +++ b/src/Obs/NormalForm/Normalise.idr @@ -7,7 +7,7 @@ import Obs.NormalForm import Obs.Sort import Obs.Substitution --- Substitution ---------------------------------------------------------------- +-- Utilities ------------------------------------------------------------------- mergeName : String -> String -> String mergeName "" s' = s' @@ -22,6 +22,38 @@ wkn (var :: vars) f = (pure $ Ntrl $ Var var FZ) (\i => pure $ rename !(wkn vars f i) FS) +export +expandContainerTy : Sort -> NormalForm n -> Sort -> Sort -> Constructor n +expandContainerTy s a s' s'' = + let tagTy : Constructor n + tagTy = Pi s (suc s') "i" a (cast s') + in + let posTy : Constructor (S n) + posTy = + Pi s (s' ~> suc s'') "i" + (weaken 1 a) + (Cnstr $ Pi s' (suc s'') "t" + (Ntrl $ App (Var "tag" 1) (Ntrl $ Var "i" 0)) + (cast s'')) + in + let nextTy : Constructor (2 + n) + nextTy = + Pi s (s' ~> suc s'' ~> s) "i" + (weaken 2 a) + (Cnstr $ Pi s' (suc s'' ~> s) "t" + (Ntrl $ App (Var "tag" 2) (Ntrl $ Var "i" 0)) + (Cnstr $ Pi (suc s'') s "p" + (Ntrl $ App (App (Var "pos" 2) (Ntrl $ Var "i" 1)) (Ntrl $ Var "p" 0)) + (weaken 5 a))) + in + Sigma (s ~> suc s') (lub (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s)) "tag" + (Cnstr tagTy) $ + Cnstr $ Sigma (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s) "pos" + (Cnstr posTy) + (Cnstr nextTy) + +-- Substitution ---------------------------------------------------------------- + partial substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m) partial @@ -39,6 +71,12 @@ doSnd : NormalForm n -> Logging ann (NormalForm n) partial export doCase : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n) partial export +doTag : NormalForm n -> Logging ann (NormalForm n) +partial export +doPosition : NormalForm n -> Logging ann (NormalForm n) +partial export +doNext : NormalForm n -> Logging ann (NormalForm n) +partial export doEqual : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n) partial doEqualL : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n) @@ -52,6 +90,10 @@ partial doCastR : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n) partial doCastU : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n) +partial export +expandContainer : NormalForm n -> Logging ann (Constructor n) +partial export +contractContainer : NormalForm n -> Logging ann (Constructor n) substCnstr (Sort s) f = pure $ Sort s substCnstr (Pi s s' var a b) f = do @@ -79,6 +121,14 @@ substCnstr (Left t) f = do substCnstr (Right t) f = do t <- subst t f pure (Right t) +substCnstr (Container s a s' s'') f = do + a <- subst a f + pure (Container s a s' s'') +substCnstr (MkContainer t p u) f = do + t <- subst t f + p <- subst p f + u <- subst u f + pure (MkContainer t p u) substCnstr Top f = pure $ Top substCnstr Bottom f = pure $ Bottom @@ -101,6 +151,15 @@ substNtrl (Case t u t') f = do u <- subst u f t' <- subst t' f doCase t u t' +substNtrl (Tag t) f = do + t <- substNtrl t f + doTag t +substNtrl (Position t) f = do + t <- substNtrl t f + doPosition t +substNtrl (Next t) f = do + t <- substNtrl t f + doNext t substNtrl Absurd f = pure $ Ntrl Absurd substNtrl (Equal a t u) f = do a <- substNtrl a f @@ -162,6 +221,21 @@ doCase (Cnstr (Left t)) f g = doApp f t doCase (Cnstr (Right t)) f g = doApp g t doCase (Cnstr t) f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal t +doTag (Ntrl t) = pure $ Ntrl (Tag t) +doTag Irrel = pure $ Irrel +doTag (Cnstr (MkContainer t p f)) = pure t +doTag (Cnstr t) = inScope "bug" $ inScope "wrong constructor in tag" $ fatal t + +doPosition (Ntrl t) = pure $ Ntrl (Position t) +doPosition Irrel = pure $ Irrel +doPosition (Cnstr (MkContainer t p f)) = pure p +doPosition (Cnstr t) = inScope "bug" $ inScope "wrong constructor in position" $ fatal t + +doNext (Ntrl t) = pure $ Ntrl (Next t) +doNext Irrel = pure $ Irrel +doNext (Cnstr (MkContainer t p f)) = pure f +doNext (Cnstr t) = inScope "bug" $ inScope "wrong constructor in next" $ fatal t + doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u) doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel" doEqual (Cnstr (Sort Prop)) t u = @@ -201,8 +275,14 @@ doEqual (Cnstr (Sum s s' a b)) t u = do fBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" ll)) (Cnstr (Lambda "y" lr)) gBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" rl)) (Cnstr (Lambda "y" rr)) doCase t (Cnstr (Lambda "x" fBody)) (Cnstr (Lambda "x" gBody)) +doEqual (Cnstr (Container s a s' s'')) t u = do + let containerTy = expandContainerTy s a s' s'' + t <- expandContainer t + u <- expandContainer u + doEqual (Cnstr containerTy) (Cnstr t) (Cnstr u) doEqual (Cnstr Top) t u = pure $ Cnstr Top doEqual (Cnstr Bottom) t u = pure $ Cnstr Top +doEqual (Cnstr a) t u = inScope "bug" $ inScope "wrong type under equal" $ fatal a doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u) doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel" @@ -229,12 +309,15 @@ doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l') b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS)) eqRhs <- doEqual (cast s') b b' pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs)) -doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == s' && l == l') of +doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == l && s' == l') of False => pure $ Cnstr Bottom True => do eqLhs <- doEqual (cast s) a a' eqRhs <- doEqual (cast s) b b' pure $ Cnstr (Sigma Prop Prop "" eqLhs (weaken 1 eqRhs)) +doEqualU i (Container s a s' s'') (Container l a' l' l'') = case (s == l && s' == l' && s'' == l'') of + False => pure $ Cnstr Bottom + True => doEqual (cast s) a a' doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t) @@ -267,6 +350,51 @@ doCastU (Sum s s' a b) (Sum l l' a' b') t = do castL <- doCastL (weaken 1 a) (weaken 1 a') x castR <- doCastL (weaken 1 b) (weaken 1 b') x doCase t (Cnstr (Lambda "x" (Cnstr (Left castL)))) (Cnstr (Lambda "x" (Cnstr (Right castR)))) +doCastU (Container s a s' s'') (Container l b l' l'') t = do + t <- expandContainer t + let a = expandContainerTy s a s' s'' + let b = expandContainerTy l b l' l'' + t <- doCastU a b (Cnstr t) + t <- contractContainer t + pure $ Cnstr t doCastU Top Top t = pure Irrel doCastU Bottom Bottom t = pure Irrel doCastU a b t = pure $ Ntrl (CastU a b t) + +expandContainer t = do + tag <- doTag t + pos <- doPosition t + next <- doNext t + pure $ Pair tag (Cnstr $ Pair pos next) + +contractContainer t = do + tag <- doFst t + t <- doSnd t + pos <- doFst t + next <- doSnd t + pure $ MkContainer tag pos next + +-- More utilities -------------------------------------------------------------- + +export +tagTy : Sort -> NormalForm n -> Sort -> Constructor n +tagTy s a s' = Pi s (suc s') "i" a (cast s') + +export +positionTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> Logging ann (Constructor n) +positionTy s a s' tag s'' = do + let i = Var "i" 0 + tagI <- doApp (weaken 1 tag) (Ntrl i) + pure $ Pi s (s' ~> suc s'') "i" a (Cnstr $ Pi s' (suc s'') "t" tagI (cast s'')) + +export +nextTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> NormalForm n -> Logging ann (Constructor n) +nextTy s a s' tag s'' pos = do + let i = Var "i" 0 + tagI <- doApp (weaken 1 tag) (Ntrl i) + let t = Var "t" 0 + posI <- doApp (weaken 1 pos) (Ntrl i) + posIT <- doApp (weaken 1 posI) (Ntrl t) + pure $ Pi s (s' ~> s'' ~> s) "i" a $ + Cnstr $ Pi s' (s'' ~> s) "t" tagI $ + Cnstr $ Pi s'' s "p" posIT (weaken 3 a) diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index acb1360..7ce31c4 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -29,6 +29,11 @@ data ObsTokenKind | OTLeft | OTRight | OTCase + | OTContainer + | OTTag + | OTPosition + | OTNext + | OTSem | OTPoint | OTVoid | OTAbsurd @@ -38,6 +43,7 @@ data ObsTokenKind | OTCastRefl -- Special symbols | OTUnit + | OTTriangle -- Grouping symbols | OTPOpen | OTPClose @@ -45,6 +51,7 @@ data ObsTokenKind | OTAClose -- Definition characters | OTBackslash + | OTSlash | OTThinArrow | OTFatArrow | OTProduct @@ -52,6 +59,7 @@ data ObsTokenKind | OTTilde | OTEqual | OTColon + | OTPipe Eq ObsTokenKind where OTNewlines == OTNewlines = True @@ -66,6 +74,11 @@ Eq ObsTokenKind where OTLeft == OTLeft = True OTRight == OTRight = True OTCase == OTCase = True + OTContainer == OTContainer = True + OTTag == OTTag = True + OTPosition == OTPosition = True + OTNext == OTNext = True + OTSem == OTSem = True OTPoint == OTPoint = True OTVoid == OTVoid = True OTAbsurd == OTAbsurd = True @@ -74,11 +87,13 @@ Eq ObsTokenKind where OTCast == OTCast = True OTCastRefl == OTCastRefl = True OTUnit == OTUnit = True + OTTriangle == OTTriangle = True OTPOpen == OTPOpen = True OTPClose == OTPClose = True OTAOpen == OTAOpen = True OTAClose == OTAClose = True OTBackslash == OTBackslash = True + OTSlash == OTSlash = True OTThinArrow == OTThinArrow = True OTFatArrow == OTFatArrow = True OTProduct == OTProduct = True @@ -86,6 +101,7 @@ Eq ObsTokenKind where OTTilde == OTTilde = True OTEqual == OTEqual = True OTColon == OTColon = True + OTPipe == OTPipe = True _ == _ = False TokenKind ObsTokenKind where @@ -105,6 +121,11 @@ TokenKind ObsTokenKind where tokValue OTLeft s = () tokValue OTRight s = () tokValue OTCase s = () + tokValue OTContainer s = () + tokValue OTTag s = () + tokValue OTPosition s = () + tokValue OTNext s = () + tokValue OTSem s = () tokValue OTPoint s = () tokValue OTVoid s = () tokValue OTAbsurd s = () @@ -113,11 +134,13 @@ TokenKind ObsTokenKind where tokValue OTCast s = () tokValue OTCastRefl s = () tokValue OTUnit s = () + tokValue OTTriangle s = () tokValue OTPOpen s = () tokValue OTPClose s = () tokValue OTAOpen s = () tokValue OTAClose s = () tokValue OTBackslash s = () + tokValue OTSlash s = () tokValue OTThinArrow s = () tokValue OTFatArrow s = () tokValue OTProduct s = () @@ -125,6 +148,7 @@ TokenKind ObsTokenKind where tokValue OTTilde s = () tokValue OTEqual s = () tokValue OTColon s = () + tokValue OTPipe s = () ObsToken : Type ObsToken = Token ObsTokenKind @@ -142,6 +166,11 @@ Show ObsToken where show (Tok OTLeft s) = "Left" show (Tok OTRight s) = "Right" show (Tok OTCase s) = "case" + show (Tok OTContainer s) = "Container" + show (Tok OTTag s) = "tag" + show (Tok OTPosition s) = "position" + show (Tok OTNext s) = "next" + show (Tok OTSem s) = "sem" show (Tok OTPoint s) = "tt" show (Tok OTVoid s) = "Void" show (Tok OTAbsurd s) = "absurd" @@ -150,11 +179,13 @@ Show ObsToken where show (Tok OTCast s) = "cast" show (Tok OTCastRefl s) = "castRefl" show (Tok OTUnit s) = "()" + show (Tok OTTriangle s) = "<|" show (Tok OTPOpen s) = "(" show (Tok OTPClose s) = ")" show (Tok OTAOpen s) = "<" show (Tok OTAClose s) = ">" show (Tok OTBackslash s) = "\\" + show (Tok OTSlash s) = "/" show (Tok OTThinArrow s) = "->" show (Tok OTFatArrow s) = "=>" show (Tok OTProduct s) = "**" @@ -162,6 +193,7 @@ Show ObsToken where show (Tok OTTilde s) = "~" show (Tok OTEqual s) = "=" show (Tok OTColon s) = ":" + show (Tok OTPipe s) = "|" identifier : Lexer identifier = alpha <+> many alphaNum @@ -176,6 +208,11 @@ keywords = , ("Left", OTLeft) , ("Right", OTRight) , ("case", OTCase) + , ("Container", OTContainer) + , ("tag", OTTag) + , ("position", OTPosition) + , ("next", OTNext) + , ("sem", OTSem) , ("tt", OTPoint) , ("Void", OTVoid) , ("absurd", OTAbsurd) @@ -200,11 +237,13 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++ , (exact "=>", OTFatArrow) , (exact "->", OTThinArrow) , (exact "\\", OTBackslash) + , (exact "/", OTSlash) , (exact "**", OTProduct) , (exact ",", OTComma) , (exact "~", OTTilde) , (exact "=", OTEqual) , (exact ":", OTColon) + , (exact "|", OTPipe) ] op : Type -> Type -> Nat -> Type @@ -230,6 +269,11 @@ headForms = , (OTLeft, (0 ** uncurry 1 Left)) , (OTRight, (0 ** uncurry 1 Right)) , (OTCase, (4 ** uncurry 5 Case)) + , (OTContainer, (2 ** uncurry 3 Container)) + , (OTTag, (0 ** uncurry 1 Tag)) + , (OTPosition, (0 ** uncurry 1 Position)) + , (OTNext, (0 ** uncurry 1 Next)) + , (OTSem, (2 ** uncurry 3 Sem)) , (OTAbsurd, (1 ** uncurry 2 Absurd)) , (OTRefl, (0 ** uncurry 1 Refl)) , (OTTransp, (4 ** uncurry 5 Transp)) @@ -286,6 +330,8 @@ head : Grammar state ObsToken True (WithBounds Syntax) partial spine : Grammar state ObsToken True (WithBounds Syntax) partial +container : Grammar state ObsToken True (WithBounds Syntax) +partial equals : Grammar state ObsToken True (WithBounds Syntax) partial exp : Grammar state ObsToken True (WithBounds Syntax) @@ -309,8 +355,21 @@ head = spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $ [| MkPair head (many (whitespace *> term)) |] +container = + map (\bounds@(MkBounded (t, u) _ _) => case u of + Nothing => t + Just (p, f) => map (\_ => MkContainer t p f) bounds) $ + bounds $ + [| MkPair spine + (optional + [| MkPair + (whitespace *> match OTTriangle *> commit *> whitespace *> spine) + (whitespace *> match OTSlash *> commit *> whitespace *> spine) + |]) + |] + equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $ - [| MkPair spine (optional (whitespace *> match OTTilde *> commit *> whitespace *> spine)) |] + [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |] exp = equals <|> @@ -358,7 +417,8 @@ whitespaceIrrelevant a = case (a.val.kind) of mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken) mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest - (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "")) (mergeBounds a b) :: mergeToks rest + (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "()")) (mergeBounds a b) :: mergeToks rest + (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest _ => a :: mergeToks tail mergeToks toks = toks diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr index bbd6975..f76453a 100644 --- a/src/Obs/Sort.idr +++ b/src/Obs/Sort.idr @@ -35,7 +35,7 @@ Pretty Sort where -- Operations ------------------------------------------------------------------ -infix 5 ~> +infixr 5 ~> public export suc : Sort -> Sort diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 9f64c38..d21569a 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -28,6 +28,13 @@ data Syntax : Type where Left : WithBounds Syntax -> Syntax Right : WithBounds Syntax -> Syntax Case : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + -- Containers + Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + Tag : WithBounds Syntax -> Syntax + Position : WithBounds Syntax -> Syntax + Next : WithBounds Syntax -> Syntax + Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax -- True Top : Syntax Point : Syntax @@ -105,6 +112,34 @@ prettyPrec d (Case t s b f g) = parenthesise (d >= App) $ group $ fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g] +prettyPrec d (Container a s s') = + parenthesise (d >= App) $ + group $ + fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s'] +prettyPrec d (MkContainer t p f) = + parenthesise (d >= User 0) $ + group $ + fillSep + [ prettyPrecBounds (User 0) t <++> pretty "<|" + , prettyPrecBounds (User 0) p <++> pretty "/" + , prettyPrecBounds (User 0) f + ] +prettyPrec d (Tag t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "tag", prettyPrecBounds App t] +prettyPrec d (Position t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "position", prettyPrecBounds App t] +prettyPrec d (Next t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "next", prettyPrecBounds App t] +prettyPrec d (Sem s a t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t] prettyPrec d Top = pretty "()" prettyPrec d Point = pretty "tt" prettyPrec d Bottom = pretty "Void" diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index be3721f..10f2129 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -29,6 +29,13 @@ data Term : Nat -> Type where Left : WithBounds (Term n) -> Term n Right : WithBounds (Term n) -> Term n Case : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n + -- Containers + Container : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n + MkContainer : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n + Tag : WithBounds (Term n) -> Term n + Position : WithBounds (Term n) -> Term n + Next : WithBounds (Term n) -> Term n + Sem : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n -- True Top : Term n Point : Term n @@ -111,6 +118,34 @@ prettyPrec d (Case t s b f g) = parenthesise (d >= App) $ group $ fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g] +prettyPrec d (Container a s s') = + parenthesise (d >= App) $ + group $ + fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s'] +prettyPrec d (MkContainer t p f) = + parenthesise (d >= User 0) $ + group $ + fillSep + [ prettyPrecBounds (User 0) t <++> pretty "<|" + , prettyPrecBounds (User 0) p <++> pretty "/" + , prettyPrecBounds (User 0) f + ] +prettyPrec d (Tag t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "tag", prettyPrecBounds App t] +prettyPrec d (Position t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "position", prettyPrecBounds App t] +prettyPrec d (Next t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "next", prettyPrecBounds App t] +prettyPrec d (Sem s a t) = + parenthesise (d >= App) $ + group $ + fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t] prettyPrec d Top = pretty "()" prettyPrec d Point = pretty "tt" prettyPrec d Bottom = pretty "Void" diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index b327397..f814f93 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -78,6 +78,8 @@ infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Norma partial inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a} -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort) +partial +inferSort : TyContext m n -> WithBounds (Term n) -> Logging ann Sort check ctx tm ty s = case (tm.val, ty) of (Lambda _ t, Cnstr (Pi s s' var a b)) => do @@ -115,6 +117,22 @@ check ctx tm ty s = case (tm.val, ty) of inScope "check" $ trace $ map (\_ => " subterm is well typed") tm pure (Cnstr $ Right t) (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty) + (MkContainer t p f, Cnstr (Container s a s' s'')) => do + inScope "check" $ trace $ map (\_ => "checking container constructor") tm + let tagTy = tagTy s a s' + inScope "check" $ trace $ map (\_ => pretty {ann} "checking tag for type" <++> pretty tagTy) tm + t <- check ctx t (Cnstr tagTy) (s ~> suc s') + inScope "check" $ trace $ map (\_ => "tag is well typed") tm + positionTy <- positionTy s a s' t s'' + inScope "check" $ trace $ map (\_ => pretty {ann} "checking position for type" <++> pretty positionTy) tm + p <- check ctx p (Cnstr positionTy) (s ~> s' ~> suc s'') + inScope "check" $ trace $ map (\_ => "position is well typed") tm + nextTy <- nextTy s a s' t s'' p + inScope "check" $ trace $ map (\_ => pretty {ann} "checking next for type" <++> pretty nextTy) tm + f <- check ctx f (Cnstr nextTy) (s ~> s' ~> s'' ~> s) + inScope "check" $ trace $ map (\_ => "next is well typed") tm + pure (Cnstr $ MkContainer t p f) + (MkContainer t p f, ty) => typeMismatch tm.bounds (pretty "container") (pretty ty) (_, _) => do inScope "check" $ trace $ map (\_ => "checking has fallen through") tm (v, a, s') <- infer ctx tm @@ -193,8 +211,7 @@ infer ctx tm = case tm.val of (t, ty@(Cnstr (Sum s s' a b)), s'') <- infer ctx t | (_, ty, _) => inScope "wrong type to case" $ fatal (map (\_ => ty) tm) inScope "infer" $ trace $ map (\_ => pretty {ann} "sum has type" <++> pretty ty) tm - (Cnstr (Sort l), _) <- inferType ctx l - | (s, _) => typeMismatch l.bounds (pretty "sort") (pretty s) + l <- inferSort ctx l inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm let ty' = Cnstr (Pi s'' (suc l) "x" ty (cast l)) inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty ty') tm @@ -214,6 +231,72 @@ infer ctx tm = case tm.val of out <- doApp out t inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty out) tm pure (res, out, l) + (Container a s' s'') => do + inScope "infer" $ trace $ map (\_ => "encountered container") tm + (a, s) <- inferType ctx a + inScope "infer" $ trace $ map (\_ => pretty {ann} "index has type" <++> pretty a) tm + s' <- inferSort ctx s' + inScope "infer" $ trace $ map (\_ => pretty {ann} "tag has sort" <++> pretty s') tm + s'' <- inferSort ctx s'' + inScope "infer" $ trace $ map (\_ => pretty {ann} "position has sort" <++> pretty s'') tm + pure (Cnstr (Container s a s' s''), cast (lub s (suc $ lub s' s'')), suc (lub s (suc $ lub s' s''))) + (MkContainer _ _ _) => inScope "cannot infer type" $ fatal tm + (Tag t) => do + inScope "infer" $ trace $ map (\_ => "encountered tag") tm + (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t + | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty) + inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm + tag <- doTag t + let out = tagTy s a s' + pure (tag, Cnstr out, s ~> suc s') + (Position t) => do + inScope "infer" $ trace $ map (\_ => "encountered position") tm + (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t + | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty) + inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm + tag <- doTag t + pos <- doPosition t + out <- positionTy s a s' tag s'' + pure (pos, Cnstr out, s ~> s' ~> suc s'') + (Next t) => do + inScope "infer" $ trace $ map (\_ => "encountered next") tm + (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t + | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty) + inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm + tag <- doTag t + pos <- doPosition t + next <- doNext t + out <- nextTy s a s' tag s'' pos + pure (next, Cnstr out, s ~> s' ~> s'' ~> s) + (Sem l b t) => do + inScope "infer" $ trace $ map (\_ => "encountered sem") tm + (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t + | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty) + inScope "infer" $ trace $ map (\_ => pretty {ann} "interpretting a container" <++> pretty ty) tm + l <- inferSort ctx l + inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm + let outTy = Cnstr (Pi s (suc l) "i" a (cast l)) + inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty outTy) tm + b <- check ctx b outTy (s ~> suc l) + inScope "infer" $ trace $ map (\_ => "output is well typed") tm + tag <- doTag t + pos <- doPosition t + next <- doNext t + let i = Ntrl (Var "i" 0) + tag <- doApp (weaken 1 tag) i + pos <- doApp (weaken 1 pos) i + next <- doApp (weaken 1 next) i + let t = Ntrl (Var "t" 0) + pos <- doApp (weaken 1 pos) t + next <- doApp (weaken 1 next) t + let p = Ntrl (Var "p" 0) + next <- doApp (weaken 1 next) p + out <- doApp (weaken 3 b) next + let out = Cnstr $ Lambda "i" $ + Cnstr $ Sigma s' (s'' ~> l) "t" tag $ + Cnstr $ Pi s'' l "p" pos out + let ty = Cnstr $ Pi s (suc (lub s' (s'' ~> l))) "i" a (cast (lub s' (s'' ~> l))) + pure (out, ty, suc (s ~> suc (lub s' (s'' ~> l)))) Top => pure $ (Cnstr Top, cast Prop, Set 0) Point => pure $ (Irrel, Cnstr Top, Prop) Bottom => pure $ (Cnstr Bottom, cast Prop, Set 0) @@ -292,6 +375,11 @@ inferType ctx a = do | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty) pure (a, s) +inferSort ctx a = do + (Cnstr (Sort s), _, _) <- infer ctx a + | (t, _, _) => inScope "infer" $ typeMismatch a.bounds (pretty "sort") (pretty t) + pure s + -- Checking Definitions and Blocks --------------------------------------------- partial diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr index 20198c5..37bdf67 100644 --- a/src/Obs/Typing/Conversion.idr +++ b/src/Obs/Typing/Conversion.idr @@ -42,6 +42,11 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do convert t2 u2 b s' -- In type Sum (manually expanding definition of doCase) convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b +-- In type Container +convert t u (Cnstr (Container s a s' s'')) (Set l) = do + t <- expandContainer t + u <- expandContainer u + convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l) -- Default convert t u a s = inScope "invalid conversion" $ fatal $ @@ -57,6 +62,9 @@ convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) = convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) = pure $ s == l && s' == l' && !(convertSet a a') && !(convertSet b b') +convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) = + pure $ + s == l && s' == l' && s'' == l'' && !(convertSet a a') convertSet (Cnstr Top) (Cnstr Top) = pure True convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True convertSet (Ntrl t) u = pure (Ntrl t == u) |