Add more program structure to normal forms.

1 files changed, 80 insertions, 56 deletions

diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index b3762cf..c3dcfbf 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -1,6 +1,6 @@
 module Obs.Typing
 
-import Control.Monad.Maybe
+import Control.Monad.Identity
 
 import Data.Nat
 
@@ -38,90 +38,99 @@ universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
 
 -- Utilities -------------------------------------------------------------------
 
-MkPair : (s, s' : Universe)
-  -> NormalForm (relevance s) ctx
-  -> NormalForm (relevance s') ctx
-  -> NormalForm (relevance (max s s')) ctx
-MkPair Prop Prop t u = u
-MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Set t u
-MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u
+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 ------------------------------------------------------
 
 check' : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> TypeNormalForm ctx
-  -> Term (length ctx)
-  -> Logging ann (NormalForm (relevance s) ctx)
+  -> (sort : Universe)
+  -> (type : TypeNormalForm ctx)
+  -> (term : Term (length ctx))
+  -> Logging ann (NormalForm (relevance sort) ctx)
 
 infer' : (tyCtx : TyContext ctx)
-  -> Term (length ctx)
-  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
+  -> (term : Term (length ctx))
+  -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx))
 
-inferType' : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
+inferType' : {default typeMismatch tag : forall a . (expected, actual : Doc ann) -> Logging ann a}
   -> (tyCtx : TyContext ctx)
-  -> Term (length ctx)
+  -> (term : Term (length ctx))
   -> Logging ann (Universe, TypeNormalForm ctx)
-inferType' ctx t = do
-  (Set _ ** (Cnstr (Universe s), a)) <- infer' ctx t
-    | (_ ** (type, a)) => tag (pretty "sort") (pretty type)
-  pure (s, a)
+inferType' ctx term = do
+  (Set _ ** (Cnstr (Universe sort), type)) <- infer' ctx term
+    | (_ ** (type, term)) => tag (pretty "sort") (pretty type)
+  pure (sort, type)
 
 check : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> TypeNormalForm ctx
-  -> WithBounds (Term (length ctx))
-  -> Logging ann (NormalForm (relevance s) ctx)
-check ctx s a (MkBounded t irrel bounds) = inBounds (MkBounded (check' ctx s a t) irrel bounds)
+  -> (sort : Universe)
+  -> (type : TypeNormalForm ctx)
+  -> (term : WithBounds (Term (length ctx)))
+  -> Logging ann (NormalForm (relevance sort) ctx)
+check ctx sort type (MkBounded term irrel bounds) =
+  inBounds (MkBounded (check' ctx sort type term) irrel bounds)
 
 checkType : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> WithBounds (Term (length ctx))
+  -> (sort : Universe)
+  -> (term : WithBounds (Term (length ctx)))
   -> Logging ann (TypeNormalForm ctx)
-checkType ctx s tm = check ctx (succ s) (cast s) tm
+checkType ctx sort term = check ctx (succ sort) (cast sort) term
 
 infer : (tyCtx : TyContext ctx)
-  -> WithBounds (Term (length ctx))
-  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
-infer ctx (MkBounded t irrel bounds) = inBounds (MkBounded (infer' ctx t) irrel bounds)
+  -> (term : WithBounds (Term (length ctx)))
+  -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx))
+infer ctx (MkBounded term irrel bounds) = inBounds (MkBounded (infer' ctx term) irrel bounds)
 
 inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
   -> (tyCtx : TyContext ctx)
-  -> WithBounds (Term (length ctx))
+  -> (term : WithBounds (Term (length ctx)))
   -> Logging ann (Universe, TypeNormalForm ctx)
-inferType ctx (MkBounded t irrel bounds) = inBounds (MkBounded (inferType' ctx t) irrel bounds)
+inferType ctx (MkBounded term irrel bounds) =
+  inBounds (MkBounded (inferType' ctx term) irrel bounds)
 
-check' ctx sort (Cnstr (Pi domainSort codomainSort _ domain codomain)) (Lambda {var, body}) = do
+check' ctx sort
+  (Cnstr (Pi {domainSort, codomainSort, domain, codomain}))
+  (Lambda {body = MkLambda var body}) = do
   info "encountered lambda"
 
   let Yes Refl = decEq sort (domainSort ~> codomainSort)
     | No _ => fatal "internal universe mismatch"
 
-  let bodyCtx = ctx ::< MkFreeVar domainSort domain var.val
+  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 domainSort var.val body)
+    Set _ => Cnstr (Lambda {domainRel = _, var = Just var.val, body})
 
-check' ctx sort type (Lambda {var, body}) = typeMismatch (pretty "function") (pretty type)
+check' ctx sort type (Lambda {body}) = typeMismatch (pretty "function") (pretty type)
 
-check' ctx sort (Cnstr (Sigma indexSort elementSort var index element)) (Pair {first, second}) = do
+check' ctx sort
+  (Cnstr (Sigma {indexSort, elementSort, index, element}))
+  (Pair {first, second}) = do
   info "encountered pair"
 
   let Yes Refl = decEq sort (max indexSort elementSort)
     | No _ => fatal "internal universe mismatch"
+  rewrite pairRelevance indexSort elementSort
 
-  trace $ pretty {ann} "checking first has type" <++> pretty index
-  first <- check ctx indexSort index first
+  trace $ pretty {ann} "checking first has type" <++> pretty index.type
+  first <- check ctx indexSort index.type first
 
   element <- subst1 first element
   trace $ pretty {ann} "checking second has type" <++> pretty element
   second <- check ctx elementSort element second
 
-  pure $ MkPair indexSort elementSort first second
+  pure $ MkPair {indexRel = _, elementRel = _, first, second}
 
 check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type)
 
@@ -145,8 +154,8 @@ check' ctx sort type t = do
   expandedType <- subst type (reduce ctx)
   expandedInferredType <- subst inferredType (reduce ctx)
 
-  Just _ <- inScope "convert" $ runMaybeT $ convert (succ sort) (cast sort) expandedType expandedInferredType
-  | Nothing => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType)
+  let True = runIdentity $ convert Relevant (cast sort) expandedType expandedInferredType
+    | False => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType)
 
   pure value
 
@@ -162,7 +171,7 @@ infer' ctx (Universe {s}) = do
 
     pure (succ (succ s) ** (cast (succ s), cast s))
 
-infer' ctx (Pi {var, domain, codomain}) = do
+infer' ctx (Pi {domain = MkDecl var domain, codomain}) = do
     info "encountered pi"
 
     (domainSort, domain) <- inferType ctx domain
@@ -175,10 +184,15 @@ infer' ctx (Pi {var, domain, codomain}) = do
     trace $ pretty {ann} "codomain type is" <++> pretty codomain
 
     let piSort = domainVar.sort ~> codomainSort
-    let term = Cnstr (Pi domainVar.sort codomainSort var.val domain codomain)
+    let term = Cnstr $ Pi
+          { domainSort = domainVar.sort
+          , codomainSort
+          , domain = MkDecl (Just var.val) domain
+          , codomain
+          }
     pure (succ piSort ** (cast piSort, term))
 
-infer' ctx (Lambda {var, body}) = fatal "cannot infer type of lambda"
+infer' ctx (Lambda {body}) = fatal "cannot infer type of lambda"
 
 infer' ctx (App {fun, arg}) = do
     info "encountered application"
@@ -186,7 +200,7 @@ infer' ctx (App {fun, arg}) = do
     (piSort ** (funType, funValue)) <- infer ctx fun
     trace $ pretty {ann} "function has type" <++> pretty funType
 
-    let Cnstr (Pi domainSort codomainSort _ domain codomain) = funType
+    let Cnstr (Pi {domainSort, codomainSort, domain, codomain}) = funType
       | _ => inBounds $ map (const $ typeMismatch (pretty "function") (pretty funType)) fun
 
     let Yes Refl = decEq piSort (domainSort ~> codomainSort)
@@ -194,8 +208,8 @@ infer' ctx (App {fun, arg}) = do
 
     let fun = funValue
 
-    trace $ pretty {ann} "checking argument has type" <++> pretty domain
-    arg <- check ctx domainSort domain arg
+    trace $ pretty {ann} "checking argument has type" <++> pretty domain.type
+    arg <- check ctx domainSort domain.type arg
     trace $ pretty {ann} "argument is well typed"
 
     returnType <- subst1 arg codomain
@@ -205,7 +219,7 @@ infer' ctx (App {fun, arg}) = do
 
     pure (codomainSort ** (returnType, returnValue))
 
-infer' ctx (Sigma {var, index, element}) = do
+infer' ctx (Sigma {index = MkDecl var index, element}) = do
     info "encountered sigma"
 
     (indexSort, index) <- inferType ctx index
@@ -218,7 +232,12 @@ infer' ctx (Sigma {var, index, element}) = do
     trace $ pretty {ann} "element type is" <++> pretty element
 
     let sigmaSort = max indexVar.sort elementSort
-    let term = Cnstr (Sigma indexVar.sort elementSort var.val index element)
+    let term = Cnstr $ Sigma
+          { indexSort = indexVar.sort
+          , elementSort
+          , index = MkDecl (Just var.val) index
+          , element
+          }
     pure (succ sigmaSort ** (cast sigmaSort, term))
 
 infer' ctx (Pair {first, second}) = fatal "cannot infer type of pair"
@@ -229,7 +248,7 @@ infer' ctx (First {arg}) = do
     (sigmaSort ** (argType, argValue)) <- infer ctx arg
     trace $ pretty {ann} "pair has type" <++> pretty argType
 
-    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+    let Cnstr (Sigma {indexSort, elementSort, index, element}) = argType
       | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
 
     let Yes Refl = decEq sigmaSort (max indexSort elementSort)
@@ -237,7 +256,7 @@ infer' ctx (First {arg}) = do
 
     let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue
 
-    let returnType = index
+    let returnType = index.type
     returnValue <- doFst (relevance indexSort) (relevance elementSort) argValue
 
     pure (indexSort ** (returnType, returnValue))
@@ -248,7 +267,7 @@ infer' ctx (Second {arg}) = do
     (sigmaSort ** (argType, argValue)) <- infer ctx arg
     trace $ pretty {ann} "pair has type" <++> pretty argType
 
-    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+    let Cnstr (Sigma {indexSort, elementSort, index, element}) = argType
       | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
 
     let Yes Refl = decEq sigmaSort (max indexSort elementSort)
@@ -274,7 +293,7 @@ infer' ctx False = do
     info "encountered false"
     pure (Set 0 ** (Cnstr Bool, Cnstr False))
 
-infer' ctx (If {var, returnType, discriminant, true, false}) = do
+infer' ctx (If {returnType = MkLambda var returnType, discriminant, true, false}) = do
     info "encountered if"
     trace "checking discriminant is bool"
 
@@ -348,7 +367,12 @@ infer' ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
     newIndex <- check ctx indexSort indexType newIndex
     trace "new index is well typed"
 
-    let indexedTypeShape = Cnstr $ Pi indexSort (Set 0) "" indexType (Cnstr (Universe Prop))
+    let indexedTypeShape = Cnstr $ Pi
+          { domainSort = indexSort
+          , codomainSort = Set 0
+          , domain = MkDecl Nothing indexType
+          , codomain = Cnstr (Universe Prop)
+          }
     indexedType <- check ctx (indexSort ~> Set 0) indexedTypeShape indexedType
     trace $ pretty {ann} "result is an index of type" <++> pretty indexedType