diff options
Diffstat (limited to 'src/Obs/NormalForm/Normalise.idr')
| -rw-r--r-- | src/Obs/NormalForm/Normalise.idr | 223 |
1 files changed, 113 insertions, 110 deletions
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr index 82e84b9..ed06fa2 100644 --- a/src/Obs/NormalForm/Normalise.idr +++ b/src/Obs/NormalForm/Normalise.idr @@ -1,14 +1,14 @@ module Obs.NormalForm.Normalise import Data.Bool -import Data.So +import Data.Nat import Decidable.Equality import Obs.Logging import Obs.NormalForm -import Obs.Sort import Obs.Substitution +import Obs.Universe import Text.PrettyPrint.Prettyprinter @@ -17,19 +17,19 @@ import Text.PrettyPrint.Prettyprinter -- Aliases --------------------------------------------------------------------- public export 0 -LogConstructor : Type -> Unsorted.Family Bool +LogConstructor : Type -> Unsorted.Family Relevance LogConstructor ann ctx = Logging ann (Constructor ctx) public export 0 -LogNormalForm : Type -> Sorted.Family Bool +LogNormalForm : Type -> Sorted.Family Relevance LogNormalForm ann b ctx = Logging ann (NormalForm b ctx) 0 -LogNormalForm' : Type -> Sorted.Family Bool +LogNormalForm' : Type -> Sorted.Family Relevance LogNormalForm' ann b ctx = Either (Logging ann (NormalForm b ctx)) (Elem b ctx) -- Copied and specialised from Obs.Substitution -lift : (ctx : List (b ** (String, (s ** isSet s = b)))) +lift : (ctx : List (r ** (String, (s ** relevance s = r)))) -> Map ctx' (LogNormalForm' ann) ctx'' -> Map (map DPair.fst ctx ++ ctx') (LogNormalForm' ann) (map DPair.fst ctx ++ ctx'') lift [] f = f @@ -42,184 +42,187 @@ lift ((s ** y) :: ctx) f = add (LogNormalForm' ann) subst' : NormalForm ~|> Hom (LogNormalForm' ann) (LogNormalForm ann) export -doApp : {b' : _} -> NormalForm b ctx -> NormalForm b' ctx -> LogNormalForm ann b ctx +doApp : {domain : _} -> + NormalForm (function domain codomain) ctx -> + NormalForm domain ctx -> + LogNormalForm ann codomain ctx doApp (Ntrl t) u = pure (Ntrl $ App _ t u) doApp (Cnstr (Lambda s var t)) u = inScope "doApp" $ do trace $ pretty {ann} "substituting" <++> pretty u <+> softline <+> pretty "for \{var} in" <++> pretty t - let Yes Refl = decEq b' (isSet s) - | No _ => fatal "internal sort mismatch" + let Yes Refl = decEq domain (relevance s) + | No _ => fatal "internal relevance mismatch" subst' t (add (LogNormalForm' ann) (Left $ pure u) Right) doApp (Cnstr t) u = inScope "wrong constructor for apply" $ fatal t doApp Irrel u = pure Irrel export -doFst : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b ctx -doFst False b' t = pure Irrel -doFst True b' (Ntrl t) = pure (Ntrl $ Fst b' t) -doFst True b' (Cnstr (Pair (Set _) s' prf t u)) = pure t -doFst True b' (Cnstr t) = inScope "wrong constructor for fst" $ fatal t +doFst : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann fst ctx +doFst Irrelevant snd t = pure Irrel +doFst Relevant snd (Ntrl t) = pure (Ntrl $ Fst snd t) +doFst Relevant snd (Cnstr (Pair (Set _) s' prf t u)) = pure t +doFst Relevant snd (Cnstr t) = inScope "wrong constructor for fst" $ fatal t export -doSnd : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b' ctx -doSnd b False t = pure Irrel -doSnd b True t = - let t' : NormalForm True ctx - t' = rewrite sym $ orTrueTrue b in t +doSnd : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann snd ctx +doSnd fst Irrelevant t = pure Irrel +doSnd fst Relevant t = + let t' : NormalForm Relevant ctx + t' = rewrite sym $ pairRelevantRight fst in t in case t' of - Ntrl t => pure (Ntrl $ Snd b t) + Ntrl t => pure (Ntrl $ Snd fst t) Cnstr (Pair _ (Set _) prf t u) => pure u Cnstr t => inScope "wrong constructor for snd" $ fatal t export -doIf : {b : _} -> - NormalForm True ctx -> - NormalForm b ctx -> - NormalForm b ctx -> - LogNormalForm ann b ctx -doIf {b = False} t u v = pure Irrel -doIf {b = True} (Ntrl t) u v = pure (Ntrl $ If t u v) -doIf {b = True} (Cnstr True) u v = pure u -doIf {b = True} (Cnstr False) u v = pure v -doIf {b = True} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t +doIf : {r : _} -> + NormalForm Relevant ctx -> + NormalForm r ctx -> + NormalForm r ctx -> + LogNormalForm ann r ctx +doIf {r = Irrelevant} t u v = pure Irrel +doIf {r = Relevant} (Ntrl t) u v = pure (Ntrl $ If t u v) +doIf {r = Relevant} (Cnstr True) u v = pure u +doIf {r = Relevant} (Cnstr False) u v = pure v +doIf {r = Relevant} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t export -doAbsurd : (b : _) -> NormalForm b ctx -doAbsurd False = Irrel -doAbsurd True = Ntrl Absurd +doAbsurd : (r : _) -> NormalForm r ctx +doAbsurd Irrelevant = Irrel +doAbsurd Relevant = Ntrl Absurd export -doCast : (b' : _) -> (a, b : NormalForm True ctx) -> NormalForm b' ctx -> LogNormalForm ann b' ctx +doCast : (r : _) -> (a, b : TypeNormalForm ctx) -> NormalForm r ctx -> LogNormalForm ann r ctx doCastR : (a : Constructor ctx) -> - (b : NormalForm True ctx) -> - NormalForm True ctx -> - LogNormalForm ann True ctx + (b : TypeNormalForm ctx) -> + NormalForm Relevant ctx -> + LogNormalForm ann Relevant ctx doCastR a (Ntrl b) t = pure (Ntrl $ CastR a b t) -doCastR (Sort _) (Cnstr (Sort _)) t = pure t +doCastR (Universe _) (Cnstr (Universe _)) t = pure t doCastR ty@(Pi s s'@(Set _) var a b) (Cnstr ty'@(Pi l l' _ a' b')) t = - let y : NormalForm (isSet s) (isSet s :: ctx) + let y : NormalForm (relevance s) (relevance s :: ctx) y = point (var, (s ** Refl)) Here in do let Yes Refl = decEq (s, s') (l, l') | No _ => pure (Ntrl $ CastStuck ty ty' t) - x <- assert_total (doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) y) + x <- assert_total (doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) y) b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure x) (Right . There))) b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure y) (Right . There))) - t <- assert_total (doApp (Sorted.weaken [isSet s] t) x) - t <- assert_total (doCast True b b' t) + t <- assert_total (doApp (Sorted.weaken [relevance s] t) x) + t <- assert_total (doCast Relevant b b' t) pure (Cnstr $ Lambda s var t) doCastR ty@(Sigma s@(Set k) s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) t = do let Yes Refl = decEq (s, s') (l, l') | No _ => pure (Ntrl $ CastStuck ty ty' t) - t1 <- doFst True (isSet s') t - u1 <- assert_total (doCast True a a' t) + t1 <- doFst Relevant (relevance s') t + u1 <- assert_total (doCast Relevant a a' t) b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right)) b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u1) Right)) - t2 <- doSnd True (isSet s') t - u2 <- assert_total (doCast (isSet s') b b' t2) - pure (Cnstr $ Pair (Set k) s' Oh u1 u2) + t2 <- doSnd Relevant (relevance s') t + u2 <- assert_total (doCast (relevance s') b b' t2) + pure (Cnstr $ Pair (Set k) s' Set u1 u2) doCastR ty@(Sigma Prop s'@(Set k) var a b) (Cnstr ty'@(Sigma Prop l' _ a' b')) t = do let Yes Refl = decEq s' l' | No _ => pure (Ntrl $ CastStuck ty ty' t) b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure Irrel) Right)) b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure Irrel) Right)) - t2 <- doSnd False True t - u2 <- assert_total (doCast True b b' t2) - pure (Cnstr $ Pair Prop (Set k) Oh Irrel u2) + t2 <- doSnd Irrelevant Relevant t + u2 <- assert_total (doCast Relevant b b' t2) + pure (Cnstr $ Pair Prop (Set k) Set Irrel u2) doCastR Bool (Cnstr Bool) t = pure t doCastR a (Cnstr b) t = pure (Ntrl $ CastStuck a b t) -doCast False a b t = pure Irrel -doCast True (Ntrl a) b t = pure (Ntrl $ CastL a b t) -doCast True (Cnstr a) b t = doCastR a b t +doCast Irrelevant a b t = pure Irrel +doCast Relevant (Ntrl a) b t = pure (Ntrl $ CastL a b t) +doCast Relevant (Cnstr a) b t = doCastR a b t export -doEqual : (b : _) -> - (a : NormalForm True ctx) -> - NormalForm b ctx -> - NormalForm b ctx -> - LogNormalForm ann True ctx +doEqual : (r : _) -> + (a : TypeNormalForm ctx) -> + NormalForm r ctx -> + NormalForm r ctx -> + LogNormalForm ann Relevant ctx -- Relies heavily on typing -doEqualR : (a : Constructor ctx) -> (b : NormalForm True ctx) -> LogNormalForm ann True ctx +doEqualR : (a : Constructor ctx) -> (b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx doEqualR a (Ntrl b) = pure (Ntrl $ EqualR a b) -doEqualR (Sort _) (Cnstr (Sort s)) = pure (Cnstr Top) +doEqualR (Universe _) (Cnstr (Universe s)) = pure (Cnstr Top) doEqualR ty@(Pi s s' var a b) (Cnstr ty'@(Pi l l' _ a' b')) = - let u : NormalForm (isSet s) (isSet s :: ctx) + let u : NormalForm (relevance s) (relevance s :: ctx) u = point (var, (s ** Refl)) Here in do let Yes Refl = decEq (s, s') (l, l') | No _ => pure (Ntrl $ EqualStuck ty ty') - eq1 <- assert_total (doEqual True (cast s) a' a) - t <- doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) u + eq1 <- assert_total (doEqual Relevant (cast s) a' a) + t <- doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) u b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There))) b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There))) - eq2 <- assert_total (doEqual True (cast s') b b') - pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2)) + eq2 <- assert_total (doEqual Relevant (cast s') b b') + pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2)) doEqualR ty@(Sigma s s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) = - let t : NormalForm (isSet s) (isSet s :: ctx) + let t : NormalForm (relevance s) (relevance s :: ctx) t = point (var, (s ** Refl)) Here in do let Yes Refl = decEq (s, s') (l, l') | No _ => pure (Ntrl $ EqualStuck ty ty') - eq1 <- assert_total (doEqual True (cast s) a a') - u <- doCast (isSet s) (weaken [isSet s] a) (weaken [isSet s] a') t + eq1 <- assert_total (doEqual Relevant (cast s) a a') + u <- doCast (relevance s) (weaken [relevance s] a) (weaken [relevance s] a') t b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There))) b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There))) - eq2 <- assert_total (doEqual True (cast s') b b') - pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2)) + eq2 <- assert_total (doEqual Relevant (cast s') b b') + pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2)) doEqualR Bool (Cnstr Bool) = pure (Cnstr Top) doEqualR Top (Cnstr Top) = pure (Cnstr Top) doEqualR Bottom (Cnstr Bottom) = pure (Cnstr Top) doEqualR a (Cnstr b) = pure (Ntrl $ EqualStuck a b) export -doEqualSet : (a, b : NormalForm True ctx) -> LogNormalForm ann True ctx +doEqualSet : (a, b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx doEqualSet (Ntrl a) b = pure (Ntrl $ EqualL a b) doEqualSet (Cnstr a) b = doEqualR a b -doEqual False a t u = pure (Cnstr Top) -doEqual True (Ntrl a) t u = pure (Ntrl $ Equal a t u) -doEqual True (Cnstr (Sort Prop)) t u = do +doEqual Irrelevant a t u = pure (Cnstr Top) +doEqual Relevant (Ntrl a) t u = pure (Ntrl $ Equal a t u) +doEqual Relevant (Cnstr (Universe Prop)) t u = do pure (Cnstr $ Sigma Prop Prop "" - (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [False] u)) - (Cnstr $ Unsorted.weaken [False] $ Pi Prop Prop "" u (Sorted.weaken [False] t))) -doEqual True (Cnstr (Sort (Set _))) t u = doEqualSet t u -doEqual True (Cnstr (Pi s (Set k) var a b)) t u = - let x : NormalForm (isSet s) (isSet s :: ctx) + (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [Irrelevant] u)) + (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi Prop Prop "" u (Sorted.weaken [Irrelevant] t))) +doEqual Relevant (Cnstr (Universe (Set _))) t u = doEqualSet t u +doEqual Relevant (Cnstr (Pi s (Set k) var a b)) t u = + let x : NormalForm (relevance s) (relevance s :: ctx) x = point (var, (s ** Refl)) Here in do - t <- assert_total (doApp (weaken [isSet s] t) x) - u <- assert_total (doApp (weaken [isSet s] u) x) - eq <- doEqual True b t u + t <- assert_total (doApp (weaken [relevance s] t) x) + u <- assert_total (doApp (weaken [relevance s] u) x) + eq <- doEqual Relevant b t u pure (Cnstr $ Pi s Prop var a eq) -doEqual True (Cnstr (Sigma s@(Set _) s' var a b)) t u = do - t1 <- doFst True (isSet s') t - u1 <- doFst True (isSet s') u - t2 <- doSnd True (isSet s') t - u2 <- doSnd True (isSet s') u - eq1 <- doEqual True a t1 u1 +doEqual Relevant (Cnstr (Sigma s@(Set _) s' var a b)) t u = do + t1 <- doFst Relevant (relevance s') t + u1 <- doFst Relevant (relevance s') u + t2 <- doSnd Relevant (relevance s') t + u2 <- doSnd Relevant (relevance s') u + eq1 <- doEqual Relevant a t1 u1 bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right)) bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure u1) Right)) - t2' <- doCast (isSet s') bt1 bu1 t2 - eq2 <- doEqual (isSet s') (assert_smaller b bu1) t2' u2 - pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [False] eq2)) -doEqual True (Cnstr (Sigma Prop (Set k) var a b)) t u = do - t2 <- doSnd False True t - u2 <- doSnd False True u + t2' <- doCast (relevance s') bt1 bu1 t2 + eq2 <- doEqual (relevance s') (assert_smaller b bu1) t2' u2 + pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [Irrelevant] eq2)) +doEqual Relevant (Cnstr (Sigma Prop (Set k) var a b)) t u = do + t2 <- doSnd Irrelevant Relevant t + u2 <- doSnd Irrelevant Relevant u bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right)) bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right)) - t2' <- doCast True bt1 bu1 t2 - eq2 <- doEqual True (assert_smaller b bu1) t2' u2 - pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [False] eq2)) -doEqual True (Cnstr Bool) t u = do - true <- doIf u (Cnstr Top) (Cnstr Bottom) - false <- doIf u (Cnstr Bottom) (Cnstr Top) - doIf t true false -doEqual True (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a + t2' <- doCast Relevant bt1 bu1 t2 + eq2 <- doEqual Relevant (assert_smaller b bu1) t2' u2 + pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [Irrelevant] eq2)) +doEqual Relevant (Cnstr Bool) t u = do + relevant <- doIf u (Cnstr Top) (Cnstr Bottom) + irrelevant <- doIf u (Cnstr Bottom) (Cnstr Top) + doIf t relevant irrelevant +doEqual Relevant (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a substCnstr : Constructor ~|> Hom (LogNormalForm' ann) (LogConstructor ann) -substCnstr (Sort s) f = pure (Sort s) +substCnstr (Universe s) f = pure (Universe s) substCnstr (Pi s s' var a b) f = do a <- subst' a f b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f) @@ -241,26 +244,26 @@ substCnstr False f = pure False substCnstr Top f = pure Top substCnstr Bottom f = pure Bottom -substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann True) +substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann Relevant) substNtrl (Var var sort prf i) f = case f i of Left t => t Right j => pure (Ntrl $ Var var sort prf j) -substNtrl (App b t u) f = do +substNtrl (App r t u) f = do t <- substNtrl t f u <- subst' u f assert_total (doApp t u) -substNtrl (Fst b t) f = do +substNtrl (Fst r t) f = do t <- substNtrl t f - doFst True b t -substNtrl (Snd b t) f = do + doFst Relevant r t +substNtrl (Snd r t) f = do t <- substNtrl t f - doSnd b True $ rewrite orTrueTrue b in t + doSnd r Relevant $ rewrite pairRelevantRight r in t substNtrl (If t u v) f = do t <- substNtrl t f u <- subst' u f v <- subst' v f doIf t u v -substNtrl Absurd f = pure (doAbsurd True) +substNtrl Absurd f = pure (doAbsurd Relevant) substNtrl (Equal a t u) f = do a <- substNtrl a f t <- subst' t f |