Added parser for most basic terms

Just variables, binders, applications, and basic declarations (data, type and function definitions)
2024-09-11 16:05:51 +03:00 · 2019-03-10 17:56:08 +00:00 · 2019-03-10 17:56:08 +00:00 · 992d8dd0f9
commit 992d8dd0f9
parent e03a2ba4b5
5 changed files with 390 additions and 4 deletions
--- a/src/Core/Name.idr
+++ b/src/Core/Name.idr
@ -12,9 +12,6 @@ data Name : Type where
     Nested : Name -> Name -> Name -- nested function name
     Resolved : Int -> Name -- resolved, index into context

-export Show Name where
-  show n = "[not done yet]"
-
 export
 userNameRoot : Name -> Maybe String
 userNameRoot (NS _ n) = userNameRoot n
@ -27,6 +24,15 @@ showSep sep [] = ""
 showSep sep [x] = x
 showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

+export Show Name where
+  show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
+  show (UN x) = x
+  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
+  show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
+  show (MV x) = "{meta-" ++ show x ++ "}"
+  show (Nested outer inner) = show outer ++ ":" ++ show inner
+  show (Resolved x) = "$resolved" ++ show x
+
 export
 Eq Name where
    (==) (NS ns n) (NS ns' n') = ns == ns' && n == n'
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@ -91,6 +91,12 @@ Eq Constant where
 public export
 data PiInfo = Implicit | Explicit | AutoImplicit

+export
+Show PiInfo where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+  show AutoImplicit = "AutoImplicit"
+
 public export
 data RigCount = Rig0 | Rig1 | RigW

