At patterns on LHS

2024-12-14 19:58:52 -08:00
parent 00a8678bd4
commit d22f3844f6
7 changed files with 63 additions and 30 deletions
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -15,7 +15,6 @@ import Lib.Eval
 import Lib.TopContext
 import Lib.Syntax

-
 ||| collectDecl collects multiple Def for one function into one
 export
 collectDecl : List Decl -> List Decl
@@ -453,7 +452,7 @@ introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't m
 findSplit : List Constraint -> Maybe Constraint
 findSplit [] = Nothing
    -- FIXME look up type, ensure it's a constructor
-findSplit (x@(nm, PatCon _ _ cnm pats) :: xs) = Just x
+findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x
 findSplit (x@(nm, PatLit _ val) :: xs) = Just x
 findSplit (x :: xs) = findSplit xs

@@ -580,7 +579,6 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
  let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}"

  case lookupDef ctx scnm of
-    -- NOW this is S var7
    Just val@(VRef fc nm y sp) =>
      if nm /= dcName
      then do
@@ -693,13 +691,15 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
        then case y of
          PatVar _ _ s => pure $ Just $ c :: (xs ++ acc)
          PatWild _ _ => pure $ Just $ c :: (xs ++ acc)
-          -- FIXME why don't we hit this ('x' for Just x)
+          -- FIXME why don't we hit this (when user puts 'x' for Just 'x')
          PatLit fc lit => error fc "Literal \{show lit} in constructor split"
-          -- FIXME check type
-          PatCon fc _ nm ys => if nm == dcName
-            then pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc
-            -- TODO can we check this when we make the PatCon?
+          PatCon fc icit nm ys as => if nm == dcName
+            then case as of
+              Nothing => pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc
+              -- putting this in constraints causes it to be renamed scnm -> nm' when we check body.
+              Just nm' => pure $ Just $ (scnm, (PatVar fc icit nm')) :: !(makeConstr vars ys) ++ xs ++ acc
            else do
+              -- TODO can we check this when we make the PatCon?
              case lookup nm !get of
                  (Just (MkEntry _ name type (DCon k tcname))) =>
                    if (tcname /= sctynm)
@@ -721,12 +721,17 @@ splitArgs tm args = (tm, args)


 mkPat : TopContext -> (Raw, Icit) -> M Pattern
+mkPat top (RAs fc as tm, icit) =
+  case !(mkPat top (tm, icit)) of
+    (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
+    (PatCon fc icit nm args Nothing) => error fc "Double as pattern \{show tm}"
+    t => error fc "Can't put as on non-constructor \{show tm}"
 mkPat top (tm, icit) = do
  case splitArgs tm [] of
    ((RVar fc nm), b) => case lookup nm top of
                (Just (MkEntry _ name type (DCon k str))) =>
                  -- TODO check arity, also figure out why we need reverse
-                  pure $ PatCon fc icit nm !(traverse (mkPat top) b)
+                  pure $ PatCon fc icit nm !(traverse (mkPat top) b) Nothing
                -- This fires when a global is shadowed by a pattern var
                -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
                _ => case b of
@@ -736,7 +741,7 @@ mkPat top (tm, icit) = do
    ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments"
    ((RLit fc lit), []) => pure $ PatLit fc lit
    ((RLit fc y), b) => error fc "lit cannot be applied to arguments"
-    (a,b) => error (getFC a) "expected pat var or constructor"
+    (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}"


 export
@@ -853,6 +858,7 @@ buildLitCase ctx prob fc scnm scty lit = do
  pure $ CaseLit lit tm

  where
+    -- FIXME - thread in M for errors
    -- replace constraint with constraints on parameters, or nothing if non-matching clause
    rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint)
    rewriteConstraint [] acc = Just acc
@@ -862,7 +868,7 @@ buildLitCase ctx prob fc scnm scty lit = do
          PatVar _ _ s => Just $ c :: (xs ++ acc)
          PatWild _ _ => Just $ c :: (xs ++ acc)
          PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing
-          PatCon _ _ str ys => Nothing -- error matching lit against constructor
+          PatCon _ _ str ys as => Nothing -- error matching lit against constructor
        else rewriteConstraint xs (c :: acc)

    rewriteClause : Clause -> Maybe Clause
@@ -896,6 +902,13 @@ litTyName (LString str) = "String"
 litTyName (LInt i) = "Int"
 litTyName (LChar c) = "Char"

+renameContext : String -> String -> Context -> Context
+renameContext from to ctx = { types $= go } ctx
+  where
+    go : Vect n (String,Val) -> Vect n (String,Val)
+    go Nil = Nil
+    go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types
+
 -- This process is similar to extendPi, but we need to stop
 -- if one clause is short on patterns.
 buildTree ctx (MkProb [] ty) = error emptyFC "no clauses"
@@ -928,9 +941,8 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
  -- REVIEW We probably need to know this is a VRef before we decide to split on this slot..
  scty' <- unlet ctx.env scty >>= forceType ctx.env
  case pat of
-    PatCon _ _ _ _ => do
+    PatCon fc _ _ _ as => do
      -- expand vars that may be solved, eval top level functions
-
      debug "EXP \{show scty} -> \{show scty'}"
      -- this is per the paper, but it would be nice to coalesce
      -- default cases
@@ -939,7 +951,6 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
      alts <- traverse (buildCase ctx prob scnm scty') cons
      debug "GOTALTS \{show alts}"
      when (length (catMaybes alts) == 0) $ error (fc) "no alts for \{show scty'}"
-      -- TODO check for empty somewhere?
      pure $ Case fc sctm (catMaybes alts)
    PatLit fc v => do
      let tyname = litTyName v
@@ -1140,5 +1151,5 @@ infer ctx (RImplicit fc) = do
 infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String"))
 infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc "Int"))
 infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), !(primType fc "Char"))
