Add more program structure to normal forms.

1 files changed, 96 insertions, 89 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 68591ee..b00f5a8 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -29,11 +29,6 @@ data ObsTokenKind
   | OTTrue
   | OTFalse
   | OTIf
-  | OTContainer
-  | OTTag
-  | OTPosition
-  | OTNext
-  | OTSem
   | OTPoint
   | OTVoid
   | OTAbsurd
@@ -43,7 +38,6 @@ data ObsTokenKind
   | OTCastRefl
   -- Special symbols
   | OTUnit
-  | OTTriangle
   -- Grouping symbols
   | OTPOpen
   | OTPClose
@@ -59,7 +53,6 @@ data ObsTokenKind
   | OTTilde
   | OTEqual
   | OTColon
-  | OTPipe
 
 Eq ObsTokenKind where
   OTNewlines == OTNewlines = True
@@ -74,11 +67,6 @@ Eq ObsTokenKind where
   OTTrue == OTTrue = True
   OTFalse == OTFalse = True
   OTIf == OTIf = True
-  OTContainer == OTContainer = True
-  OTTag == OTTag = True
-  OTPosition == OTPosition = True
-  OTNext == OTNext = True
-  OTSem == OTSem = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
@@ -87,7 +75,6 @@ Eq ObsTokenKind where
   OTCast == OTCast = True
   OTCastRefl == OTCastRefl = True
   OTUnit == OTUnit = True
-  OTTriangle == OTTriangle = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
   OTAOpen == OTAOpen = True
@@ -101,9 +88,43 @@ Eq ObsTokenKind where
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
-  OTPipe == OTPipe = True
   _ == _ = False
 
+Show ObsTokenKind where
+  show OTNewlines = "\\n"
+  show OTSpaces = " "
+  show OTIdent = "ident"
+  show OTProp = "Prop"
+  show OTSet = "Set"
+  show OTNat = "nat"
+  show OTFst = "fst"
+  show OTSnd = "snd"
+  show OTBool = "Bool"
+  show OTTrue = "True"
+  show OTFalse = "False"
+  show OTIf = "if"
+  show OTPoint = "tt"
+  show OTVoid = "Void"
+  show OTAbsurd = "absurd"
+  show OTRefl = "refl"
+  show OTTransp = "transp"
+  show OTCast = "cast"
+  show OTCastRefl = "castRefl"
+  show OTUnit = "()"
+  show OTPOpen = "("
+  show OTPClose = ")"
+  show OTAOpen = "<"
+  show OTAClose = ">"
+  show OTBackslash = "\\"
+  show OTSlash = "/"
+  show OTThinArrow = "->"
+  show OTFatArrow = "=>"
+  show OTProduct = "**"
+  show OTComma = ","
+  show OTTilde = "~"
+  show OTEqual = "="
+  show OTColon = ":"
+
 TokenKind ObsTokenKind where
   TokType OTIdent = String
   TokType OTNat   = Nat
@@ -121,11 +142,6 @@ TokenKind ObsTokenKind where
   tokValue OTTrue s = ()
   tokValue OTFalse s = ()
   tokValue OTIf s = ()
-  tokValue OTContainer s = ()
-  tokValue OTTag s = ()
-  tokValue OTPosition s = ()
-  tokValue OTNext s = ()
-  tokValue OTSem s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
@@ -134,7 +150,6 @@ TokenKind ObsTokenKind where
   tokValue OTCast s = ()
   tokValue OTCastRefl s = ()
   tokValue OTUnit s = ()
-  tokValue OTTriangle s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
   tokValue OTAOpen s = ()
@@ -148,7 +163,6 @@ TokenKind ObsTokenKind where
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
-  tokValue OTPipe s = ()
 
 ObsToken : Type
 ObsToken = Token ObsTokenKind
@@ -166,11 +180,6 @@ Show ObsToken where
   show (Tok OTTrue s) = "True"
   show (Tok OTFalse s) = "False"
   show (Tok OTIf s) = "if"
-  show (Tok OTContainer s) = "Container"
-  show (Tok OTTag s) = "tag"
-  show (Tok OTPosition s) = "position"
-  show (Tok OTNext s) = "next"
-  show (Tok OTSem s) = "sem"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
   show (Tok OTAbsurd s) = "absurd"
@@ -179,7 +188,6 @@ Show ObsToken where
   show (Tok OTCast s) = "cast"
   show (Tok OTCastRefl s) = "castRefl"
   show (Tok OTUnit s) = "()"
-  show (Tok OTTriangle s) = "<|"
   show (Tok OTPOpen s) = "("
   show (Tok OTPClose s) = ")"
   show (Tok OTAOpen s) = "<"