--- a/src/TTImp/Parser.idr
+++ b/src/TTImp/Parser.idr
@ -0,0 +1,298 @@
+module TTImp.Parser
+
+import Core.TT
+import Parser.Support
+import TTImp.TTImp
+
+topDecl : FileName -> IndentInfo -> Rule ImpDecl
+
+atom : FileName -> Rule RawImp
+atom fname
+    = do start <- location
+         x <- constant
+         end <- location
+         pure (IPrimVal (MkFC fname start end) x)
+  <|> do start <- location
+         keyword "Type"
+         end <- location
+         pure (IType (MkFC fname start end))
+  <|> do start <- location
+         symbol "_"
+         end <- location
+         pure (Implicit (MkFC fname start end))
+  <|> do start <- location
+         x <- name
+         end <- location
+         pure (IVar (MkFC fname start end) x)
+
+visibility : EmptyRule Visibility
+visibility
+    = do keyword "public"
+         keyword "export"
+         pure Public
+  <|> do keyword "export"
+         pure Export
+  <|> do keyword "private"
+         pure Private
+  <|> pure Private
+
+bindSymbol : Rule PiInfo
+bindSymbol
+    = do symbol "->"
+         pure Explicit
+  <|> do symbol "=>"
+         pure AutoImplicit
+
+mutual
+  appExpr : FileName -> IndentInfo -> Rule RawImp
+  appExpr fname indents
+      = do start <- location
+           f <- simpleExpr fname indents
+           args <- many (argExpr fname indents)
+           end <- location
+           pure (applyExpImp start end f args)
+    where
+      applyExpImp : FilePos -> FilePos ->
+                    RawImp -> List (Either RawImp (Maybe Name, RawImp)) ->
+                    RawImp
+      applyExpImp start end f [] = f
+      applyExpImp start end f (Left exp :: args)
+          = applyExpImp start end (IApp (MkFC fname start end) f exp) args
+      applyExpImp start end f (Right (n, imp) :: args) 
+          = applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
+
+  argExpr : FileName -> IndentInfo -> 
+            Rule (Either RawImp (Maybe Name, RawImp))
+  argExpr fname indents
+      = do continue indents
+           arg <- simpleExpr fname indents
+           pure (Left arg)
+    <|> do continue indents
+           arg <- implicitArg fname indents
+           pure (Right arg)
+
+  implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp)
+  implicitArg fname indents
+      = do start <- location
+           symbol "{"
+           x <- unqualifiedName
+           (do symbol "="
+               commit
+               tm <- expr fname indents
+               symbol "}"
+               pure (Just (UN x), tm))
+             <|> (do symbol "}"
+                     end <- location
+                     pure (Just (UN x), IVar (MkFC fname start end) (UN x)))
+    <|> do symbol "@{"
+           commit
+           tm <- expr fname indents
+           symbol "}"
+           pure (Nothing, tm)
+
+  simpleExpr : FileName -> IndentInfo -> Rule RawImp
+  simpleExpr fname indents
+       = atom fname
+     <|> binder fname indents
+     <|> do symbol "("
+            e <- expr fname indents
+            symbol ")"
+            pure e
+
+  multiplicity : EmptyRule (Maybe Integer)
+  multiplicity
+      = do c <- intLit
+           pure (Just c)
+    <|> pure Nothing
+
+  getMult : Maybe Integer -> EmptyRule RigCount
+  getMult (Just 0) = pure Rig0
+  getMult (Just 1) = pure Rig1
+  getMult Nothing = pure RigW
+  getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"
+
+  pibindAll : FC -> PiInfo -> List (RigCount, Maybe Name, RawImp) -> 
+              RawImp -> RawImp
+  pibindAll fc p [] scope = scope
+  pibindAll fc p ((rig, n, ty) :: rest) scope
+           = IPi fc rig p n ty (pibindAll fc p rest scope)
+
+  bindList : FileName -> FilePos -> IndentInfo -> 
+             Rule (List (RigCount, Name, RawImp))
+  bindList fname start indents
+      = sepBy1 (symbol ",")
+               (do rigc <- multiplicity
+                   n <- unqualifiedName
+                   ty <- option 
+                            (Implicit (MkFC fname start start))
+                            (do symbol ":"
+                                appExpr fname indents)
+                   rig <- getMult rigc
+                   pure (rig, UN n, ty))
+
+
+  pibindList : FileName -> FilePos -> IndentInfo -> 
+               Rule (List (RigCount, Maybe Name, RawImp))
+  pibindList fname start indents
+       = do rigc <- multiplicity
+            ns <- sepBy1 (symbol ",") unqualifiedName
+            symbol ":"
+            ty <- expr fname indents
+            atEnd indents
+            rig <- getMult rigc
+            pure (map (\n => (rig, Just (UN n), ty)) ns)
+     <|> sepBy1 (symbol ",")
+                (do rigc <- multiplicity
+                    n <- name
+                    symbol ":"
+                    ty <- expr fname indents
+                    rig <- getMult rigc
+                    pure (rig, Just n, ty))
+      
+  autoImplicitPi : FileName -> IndentInfo -> Rule RawImp
+  autoImplicitPi fname indents
+      = do start <- location
+           symbol "{"
+           keyword "auto"
+           commit
+           binders <- pibindList fname start indents
+           symbol "}"
+           symbol "->"
+           scope <- typeExpr fname indents
+           end <- location
+           pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
+
+  forall_ : FileName -> IndentInfo -> Rule RawImp
+  forall_ fname indents
+      = do start <- location
+           keyword "forall"
+           commit
+           nstart <- location
+           ns <- sepBy1 (symbol ",") unqualifiedName
+           nend <- location
+           let nfc = MkFC fname nstart nend
+           let binders = map (\n => (Rig0, Just (UN n), Implicit nfc)) ns
+           symbol "."
+           scope <- typeExpr fname indents
+           end <- location
+           pure (pibindAll (MkFC fname start end) Implicit binders scope)
+
+  implicitPi : FileName -> IndentInfo -> Rule RawImp
+  implicitPi fname indents
+      = do start <- location
+           symbol "{"
+           binders <- pibindList fname start indents
+           symbol "}"
+           symbol "->"
+           scope <- typeExpr fname indents
+           end <- location
+           pure (pibindAll (MkFC fname start end) Implicit binders scope)
+
+  explicitPi : FileName -> IndentInfo -> Rule RawImp
+  explicitPi fname indents
+      = do start <- location
+           symbol "("
+           binders <- pibindList fname start indents
+           symbol ")"
+           exp <- bindSymbol
+           scope <- typeExpr fname indents
+           end <- location
+           pure (pibindAll (MkFC fname start end) exp binders scope)
+
+  lam : FileName -> IndentInfo -> Rule RawImp
+  lam fname indents
+      = do start <- location
+           symbol "\\"
+           binders <- bindList fname start indents
+           symbol "=>"
+           mustContinue indents Nothing
+           scope <- expr fname indents
+           end <- location
+           pure (bindAll (MkFC fname start end) binders scope)
+     where
+       bindAll : FC -> List (RigCount, Name, RawImp) -> RawImp -> RawImp
+       bindAll fc [] scope = scope
+       bindAll fc ((rig, n, ty) :: rest) scope
+           = ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)
+
+  binder : FileName -> IndentInfo -> Rule RawImp
+  binder fname indents
+      = autoImplicitPi fname indents
+    <|> forall_ fname indents
+    <|> implicitPi fname indents
+    <|> explicitPi fname indents
+    <|> lam fname indents
+
+  typeExpr : FileName -> IndentInfo -> Rule RawImp
+  typeExpr fname indents
+      = do start <- location
+           arg <- appExpr fname indents
+           (do continue indents
+               rest <- some (do exp <- bindSymbol
+                                op <- appExpr fname indents
+                                pure (exp, op))
+               end <- location
+               pure (mkPi start end arg rest))
+             <|> pure arg
+    where
+      mkPi : FilePos -> FilePos -> RawImp -> List (PiInfo, RawImp) -> RawImp
+      mkPi start end arg [] = arg
+      mkPi start end arg ((exp, a) :: as) 
+            = IPi (MkFC fname start end) RigW exp Nothing arg 
+                  (mkPi start end a as)
+
+  export
+  expr : FileName -> IndentInfo -> Rule RawImp
+  expr = typeExpr
+
+tyDecl : FileName -> IndentInfo -> Rule ImpTy
+tyDecl fname indents
+    = do start <- location
+         n <- name
+         symbol ":"
+         ty <- expr fname indents
+         end <- location
+         atEnd indents
+         pure (MkImpTy (MkFC fname start end) n ty)
+
+fnDef : FileName -> IndentInfo -> Rule ImpDecl
+fnDef fname indents
+    = do start <- location
+         n <- name
+         symbol "="
+         ty <- expr fname indents
+         end <- location
+         atEnd indents
+         pure (IDef (MkFC fname start end) n ty)
+
+dataDecl : FileName -> IndentInfo -> Rule ImpData
+dataDecl fname indents
+    = do start <- location
+         keyword "data"
+         n <- name
+         symbol ":"
+         ty <- expr fname indents
+         keyword "where"
+         cs <- block (tyDecl fname)
+         end <- location
+         pure (MkImpData (MkFC fname start end) n ty [] cs)
+
+-- Declared at the top
+-- topDecl : FileName -> IndentInfo -> Rule ImpDecl
+topDecl fname indents
+    = do start <- location
+         vis <- visibility
+         dat <- dataDecl fname indents
+         end <- location
+         pure (IData (MkFC fname start end) vis dat)
+  <|> do start <- location
+         vis <- visibility
+         claim <- tyDecl fname indents
+         end <- location
+         pure (IClaim (MkFC fname start end) RigW vis [] claim)
+  <|> fnDef fname indents
+
+export
+prog : FileName -> Rule (List ImpDecl)
+prog fname
+    = nonEmptyBlock (topDecl fname)
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@ -0,0 +1,73 @@
+module TTImp.TTImp
+
+import Core.TT
+
+mutual
+  public export
+  data RawImp : Type where
+       IVar : FC -> Name -> RawImp
+       IPi : FC -> RigCount -> PiInfo -> Maybe Name ->
+             (argTy : RawImp) -> (retTy : RawImp) -> RawImp
+       ILam : FC -> RigCount -> PiInfo -> Maybe Name ->
+              (argTy : RawImp) -> (lamTy : RawImp) -> RawImp
+       IApp : FC -> RawImp -> RawImp -> RawImp
+       IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
+
+       IPrimVal : FC -> (c : Constant) -> RawImp
+       IType : FC -> RawImp
+       Implicit : FC -> RawImp
+
+  export
+    Show RawImp where
+      show (IVar fc n) = show n
+      show (IPi fc c p n arg ret)
+         = "(%pi " ++ show c ++ " " ++ show p ++
+           " " ++ show n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
+      show (ILam fc c p n arg sc)
+         = "(%lam " ++ show c ++ " " ++ show p ++
+           " " ++ show n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
+      show (IApp fc f a)
+         = "(" ++ show f ++ " " ++ show a ++ ")"
+      show (IImplicitApp fc f n a)
+         = "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
+      show (IPrimVal fc c) = show c
+      show (IType fc) = "%type"
+      show (Implicit fc) = "_"
+
+  public export
+  data FnOpt : Type where
+       Inline : FnOpt
+
+  export
+  Eq FnOpt where
+    (==) Inline Inline = True
+    (==) _ _ = False
+
+  public export
+  data ImpTy : Type where
+       MkImpTy : FC -> (n : Name) -> (ty : RawImp) -> ImpTy
+
+  public export
+  data DataOpt : Type where
+       SearchBy : List Name -> DataOpt -- determining arguments
+       NoHints : DataOpt -- Don't generate search hints for constructors
+
+  export
+  Eq DataOpt where
+    (==) (SearchBy xs) (SearchBy ys) = xs == ys
+    (==) NoHints NoHints = True
+    (==) _ _ = False
+
+  public export
+  data ImpData : Type where
+       MkImpData : FC -> (n : Name) -> (tycon : RawImp) ->
+                   (opts : List DataOpt) -> 
+                   (datacons : List ImpTy) -> ImpData
+       MkImpLater : FC -> (n : Name) -> (tycon : RawImp) -> ImpData
+
+  public export
+  data ImpDecl : Type where
+       IClaim : FC -> RigCount -> Visibility -> List FnOpt ->
+                ImpTy -> ImpDecl
+       IData : FC -> Visibility -> ImpData -> ImpDecl
+       IDef : FC -> Name -> RawImp -> ImpDecl
--- a/yaffle.ipkg
+++ b/yaffle.ipkg
@ -24,7 +24,10 @@ modules =
    Text.Parser,
    Text.Parser.Core,
    Text.Quantity,
-    Text.Token
+    Text.Token,
+
+    TTImp.Parser,
+    TTImp.TTImp

 sourcedir = src
 -- executable = ttimp