diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index c5d837f..bf7ebc1 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -52,6 +52,10 @@ covering partial subst : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m) covering partial doApp : NormalForm n -> NormalForm n -> Logging ann (NormalForm n) +covering partial +doFst : NormalForm n -> Logging ann (NormalForm n) +covering partial +doSnd : NormalForm n -> Logging ann (NormalForm n) substCnstr (Sort s) f = pure $ Sort s substCnstr (Pi s s' var a b) f = do @@ -61,6 +65,14 @@ substCnstr (Pi s s' var a b) f = do substCnstr (Lambda var t) f = do t <- subst t (wkn [var] f) pure (Lambda var t) +substCnstr (Sigma s s' var a b) f = do + a <- subst a f + b <- subst b (wkn [var] f) + pure (Sigma s s' var a b) +substCnstr (Pair t u) f = do + t <- subst t f + u <- subst u f + pure (Pair t u) substCnstr Top f = pure $ Top substCnstr Bottom f = pure $ Bottom @@ -72,6 +84,12 @@ substNtrl (App t u) f = do t <- substNtrl t f u <- subst u f doApp t u +substNtrl (Fst t) f = do + t <- substNtrl t f + doFst t +substNtrl (Snd t) f = do + t <- substNtrl t f + doSnd t substNtrl Absurd f = pure $ Ntrl Absurd subst (Ntrl t) f = substNtrl t f @@ -83,6 +101,16 @@ doApp Irrel u = pure $ Irrel doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point)) doApp (Cnstr t) u = inScope "wrong constructor in apply:" $ fatal t +doFst (Ntrl t) = pure $ Ntrl (Fst t) +doFst Irrel = pure $ Irrel +doFst (Cnstr (Pair t u)) = pure $ t +doFst (Cnstr t) = inScope "wrong constructor in fst:" $ fatal t + +doSnd (Ntrl t) = pure $ Ntrl (Snd t) +doSnd Irrel = pure $ Irrel +doSnd (Cnstr (Pair t u)) = pure $ u +doSnd (Cnstr t) = inScope "wrong constructor in snd:" $ fatal t + partial subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n) subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point)) @@ -102,6 +130,9 @@ convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ s convert (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) (Cnstr (Sort _)) (Set _) = pure $ s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s')) +convert (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) (Cnstr (Sort _)) (Set _) = + pure $ + s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s')) convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = pure True convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = pure True convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = pure $ Ntrl t == u @@ -112,6 +143,16 @@ convert t u (Cnstr (Pi s s' var a b)) (Set k) = do t <- doApp (weaken 1 t) (Ntrl $ Var var FZ) u <- doApp (weaken 1 u) (Ntrl $ Var var FZ) convert t u b s' +-- In type Sigma +convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do + t1 <- doFst t + u1 <- doFst t + True <- convert t1 u1 a s + | False => pure False + b <- subst1 t1 b + t2 <- doSnd t + u2 <- doSnd t + convert t2 u2 b s' -- Default convert t u a s = inScope "invalid conversion:" $ fatal $ @@ -166,6 +207,15 @@ check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do t <- check (ctx ::< (var, a, s)) t b s' pure (Cnstr $ Lambda var t) check ctx tm@(Lambda _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "pi") (pretty ty) +check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do + inScope "check" $ trace $ map (\_ => "checking pair") (fullBounds tm) + inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) (fullBounds tm) + t <- check ctx t a s + b <- subst1 t b + inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) (fullBounds tm) + u <- check ctx u b s' + inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") (fullBounds tm) + pure (Cnstr $ Pair t u) check ctx tm ty s = do let bounded = fullBounds tm inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded @@ -205,6 +255,33 @@ infer ctx tm@(App t u) = do ty <- subst1 u b inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) (fullBounds tm) pure (res, ty, s') +infer ctx tm@(Sigma _ var a b) = do + inScope "infer" $ trace $ map (\_ => "encountered Sigma type") (fullBounds tm) + (a, s) <- inferType ctx a + inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) (fullBounds tm) + (b, s') <- inferType (ctx ::< (var, a, s)) b + inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) (fullBounds tm) + pure (Cnstr (Sigma s s' var a b), cast (lub s s'), suc (lub s s')) +infer ctx tm@(Fst _ t) = do + inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm) + let bounded = fullBounds t + (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t + | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded) + inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm) + res <- doFst t + inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) (fullBounds tm) + pure (res, a, s) +infer ctx tm@(Snd _ t) = do + inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm) + let bounded = fullBounds t + (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t + | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded) + inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm) + t1 <- doFst t + res <- doSnd t + b <- subst1 t1 b + inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) (fullBounds tm) + pure (res, b, s') infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0) infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop) infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0) |