@@ -193,7 +201,6 @@ Show ObsToken where
   show (Tok OTTilde s) = "~"
   show (Tok OTEqual s) = "="
   show (Tok OTColon s) = ":"
-  show (Tok OTPipe s) = "|"
 
 identifier : Lexer
 identifier = alpha <+> many alphaNum
@@ -208,11 +215,6 @@ keywords =
   , ("True", OTTrue)
   , ("False", OTFalse)
   , ("if", OTIf)
-  , ("Container", OTContainer)
-  , ("tag", OTTag)
-  , ("position", OTPosition)
-  , ("next", OTNext)
-  , ("sem", OTSem)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
@@ -243,7 +245,6 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++
   , (exact "~", OTTilde)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
-  , (exact "|", OTPipe)
   ]
 
 op : Type -> Type -> Nat -> Type
@@ -264,66 +265,77 @@ termForms =
   , (OTUnit, Top)
   ]
 
-headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)))
+headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n)))
 headForms =
-  [ (OTFst, (0 ** uncurry 1 First))
-  , (OTSnd, (0 ** uncurry 1 Second))
-  , (OTAbsurd, (0 ** uncurry 1 Absurd))
-  , (OTRefl, (0 ** uncurry 1 Refl))
-  , (OTTransp, (4 ** (uncurry 5 Transp)))
-  , (OTCast, (3 ** uncurry 4 Cast))
-  , (OTCastRefl, (0 ** uncurry 1 CastId))
+  [ (OTFst, (0 ** First))
+  , (OTSnd, (0 ** Second))
+  , (OTAbsurd, (0 ** Absurd))
+  , (OTRefl, (0 ** Refl))
+  , (OTTransp, (4 ** Transp))
+  , (OTCast, (3 ** Cast))
+  , (OTCastRefl, (0 ** CastId))
   ]
 
-headLambdaForms : List (ObsTokenKind, (n ** ((WithBounds String, WithBounds Syntax) -> Vect n (WithBounds Syntax) -> Syntax)))
-headLambdaForms =
-  [ (OTIf, (3 ** (uncurry 3 . uncurry If)))
-  ]
+headLambdaForms : List (ObsTokenKind, (n ** (LambdaForm -> op (WithBounds Syntax) Syntax n)))
+headLambdaForms = [(OTIf, (3 ** If))]
 
-declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
-declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)]
+declForms : List (ObsTokenKind, (n ** op DeclForm (WithBounds Syntax -> Syntax) (S n)))
+declForms =
+  [ (OTThinArrow, (0 ** Pi))
+  , (OTProduct, (0 ** Sigma))
+  ]
 
 count : (n : _) -> Grammar state tok True a -> Grammar state tok (isSucc n) (Vect n a)
 count 0     p = pure []
 count (S n) p = [| p :: count n p |]
 
+match' : (tok : ObsTokenKind) -> Grammar state ObsToken True (TokType tok)
+match' tok = do
+  pos <- position
+  token <- peek
+  let True = token.kind == tok
+    | False => failLoc pos "expected \{show tok}"
+  match tok
+
 ident : Grammar state ObsToken True (WithBounds String)
-ident = bounds $ match OTIdent
+ident = bounds $ match' OTIdent
 
 whitespace : Grammar state ObsToken True ()
