diff --git a/Main.lean b/Main.lean index 3da305a..2cd9ce2 100644 --- a/Main.lean +++ b/Main.lean @@ -2,32 +2,57 @@ import Mlang open Mlang -unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) := do +def refineJudgmentFromValue (value : Value) (judgment : Judgment) : Judgment := + match value with + | .data term => + let refinedTy := refineKnownDataTy (dataType term) + match judgment.ty with + | .data + | .dataInt + | .dataBool + | .dataString + | .dataNull + | .dataArray _ + | .dataRecord _ => + { judgment with ty := refinedTy } + | _ => judgment + | _ => judgment + +def renderResult (value : Value) (judgment : Judgment) : String := + s!"{renderValue value} : {renderJudgment (refineJudgmentFromValue value judgment)}" + +unsafe def checkExprsWith (tyEnv : TyEnv) (env : Env) (exprs : List Expr) : IO (Except String (List (Value × Judgment))) := do + let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do + match pending with + | [] => pure (.ok acc.reverse) + | expr :: rest => + match inferType tyEnv expr with + | .error err => + pure (.error s!"type error: {reprStr err}") + | .ok judgment => + match (← (eval env expr).toIO') with + | .ok value => + loop rest ((value, judgment) :: acc) + | .error err => + pure (.error s!"runtime error: {reprStr err}") + loop exprs [] + +unsafe def checkAndEvalWith (tyEnv : TyEnv) (env : Env) (source : String) : IO (Except String (List (Value × Judgment))) := do match parseProgram source with | .error err => pure (.error s!"parse error: {reprStr err}") | .ok exprs => do - let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do - match pending with - | [] => pure (.ok acc.reverse) - | expr :: rest => - match inferType [] expr with - | .error err => - pure (.error s!"type error: {reprStr err}") - | .ok judgment => - match (← (eval [] expr).toIO') with - | .ok value => - loop rest ((value, judgment) :: acc) - | .error err => - pure (.error s!"runtime error: {reprStr err}") - loop exprs [] + checkExprsWith tyEnv env exprs + +unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) := + checkAndEvalWith [] [] source unsafe def runFile (path : String) : IO UInt32 := do let source ← IO.FS.readFile path match (← checkAndEval source) with | .ok results => for (value, judgment) in results do - IO.println s!"{renderValue value} : {renderJudgment judgment}" + IO.println (renderResult value judgment) pure 0 | .error msg => IO.eprintln s!"{path}: {msg}" @@ -37,28 +62,48 @@ unsafe def runEval (source : String) : IO UInt32 := do match (← checkAndEval source) with | .ok results => for (value, judgment) in results do - IO.println s!"{renderValue value} : {renderJudgment judgment}" + IO.println (renderResult value judgment) pure 0 | .error msg => IO.eprintln msg pure 1 -unsafe def repl : IO UInt32 := do +unsafe def repl (tyEnv : TyEnv := []) (env : Env := []) : IO UInt32 := do let stdin ← IO.getStdin let line ← stdin.getLine let input := (String.trimAscii line).toString if input.isEmpty then - repl + repl tyEnv env else if input = ":quit" || input = ":q" then pure 0 else do - match (← checkAndEval input) with - | .ok results => - for (value, judgment) in results do - IO.println s!"{renderValue value} : {renderJudgment judgment}" - | .error msg => - IO.eprintln msg - repl + match parseReplCommand input with + | .error err => + IO.eprintln s!"parse error: {reprStr err}" + repl tyEnv env + | .ok command => + match command with + | .bind name value => + match inferType tyEnv value with + | .error err => + IO.eprintln s!"type error: {reprStr err}" + repl tyEnv env + | .ok judgment => + match (← (eval env value).toIO') with + | .error err => + IO.eprintln s!"runtime error: {reprStr err}" + repl tyEnv env + | .ok boundValue => + IO.println (renderResult boundValue judgment) + repl ((name, judgment.ty) :: tyEnv) ((name, boundValue) :: env) + | .evalProgram exprs => + match (← checkExprsWith tyEnv env exprs) with + | .ok results => + for (value, judgment) in results do + IO.println (renderResult value judgment) + | .error msg => + IO.eprintln msg + repl tyEnv env def printUsage : IO Unit := do IO.println "usage:" diff --git a/Mlang/Interpreter.lean b/Mlang/Interpreter.lean index 2e3ccb8..b634b56 100644 --- a/Mlang/Interpreter.lean +++ b/Mlang/Interpreter.lean @@ -65,7 +65,10 @@ inductive Expr where | int : Int → Expr | bool : Bool → Expr | string : String → Expr + | null : Expr | var : Name → Expr + | arrayE : List Expr → Expr + | recordE : List (String × Expr) → Expr | add : Expr → Expr → Expr | sub : Expr → Expr → Expr | mul : Expr → Expr → Expr @@ -92,6 +95,7 @@ inductive Value where | builtinHttpGet : Value | builtinReadFileNickel : Value | builtinParseNickel : Value + | builtinParseJson : Value | builtinDataGet : Value | builtinDataGetField : Data → Value | builtinDataAt : Value @@ -99,6 +103,8 @@ inductive Value where | builtinDataAsInt : Value | builtinDataAsString : Value | builtinDataAsBool : Value + | builtinDataToJson : Value + | builtinDataToNickel : Value | closure : Name → Expr → List (Name × Value) → Value deriving Repr, Inhabited @@ -134,6 +140,13 @@ def expectData : Value → EvalM Data | .data term => pure term | _ => throw (.typeError "expected a data value") +def valueToData : Value → EvalM Data + | .data term => pure term + | .int n => pure (.int n) + | .bool b => pure (.bool b) + | .string s => pure (.string s) + | _ => throw (.typeError "data literals only support Int, Bool, String, and Data values") + partial def dataType : Data → Ty | .null => .dataNull | .bool _ => .dataBool @@ -160,6 +173,17 @@ def liftScalarDataTy : Ty → Ty | .dataString => .string | ty => ty +partial def refineKnownDataTy (ty : Ty) : Ty := + match ty with + | .dataInt => .int + | .dataBool => .bool + | .dataString => .string + | .dataNull => .data + | .dataArray itemTy => .dataArray (refineKnownDataTy itemTy) + | .dataRecord fields => + .dataRecord (fields.map (fun (name, fieldTy) => (name, refineKnownDataTy fieldTy))) + | other => other + def dataArrayGet? : List Data → Nat → Option Data | [], _ => none | x :: _, 0 => some x @@ -194,17 +218,66 @@ def encodeMapResult : Except RuntimeError Value → Value | .ok value => .resultOk value | .error err => .resultErr (runtimeErrorToMessage err) +def escapeJsonChar : Char → String + | '"' => "\\\"" + | '\\' => "\\\\" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | c => c.toString + +def renderJsonString (s : String) : String := + "\"" ++ String.join (s.toList.map escapeJsonChar) ++ "\"" + +def isNickelKeyStart (c : Char) : Bool := + c.isAlpha || c = '_' + +def isNickelKeyContinue (c : Char) : Bool := + c.isAlpha || c.isDigit || c = '_' || c = '-' + +def renderNickelKey (s : String) : String := + match s.toList with + | [] => renderJsonString s + | c :: cs => + if isNickelKeyStart c && cs.all isNickelKeyContinue then + s + else + renderJsonString s + +partial def renderNickelData : Data → String + | .null => "null" + | .bool b => toString b + | .int n => toString n + | .string s => renderJsonString s + | .array xs => "[" ++ String.intercalate ", " (xs.map renderNickelData) ++ "]" + | .record fields => + let rendered := fields.map (fun (k, v) => s!"{renderNickelKey k} = {renderNickelData v}") + "{ " ++ String.intercalate ", " rendered ++ " }" + +partial def renderJsonData : Data → String + | .null => "null" + | .bool b => if b then "true" else "false" + | .int n => toString n + | .string s => renderJsonString s + | .array xs => "[" ++ String.intercalate ", " (xs.map renderJsonData) ++ "]" + | .record fields => + let rendered := fields.map (fun (k, v) => s!"{renderJsonString k}: {renderJsonData v}") + "{" ++ String.intercalate ", " rendered ++ "}" + def builtinType? (name : Name) : Option Ty := match name with | "readFile" => some (.funTy .string [.error, .io] .string) | "httpGet" => some (.funTy .string [.error, .io] .string) | "readFileNickel" => some (.funTy .string [.error, .io] .data) | "parseNickel" => some (.funTy .string [.error] .data) + | "parseJson" => some (.funTy .string [.error] .data) | "get" => some (.funTy .data [] (.funTy .string [.error] .data)) | "at" => some (.funTy .data [] (.funTy .int [.error] .data)) | "asInt" => some (.funTy .data [.error] .int) | "asString" => some (.funTy .data [.error] .string) | "asBool" => some (.funTy .data [.error] .bool) + | "toJson" => some (.funTy .data [] .string) + | "toNickel" => some (.funTy .data [] .string) | _ => none def builtinValue? (name : Name) : Option Value := @@ -213,11 +286,14 @@ def builtinValue? (name : Name) : Option Value := | "httpGet" => some .builtinHttpGet | "readFileNickel" => some .builtinReadFileNickel | "parseNickel" => some .builtinParseNickel + | "parseJson" => some .builtinParseJson | "get" => some .builtinDataGet | "at" => some .builtinDataAt | "asInt" => some .builtinDataAsInt | "asString" => some .builtinDataAsString | "asBool" => some .builtinDataAsBool + | "toJson" => some .builtinDataToJson + | "toNickel" => some .builtinDataToNickel | _ => none mutual @@ -241,6 +317,10 @@ mutual let source ← expectString argVal let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalString source) pure (.data (← parseRenderedData rendered)) + | .builtinParseJson => do + let source ← expectString argVal + let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalJsonString source) + pure (.data (← parseRenderedData rendered)) | .builtinDataGet => do let term ← expectData argVal pure (.builtinDataGetField term) @@ -281,6 +361,12 @@ mutual match term with | .bool b => pure (.bool b) | _ => throw (.typeError "asBool expects a boolean") + | .builtinDataToJson => do + let term ← expectData argVal + pure (.string (renderJsonData term)) + | .builtinDataToNickel => do + let term ← expectData argVal + pure (.string (renderNickelData term)) | _ => match fnVal, argVal with | .data (.record fields), .string key => @@ -305,6 +391,7 @@ mutual | .int n => pure (.int n) | .bool b => pure (.bool b) | .string s => pure (.string s) + | .null => pure (.data .null) | .var name => match env.lookup name with | some v => pure v @@ -312,6 +399,14 @@ mutual match builtinValue? name with | some v => pure v | none => throw (.unboundVariable name) + | .arrayE items => do + let values ← items.mapM (eval env) + pure (.data (.array (← values.mapM valueToData))) + | .recordE fields => do + let fields' ← fields.mapM (fun (name, value) => do + let value' ← eval env value + pure (name, (← valueToData value'))) + pure (.data (.record fields')) | .add lhs rhs => do let l ← expectInt (← eval env lhs) let r ← expectInt (← eval env rhs) @@ -367,15 +462,7 @@ mutual applyValue fnVal argVal end -partial def renderData : Data → String - | .null => "null" - | .bool b => toString b - | .int n => toString n - | .string s => s!"\"{s}\"" - | .array xs => "[" ++ String.intercalate ", " (xs.map renderData) ++ "]" - | .record fields => - let rendered := fields.map (fun (k, v) => s!"{k} = {renderData v}") - "{ " ++ String.intercalate ", " rendered ++ " }" +def renderData : Data → String := renderNickelData def renderValue : Value → String | .int n => toString n @@ -390,6 +477,7 @@ def renderValue : Value → String | .builtinHttpGet => "" | .builtinReadFileNickel => "" | .builtinParseNickel => "" + | .builtinParseJson => "" | .builtinDataGet => "" | .builtinDataGetField _ => "" | .builtinDataAt => "" @@ -397,6 +485,8 @@ def renderValue : Value → String | .builtinDataAsInt => "" | .builtinDataAsString => "" | .builtinDataAsBool => "" + | .builtinDataToJson => "" + | .builtinDataToNickel => "" | .closure _ _ _ => "" abbrev TyEnv := List (Name × Ty) @@ -451,10 +541,17 @@ partial def constString? : Expr → Option String | _ => none unsafe def evalConstData? (env : List (Name × Data)) : Expr → Option Data + | .null => some .null | .string s => some (.string s) | .int n => some (.int n) | .bool b => some (.bool b) | .var name => env.lookup name + | .arrayE items => do + some (.array (← items.mapM (evalConstData? env))) + | .recordE fields => do + some (.record (← fields.mapM (fun (name, value) => do + let value' ← evalConstData? env value + pure (name, value')))) | .letE name value body => do let value' ← evalConstData? env value evalConstData? ((name, value') :: env) body @@ -476,6 +573,25 @@ unsafe def evalConstData? (env : List (Name × Data)) : Expr → Option Data | .error _ => none | .error _ => none | _ => none + | .var "parseJson" => + let source ← evalConstData? env arg + match source with + | .string s => + match unsafeIO (NickelHost.evalJsonString s) with + | .ok rendered => + match Nickel.parse rendered with + | .ok term => some (Data.ofNickel term) + | .error _ => none + | .error _ => none + | _ => none + | .var "httpGet" => + let url ← evalConstData? env arg + match url with + | .string s => + match unsafeIO (Http.httpGet s) with + | .ok body => some (.string body) + | .error _ => none + | _ => none | .var "readFileNickel" => let path ← evalConstData? env arg match path with @@ -510,6 +626,7 @@ unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment | .int _ => pure (pureJudgment .int) | .bool _ => pure (pureJudgment .bool) | .string _ => pure (pureJudgment .string) + | .null => pure (pureJudgment .dataNull) | .var name => match env.lookup name with | some ty => pure (pureJudgment ty) @@ -517,6 +634,49 @@ unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment match builtinType? name with | some ty => pure (pureJudgment ty) | none => throw (.unboundVariable name) + | .arrayE items => do + let itemJs ← items.mapM (inferType env) + let dataTys ← itemJs.mapM (fun j => + match j.ty with + | .int => pure .dataInt + | .bool => pure .dataBool + | .string => pure .dataString + | .data => pure .data + | .dataInt => pure .dataInt + | .dataBool => pure .dataBool + | .dataString => pure .dataString + | .dataNull => pure .dataNull + | .dataArray ty => pure (.dataArray ty) + | .dataRecord fields => pure (.dataRecord fields) + | ty => throw (.mismatch .data ty)) + let itemTy := + match dataTys with + | [] => .data + | first :: rest => if rest.all (· == first) then first else .data + pure { + ty := .dataArray itemTy + effects := itemJs.foldl (fun acc j => acc.union j.effects) [] + } + | .recordE fields => do + let fieldJs ← fields.mapM (fun (name, value) => do pure (name, ← inferType env value)) + let fieldTys ← fieldJs.mapM (fun (name, j) => do + let ty ← match j.ty with + | .int => pure .dataInt + | .bool => pure .dataBool + | .string => pure .dataString + | .data => pure .data + | .dataInt => pure .dataInt + | .dataBool => pure .dataBool + | .dataString => pure .dataString + | .dataNull => pure .dataNull + | .dataArray ty => pure (.dataArray ty) + | .dataRecord fields => pure (.dataRecord fields) + | ty => throw (.mismatch .data ty) + pure (name, ty, j.effects)) + pure { + ty := .dataRecord (fieldTys.map (fun (name, ty, _) => (name, ty))) + effects := fieldTys.foldl (fun acc (_, _, effects) => acc.union effects) [] + } | .add lhs rhs | .sub lhs rhs | .mul lhs rhs => do @@ -617,11 +777,15 @@ unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment | .error _ => .data | .var "parseNickel", _, .data => match evalConstData? [] (.app fn arg) with - | some data => dataType data + | some data => refineKnownDataTy (dataType data) + | none => .data + | .var "parseJson", _, .data => + match evalConstData? [] (.app fn arg) with + | some data => refineKnownDataTy (dataType data) | none => .data | .var "readFileNickel", _, .data => match evalConstData? [] (.app fn arg) with - | some data => dataType data + | some data => refineKnownDataTy (dataType data) | none => .data | .var "asInt", _, .int => match argJ.ty with diff --git a/Mlang/NickelHost.lean b/Mlang/NickelHost.lean index 9369efd..6a1d534 100644 --- a/Mlang/NickelHost.lean +++ b/Mlang/NickelHost.lean @@ -2,5 +2,6 @@ namespace Mlang.NickelHost @[extern "mlang_nickel_eval_string"] opaque evalString (source : @& String) : IO String @[extern "mlang_nickel_eval_file_string"] opaque evalFile (path : @& String) : IO String +@[extern "mlang_json_eval_string"] opaque evalJsonString (source : @& String) : IO String end Mlang.NickelHost diff --git a/Mlang/Parser.lean b/Mlang/Parser.lean index 07362d2..f3e2664 100644 --- a/Mlang/Parser.lean +++ b/Mlang/Parser.lean @@ -9,6 +9,10 @@ inductive Token where | ident : String → Token | lparen : Token | rparen : Token + | lbracket : Token + | rbracket : Token + | lbrace : Token + | rbrace : Token | semicolon : Token | comma : Token | colon : Token @@ -28,6 +32,7 @@ inductive Token where | kwTry : Token | kwWith : Token | kwPmap : Token + | kwNull : Token deriving Repr, BEq, Inhabited inductive ParseError where @@ -49,7 +54,7 @@ def isIdentContinue (c : Char) : Bool := isIdentStart c || isDigit c def isAtomStart : Token → Bool - | .int _ | .bool _ | .string _ | .ident _ | .lparen => true + | .int _ | .bool _ | .string _ | .ident _ | .lparen | .lbracket | .lbrace | .kwNull => true | _ => false partial def spanChars (p : Char → Bool) : List Char → List Char × List Char @@ -78,6 +83,7 @@ def lexIdent (chars : List Char) : Token × List Char := | "try" => .kwTry | "with" => .kwWith | "pmap" => .kwPmap + | "null" => .kwNull | "true" => .bool true | "false" => .bool false | _ => .ident name @@ -127,6 +133,10 @@ partial def lexChars : List Char → ParseM (List Token) pure (tok :: toks) | '(', _ => do pure (.lparen :: (← lexChars cs)) | ')', _ => do pure (.rparen :: (← lexChars cs)) + | '[', _ => do pure (.lbracket :: (← lexChars cs)) + | ']', _ => do pure (.rbracket :: (← lexChars cs)) + | '{', _ => do pure (.lbrace :: (← lexChars cs)) + | '}', _ => do pure (.rbrace :: (← lexChars cs)) | ';', _ => do pure (.semicolon :: (← lexChars cs)) | ',', _ => do pure (.comma :: (← lexChars cs)) | ':', _ => do pure (.colon :: (← lexChars cs)) @@ -144,6 +154,11 @@ def lex (input : String) : ParseM (List Token) := abbrev ParserState := List Token +inductive ReplCommand where + | bind : Name → Expr → ReplCommand + | evalProgram : List Expr → ReplCommand + deriving Repr, Inhabited + def expectToken (expected : Token) : ParserState → ParseM ParserState | tok :: rest => if tok == expected then @@ -292,11 +307,52 @@ mutual pure (fn, tokens) | [] => pure (fn, []) + partial def parseArrayItems (items : List Expr) : ParserState → ParseM (Expr × ParserState) + | .rbracket :: rest => pure (.arrayE items.reverse, rest) + | .comma :: rest => do + let (item, rest) ← parseExpr rest + parseArrayItems (item :: items) rest + | tok :: _ => throw (.unexpectedToken s!"expected ',' or ']', got {reprStr tok}") + | [] => throw (.unexpectedEof "unterminated array") + + partial def parseArray : ParserState → ParseM (Expr × ParserState) + | .rbracket :: rest => pure (.arrayE [], rest) + | tokens => do + let (first, rest) ← parseExpr tokens + parseArrayItems [first] rest + + partial def parseFieldKey : ParserState → ParseM (String × ParserState) + | .ident name :: rest => pure (name, rest) + | .string name :: rest => pure (name, rest) + | tok :: _ => throw (.unexpectedToken s!"expected field key, got {reprStr tok}") + | [] => throw (.unexpectedEof "expected field key") + + partial def parseRecordFields (fields : List (String × Expr)) : ParserState → ParseM (Expr × ParserState) + | .rbrace :: rest => pure (.recordE fields.reverse, rest) + | .comma :: rest => do + let (name, rest) ← parseFieldKey rest + let rest ← expectToken .eq rest + let (value, rest) ← parseExpr rest + parseRecordFields ((name, value) :: fields) rest + | tok :: _ => throw (.unexpectedToken s!"expected ',' or '}}', got {reprStr tok}") + | [] => throw (.unexpectedEof "unterminated record") + + partial def parseRecord : ParserState → ParseM (Expr × ParserState) + | .rbrace :: rest => pure (.recordE [], rest) + | tokens => do + let (name, rest) ← parseFieldKey tokens + let rest ← expectToken .eq rest + let (value, rest) ← parseExpr rest + parseRecordFields [(name, value)] rest + partial def parseAtom : ParserState → ParseM (Expr × ParserState) | .int n :: rest => pure (.int n, rest) | .bool b :: rest => pure (.bool b, rest) | .string s :: rest => pure (.string s, rest) + | .kwNull :: rest => pure (.null, rest) | .ident name :: rest => pure (.var name, rest) + | .lbracket :: rest => parseArray rest + | .lbrace :: rest => parseRecord rest | .lparen :: rest => do let (expr, rest) ← parseExpr rest let rest ← expectToken .rparen rest @@ -321,6 +377,19 @@ def parseProgram (input : String) : ParseM (List Expr) := do let tokens ← lex input parseProgramTokens tokens +def parseReplCommand (input : String) : ParseM ReplCommand := do + let tokens ← lex input + match tokens with + | .kwLet :: .ident name :: .eq :: rest => + match parseExpr rest with + | .ok (value, []) => pure (.bind name value) + | _ => + let program ← parseProgramTokens tokens + pure (.evalProgram program) + | _ => + let program ← parseProgramTokens tokens + pure (.evalProgram program) + def parse (input : String) : ParseM Expr := do let program ← parseProgram input match program with diff --git a/README.md b/README.md index 21fefe7..9ed67df 100644 --- a/README.md +++ b/README.md @@ -64,6 +64,9 @@ expr ::= let name = expr in expr | expr - expr | expr * expr | expr expr + | [expr, ...] + | { key = expr, ... } + | null | (expr) | true | false | 123 | "text" | name @@ -72,15 +75,31 @@ program ::= expr (';' expr)* type ::= Int | Bool | String | Data | List | Result | Error | type -> type | (type) ``` +Inside the REPL, there is also a top-level binding form: + +```text +repl ::= let name = expr +``` + +Bare REPL bindings persist across later entries, so you can write: + +```mlang +let x = 42 +x + 1 +``` + Expressions are checked as `Type ! Effects`. Pure expressions get `{}`; division carries `{Error}` implicitly. `readFile` is a builtin with type `String -> String ! {IO, Error}`. `readFileNickel` is a builtin with type `String -> Data ! {IO, Error}`. `parseNickel` is a builtin with type `String -> Data ! {Error}` and is backed by the real Nickel Rust crate. Nickel source is evaluated on the host side and converted back into `mlang` `Data`. Parsed data inspection is available through: - `httpGet : String -> String ! {IO, Error}` +- `parseJson : String -> Data ! {Error}` - `get : Data -> String -> Data ! {Error}` - `at : Data -> Int -> Data ! {Error}` - `asInt : Data -> Int ! {Error}` - `asString : Data -> String ! {Error}` - `asBool : Data -> Bool ! {Error}` +- `toJson : Data -> String` +- `toNickel : Data -> String` `httpGet` is implemented through a thin Rust host library plus a small C shim for Lean FFI. The Rust layer uses a real HTTP client crate rather than spawning an external tool. `try ... with name => ...` handles `Error`, binds the caught error as an `Error` value, and removes `Error` from the resulting effect set when recovered locally. @@ -95,6 +114,14 @@ The host-side Nickel bridge currently maps evaluated Nickel values back into `ml Non-integer numeric Nickel values are not supported yet by `mlang`'s `Data` model. +Native `Data` literals are also supported directly in `mlang`: + +```mlang +{ answer = 42, flags = [true, false], note = "ok", empty = null } +``` + +Fields and array elements may be `Int`, `Bool`, `String`, or existing `Data` expressions. + `pmap name in expr => body` expects `expr` to evaluate to a native `Data` array. It evaluates `body` concurrently for each element bound to `name`, preserves input order, and returns a native `List` of native `Result` values instead of failing the whole traversal. There is also a thread-first form that desugars statically to nested application: @@ -110,7 +137,7 @@ pmap x in parseNickel "[{ answer = 1 }, { missing = 2 }, { answer = 3 }]" => get x "answer" ``` -Files and REPL entries may contain multiple expressions separated by `;`. Each expression is parsed, typechecked, evaluated, and printed in order. `devenv shell -- run` now launches a Rust `rustyline` frontend for the REPL, while the Lean binary still handles evaluation. Use `:quit` to exit the REPL. +Files and REPL entries may contain multiple expressions separated by `;`. Each expression is parsed, typechecked, evaluated, and printed in order. REPL-specific bare `let` bindings persist across later entries. `devenv shell -- run` now launches a Rust `rustyline` frontend for the REPL, while the Lean binary still handles evaluation. Use `:quit` to exit the REPL. The checked-in sample program is [examples/samples.mlg](/home/nandi/code/mlang/examples/samples.mlg:1), which now contains the old demo coverage as semicolon-separated expressions, including file IO, Nickel parsing, threading, `pmap`, local error handling, and an HTTP fetch. It reads from [examples/sample.ncl](/home/nandi/code/mlang/examples/sample.ncl:1). @@ -118,7 +145,6 @@ A separate HTTP example is [examples/http.mlg](/home/nandi/code/mlang/examples/h ## Next steps -- persist top-level bindings across REPL entries - add recursive functions - add algebraic data types and pattern matching - compile to a bytecode VM or another backend diff --git a/examples/samples.mlg b/examples/samples.mlg index 0495710..7e96aa9 100644 --- a/examples/samples.mlg +++ b/examples/samples.mlg @@ -5,7 +5,15 @@ if 6 * 7 = 42 then 1 else 0; readFile "examples/sample.ncl"; readFileNickel "examples/sample.ncl"; parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"; +parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"; +{ answer = 42, flags = [true, false], note = "ok", empty = null }; +toJson (parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"); +toJson (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"); +toJson { answer = 42, flags = [true, false], note = "ok", empty = null }; +toNickel (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"odd key\":null}"); get (parseNickel "{ answer = 42, flags = [true, false] }") "answer"; +get (parseJson "{\"answer\":42,\"flags\":[true,false]}") "answer"; +get { answer = 42, flags = [true, false] } "answer"; at (get (parseNickel "{ flags = [true, false] }") "flags") 1; -> "examples/sample.ncl" readFileNickel (get "answer"); -> "{ flags = [true, false] }" parseNickel (get "flags") (at 1); diff --git a/native/mlang_http/src/lib.rs b/native/mlang_http/src/lib.rs index 07bdcca..5a5d837 100644 --- a/native/mlang_http/src/lib.rs +++ b/native/mlang_http/src/lib.rs @@ -68,6 +68,12 @@ fn nickel_file_to_data_string(path: &str) -> Result { render_json_value(&value) } +fn json_to_data_string(source: &str) -> Result { + let value: serde_json::Value = + serde_json::from_str(source).map_err(|err| format!("{err}"))?; + render_json_value(&value) +} + fn alloc_c_string(s: String) -> *mut c_char { CString::new(s) .unwrap_or_else(|_| CString::new("string contained interior NUL").unwrap()) @@ -211,3 +217,42 @@ pub extern "C" fn mlang_nickel_eval_file( } } } + +#[no_mangle] +pub extern "C" fn mlang_json_eval( + source: *const c_char, + out_body: *mut *mut c_char, + out_error: *mut *mut c_char, +) -> i32 { + if source.is_null() || out_body.is_null() || out_error.is_null() { + return 0; + } + unsafe { + *out_body = ptr::null_mut(); + *out_error = ptr::null_mut(); + } + let source = unsafe { CStr::from_ptr(source) }; + let source = match source.to_str() { + Ok(source) => source, + Err(err) => { + unsafe { + *out_error = alloc_c_string(format!("invalid JSON source UTF-8: {err}")); + } + return 0; + } + }; + match json_to_data_string(source) { + Ok(rendered) => { + unsafe { + *out_body = alloc_c_string(rendered); + } + 1 + } + Err(err) => { + unsafe { + *out_error = alloc_c_string(format!("JSON parse error: {err}")); + } + 0 + } + } +} diff --git a/native/mlang_http_ffi.c b/native/mlang_http_ffi.c index bfe7311..bba9ef1 100644 --- a/native/mlang_http_ffi.c +++ b/native/mlang_http_ffi.c @@ -6,6 +6,7 @@ extern uint8_t mlang_http_get_body(const char *url, char **out_body, char **out_error); extern uint8_t mlang_nickel_eval(const char *source, char **out_body, char **out_error); extern uint8_t mlang_nickel_eval_file(const char *path, char **out_body, char **out_error); +extern uint8_t mlang_json_eval(const char *source, char **out_body, char **out_error); extern void mlang_http_string_free(char *ptr); extern lean_obj_res lean_mk_io_user_error(lean_obj_arg msg); @@ -65,3 +66,11 @@ LEAN_EXPORT lean_obj_res mlang_nickel_eval_file_string(b_lean_obj_arg path, lean uint8_t ok = mlang_nickel_eval_file(lean_string_cstr(path), &body, &error); return wrap_string_result(ok, body, error); } + +LEAN_EXPORT lean_obj_res mlang_json_eval_string(b_lean_obj_arg source, lean_obj_arg world) { + (void)world; + char *body = NULL; + char *error = NULL; + uint8_t ok = mlang_json_eval(lean_string_cstr(source), &body, &error); + return wrap_string_result(ok, body, error); +} diff --git a/native/mlang_repl/src/main.rs b/native/mlang_repl/src/main.rs index 316ba52..7c32228 100644 --- a/native/mlang_repl/src/main.rs +++ b/native/mlang_repl/src/main.rs @@ -33,6 +33,48 @@ fn eval(binary: &Path, input: &str) -> Result<(), String> { } } +fn parse_bare_let_binding(input: &str) -> Option<(&str, &str)> { + let rest = input.strip_prefix("let ")?; + let eq_idx = rest.find('=')?; + let name = rest[..eq_idx].trim(); + if name.is_empty() + || !name + .chars() + .all(|c| c == '_' || c.is_ascii_alphanumeric()) + || !name + .chars() + .next() + .is_some_and(|c| c == '_' || c.is_ascii_alphabetic()) + { + return None; + } + + let value = rest[eq_idx + 1..].trim(); + if value.is_empty() || input.contains(';') { + return None; + } + + Some((name, value)) +} + +fn render_repl_input(prelude: &[String], input: &str) -> String { + let body = match parse_bare_let_binding(input) { + Some((name, value)) => format!("let {name} = {value} in {name}"), + None => input.to_owned(), + }; + + if prelude.is_empty() { + body + } else { + let mut rendered = prelude + .iter() + .rev() + .fold(body, |acc, binding| format!("{binding} in {acc}")); + rendered.shrink_to_fit(); + rendered + } +} + fn main() -> ExitCode { let root = match repo_root() { Ok(root) => root, @@ -56,6 +98,7 @@ fn main() -> ExitCode { }; println!("mlang REPL. enter :quit to exit."); + let mut prelude: Vec = Vec::new(); loop { match rl.readline("mlang> ") { Ok(line) => { @@ -67,7 +110,12 @@ fn main() -> ExitCode { return ExitCode::SUCCESS; } let _ = rl.add_history_entry(input); - let _ = eval(&binary, input); + let rendered = render_repl_input(&prelude, input); + if eval(&binary, &rendered).is_ok() { + if let Some((name, value)) = parse_bare_let_binding(input) { + prelude.push(format!("let {name} = {value}")); + } + } } Err(ReadlineError::Interrupted) | Err(ReadlineError::Eof) => { println!();