diff options
Diffstat (limited to 'src/Obs/NormalForm')
| -rw-r--r-- | src/Obs/NormalForm/Normalise.idr | 329 |
1 files changed, 329 insertions, 0 deletions
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr index 2ea6296..e36e57c 100644 --- a/src/Obs/NormalForm/Normalise.idr +++ b/src/Obs/NormalForm/Normalise.idr @@ -1,6 +1,7 @@ module Obs.NormalForm.Normalise import Data.Bool +import Data.List import Data.Nat import Decidable.Equality @@ -57,6 +58,14 @@ map1 : {s' : _} -> map1 t u = subst' u (add (LogNormalForm' ann) (Left $ pure t) (Right . There)) export +MkLambda : {rel, domainRel : _} -> + (var : Maybe String) -> + (body : NormalForm rel (domainRel :: ctx)) -> + NormalForm (function domainRel rel) ctx +MkLambda {rel = Irrelevant} var body = Irrel +MkLambda {rel = Relevant} var body = Cnstr $ Lambda {var, body, domainRel} + +export doApp : {domainRel : _} -> (fun : NormalForm (function domainRel codomainRel) ctx) -> (arg : NormalForm domainRel ctx) -> @@ -72,6 +81,17 @@ doApp (Cnstr t) arg = inScope "wrong constructor for apply" $ fatal t doApp Irrel arg = pure Irrel export +MkPair : {indexRel, elementRel : Relevance} + -> (first : NormalForm indexRel ctx) + -> (second : NormalForm elementRel ctx) + -> NormalForm (pair indexRel elementRel) ctx +MkPair {indexRel = Irrelevant, elementRel = Irrelevant, first, second} = Irrel +MkPair {indexRel = Irrelevant, elementRel = Relevant, first, second} = + Cnstr $ Pair {indexRel = Irrelevant, elementRel = Relevant, prf = Relevant, first, second} +MkPair {indexRel = Relevant, elementRel, first, second} = + Cnstr $ Pair {indexRel = Relevant, elementRel, prf = Relevant, first, second} + +export doFst : (firstRel, secondRel : _) -> (arg : NormalForm (pair firstRel secondRel) ctx) -> LogNormalForm ann firstRel ctx @@ -97,6 +117,193 @@ doSnd firstRel Relevant arg = Cnstr t => inScope "wrong constructor for snd" $ fatal t export +doContainer : ContainerTy ctx -> TypeNormalForm ctx +doContainer container = + Cnstr $ Pi + { domainSort = container.inputSort + , codomainSort = + max (succ container.shapeSort) + (container.shapeSort ~> + max (succ container.positionSort) (container.positionSort ~> container.outputSort)) + , domain = MkDecl Nothing container.input + , codomain = Cnstr $ Sigma + { indexSort = succ container.shapeSort + , elementSort = container.shapeSort ~> + max (succ container.positionSort) + (container.positionSort ~> container.outputSort) + , index = MkDecl (Just "Shape") (cast container.shapeSort) + , element = Cnstr $ Pi + { domainSort = container.shapeSort + , codomainSort = max (succ container.positionSort) + (container.positionSort ~> container.outputSort) + , domain = MkDecl Nothing (Ntrl $ Var "Shape" Here) + , codomain = Cnstr $ Sigma + { indexSort = succ container.positionSort + , elementSort = container.positionSort ~> container.outputSort + , index = MkDecl (Just "Position") (cast container.positionSort) + , element = Cnstr $ Pi + { domainSort = container.positionSort + , codomainSort = container.outputSort + , domain = MkDecl Nothing (Ntrl $ Var "Position" Here) + , codomain = weaken [_, _, _, _, _] container.output + } + } + } + } + } + +export +MkContainer : (inputRel, shapeRel : Relevance) -> + {outputRel : Relevance} -> + (shape : TypeNormalForm ctx) -> + (position : TypeNormalForm ctx) -> + (next : NormalForm outputRel ctx) -> + LogNormalForm ann Relevant ctx +MkContainer {inputRel, shapeRel, outputRel, shape, position, next} = do + shape <- doApp (Sorted.weaken [inputRel] shape) (point Nothing Here) + position <- doApp (weaken [shapeRel, inputRel] position) (point Nothing (There Here)) + position <- doApp position (point Nothing Here) + next <- doApp (weaken [shapeRel, inputRel] next) (point Nothing (There Here)) + next <- doApp next (point Nothing Here) + pure $ MkLambda + { var = Nothing + , body = MkPair + { first = shape + , second = MkLambda + { var = Nothing + , body = MkPair + { first = position + , second = next + } + } + } + } + +export +doShape : (inputRel : Relevance) -> + (arg : NormalForm Relevant ctx) -> + LogNormalForm ann Relevant ctx +doShape inputRel arg = + let inputIndex : NormalForm inputRel (inputRel :: ctx) + inputIndex = point Nothing Here + in do + inputIndexed <- doApp (weaken [_] arg) inputIndex + body <- doFst Relevant Relevant inputIndexed + + pure $ MkLambda {var = Nothing, body} + +export +doPosition : (inputRel, shapeRel, outputRel : Relevance) -> + (arg : NormalForm Relevant ctx) -> + LogNormalForm ann Relevant ctx +doPosition {inputRel, shapeRel, outputRel, arg} = + let inputIndex : NormalForm inputRel (inputRel :: ctx) + inputIndex = point Nothing Here + in + let shapeIndex : NormalForm shapeRel (shapeRel :: inputRel :: ctx) + shapeIndex = point Nothing Here + in do + inputIndexed <- doApp (weaken [_] arg) inputIndex + + positionNextPair <- doSnd Relevant Relevant inputIndexed + let positionNextPair = weaken [_] positionNextPair + + shapeIndexed <- doApp positionNextPair shapeIndex + body <- doFst Relevant outputRel shapeIndexed + + pure $ MkLambda + { var = Nothing + , body = MkLambda {var = Nothing, body} + } + +export +doNext : (inputRel, shapeRel, outputRel : Relevance) -> + (arg : NormalForm Relevant ctx) -> + LogNormalForm ann outputRel ctx +doNext {inputRel, shapeRel, outputRel, arg} = + let inputIndex : NormalForm inputRel (inputRel :: ctx) + inputIndex = point Nothing Here + in + let shapeIndex : NormalForm shapeRel (shapeRel :: inputRel :: ctx) + shapeIndex = point Nothing Here + in do + inputIndexed <- doApp (weaken [_] arg) inputIndex + + positionNextPair <- doSnd Relevant Relevant inputIndexed + let positionNextPair = weaken [_] positionNextPair + + shapeIndexed <- doApp positionNextPair shapeIndex + body <- doSnd Relevant outputRel shapeIndexed + + pure $ MkLambda + { var = Nothing + , body = MkLambda {var = Nothing, body} + } + +export +doSem : (container : ContainerTy ctx) -> + (predSort : Universe) -> + (pred : TypeNormalForm (relevance container.outputSort :: ctx)) -> + (arg : NormalForm Relevant ctx) -> + LogNormalForm ann Relevant ctx +doSem {container, predSort, pred, arg} = do + let inputVar = Nothing + let shapeVar = Nothing + let positionVar = Nothing + + let inputDomain = MkDecl inputVar container.input + + shape <- doShape {inputRel = relevance container.inputSort, arg} + let shape = Sorted.weaken [_] shape + + shapeType <- doApp shape (point inputVar Here) + let shapeIndex = MkDecl shapeVar shapeType + + position <- doPosition + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , outputRel = relevance container.outputSort + , arg + } + let position = Sorted.weaken [_,_] position + + positionType <- doApp position (point inputVar (There Here)) + positionType <- doApp positionType (point shapeVar Here) + let positionDomain = MkDecl positionVar positionType + + next <- doNext + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , outputRel = relevance container.outputSort + , arg + } + let next = Sorted.weaken [_,_,_] next + + next <- doApp next (point inputVar (There (There Here))) + next <- doApp next (point shapeVar (There Here)) + next <- doApp next (point positionVar Here) + + let f = add (LogNormalForm' ann) (Left $ pure next) (Right . There . There . There) + codomain <- subst' pred f + + pure $ Cnstr $ Pi + { domainSort = container.inputSort + , codomainSort = max container.shapeSort (container.positionSort ~> predSort) + , domain = inputDomain + , codomain = Cnstr $ Sigma + { indexSort = container.shapeSort + , elementSort = container.positionSort ~> predSort + , index = shapeIndex + , element = Cnstr $ Pi + { domainSort = container.positionSort + , codomainSort = predSort + , domain = positionDomain + , codomain + } + } + } + +export doIf : {rel : _} -> (discriminant : NormalForm Relevant ctx) -> (true, false : NormalForm rel ctx) -> @@ -574,3 +781,125 @@ subst' Irrel f = pure Irrel export subst : NormalForm ~|> Hom (LogNormalForm ann) (LogNormalForm ann) subst t f = subst' t (Left . f) + +export +strengthen : (ctx' : List Relevance) -> + Map ctx' (LogNormalForm' ann) ctx -> + Map (ctx' ++ ctx) (LogNormalForm' ann) ctx +strengthen [] f = Right +strengthen (rel :: ctx) f = add (LogNormalForm' ann) (f Here) (strengthen ctx (f . There)) + +-- Container Utilities --------------------------------------------------------- + +public export +containerSort : (container : ContainerTy ctx) -> Universe +containerSort container = + container.inputSort ~> + max (succ container.shapeSort) + (container.shapeSort ~> + max (succ container.positionSort) (container.positionSort ~> container.outputSort)) + +export +matchContainer : (type : TypeNormalForm ctx) -> Logging ann (ContainerTy ctx) +matchContainer type@(Cnstr (Pi + { domainSort = inputSort + , codomainSort = inputCodomainSort + , domain = MkDecl _ input + , codomain = Cnstr (Sigma + { indexSort = succShapeSort@(Set _) + , elementSort = shapeElementSort + , index = MkDecl _ (Cnstr (Universe shapeSort)) + , element = Cnstr (Pi + { domainSort = shapeSort' + , codomainSort = shapeCodomainSort + , domain = MkDecl _ (Ntrl (Var _ Here)) + , codomain = Cnstr (Sigma + { indexSort = succPositionSort@(Set _) + , elementSort = positionElementSort + , index = MkDecl _ (Cnstr (Universe positionSort)) + , element = Cnstr (Pi + { domainSort = positionSort' + , codomainSort = outputSort + , domain = MkDecl _ (Ntrl (Var _ Here)) + , codomain = output' + }) + }) + }) + }) + })) = do + let Yes Refl = decEq + ( inputCodomainSort + , succShapeSort + , shapeElementSort + , shapeSort' + , shapeCodomainSort + , succPositionSort + , positionElementSort + , positionSort') + ( max (succ shapeSort) + (shapeSort ~> max (succ positionSort) (positionSort ~> outputSort)) + , succ shapeSort + , shapeSort ~> max (succ positionSort) (positionSort ~> outputSort) + , shapeSort + , max (succ positionSort) (positionSort ~> outputSort) + , succ positionSort + , positionSort ~> outputSort + , positionSort) + | No _ => typeMismatch (pretty "container") (pretty type) + + output <- subst' output' $ + strengthen [_, _, _, _, _] $ + const $ Left $ typeMismatch (pretty "container") (pretty type) + pure (MkContainerTy {inputSort, shapeSort, positionSort, outputSort, input, output}) +matchContainer type = typeMismatch (pretty "container") (pretty type) + +export +containerShapeType : ContainerTy ctx -> TypeNormalForm ctx +containerShapeType container = + Cnstr $ Pi + { domainSort = container.inputSort + , codomainSort = succ container.shapeSort + , domain = MkDecl Nothing container.input + , codomain = cast container.shapeSort + } + +export +containerPositionType : (container : ContainerTy ctx) -> + (shape : TypeNormalForm (relevance container.inputSort :: ctx)) -> + TypeNormalForm ctx +containerPositionType container shape = + Cnstr $ Pi + { domainSort = container.inputSort + , codomainSort = container.shapeSort ~> succ container.positionSort + , domain = MkDecl Nothing container.input + , codomain = Cnstr $ Pi + { domainSort = container.shapeSort + , codomainSort = succ container.positionSort + , domain = MkDecl Nothing shape + , codomain = cast container.positionSort + } + } + +export +containerNextType : (container : ContainerTy ctx) -> + (shape : TypeNormalForm (relevance container.inputSort :: ctx)) -> + (position : + TypeNormalForm (relevance container.shapeSort :: relevance container.inputSort :: ctx)) -> + TypeNormalForm ctx +containerNextType container shape position = + Cnstr $ Pi + { domainSort = container.inputSort + , codomainSort = container.shapeSort ~> container.positionSort ~> container.outputSort + , domain = MkDecl Nothing container.input + , codomain = Cnstr $ Pi + { domainSort = container.shapeSort + , codomainSort = container.positionSort ~> container.outputSort + , domain = MkDecl Nothing shape + , codomain = Cnstr $ Pi + { domainSort = container.positionSort + , codomainSort = container.outputSort + , domain = MkDecl Nothing position + , codomain = weaken [_, _, _] container.output + } + } + } |