From ab2508e0ce1130ce067973bb2fc713d29df27458 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 5 Mar 2023 16:49:50 +0100 Subject: [PATCH] add fromPTerm, etc --- lib/Quox/Context.idr | 6 ++ lib/Quox/Parser/Syntax.idr | 148 +++++++++++++++++++++++++++++++++++++ 2 files changed, 154 insertions(+) diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index 3713656..a1183f8 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -93,6 +93,12 @@ public export %inline (!!!) : Context' tm len -> Var len -> tm (!!!) = getWith const +public export +find : Alternative f => + (forall n. tm n -> Bool) -> Context tm len -> f (Var len) +find p [<] = empty +find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx) + ||| a triangle of bindings. each type binding in a context counts the ues of ||| others in its type, and all of these together form a triangle. diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 001570f..edd13fc 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -3,6 +3,8 @@ module Quox.Parser.Syntax import public Quox.Syntax import public Quox.Syntax.Qty.Three +import public Control.Monad.Either + import Derive.Prelude %hide TT.Name @@ -25,6 +27,7 @@ PQty = Three namespace PDim public export data PDim = K DimConst | V BaseName + %name PDim p, q %runElab derive "PDim" [Eq, Ord, Show] namespace PTerm @@ -51,11 +54,13 @@ namespace PTerm | V Name | (:#) PTerm PTerm + %name PTerm s, t public export data PCaseBody = CasePair (BName, BName) PTerm | CaseEnum (List (TagVal, PTerm)) + %name PCaseBody body %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show] @@ -150,3 +155,146 @@ namespace Elim export toPTerm : Elim Three 0 0 -> PTerm toPTerm = toPTermWith [<] [<] + + + +public export +data FromPTermError = + AnnotationNeeded PTerm + | DuplicatesInEnum (List TagVal) + | DimNotInScope Name + +public export +FromPTerm : (Type -> Type) -> Type +FromPTerm m = MonadError FromPTermError m + +private +extendVect : Telescope' a from to -> Vect n a -> Telescope' a from (n + to) +extendVect tel [] = tel +extendVect tel (x :: xs) {n = S n} = + rewrite plusSuccRightSucc n to in + extendVect (tel :< x) xs + + +parameters {auto _ : FromPTerm m} (b : Var n -> m a) (f : Name -> m a) + (xs : Context' BName n) + private + fromBaseName : BaseName -> m a + fromBaseName x = maybe (f $ unq x) b $ Context.find (== Just x) xs + + fromName : Name -> m a + fromName x = if null x.mods then fromBaseName x.base else f x + +export +fromPDimWith : FromPTerm m => + Context' BName d -> PDim -> m (Dim d) +fromPDimWith ds (K e) = pure $ K e +fromPDimWith ds (V i) = + fromBaseName (pure . B) (throwError . DimNotInScope) ds i + +mutual + export + fromPTermWith : FromPTerm m => + Context' BName d -> Context' BName n -> + PTerm -> m (Term Three d n) + fromPTermWith ds ns t0 = case t0 of + TYPE k => + pure $ TYPE $ k + + Pi pi x s t => + Pi pi <$> fromPTermWith ds ns s + <*> fromPTermTScope ds ns [x] t + + Lam x s => + Lam <$> fromPTermTScope ds ns [x] s + + s :@ t => + map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t + + Sig x s t => + Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t + + Pair s t => + Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t + + Case pi pair (r, ret) (CasePair (x, y) body) => + map E $ Base.CasePair pi + <$> fromPTermElim ds ns pair + <*> fromPTermTScope ds ns [r] ret + <*> fromPTermTScope ds ns [x, y] body + + Case pi tag (r, ret) (CaseEnum arms) => + map E $ Base.CaseEnum pi + <$> fromPTermElim ds ns tag + <*> fromPTermTScope ds ns [r] ret + <*> assert_total fromPTermEnumArms ds ns arms + + Enum strs => + let set = SortedSet.fromList strs in + if length strs == length (SortedSet.toList set) then + pure $ Enum set + else + throwError $ DuplicatesInEnum strs + + Tag str => pure $ Tag str + + Eq (i, ty) s t => + Eq <$> fromPTermDScope ds ns [i] ty + <*> fromPTermWith ds ns s + <*> fromPTermWith ds ns t + + DLam i s => + DLam <$> fromPTermDScope ds ns [i] s + + s :% p => + map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p + + V x => + fromName (pure . E . B) (pure . FT) ns x + + s :# a => + map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a + + private + fromPTermEnumArms : FromPTerm m => + Context' BName d -> Context' BName n -> + List (TagVal, PTerm) -> m (CaseEnumArms Three d n) + fromPTermEnumArms ds ns = + map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns) + + private + fromPTermElim : FromPTerm m => + Context' BName d -> Context' BName n -> + PTerm -> m (Elim Three d n) + fromPTermElim ds ns e = + case !(fromPTermWith ds ns e) of + E e => pure e + _ => throwError $ AnnotationNeeded e + + -- [todo] use SN if the var is named but still unused + private + fromPTermTScope : {s : Nat} -> FromPTerm m => + Context' BName d -> Context' BName n -> + Vect s BName -> + PTerm -> m (ScopeTermN s Three d n) + fromPTermTScope ds ns xs t = + if all isNothing xs then + SN <$> fromPTermWith ds ns t + else + SY (map (fromMaybe "_") xs) <$> fromPTermWith ds (extendVect ns xs) t + + private + fromPTermDScope : {s : Nat} -> FromPTerm m => + Context' BName d -> Context' BName n -> + Vect s BName -> + PTerm -> m (DScopeTermN s Three d n) + fromPTermDScope ds ns xs t = + if all isNothing xs then + SN <$> fromPTermWith ds ns t + else + SY (map (fromMaybe "_") xs) <$> fromPTermWith (extendVect ds xs) ns t + + +export %inline +fromPTerm : FromPTerm m => PTerm -> m (Term Three 0 0) +fromPTerm = fromPTermWith [<] [<]