From 9148852eb506918bce3e396528e6064207cfb80a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 21 Oct 2024 22:46:26 -0700 Subject: [PATCH] character lits, initial work on literal case trees --- TODO.md | 5 + newt-vscode/syntaxes/newt.tmLanguage.json | 14 +++ src/Lib/Compile.idr | 25 +++- src/Lib/CompileExp.idr | 4 +- src/Lib/Elab.idr | 145 +++++++++++++++++----- src/Lib/Eval.idr | 1 + src/Lib/Parser.idr | 10 +- src/Lib/Prettier.idr | 6 +- src/Lib/Syntax.idr | 24 ++-- src/Lib/Token.idr | 3 + src/Lib/Tokenizer.idr | 3 +- src/Lib/Types.idr | 31 +++-- 12 files changed, 209 insertions(+), 62 deletions(-) diff --git a/TODO.md b/TODO.md index bca2a21..b19665a 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,11 @@ ## TODO +- [ ] Default cases (currently gets expanded to all constructors) +- [ ] Case for primitives +- [ ] aoc2023 translation + - some "real world" examples +- [ ] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet - [ ] unsolved meta errors repeat (need to freeze or only report at end) - [x] Sanitize JS idents, e.g. `_+_` - [ ] Generate some programs that do stuff diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index d0716e0..bf159a3 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -17,6 +17,20 @@ { "name": "keyword.newt", "match": "\\b(data|where|case|of|let|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + }, + { + "name": "string.js", + "begin": ":=\\s*\"", + "end": "\"", + "patterns": [ + { "include": "source.js" } + ] + }, + { + "name": "string.newt", + "begin": "\"", + "end": "\"" } + ] } diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index aa11776..4fd45c2 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -11,10 +11,12 @@ import Data.Nat data Kind = Plain | Return | Assign String data JSStmt : Kind -> Type +data JSExp : Type data JAlt : Type where JConAlt : String -> JSStmt e -> JAlt JDefAlt : JSStmt e -> JAlt + JLitAlt : JSExp -> JSStmt e -> JAlt data JSExp : Type where LitArray : List JSExp -> JSExp @@ -49,6 +51,11 @@ Cont e = JSExp -> JSStmt e JSEnv : Type JSEnv = List JSExp +litToJS : Literal -> JSExp +litToJS (LString str) = LitString str +litToJS (LChar c) = LitString $ cast c +litToJS (LInt i) = LitInt i + -- Stuff nm.h1, nm.h2, ... into environment mkEnv : String -> Nat -> List JSExp -> List String -> List JSExp mkEnv nm k env [] = env @@ -89,6 +96,7 @@ termToJS env (CFun nms t) f = termToJS env (CRef nm) f = f $ Var nm termToJS env (CMeta k) f = f $ LitString "META \{show k}" termToJS env (CLit (LString str)) f = f (LitString str) +termToJS env (CLit (LChar c)) f = f (LitString $ cast c) termToJS env (CLit (LInt i)) f = f (LitInt i) -- if it's a var, just use the original termToJS env (CLet nm (CBnd k) u) f = case getAt k env of @@ -125,11 +133,12 @@ termToJS env (CCase t alts) f = termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) -- intentionally reusing scrutinee name here termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (Var nm :: env) u f) + termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS (Var nm :: env) u f) maybeCaseStmt : List JSExp -> String -> List CAlt -> JSStmt e -- If there is a single alt, assume it matched maybeCaseStmt env nm [(CConAlt _ args u)] = (termToJS (mkEnv nm 0 env args) u f) - maybeCaseStmt env nm alts = + maybeCaseStmt env nm alts = (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) @@ -185,18 +194,21 @@ expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ jsIdent nm caseBody : JSStmt e -> Doc caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt) -caseBody stmt = "{" nest 2 (line ++ stmtToDoc stmt text "break;") "}" +-- caseBody {e = Return} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt) +caseBody {e} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt text "break;") +caseBody stmt = line ++ "{" ++ nest 2 (line ++ stmtToDoc stmt text "break;") "}" altToDoc : JAlt -> Doc altToDoc (JConAlt nm stmt) = text "case" <+> jsString nm ++ ":" ++ caseBody stmt altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt +altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ ":" ++ caseBody stmt stmtToDoc (JSnoc x y) = stmtToDoc x stmtToDoc y stmtToDoc (JPlain x) = expToDoc x ++ ";" -- I might not need these split yet. stmtToDoc (JLet nm body) = "let" <+> jsIdent nm ++ ";" stmtToDoc body stmtToDoc (JAssign nm expr) = jsIdent nm <+> "=" <+> expToDoc expr ++ ";" -stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> "=" <+/> expToDoc x ++ ";" +stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 ("=" <+/> expToDoc x ++ ";") stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";" stmtToDoc (JError str) = text "throw new Error(" ++ jsString str ++ ");" stmtToDoc (JCase sc alts) = @@ -220,9 +232,10 @@ entryToDoc (MkEntry name ty (Fn tm)) = do -- and we might need betas? It seems like a mirror of what happens in CExp debug "compileFun \{pprint [] tm}" ct <- compileFun tm - -- now show for ct... - let body = stmtToDoc $ termToJS [] ct JPlain - pure (text "const" <+> jsIdent name <+> text "=" <+/> body) + -- If ct has zero arity and is a compount expression, this fails.. + let body@(JPlain {}) = termToJS [] ct JPlain + | js => error (getFC tm) "Not a plain expression: \{render 80 $ stmtToDoc js}" + pure (text "const" <+> jsIdent name <+> text "=" <+/> stmtToDoc body) entryToDoc (MkEntry name type Axiom) = pure "" entryToDoc (MkEntry name type (TCon strs)) = pure $ dcon name (piArity type) entryToDoc (MkEntry name type (DCon arity str)) = pure $ dcon name arity diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 6fcf075..651a4e1 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -20,6 +20,7 @@ data CAlt : Type where -- REVIEW keep var name? CDefAlt : CExp -> CAlt -- literal + CLitAlt : Literal -> CExp -> CAlt data CExp : Type where CBnd : Nat -> CExp @@ -110,7 +111,8 @@ compileTerm (Case _ t alts) = do t' <- compileTerm t alts' <- traverse (\case CaseDefault tm => pure $ CDefAlt !(compileTerm tm) - CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm)) alts + CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm) + CaseLit lit tm => pure $ CLitAlt lit !(compileTerm tm)) alts pure $ CCase t' alts' compileTerm (Lit _ lit) = pure $ CLit lit compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index ec38e5b..c035734 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -321,6 +321,9 @@ data Bind = MkBind String Icit Val Show Bind where show (MkBind str icit x) = "\{str} \{show icit}" + +---------------- Case builder + public export record Problem where constructor MkProb @@ -356,7 +359,8 @@ 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 (_ :: xs) = findSplit xs +findSplit (x@(nm, PatLit _ val) :: xs) = Just x +findSplit (x :: xs) = findSplit xs -- *************** @@ -550,20 +554,22 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do else (nm, pat) :: makeConst xs pats makeConst ((MkBind nm Explicit x) :: xs) (pat :: pats) = (nm, pat) :: makeConst xs pats - rewriteCons : List Bind -> List Constraint -> List Constraint -> Maybe (List Constraint) - rewriteCons vars [] acc = Just acc - rewriteCons vars (c@(nm, y) :: xs) acc = + -- replace constraint with constraints on parameters, or nothing if non-matching clause + rewriteConstraint : List Bind -> List Constraint -> List Constraint -> Maybe (List Constraint) + rewriteConstraint vars [] acc = Just acc + rewriteConstraint vars (c@(nm, y) :: xs) acc = if nm == scnm then case y of PatVar _ _ s => Just $ c :: (xs ++ acc) PatWild _ _ => Just $ c :: (xs ++ acc) + PatLit fc lit => Nothing -- error fc "Literal \{show lit} in constructor split" PatCon _ _ str ys => if str == dcName then Just $ (makeConst vars ys) ++ xs ++ acc else Nothing - else rewriteCons vars xs (c :: acc) + else rewriteConstraint vars xs (c :: acc) rewriteClause : List Bind -> Clause -> Maybe Clause - rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteCons vars cons []) pats expr + rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteConstraint vars cons []) pats expr splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit)) @@ -583,8 +589,9 @@ mkPat top (tm, icit) = do [] => pure $ PatVar fc icit nm _ => error (getFC tm) "patvar applied to args" ((RImplicit fc), []) => pure $ PatWild fc icit - ((RImplicit fc), _) => error fc "implicit pat can't be applied" - -- ((RLit x y), b) => ?rhs_19 + ((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" @@ -624,7 +631,74 @@ checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty = checkDone ({ types $= ren then (nm', ty) :: xs else (name, ty) :: rename xs -checkDone ctx ((x, pat) :: xs) body ty = error emptyFC "stray constraint \{x} /? \{show pat}" +checkDone ctx ((x, pat) :: xs) body ty = error (getFC pat) "stray constraint \{x} /? \{show pat}" + +-- need to run constructors, then run default + +-- wild/var can come before 'x' so we need a list first +getLits : String -> List Clause -> List Literal +getLits nm [] = [] +getLits nm ((MkClause fc cons pats expr) :: cs) = case find ((nm==) . fst) cons of + Just (_, (PatLit _ lit)) => lit :: getLits nm cs + _ => getLits nm cs + + +-- then build a lit case for each of those + +buildLitCase : Context -> Problem -> FC -> String -> Val -> Literal -> M CaseAlt +buildLitCase ctx prob fc scnm scty lit = do + + -- Constrain the scrutinee's variable to be lit value + let Just ix = findIndex ((==scnm) . fst) ctx.types + | Nothing => error ctx.fc "\{scnm} not is scope?" + let lvl = ((length ctx.env) `minus` (cast ix)) `minus` 1 + let scon : (Nat, Val) = (lvl, VLit fc lit) + ctx' <- updateContext ctx [scon] + let clauses = mapMaybe rewriteClause prob.clauses + + when (length clauses == 0) $ error ctx.fc "Missing case for \{show lit} splitting \{scnm}" + tm <- buildTree ctx' (MkProb clauses prob.ty) + pure $ CaseLit lit tm + + where + -- replace constraint with constraints on parameters, or nothing if non-matching clause + rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint) + rewriteConstraint [] acc = Just acc + rewriteConstraint (c@(nm, y) :: xs) acc = + if nm == scnm + then case y of + 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 + else rewriteConstraint xs (c :: acc) + + rewriteClause : Clause -> Maybe Clause + rewriteClause (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteConstraint cons []) pats expr + + + +buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt) +buildLitCases ctx prob fc scnm scty = do + let lits = getLits scnm prob.clauses + alts <- traverse (buildLitCase ctx prob fc scnm scty) lits + -- TODO build default case + -- run getLits + -- buildLitCase for each + + let defclauses = filter isDefault prob.clauses + when (length defclauses == 0) $ error fc "no default for literal slot on \{show scnm}" + tm <- buildTree ctx (MkProb defclauses prob.ty) + + pure $ alts ++ [ CaseDefault tm ] + where + isDefault : Clause -> Bool + isDefault cl = case find ((==scnm) . fst) cl.cons of + Just (_, (PatVar _ _ _)) => True + Just (_, (PatWild _ _)) => True + Nothing => True + _ => False + -- This process is similar to extendPi, but we need to stop -- if one clause is short on patterns. @@ -643,26 +717,38 @@ buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = -- need to find some name we can split in (x :: xs) -- so LHS of constraint is name (or VVar - if we do Val) -- then run the split +-- some of this is copied into check buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do debug "buildTree \{show constraints} \{show expr}" let Just (scnm, pat) := findSplit constraints - | _ => checkDone ctx constraints expr ty + | _ => do + debug "checkDone \{show constraints}" + checkDone ctx constraints expr ty debug "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}" let Just (sctm, scty) := lookupName ctx scnm | _ => error fc "Internal Error: can't find \{scnm} in environment" - -- expand vars that may be solved - scty' <- unlet ctx scty - debug "EXP \{show scty} -> \{show scty'}" - cons <- getConstructors ctx (getFC pat) scty' - debug "CONS \{show $ map fst cons}" - 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) - + case pat of + PatCon _ _ _ _ => do + -- expand vars that may be solved + scty' <- unlet ctx scty + debug "EXP \{show scty} -> \{show scty'}" + -- this is per the paper, but it would be nice to coalesce + -- default cases + cons <- getConstructors ctx (getFC pat) scty' + debug "CONS \{show $ map fst cons}" + 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 + -- need to run through all of the PatLits in this slot and then find a fallback + -- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't + alts <- buildLitCases ctx prob fc scnm scty + pure $ Case fc sctm alts + pat => error (getFC pat) "Internal error - tried to split on \{show pat}" showDef : Context -> List String -> Nat -> Val -> M String showDef ctx names n v@(VVar _ n' [<]) = if n == n' then pure "" else pure "= \{pprint names !(quote ctx.lvl v)}" @@ -670,8 +756,6 @@ showDef ctx names n v = pure "= \{pprint names !(quote ctx.lvl v)}" check ctx tm ty = case (tm, !(forceType ty)) of (RCase fc rsc alts, ty) => do - -- We've got a beta redex or need to do something... - -- Maybe we can let the scrutinee and jump into the middle? (sc, scty) <- infer ctx rsc scty <- forceMeta scty debug "SCTM \{pprint (names ctx) sc}" @@ -679,16 +763,10 @@ check ctx tm ty = case (tm, !(forceType ty)) of let scnm = fresh "sc" top <- get - -- FIXME FC - clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause fc [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts - - -- buildCase expects scrutinee to be a name in the context because - -- it's compared against the first part of Constraint. We could switch - -- to a level and only let if the scrutinee is not a var. + clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause (getFC pat) [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts + -- buildCase expects scrutinee to be a name in the context, so we need to let it. let ctx' = extend ctx scnm scty - cons <- getConstructors ctx' fc scty - alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons - pure $ Let fc scnm sc $ Case fc (Bnd fc 0) (catMaybes alts) + pure $ Let fc scnm sc !(buildTree ctx' $ MkProb clauses ty) -- Document a hole, pretend it's implemented (RHole fc, ty) => do @@ -697,8 +775,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" let msg = unlines (toList $ reverse env) ++ " -----------\n" ++ " goal \{pprint names ty'}" - putStrLn "INFO at \{show fc}: " - putStrLn msg + info fc "\n\{msg}" -- let context = unlines foo -- need to print 'warning' with position -- fixme - just put a name on it like idris and stuff it into top. diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 59d0528..ca000a3 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -212,6 +212,7 @@ zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt zonkAlt top l env (CaseDefault t) = CaseDefault <$> zonkBind top l env t +zonkAlt top l env (CaseLit lit t) = CaseLit lit <$> zonkBind top l env t zonkAlt top l env (CaseCons name args t) = CaseCons name args <$> go l env args t where go : Nat -> Env -> List String -> Tm -> M Tm diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 75a54ec..17903e3 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -1,7 +1,7 @@ module Lib.Parser import Lib.Types import Debug.Trace - +import Data.String -- app: foo {a} a b -- lam: λ {A} {b : A} (c : Blah) d e f => something @@ -50,8 +50,14 @@ intLit = do pure $ RLit fc (LInt (cast t)) +charLit : Parser Raw +charLit = do + fc <- getPos + v <- token Character + pure $ RLit fc (LChar $ assert_total $ strIndex v 1) + lit : Parser Raw -lit = intLit <|> stringLit +lit = intLit <|> stringLit <|> charLit -- typeExpr is term with arrows. export typeExpr : Parser Raw diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index 65cac2f..b0dc33a 100644 --- a/src/Lib/Prettier.idr +++ b/src/Lib/Prettier.idr @@ -55,8 +55,8 @@ be fit acc w k [] = Just (acc <>> []) be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs) be fit acc w k ((i, (Text s)) :: xs) = - if not fit || (k + length s < w) - then (be fit (acc :< TEXT s) w (k + length s) xs) + if not fit || (k + length s < w) + then (be fit (acc :< TEXT s) w (k + length s) xs) else Nothing be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i+j,x)::xs) be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs) @@ -124,7 +124,7 @@ export bracket : String -> Doc -> String -> Doc bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r) -infixl 5 <+/> +export infixl 5 <+/> ||| Either space or newline export diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index fd95280..e4c640e 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -18,13 +18,14 @@ data Pattern | PatCon FC Icit Name (List Pattern) | PatWild FC Icit -- Not handling this yet, but we need to be able to work with numbers and strings... - -- | PatLit Literal + | PatLit FC Literal export getIcit : Pattern -> Icit getIcit (PatVar x icit str) = icit getIcit (PatCon x icit str xs) = icit getIcit (PatWild x icit) = icit +getIcit (PatLit fc lit) = Explicit export @@ -32,6 +33,7 @@ HasFC Pattern where getFC (PatVar fc _ _) = fc getFC (PatCon fc _ _ _) = fc getFC (PatWild fc _) = fc + getFC (PatLit fc lit) = fc -- %runElab deriveShow `{Pattern} public export @@ -117,9 +119,10 @@ record Module where foo : List String -> String foo ts = "(" ++ unwords ts ++ ")" -Show Literal where - show (LString str) = foo [ "LString", show str] - show (LInt i) = foo [ "LInt", show i] +-- Show Literal where +-- show (LString str) = foo [ "LString", show str] +-- show (LInt i) = foo [ "LInt", show i] +-- show (LChar c) = foo [ "LChar", show c] export covering @@ -160,6 +163,7 @@ 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 (PatWild _ icit) = foo ["PatWild", show icit] + show (PatLit _ lit) = foo ["PatLit", show lit] covering Show RCaseAlt where @@ -180,12 +184,19 @@ Show Raw where show (RParseError _ str) = foo [ "ParseError", "str"] show (RU _) = "U" +export +Pretty Literal where + pretty (LString str) = text $ interpolate str + pretty (LInt i) = text $ show i + pretty (LChar c) = text $ show c + 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 (PatWild _icit)= "_" + pretty (PatWild _icit) = "_" + pretty (PatLit _ lit) = pretty lit @@ -218,8 +229,7 @@ Pretty Raw where <+/> text "in" <+> asDoc p scope -- does this exist? asDoc p (RAnn _ x y) = text "TODO - RAnn" - asDoc p (RLit _ (LString str)) = text $ interpolate str - asDoc p (RLit _ (LInt i)) = text $ show i + asDoc p (RLit _ lit) = pretty lit asDoc p (RCase _ x xs) = text "TODO - RCase" asDoc p (RImplicit _) = text "_" asDoc p (RHole _) = text "?" diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr index 853f7b6..a7056e6 100644 --- a/src/Lib/Token.idr +++ b/src/Lib/Token.idr @@ -12,6 +12,7 @@ data Kind | Oper | MixFix | Number + | Character | StringKind | Symbol | Space @@ -31,6 +32,7 @@ Show Kind where show Oper = "Oper" show MixFix = "MixFix" show Number = "Number" + show Character = "Character" show Symbol = "Symbol" show Space = "Space" show LBrace = "LBrace" @@ -48,6 +50,7 @@ Eq Kind where Oper == Oper = True MixFix == MixFix = True Number == Number = True + Character == Character = True Symbol == Symbol = True Space == Space = True LBrace == LBrace = True diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 47a6204..5cfb744 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -27,7 +27,7 @@ opChar : Lexer opChar = pred isOpChar identMore : Lexer -identMore = alphaNum <|> exact "." <|> exact "'" +identMore = alphaNum <|> exact "." <|> exact "'" <|> exact "_" quo : Recognise True quo = is '"' @@ -53,6 +53,7 @@ rawTokens <|> match (upper <+> many identMore) checkUKW <|> match (some digit) (Tok Number) <|> match (is '#' <+> many alpha) (Tok Pragma) + <|> match charLit (Tok Character) <|> match (exact "_" <+> (some opChar <|> exact ",") <+> exact "_") (Tok MixFix) <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote) <|> match (lineComment (exact "--")) (Tok Space) diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 6efb300..bb95290 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -54,25 +54,38 @@ data PrimType = StringType | IntType data PrimVal : Type where PrimString : String -> PrimVal PrimInt : Int -> PrimVal + PrimChar : Char -> PrimVal public export data Tm : Type +public export +data Literal = LString String | LInt Int | LChar Char + +%name Literal lit + +public export +Show Literal where + show (LString str) = show str + show (LInt i) = show i + show (LChar c) = show c + public export data CaseAlt : Type where CaseDefault : Tm -> CaseAlt -- I've also seen a list of stuff that gets replaced CaseCons : (name : String) -> (args : List String) -> Tm -> CaseAlt - -- CaseLit : Literal -> Tm -> CaseAlt + CaseLit : Literal -> Tm -> CaseAlt data Def : Type -public export -data Literal = LString String | LInt Int -Show Literal where - show (LString str) = show str - show (LInt i) = show i +public export +Eq Literal where + LString x == LString y = x == y + LInt x == LInt y = x == y + LChar x == LChar y = x == y + _ == _ = False data Tm : Type where Bnd : FC -> Nat -> Tm @@ -113,6 +126,7 @@ public export covering Show CaseAlt where show (CaseDefault tm) = "_ => \{show tm}" show (CaseCons nm args tm) = "\{nm} \{unwords args} => \{show tm}" + show (CaseLit lit tm) = "\{show lit} => \{show tm}" public export covering Show Tm where @@ -159,7 +173,8 @@ pprint names tm = render 80 $ go names tm goAlt : List String -> CaseAlt -> Doc goAlt names (CaseDefault t) = "_" <+> "=>" <+> go ("_" :: names) t - goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+> go (args ++ names) t + goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (args ++ names) t + goAlt names (CaseLit lit t) = text (show lit) <+> "=>" <+/> go names t go names (Bnd _ k) = case getAt k names of Nothing => text "BND:\{show k}" @@ -175,7 +190,7 @@ pprint names tm = render 80 $ go names tm text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "->" <+> go (nm :: names) u <+> ")" -- FIXME - probably way wrong on the names here. There is implicit binding going on go names (Case _ sc alts) = text "case" <+> go names sc <+> text "of" (nest 2 (line ++ stack (map (goAlt names) alts))) - go names (Lit _ lit) = text "\{show lit}" + go names (Lit _ lit) = text (show lit) go names (Let _ nm t u) = text "let" <+> text nm <+> ":=" <+> go names t (nest 2 $ go names u) -- public export