-
+infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns"
 infer ctx tm = error (getFC tm) "Implement infer \{show tm}"
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -74,10 +74,20 @@ export term : (Parser Raw)
 withPos : Parser a -> Parser (FC, a)
 withPos pa = (,) <$> getPos <*> pa

+asAtom : Parser Raw
+asAtom = do
+  fc <- getPos
+  nm <- ident
+  asPat <- optional $ keyword "@" *> parens typeExpr
+  case asPat of
+    Just exp => pure $ RAs fc nm exp
+    Nothing  => pure $ RVar fc nm
+
 -- the inside of Raw
 atom : Parser Raw
 atom = RU <$> getPos <* keyword "U"
-    <|> RVar <$> getPos <*> ident
+    -- <|> RVar <$> getPos <*> ident
+    <|> asAtom
    <|> RVar <$> getPos <*> uident
    <|> lit
    <|> RImplicit <$> getPos <* keyword "_"
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -12,7 +12,7 @@ data Raw : Type where
 public export
 data Pattern
  = PatVar FC Icit Name
-  | PatCon FC Icit Name (List Pattern)
+  | PatCon FC Icit Name (List Pattern) (Maybe Name)
  | PatWild FC Icit
  -- Not handling this yet, but we need to be able to work with numbers and strings...
  | PatLit FC Literal
@@ -20,7 +20,7 @@ data Pattern
 export
 getIcit : Pattern -> Icit
 getIcit (PatVar x icit str) = icit
-getIcit (PatCon x icit str xs) = icit
+getIcit (PatCon x icit str xs as) = icit
 getIcit (PatWild x icit) = icit
 getIcit (PatLit fc lit) = Explicit

@@ -28,7 +28,7 @@ getIcit (PatLit fc lit) = Explicit
 export
 HasFC Pattern where
  getFC (PatVar fc _ _) = fc
-  getFC (PatCon fc _ _ _) = fc
+  getFC (PatCon fc _ _ _ _) = fc
  getFC (PatWild fc _) = fc
  getFC (PatLit fc lit) = fc

@@ -78,6 +78,7 @@ data Raw : Type where
  RDo : (fc : FC) -> List DoStmt -> Raw
  RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw
  RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw
+  RAs : (fc : FC) -> Name -> Raw -> Raw

 %name Raw tm

@@ -98,6 +99,7 @@ HasFC Raw where
  getFC (RDo fc stmts) = fc
  getFC (RIf fc _ _ _) = fc
  getFC (RWhere fc _ _) = fc
+  getFC (RAs fc _ _) = fc


 -- derive some stuff - I'd like json, eq, show, ...
@@ -187,7 +189,7 @@ Show Module where
 export
 Show Pattern where
  show (PatVar _ icit str) = foo ["PatVar", show icit, show str]
-  show (PatCon _ icit str xs) = foo ["PatCon", show icit, show str, assert_total $ show xs]
+  show (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, assert_total $ show xs, show as]
  show (PatWild _ icit) = foo ["PatWild", show icit]
  show (PatLit _ lit) = foo ["PatLit", show lit]

@@ -214,6 +216,7 @@ Show Raw where
  show (RU _) = "U"
  show (RIf _ x y z) = foo [ "If", show x, show y, show z]
  show (RWhere _ _ _) = foo [ "Where", "FIXME"]
+  show (RAs _ nm x) = foo [ "RAs", nm, show x]

 export
 Pretty Literal where
@@ -225,12 +228,11 @@ export
 Pretty Pattern where
  -- FIXME - wrap Implicit with {}
  pretty (PatVar _ icit nm) = text nm
-  pretty (PatCon _ icit nm args) = text nm <+> spread (map pretty args)
+  pretty (PatCon _ icit nm args Nothing) = text nm <+> spread (map pretty args)
+  pretty (PatCon _ icit nm args (Just as)) = text as ++ "@(" ++ text nm <+> spread (map pretty args) ++ ")"
  pretty (PatWild _icit) = "_"
  pretty (PatLit _ lit) = pretty lit

-
-
 export
 Pretty Raw where
  pretty = asDoc 0
@@ -269,6 +271,7 @@ Pretty Raw where
    asDoc p (RDo _ stmts) = text "TODO - RDo"
    asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> "then" <+> asDoc 0 y <+/> "else" <+> asDoc 0 z
    asDoc p (RWhere _ dd b) = text "TODO pretty where"
+    asDoc p (RAs _ nm x) = text nm ++ "@(" ++ asDoc 0 x ++ ")"

 export
 Pretty Decl where
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -11,7 +11,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
            "∀", "forall",
            "class", "instance",
            "if", "then", "else",
-            "$", "λ", "?",
+            "$", "λ", "?", "@",
             "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]

 checkKW : String -> Token Kind
@@ -27,7 +27,7 @@ identMore : Lexer
 identMore = alphaNum <|> exact "'" <|> exact "_"

 singleton : Lexer
-singleton = oneOf "()\\{}[],."
+singleton = oneOf "()\\{}[],.@"

 quo : Recognise True
 quo = is '"'
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -449,6 +449,14 @@ record Context where
  -- FC to use if we don't have a better option
  fc : FC

+setName : Context -> Nat -> String -> Context
+setName ctx ix name = case natToFin ix ctx.lvl of
+  Just ix' => { types $= updateAt ix' go  } ctx
+  Nothing => ctx
+  where
+    go : (String,Val) -> (String, Val)
+    go (a,b) = (name,b)
+
 %name Context ctx

 ||| add a binding to environment