diff options
Diffstat (limited to 'src/Obs/Typing.idr')
| -rw-r--r-- | src/Obs/Typing.idr | 204 |
1 files changed, 178 insertions, 26 deletions
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr index c3dcfbf..8369fe0 100644 --- a/src/Obs/Typing.idr +++ b/src/Obs/Typing.idr @@ -23,30 +23,8 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal %default total --- Loggings ---------------------------------------------------------------------- - -mismatch : (expected, got : Doc ann) -> Logging ann a -mismatch lhs rhs = fatal $ - hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+> - hang 2 (pretty "got" <+> line <+> align rhs) - -typeMismatch : Doc ann -> Doc ann -> Logging ann a -typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs - -universeMismatch : Doc ann -> Doc ann -> Logging ann a -universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs - -- Utilities ------------------------------------------------------------------- -MkPair : (indexRel, elementRel : Relevance) - -> (first : NormalForm indexRel ctx) - -> (second : NormalForm elementRel ctx) - -> NormalForm (pair indexRel elementRel) ctx -MkPair Irrelevant Irrelevant first second = Irrel -MkPair Irrelevant Relevant first second = - Cnstr $ Pair {indexRel = Irrelevant, elementRel = Relevant, prf = Relevant, first, second} -MkPair Relevant elementRel first second = - Cnstr $ Pair {indexRel = Relevant, elementRel, prf = Relevant, first, second} -- Checking and Inference ------------------------------------------------------ @@ -102,15 +80,14 @@ check' ctx sort let Yes Refl = decEq sort (domainSort ~> codomainSort) | No _ => fatal "internal universe mismatch" + rewrite functionRelevance domainSort codomainSort let bodyCtx = ctx ::< MkFreeVar domainSort domain.type var.val trace $ pretty {ann} "checking body has type" <++> pretty codomainSort body <- check bodyCtx codomainSort codomain body - pure $ case codomainSort of - Prop => Irrel - Set _ => Cnstr (Lambda {domainRel = _, var = Just var.val, body}) + pure $ MkLambda {var = Just var.val, body} check' ctx sort type (Lambda {body}) = typeMismatch (pretty "function") (pretty type) @@ -130,10 +107,58 @@ check' ctx sort trace $ pretty {ann} "checking second has type" <++> pretty element second <- check ctx elementSort element second - pure $ MkPair {indexRel = _, elementRel = _, first, second} + pure $ MkPair {first, second} check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type) +check' ctx sort type (MkContainer {shape, position, next}) = do + container <- matchContainer type + + let Yes Refl = decEq sort $ + container.inputSort ~> + max (succ container.shapeSort) + (container.shapeSort ~> + max (succ container.positionSort) (container.positionSort ~> container.outputSort)) + | No _ => fatal "internal universe mismatch" + + info "encountered container constructor" + + let shapeType = containerShapeType container + trace $ pretty {ann} "checking shape has type" <++> pretty shapeType + shape <- check ctx (container.inputSort ~> succ container.shapeSort) shapeType shape + + shapeInstance <- doApp (weaken [relevance container.inputSort] shape) (point Nothing Here) + + let positionType = containerPositionType container shapeInstance + trace $ pretty {ann} "checking position has type" <++> pretty positionType + position <- check + { tyCtx = ctx + , sort = container.inputSort ~> container.shapeSort ~> succ container.positionSort + , type = positionType + , term = position + } + + let positionInstance = weaken [relevance container.shapeSort, relevance container.inputSort] position + positionInstance <- doApp positionInstance (point Nothing (There Here)) + positionInstance <- doApp positionInstance (point Nothing Here) + + let nextType = containerNextType container shapeInstance positionInstance + trace $ pretty {ann} "checking next has type" <++> pretty nextType + next <- check + { tyCtx = ctx + , sort = container.inputSort ~> container.shapeSort ~> container.positionSort ~> container.outputSort + , type = nextType + , term = next + } + + MkContainer + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , shape + , position + , next + } + check' ctx sort type (Absurd {contradiction}) = do info "encountered absurd" @@ -281,6 +306,133 @@ infer' ctx (Second {arg}) = do pure (elementSort ** (returnType, returnValue)) +infer' ctx (Container {input, output, shapeSort, positionSort}) = do + info "encountered container" + + (inputSort, input) <- inferType ctx input + trace $ pretty {ann} "input type is" <++> pretty input + + (outputSort, output) <- inferType ctx output + trace $ pretty {ann} "output type is" <++> pretty output + + let shapeSort = shapeSort.val + let positionSort = positionSort.val + + let containerSort = foldr1 max + [ inputSort ~> succ shapeSort + , inputSort ~> shapeSort ~> succ positionSort + , inputSort ~> shapeSort ~> positionSort ~> outputSort + ] + let container = MkContainerTy {inputSort, shapeSort, positionSort, outputSort, input, output} + let container = doContainer container + + pure (succ containerSort ** (cast containerSort, container)) + +infer' ctx (MkContainer {shape, position, next}) = fatal "cannot infer type of container" + +infer' ctx (Shape {arg}) = do + info "encountered Shape" + + (sort ** (type, arg)) <- infer ctx arg + trace $ pretty {ann} "argument type is" <++> pretty type + + container <- matchContainer type + + let Yes Refl = decEq sort (containerSort container) + | No _ => fatal "internal universe mismatch" + + let shapeType = containerShapeType container + shape <- doShape {inputRel = relevance container.inputSort, arg} + + pure ((container.inputSort ~> succ container.shapeSort) ** (shapeType, shape)) + +infer' ctx (Position {arg}) = do + info "encountered Position" + + (sort ** (type, arg)) <- infer ctx arg + trace $ pretty {ann} "argument type is" <++> pretty type + + container <- matchContainer type + + let Yes Refl = decEq sort (containerSort container) + | No _ => fatal "internal universe mismatch" + + shape <- doShape {inputRel = relevance container.inputSort, arg} + shape <- doApp (weaken [_] shape) (point Nothing Here) + + let positionType = containerPositionType container shape + position <- doPosition + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , outputRel = relevance container.outputSort + , arg + } + + pure ((container.inputSort ~> container.shapeSort ~> succ container.positionSort) ** + (positionType, position)) + +infer' ctx (Next {arg}) = + let eq : (a, b, c, d : Universe) -> relevance (a ~> b ~> c ~> d) = relevance d + eq a b c d = + rewrite sym $ functionRelevance c d in + rewrite sym $ functionRelevance b (c ~> d) in + rewrite sym $ functionRelevance a (b ~> c ~> d) in + Refl + in do + info "encountered nextIndex" + + (sort ** (type, arg)) <- infer ctx arg + trace $ pretty {ann} "argument type is" <++> pretty type + + container <- matchContainer type + + let Yes Refl = decEq sort (containerSort container) + | No _ => fatal "internal universe mismatch" + + shape <- doShape {inputRel = relevance container.inputSort, arg} + shape <- doApp (weaken [_] shape) (point Nothing Here) + + position <- doPosition + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , outputRel = relevance container.outputSort + , arg + } + position <- doApp (weaken [_, _] position) (point Nothing (There Here)) + position <- doApp position (point Nothing Here) + + let nextType = containerNextType container shape position + nextIndex <- doNext + { inputRel = relevance container.inputSort + , shapeRel = relevance container.shapeSort + , outputRel = relevance container.outputSort + , arg + } + + let next' = rewrite eq container.inputSort container.shapeSort container.positionSort container.outputSort in nextIndex + + pure ((container.inputSort ~> container.shapeSort ~> container.positionSort ~> container.outputSort) ** + (nextType, next')) + +infer' ctx (Sem {pred = MkLambda var pred, arg}) = do + info "encountered extension" + + (sort ** (type, arg)) <- infer ctx arg + trace $ pretty {ann} "argument type is" <++> pretty type + + container <- matchContainer type + + let Yes Refl = decEq sort (containerSort container) + | No _ => fatal "internal universe mismatch" + + let predCtx = ctx ::< MkFreeVar container.outputSort container.output var.val + (predSort, pred) <- inferType predCtx pred + + let semSort = container.inputSort ~> max container.shapeSort (container.positionSort ~> predSort) + semType <- doSem container predSort pred arg + + pure (succ semSort ** (cast semSort, semType)) + infer' ctx Bool = do info "encountered bool" pure (Set 1 ** (cast (Set 0), Cnstr Bool)) |