-whitespace = map (\_ => ()) $ some (optional (match OTNewlines) *> match OTSpaces)
+whitespace = map (\_ => ()) $ some (optional (match' OTNewlines) *> match' OTSpaces)
 
 parens : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True a
-parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* match OTPClose
+parens p = match' OTPOpen *> optional whitespace *> p <* optional whitespace <* match' OTPClose
 
 var : Grammar state ObsToken True (WithBounds Syntax)
 var = map (map Var) ident
 
 noArgUniverse : Grammar state ObsToken True (WithBounds Universe)
 noArgUniverse = bounds $
-  map (const Prop) (match OTProp <* commit) <|>
-  map (const (Set 0)) (match OTSet <* commit)
+  map (const Prop) (match' OTProp <* commit) <|>
+  map (const (Set 0)) (match' OTSet <* commit)
 
 universe : Grammar state ObsToken True (WithBounds Universe)
 universe = bounds $
-  map (const Prop) (match OTProp <* commit) <|>
-  map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
+  map (const Prop) (match' OTProp <* commit) <|>
+  map Set (match' OTSet *> commit *> option 0 (match' OTNat <* commit))
 
-decl : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
-decl p = [| MkPair (ident <* whitespace <* match OTColon <* whitespace) p |]
+decl : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
+  Grammar state ObsToken True DeclForm
+decl p = [| MkDecl (ident <* whitespace <* match' OTColon <* whitespace) p |]
 
 pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a)
 pair p =
-  match OTAOpen *> commit *>
+  match' OTAOpen *> commit *>
   [| MkPair
-      (optional whitespace *> p <* optional whitespace <* match OTComma <* commit)
+      (optional whitespace *> p <* optional whitespace <* match' OTComma <* commit)
       (optional whitespace *> p <* optional whitespace) |]
-  <* match OTAClose <* commit
+  <* match' OTAClose <* commit
 
-lambda : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
+lambda : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
+  Grammar state ObsToken True LambdaForm
 lambda p =
-  match OTBackslash *> commit *>
-  [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
+  match' OTBackslash *> commit *>
+  [| MkLambda (ident <* whitespace <* match' OTFatArrow <* whitespace) p |]
 
 partial
 noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax)
@@ -334,8 +346,6 @@ head : Grammar state ObsToken True (WithBounds Syntax)
 partial
 spine : Grammar state ObsToken True (WithBounds Syntax)
 partial
-container : Grammar state ObsToken True (WithBounds Syntax)
-partial
 equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
 exp : Grammar state ObsToken True (WithBounds Syntax)
@@ -344,7 +354,7 @@ noUniversesTerm =
   parens exp <|>
   var <|>
   bounds (map (uncurry Pair) (pair exp)) <|>
-  bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
+  bounds (choiceMap (\(k, s) => map (const s) (match' k)) termForms)
 
 term = noUniversesTerm <|> map (map Universe) noArgUniverse
 
@@ -353,54 +363,52 @@ head =
   map (map Universe) universe <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *>
-        [| f (whitespace *> parens (lambda exp)) (count n (whitespace *> term))|])
+      (\(hd, (n ** f)) =>
+        match' hd *> commit *> whitespace *>
+        pure (uncurry n . f) <*> parens (lambda exp) <*> count n (whitespace *> term))
       headLambdaForms) <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |])
+      (\(hd, (n ** f)) => match' hd *> commit *>
+        pure (uncurry (S n) f) <*> count (S n) (whitespace *> term))
       headForms)
 
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
   [| MkPair head (many (whitespace *> term)) |]
 
-container = spine
-
 equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $
-  [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |]
+  [| MkPair spine (optional (whitespace *> match' OTTilde *> commit *> whitespace *> spine)) |]
 
 exp =
   equals <|>
-  bounds (map (uncurry Lambda) $ lambda exp) <|>
+  bounds (map Lambda $ lambda exp) <|>
   bounds
-    (map (\((var, a), (b, f)) => f var a b) $
-     [| MkPair
-          (parens (decl exp) <* whitespace)
-          (choiceMap
-            (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |])
-            declForms)
-     |])
+    (choiceMap
+      (\(sep, (n ** f)) =>
+        pure (uncurry (S n) f) <*>
+        count (S n) (parens (decl exp) <* whitespace <* match' sep <* commit <* whitespace) <*>
+        exp)
+      declForms)
 
 partial
 def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
-def = [| MkPair (ident <* whitespace <* match OTEqual <* whitespace) exp |]
+def = [| MkPair (ident <* whitespace <* match' OTEqual <* whitespace) exp |]
 
 partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
-    [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |]
-    (\((name, ty), (name', tm)) =>
+    [| MkPair (decl exp <* commit) (optional whitespace *> match' OTNewlines *> def <* commit) |]
+    (\((MkDecl name ty), (name', tm)) =>
       if name.val == name'.val
         then pure (MkDefinition {name = name, ty, tm})
-        else fatalLoc name.bounds "name mismatch for declaration and definition")
+        else fatalLoc name.bounds "name mismatch' for declaration and definition")
 
 partial
 file : Grammar state ObsToken False (List Definition)
 file =
-  optional (whitespace *> match OTNewlines) *>
-  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit)
-  -- <* eof
+  optional (whitespace *> match' OTNewlines) *>
+  sepEndBy (optional whitespace *> match' OTNewlines) (fullDef <* commit)
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
 whitespaceIrrelevant a = case (a.val.kind) of
@@ -413,7 +421,6 @@ mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
 mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of
   (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest
   (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "()")) (mergeBounds a b) :: mergeToks rest
-  (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest
   _ => a :: mergeToks tail
 mergeToks toks = toks
 
@@ -425,7 +432,7 @@ castErr (Right x) = pure x
 castErr (Left errs) = do
   for_ {b = ()} errs
     (\(Error msg bounds) =>
-      inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg True) bounds)
+      inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg False) bounds)
   abort
 
 partial