From 232857131888607ee3cd2ae4a5ccdc14e0c6f015 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 15:43:29 +0000
Subject: Define conversion from raw to abstract syntax.

---
 src/Obs/Abstract.idr | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/Obs/Main.idr     |  5 ++++-
 2 files changed, 64 insertions(+), 1 deletion(-)
 create mode 100644 src/Obs/Abstract.idr

(limited to 'src/Obs')

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
new file mode 100644
index 0000000..33c2460
--- /dev/null
+++ b/src/Obs/Abstract.idr
@@ -0,0 +1,60 @@
+module Obs.Abstract
+
+import Data.Fin
+import Data.String
+
+import Obs.Syntax
+import Obs.Term
+
+import System
+import Text.Bounded
+
+public export
+Context : Nat -> Type
+Context n = List (String, Fin n)
+
+bind : Context n -> String -> Context (S n)
+bind ctx str = (str, 0) :: map (mapSnd FS) ctx
+
+Error : Type -> Type
+Error = Either (Bounds, String)
+
+report : Bounds -> String -> Error a
+report = curry Left
+
+export
+printErr : Error a -> IO a
+printErr (Left (b, str)) = do
+  () <- putStrLn "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
+  exitFailure
+printErr (Right x) = pure x
+
+export
+abstractSyntax : Context n -> Syntax -> Error (Term n)
+abstractSyntax ctx (Var b str) = do
+  let Just i = lookup str ctx
+    | Nothing => report b "unbound variable: \{str}"
+  pure (Var b i)
+abstractSyntax ctx (Sort b s)  = pure (Sort b s)
+
+export
+abstractDefinition : Context n -> Definition -> Error (Definition n)
+abstractDefinition ctx def = pure $ MkDefinition
+  { name = def.name
+  , bounds = def.bounds
+  , ty = !(abstractSyntax ctx def.ty)
+  , tm = !(abstractSyntax ctx def.tm)
+  }
+
+export
+abstractBlock : (defs : List Definition) -> Error (Block (length defs))
+abstractBlock defs =
+  let asContext : Block n -> Context n
+      asContext []            = []
+      asContext (defs :< def) = bind (asContext defs) def.name
+  in let helper : Block n -> (defs : List Definition) -> Error (Block (length defs + n))
+         helper blk []            = pure blk
+         helper blk (def :: defs) = do
+           def <- abstractDefinition (asContext blk) def
+           (rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
+  in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 0ff1d70..639094f 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -1,7 +1,9 @@
 module Obs.Main
 
+import Obs.Abstract
 import Obs.Parser
 import Obs.Syntax
+import Obs.Term
 
 import System
 
@@ -18,4 +20,5 @@ main = do
   [_, file] <- getArgs
     | _ => usage
   defs <- parseFile file
-  putDoc $ concatWith (\x, y => x <+> hardline <+> hardline <+> y) (map pretty defs)
+  blk <- printErr $ abstractBlock defs
+  putDoc $ pretty blk
-- 
cgit v1.2.3