Fix implicit/explicit printing, various other issues

README.md

@@ -1,19 +1,17 @@
 
 Parser is in place. 
-
+Ditched well-scoped for now.
-Currently trying to make TT well-scoped, considering well-named..
-
-Need to update todos below.
-Should I use well-scoped indices or well-scoped names...
 
 Parser:
 - [x] import statement
 - [x] def
 - [x] simple decl
-- [ ] type definition
+- [ ] fix / test parsing and pretty printing
+- [ ] inductive types
 - [x] read files
-
+- [ ] figure out context representation - Global context?
 - [ ] type checking / elab
+- [ ] process a file
 - [ ] 
 - [ ] 
 - [ ] 

src/Lib/Check.idr

@@ -8,22 +8,13 @@ import Data.String
 import Lib.TT
 import Syntax
 
-record Context (n : Nat) (f : Nat)  where
-  -- review this
-  env : Env f n -- Vect n (Val f)
-  types : List (String, Val f)
-  pos : SourcePos
 
 
-extend : Context n f -> Val f -> Context (S n) f
-extend ctx ty = { env := ty :: ctx.env } ctx
-
 -- cribbed this, it avoids MonadError String m => everywhere
 parameters {0 m : Type -> Type} {auto _ : MonadError String m}
 
-  infer : {f : Nat} -> Context n f -> Raw -> m (Tm n, Val f)
+  infer : {f : Nat} -> Context -> Raw -> m (Tm, Val)
-  -- I think I'm hand-waving n here, probably need it in Context
+  check : {f : Nat} -> Context -> Raw -> Val -> m Tm
-  check : {f : Nat} -> Context n f -> Raw -> Val f -> m (Tm n)
 
   check ctx (RLam _ _ _) ty = ?ch_rhs
   check ctx tm ty = do
@@ -35,10 +26,10 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
 
   infer ctx (RVar nm) = go 0 ctx.types
     where
-      go : Nat -> List (String, Val f) -> m (Tm n, Val f)
+      go : Nat -> List (String, Val) -> m (Tm, Val)
       go i [] = throwError "\{show nm} not in scope"
       -- REVIEW Local or Bnd (ezoo does not have both)
-      go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd ?i_not_fin, ty) 
+      go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty) 
         else go (i + 1) xs
 
       

src/Lib/Prettier.idr

@@ -3,7 +3,8 @@ module Lib.Prettier
 import Data.String
 import Data.Nat
 
--- A prettier printer, Wadler
+-- A prettier printer, Philip Wadler
+-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
 
 ||| `Doc` is a pretty printing document.  Constructors are private, use
 ||| methods below.  `Alt` in particular has some invariants on it, see paper

src/Lib/TT.idr

@@ -1,3 +1,4 @@
+-- I'm not sure this is related, or just a note to self (Presheaves on Porpoise)
 -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
 -- or drop the indices for now.
 
@@ -133,24 +134,23 @@ nf env t = quote n (eval [] env t)
 public export
 conv : (lvl : Nat) -> Val -> Val -> Bool
 
-data BD = Bound | Defined
+-- data BD = Bound | Defined
+
+-- public export
+-- Types : Type
+-- Types = List (Name, Lazy Val)
 
-public export
-Types : Type
-Types = List (Name, Lazy Val)
 
--- REVIEW indices
 public export
 record Context where
   constructor MkCtx
-  env : Env
+  env : Env                  -- Values in scope
-  types : List (String, Val)
+  types : List (String, Val) -- types and names in scope
-  pos : SourcePos
+  -- bds  : List BD          -- bind or define
-
+  -- lvl = length types
--- data Env : (tm : SnocList Name -> Type) -> SnocList Name -> Type where
+  pos : SourcePos            -- the last SourcePos that we saw
 
 -- Kovacs Small-TT has locals and globals, lets do that.  
--- Still need to sort out the indices - one or two on env?
 
 ||| add a binding to environment
 extend : { n : Nat} -> Context -> String -> Val -> Context
@@ -164,7 +164,7 @@ extend (MkCtx env types pos) name ty =
 -- Is it ok to leaving them in there (if they pass checkType) as long as
 -- we don't register the def if it fails checking?
 
--- shoot, I have another of these in Check.idr
+-- shoot, I have another context in Check.idr
 
 
 -- -- public export

src/Main.idr

@@ -14,11 +14,27 @@ import Control.App
 import Syntax
 import Lib.Prettier
 
+{-
+
+Ok, dropped indexes.
+
+- The "sample" file I wrote looks like nonsense to test the parser. I'll need something that typechecks to get this going.
+- I want end to end before adding implicits, so something explicit.
+- maybe some #check / #eval pragmas?
+
+But checking that claims and functions are correct is a very good start.  Maybe spent too much time on making a full parser
+rather than piecing together end to end. (And way too much time on those indices.)
+
+
+
+ -}
+
+
 -- [ ] Put stuff in attic
 -- [ ] Error printing
 -- [ ] Review surface syntax
 -- [x] Prettier printer
--- [ ] First pass at typecheck
+-- [ ] First pass at typecheck (test cases are just parsing)
 -- Just do it in zoo order
 
 

src/Syntax.idr

@@ -145,8 +145,8 @@ Pretty Raw where
   pretty = asDoc 0
     where
     wrap : Icit -> Doc -> Doc
-    wrap Implicit x = x
+    wrap Explicit x = x
-    wrap Explicit x = text "{" ++ x ++ text "}"
+    wrap Implicit x = text "{" ++ x ++ text "}"
 
     par : Nat -> Nat -> Doc -> Doc
     par p p' d = if p' < p then text "(" ++ d ++ text ")" else d
@@ -158,10 +158,10 @@ Pretty Raw where
     asDoc p (RApp x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y
     asDoc p (RApp x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
     asDoc p RU = text "U"
-    asDoc p (RPi Nothing Implicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
+    asDoc p (RPi Nothing Explicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi (Just x) Implicit ty scope) = 
+    asDoc p (RPi (Just x) Explicit ty scope) = 
       par p 1 $ text "(" <+> text x <+> text ":" <+> asDoc p ty <+> text ")" <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi nm Explicit ty scope) =
+    asDoc p (RPi nm Implicit ty scope) =
       par p 1 $ text "{" <+> text (fromMaybe "_" nm) <+> text ":" <+> asDoc p ty <+> text "}" <+> text "->" <+/> asDoc 1 scope
     asDoc p (RLet x v ty scope) = 
       par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty 
@@ -170,8 +170,10 @@ Pretty Raw where
     asDoc p (RSrcPos x y) = asDoc p y
     -- does this exist?
     asDoc p (RAnn x y) = text "TODO - RAnn"
-    asDoc p (RLit x) = text (show x)
+    asDoc p (RLit (LString str)) = text $ interpolate str
-    asDoc p (RCase x xs) = text "TODO - RCase" --?asDoc p_rhs_9
+    asDoc p (RLit (LInt i)) = text $ show i
+    asDoc p (RLit (LBool x)) = text $ show x
+    asDoc p (RCase x xs) = text "TODO - RCase"
     asDoc p RHole = text "_"
     asDoc p (RParseError str) = text "PraseError \{str}"
     
@@ -184,4 +186,5 @@ Pretty Module where
         doDecl (TypeSig nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
         doDecl (Def nm tm) = text nm <+> text "=" <+> nest 2 (pretty tm)
         doDecl (DImport nm) = text "import" <+> text nm ++ line
-        doDecl (Data str x xs) = text "TODO data"
+        -- the behavior of nest is kinda weird, I have to do the nest before/around the </>. 
+        doDecl (Data nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))