add fromPTerm, etc

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.

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 [<] [<]