diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 267 |
1 files changed, 137 insertions, 130 deletions
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr index d660111..0b9d2b6 100644 --- a/src/Obs/NormalForm.idr +++ b/src/Obs/NormalForm.idr @@ -2,6 +2,7 @@ module Obs.NormalForm import Data.List.Elem +import Obs.Pretty import Obs.Substitution import Obs.Universe @@ -19,27 +20,31 @@ TypeNormalForm : Unsorted.Family Relevance TypeNormalForm = NormalForm Relevant public export +record DeclForm (ctx : List Relevance) where + constructor MkDecl + var : Maybe String + type : TypeNormalForm ctx + +public export data Constructor : Unsorted.Family Relevance where Universe : (s : Universe) -> Constructor ctx - Pi : (s, s' : Universe) - -> (var : String) - -> (a : TypeNormalForm ctx) - -> (b : TypeNormalForm (relevance s :: ctx)) - -> Constructor ctx - Lambda : (s : Universe) - -> (var : String) - -> NormalForm Relevant (relevance s :: ctx) - -> Constructor ctx - Sigma : (s, s' : Universe) - -> (var : String) - -> (a : TypeNormalForm ctx) - -> (b : TypeNormalForm (relevance s :: ctx)) - -> Constructor ctx - Pair : (s, s' : Universe) - -> (prf : IsRelevant (max s s')) - -> NormalForm (relevance s) ctx - -> NormalForm (relevance s') ctx - -> Constructor ctx + Pi : (domainSort, codomainSort : Universe) -> + (domain : DeclForm ctx) -> + (codomain : TypeNormalForm (relevance domainSort :: ctx)) -> + Constructor ctx + Lambda : (domainRel : Relevance) -> + (var : Maybe String) -> + (body : NormalForm Relevant (domainRel :: ctx)) -> + Constructor ctx + Sigma : (indexSort, elementSort : Universe) -> + (index : DeclForm ctx) -> + (element : TypeNormalForm (relevance indexSort :: ctx)) -> + Constructor ctx + Pair : (indexRel, elementRel : Relevance) -> + (prf : IsRelevant (pair indexRel elementRel)) -> + (first : NormalForm indexRel ctx) -> + (second : NormalForm elementRel ctx) -> + Constructor ctx Bool : Constructor ctx True : Constructor ctx False : Constructor ctx @@ -48,26 +53,27 @@ data Constructor : Unsorted.Family Relevance where public export data Neutral : Unsorted.Family Relevance where - Var : (var : String) - -> (sort : Universe) - -> (prf : IsRelevant sort) - -> (i : Elem Relevant ctx) - -> Neutral ctx - App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx - Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx - Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx - If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx + Var : (var : String) -> (i : Elem Relevant ctx) -> Neutral ctx + App : (argRel : Relevance) -> (fun : Neutral ctx) -> (arg : NormalForm argRel ctx) -> Neutral ctx + First : (secondRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx + Second : (firstRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx + If : (discriminant : Neutral ctx) -> (true, false : NormalForm Relevant ctx) -> Neutral ctx Absurd : Neutral ctx - Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx - EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx - EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx - EqualStuck : (a, b : Constructor ctx) -> Neutral ctx - CastL : (a : Neutral ctx) -> - (b : TypeNormalForm ctx) -> - NormalForm Relevant ctx -> + Equal : (type : Neutral ctx) -> (left, right : NormalForm Relevant ctx) -> Neutral ctx + EqualL : (left : Neutral ctx) -> (right : TypeNormalForm ctx) -> Neutral ctx + EqualR : (left : Constructor ctx) -> (right : Neutral ctx) -> Neutral ctx + EqualStuck : (left, right : Constructor ctx) -> Neutral ctx + CastL : (oldType : Neutral ctx) -> + (newType : TypeNormalForm ctx) -> + (value : NormalForm Relevant ctx) -> + Neutral ctx + CastR : (oldType : Constructor ctx) -> + (newType : Neutral ctx) -> + (value : NormalForm Relevant ctx) -> + Neutral ctx + CastStuck : (oldType, newType : Constructor ctx) -> + (value : NormalForm Relevant ctx) -> Neutral ctx - CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx - CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx public export data NormalForm : Sorted.Family Relevance where @@ -108,34 +114,19 @@ Cast Universe (NormalForm Relevant ctx) where prettyPrec : Prec -> NormalForm b ctx -> Doc ann +prettyPrecDecl : DeclForm ctx -> Doc ann +prettyPrecDecl (MkDecl var type) = prettyDecl var (prettyPrec Open type) + prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann -prettyPrecCnstr d (Universe s) = prettyPrec d s -prettyPrecCnstr d (Pi s s' var a b) = - let lhs = case var of - "" => align (prettyPrec App a) - _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a)) - in - parenthesise (d > Open) $ - group $ - lhs <++> pretty "->" <+> line <+> align (prettyPrec Open b) -prettyPrecCnstr d (Lambda _ var t) = - parenthesise (d > Open) $ - group $ - backslash <+> pretty var <++> - pretty "=>" <+> line <+> - align (prettyPrec Open t) -prettyPrecCnstr d (Sigma s s' var a b) = - let lhs = case var of - "" => align (prettyPrec App a) - _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a)) - in - parenthesise (d > Open) $ - group $ - lhs <++> pretty "**" <+> line <+> align (prettyPrec Open b) -prettyPrecCnstr d (Pair s s' prf t u) = - angles $ - group $ - neutral <++> prettyPrec Open t <+> comma <+> line <+> prettyPrec Open u <++> neutral +prettyPrecCnstr d (Universe {s}) = prettyPrec d s +prettyPrecCnstr d (Pi {domainSort, codomainSort, domain, codomain}) = + prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrec Open codomain) +prettyPrecCnstr d (Lambda {domainRel, var, body}) = + prettyLambda d (maybe "_" id var) (prettyPrec Open body) +prettyPrecCnstr d (Sigma {indexSort, elementSort, index, element}) = + prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrec Open element) +prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) = + prettyPair (prettyPrec Open first) (prettyPrec Open second) prettyPrecCnstr d Bool = pretty "Bool" prettyPrecCnstr d True = pretty "True" prettyPrecCnstr d False = pretty "False" @@ -143,52 +134,34 @@ prettyPrecCnstr d Top = pretty "()" prettyPrecCnstr d Bottom = pretty "Void" prettyPrecNtrl : Prec -> Neutral ctx -> Doc ann -prettyPrecNtrl d (Var var sort prf i) = pretty "\{var}@\{show $ elemToNat i}" -prettyPrecNtrl d (App _ t u) = - parenthesise (d >= App) $ - group $ - vsep [prettyPrecNtrl Open t, prettyPrec App u] -prettyPrecNtrl d (Fst _ t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "fst", prettyPrecNtrl App t] -prettyPrecNtrl d (Snd _ t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "snd", prettyPrecNtrl App t] -prettyPrecNtrl d (If t f g) = - parenthesise (d >= App) $ - group $ - vsep [pretty "if", prettyPrecNtrl App t, prettyPrec App f, prettyPrec App g] +prettyPrecNtrl d (Var {var, i}) = pretty "\{var}@\{show $ elemToNat i}" +prettyPrecNtrl d (App {argRel, fun, arg}) = + prettyApp d (prettyPrecNtrl Open fun) [prettyPrec App arg] +prettyPrecNtrl d (First {secondRel, arg}) = + prettyApp d (pretty "fst") [prettyPrecNtrl App arg] +prettyPrecNtrl d (Second {firstRel, arg}) = + prettyApp d (pretty "snd") [prettyPrecNtrl App arg] +prettyPrecNtrl d (If {discriminant, true, false}) = + prettyApp d (pretty "if") $ + [prettyPrecNtrl App discriminant, prettyPrec App true, prettyPrec App false] prettyPrecNtrl d Absurd = pretty "absurd" -prettyPrecNtrl d (Equal a t u) = - parenthesise (d >= Equal) $ - group $ - prettyPrec Equal t <++> pretty "~" <+> line <+> prettyPrec Equal u -prettyPrecNtrl d (EqualL a b) = - parenthesise (d >= Equal) $ - group $ - prettyPrecNtrl Equal a <++> pretty "~" <+> line <+> prettyPrec Equal b -prettyPrecNtrl d (EqualR a b) = - parenthesise (d >= Equal) $ - group $ - prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecNtrl Equal b -prettyPrecNtrl d (EqualStuck a b) = - parenthesise (d >= Equal) $ - group $ - prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecCnstr Equal b -prettyPrecNtrl d (CastL a b t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "cast", prettyPrecNtrl App a, prettyPrec App b, prettyPrec App t] -prettyPrecNtrl d (CastR a b t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrec App t] -prettyPrecNtrl d (CastStuck a b t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrec App t] +prettyPrecNtrl d (Equal {type, left, right}) = + prettyEqual d (prettyPrec Equal left) (prettyPrec Equal right) +prettyPrecNtrl d (EqualL {left, right}) = + prettyEqual d (prettyPrecNtrl Equal left) (prettyPrec Equal right) +prettyPrecNtrl d (EqualR {left, right}) = + prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecNtrl Equal right) +prettyPrecNtrl d (EqualStuck {left, right}) = + prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecCnstr Equal right) +prettyPrecNtrl d (CastL {oldType, newType, value}) = + prettyApp d (pretty "cast") $ + [prettyPrecNtrl App oldType, prettyPrec App newType, prettyPrec App value] +prettyPrecNtrl d (CastR {oldType, newType, value}) = + prettyApp d (pretty "cast") $ + [prettyPrecCnstr App oldType, prettyPrecNtrl App newType, prettyPrec App value] +prettyPrecNtrl d (CastStuck {oldType, newType, value}) = + prettyApp d (pretty "cast") $ + [prettyPrecCnstr App oldType, prettyPrecCnstr App newType, prettyPrec App value] prettyPrec d (Ntrl t) = prettyPrecNtrl d t prettyPrec d (Cnstr t) = prettyPrecCnstr d t @@ -210,13 +183,35 @@ Pretty (NormalForm b ctx) where rename : NormalForm ~|> Hom Elem NormalForm +renameDecl : DeclForm ~|> Hom Elem DeclForm +renameDecl (MkDecl var type) f = MkDecl var (rename type f) + renameCnstr : Constructor ~|> Hom Elem Constructor -renameCnstr (Universe s) f = Universe s -renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f)) -renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f)) -renameCnstr (Sigma s s' var a b) f = - Sigma s s' var (rename a f) (rename b (lift [(_ ** ())] f)) -renameCnstr (Pair s s' prf t u) f = Pair s s' prf (rename t f) (rename u f) +renameCnstr (Universe {s}) f = Universe {s} +renameCnstr (Pi {domainSort, codomainSort, domain, codomain}) f = + Pi + { domainSort + , codomainSort + , domain = renameDecl domain f + , codomain = rename codomain (lift [(_ ** ())] f) + } +renameCnstr (Lambda {domainRel, var, body}) f = + Lambda {domainRel, var, body = rename body (lift [(_ ** ())] f)} +renameCnstr (Sigma {indexSort, elementSort, index, element}) f = + Sigma + { indexSort + , elementSort + , index = renameDecl index f + , element = rename element (lift [(_ ** ())] f) + } +renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f = + Pair + { indexRel + , elementRel + , prf + , first = rename first f + , second = rename second f + } renameCnstr Bool f = Bool renameCnstr True f = True renameCnstr False f = False @@ -224,19 +219,30 @@ renameCnstr Top f = Top renameCnstr Bottom f = Bottom renameNtrl : Neutral ~|> Hom Elem Neutral -renameNtrl (Var var sort prf i) f = Var var sort prf (f i) -renameNtrl (App b t u) f = App b (renameNtrl t f) (rename u f) -renameNtrl (Fst b t) f = Fst b (renameNtrl t f) -renameNtrl (Snd b t) f = Snd b (renameNtrl t f) -renameNtrl (If t u v) f = If (renameNtrl t f) (rename u f) (rename v f) +renameNtrl (Var {var, i}) f = Var {var, i = f i} +renameNtrl (App {argRel, fun, arg}) f = App {argRel, fun = renameNtrl fun f, arg = rename arg f} +renameNtrl (First {secondRel, arg}) f = First {secondRel, arg = renameNtrl arg f} +renameNtrl (Second {firstRel, arg}) f = Second {firstRel, arg = renameNtrl arg f} +renameNtrl (If {discriminant, true, false}) f = + If {discriminant = renameNtrl discriminant f, true = rename true f, false = rename false f} renameNtrl Absurd f = Absurd -renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (rename t f) (rename u f) -renameNtrl (EqualL a b) f = EqualL (renameNtrl a f) (rename b f) -renameNtrl (EqualR a b) f = EqualR (renameCnstr a f) (renameNtrl b f) -renameNtrl (EqualStuck a b) f = EqualStuck (renameCnstr a f) (renameCnstr b f) -renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (rename b f) (rename t f) -renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (rename t f) -renameNtrl (CastStuck a b t) f = CastStuck (renameCnstr a f) (renameCnstr b f) (rename t f) +renameNtrl (Equal {type, left, right}) f = + Equal {type = renameNtrl type f, left = rename left f, right = rename right f} +renameNtrl (EqualL {left, right}) f = EqualL {left = renameNtrl left f, right = rename right f} +renameNtrl (EqualR {left, right}) f = + EqualR {left = renameCnstr left f, right = renameNtrl right f} +renameNtrl (EqualStuck {left, right}) f = + EqualStuck {left = renameCnstr left f, right = renameCnstr right f} +renameNtrl (CastL {oldType, newType, value}) f = + CastL {oldType = renameNtrl oldType f, newType = rename newType f, value = rename value f} +renameNtrl (CastR {oldType, newType, value}) f = + CastR {oldType = renameCnstr oldType f, newType = renameNtrl newType f, value = rename value f} +renameNtrl (CastStuck {oldType, newType, value}) f = + CastStuck + { oldType = renameCnstr oldType f + , newType = renameCnstr newType f + , value = rename value f + } rename (Ntrl t) f = Ntrl $ renameNtrl t f rename (Cnstr t) f = Cnstr $ renameCnstr t f @@ -249,12 +255,13 @@ Unsorted.Rename Relevance Constructor where export Unsorted.Rename Relevance Neutral where rename = renameNtrl - + export Sorted.Rename Relevance NormalForm where rename = NormalForm.rename export -PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where +PointedRename Relevance (\r => Maybe String) NormalForm where point {s = Irrelevant} _ _ = Irrel - point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i) + point {s = Relevant} var i = + Ntrl (Var {var = maybe "" id var, i}) |