Add richer Data REPL and conversion support · nandi.uk/mlang@d22f5bf

+71 -26

Main.lean

··· 2 2 3 3 open Mlang 4 4 5 - unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) := do 5 + def refineJudgmentFromValue (value : Value) (judgment : Judgment) : Judgment := 6 + match value with 7 + | .data term => 8 + let refinedTy := refineKnownDataTy (dataType term) 9 + match judgment.ty with 10 + | .data 11 + | .dataInt 12 + | .dataBool 13 + | .dataString 14 + | .dataNull 15 + | .dataArray _ 16 + | .dataRecord _ => 17 + { judgment with ty := refinedTy } 18 + | _ => judgment 19 + | _ => judgment 20 + 21 + def renderResult (value : Value) (judgment : Judgment) : String := 22 + s!"{renderValue value} : {renderJudgment (refineJudgmentFromValue value judgment)}" 23 + 24 + unsafe def checkExprsWith (tyEnv : TyEnv) (env : Env) (exprs : List Expr) : IO (Except String (List (Value × Judgment))) := do 25 + let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do 26 + match pending with 27 + | [] => pure (.ok acc.reverse) 28 + | expr :: rest => 29 + match inferType tyEnv expr with 30 + | .error err => 31 + pure (.error s!"type error: {reprStr err}") 32 + | .ok judgment => 33 + match (← (eval env expr).toIO') with 34 + | .ok value => 35 + loop rest ((value, judgment) :: acc) 36 + | .error err => 37 + pure (.error s!"runtime error: {reprStr err}") 38 + loop exprs [] 39 + 40 + unsafe def checkAndEvalWith (tyEnv : TyEnv) (env : Env) (source : String) : IO (Except String (List (Value × Judgment))) := do 6 41 match parseProgram source with 7 42 | .error err => 8 43 pure (.error s!"parse error: {reprStr err}") 9 44 | .ok exprs => do 10 - let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do 11 - match pending with 12 - | [] => pure (.ok acc.reverse) 13 - | expr :: rest => 14 - match inferType [] expr with 15 - | .error err => 16 - pure (.error s!"type error: {reprStr err}") 17 - | .ok judgment => 18 - match (← (eval [] expr).toIO') with 19 - | .ok value => 20 - loop rest ((value, judgment) :: acc) 21 - | .error err => 22 - pure (.error s!"runtime error: {reprStr err}") 23 - loop exprs [] 45 + checkExprsWith tyEnv env exprs 46 + 47 + unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) := 48 + checkAndEvalWith [] [] source 24 49 25 50 unsafe def runFile (path : String) : IO UInt32 := do 26 51 let source ← IO.FS.readFile path 27 52 match (← checkAndEval source) with 28 53 | .ok results => 29 54 for (value, judgment) in results do 30 - IO.println s!"{renderValue value} : {renderJudgment judgment}" 55 + IO.println (renderResult value judgment) 31 56 pure 0 32 57 | .error msg => 33 58 IO.eprintln s!"{path}: {msg}" ··· 37 62 match (← checkAndEval source) with 38 63 | .ok results => 39 64 for (value, judgment) in results do 40 - IO.println s!"{renderValue value} : {renderJudgment judgment}" 65 + IO.println (renderResult value judgment) 41 66 pure 0 42 67 | .error msg => 43 68 IO.eprintln msg 44 69 pure 1 45 70 46 - unsafe def repl : IO UInt32 := do 71 + unsafe def repl (tyEnv : TyEnv := []) (env : Env := []) : IO UInt32 := do 47 72 let stdin ← IO.getStdin 48 73 let line ← stdin.getLine 49 74 let input := (String.trimAscii line).toString 50 75 if input.isEmpty then 51 - repl 76 + repl tyEnv env 52 77 else if input = ":quit" || input = ":q" then 53 78 pure 0 54 79 else do 55 - match (← checkAndEval input) with 56 - | .ok results => 57 - for (value, judgment) in results do 58 - IO.println s!"{renderValue value} : {renderJudgment judgment}" 59 - | .error msg => 60 - IO.eprintln msg 61 - repl 80 + match parseReplCommand input with 81 + | .error err => 82 + IO.eprintln s!"parse error: {reprStr err}" 83 + repl tyEnv env 84 + | .ok command => 85 + match command with 86 + | .bind name value => 87 + match inferType tyEnv value with 88 + | .error err => 89 + IO.eprintln s!"type error: {reprStr err}" 90 + repl tyEnv env 91 + | .ok judgment => 92 + match (← (eval env value).toIO') with 93 + | .error err => 94 + IO.eprintln s!"runtime error: {reprStr err}" 95 + repl tyEnv env 96 + | .ok boundValue => 97 + IO.println (renderResult boundValue judgment) 98 + repl ((name, judgment.ty) :: tyEnv) ((name, boundValue) :: env) 99 + | .evalProgram exprs => 100 + match (← checkExprsWith tyEnv env exprs) with 101 + | .ok results => 102 + for (value, judgment) in results do 103 + IO.println (renderResult value judgment) 104 + | .error msg => 105 + IO.eprintln msg 106 + repl tyEnv env 62 107 63 108 def printUsage : IO Unit := do 64 109 IO.println "usage:"

+175 -11

Mlang/Interpreter.lean

View file

··· 65 65 | int : Int → Expr 66 66 | bool : Bool → Expr 67 67 | string : String → Expr 68 + | null : Expr 68 69 | var : Name → Expr 70 + | arrayE : List Expr → Expr 71 + | recordE : List (String × Expr) → Expr 69 72 | add : Expr → Expr → Expr 70 73 | sub : Expr → Expr → Expr 71 74 | mul : Expr → Expr → Expr ··· 92 95 | builtinHttpGet : Value 93 96 | builtinReadFileNickel : Value 94 97 | builtinParseNickel : Value 98 + | builtinParseJson : Value 95 99 | builtinDataGet : Value 96 100 | builtinDataGetField : Data → Value 97 101 | builtinDataAt : Value ··· 99 103 | builtinDataAsInt : Value 100 104 | builtinDataAsString : Value 101 105 | builtinDataAsBool : Value 106 + | builtinDataToJson : Value 107 + | builtinDataToNickel : Value 102 108 | closure : Name → Expr → List (Name × Value) → Value 103 109 deriving Repr, Inhabited 104 110 ··· 134 140 | .data term => pure term 135 141 | _ => throw (.typeError "expected a data value") 136 142 143 + def valueToData : Value → EvalM Data 144 + | .data term => pure term 145 + | .int n => pure (.int n) 146 + | .bool b => pure (.bool b) 147 + | .string s => pure (.string s) 148 + | _ => throw (.typeError "data literals only support Int, Bool, String, and Data values") 149 + 137 150 partial def dataType : Data → Ty 138 151 | .null => .dataNull 139 152 | .bool _ => .dataBool ··· 159 172 | .dataBool => .bool 160 173 | .dataString => .string 161 174 | ty => ty 175 + 176 + partial def refineKnownDataTy (ty : Ty) : Ty := 177 + match ty with 178 + | .dataInt => .int 179 + | .dataBool => .bool 180 + | .dataString => .string 181 + | .dataNull => .data 182 + | .dataArray itemTy => .dataArray (refineKnownDataTy itemTy) 183 + | .dataRecord fields => 184 + .dataRecord (fields.map (fun (name, fieldTy) => (name, refineKnownDataTy fieldTy))) 185 + | other => other 162 186 163 187 def dataArrayGet? : List Data → Nat → Option Data 164 188 | [], _ => none ··· 194 218 | .ok value => .resultOk value 195 219 | .error err => .resultErr (runtimeErrorToMessage err) 196 220 221 + def escapeJsonChar : Char → String 222 + | '"' => "\\\"" 223 + | '\\' => "\\\\" 224 + | '\n' => "\\n" 225 + | '\r' => "\\r" 226 + | '\t' => "\\t" 227 + | c => c.toString 228 + 229 + def renderJsonString (s : String) : String := 230 + "\"" ++ String.join (s.toList.map escapeJsonChar) ++ "\"" 231 + 232 + def isNickelKeyStart (c : Char) : Bool := 233 + c.isAlpha || c = '_' 234 + 235 + def isNickelKeyContinue (c : Char) : Bool := 236 + c.isAlpha || c.isDigit || c = '_' || c = '-' 237 + 238 + def renderNickelKey (s : String) : String := 239 + match s.toList with 240 + | [] => renderJsonString s 241 + | c :: cs => 242 + if isNickelKeyStart c && cs.all isNickelKeyContinue then 243 + s 244 + else 245 + renderJsonString s 246 + 247 + partial def renderNickelData : Data → String 248 + | .null => "null" 249 + | .bool b => toString b 250 + | .int n => toString n 251 + | .string s => renderJsonString s 252 + | .array xs => "[" ++ String.intercalate ", " (xs.map renderNickelData) ++ "]" 253 + | .record fields => 254 + let rendered := fields.map (fun (k, v) => s!"{renderNickelKey k} = {renderNickelData v}") 255 + "{ " ++ String.intercalate ", " rendered ++ " }" 256 + 257 + partial def renderJsonData : Data → String 258 + | .null => "null" 259 + | .bool b => if b then "true" else "false" 260 + | .int n => toString n 261 + | .string s => renderJsonString s 262 + | .array xs => "[" ++ String.intercalate ", " (xs.map renderJsonData) ++ "]" 263 + | .record fields => 264 + let rendered := fields.map (fun (k, v) => s!"{renderJsonString k}: {renderJsonData v}") 265 + "{" ++ String.intercalate ", " rendered ++ "}" 266 + 197 267 def builtinType? (name : Name) : Option Ty := 198 268 match name with 199 269 | "readFile" => some (.funTy .string [.error, .io] .string) 200 270 | "httpGet" => some (.funTy .string [.error, .io] .string) 201 271 | "readFileNickel" => some (.funTy .string [.error, .io] .data) 202 272 | "parseNickel" => some (.funTy .string [.error] .data) 273 + | "parseJson" => some (.funTy .string [.error] .data) 203 274 | "get" => some (.funTy .data [] (.funTy .string [.error] .data)) 204 275 | "at" => some (.funTy .data [] (.funTy .int [.error] .data)) 205 276 | "asInt" => some (.funTy .data [.error] .int) 206 277 | "asString" => some (.funTy .data [.error] .string) 207 278 | "asBool" => some (.funTy .data [.error] .bool) 279 + | "toJson" => some (.funTy .data [] .string) 280 + | "toNickel" => some (.funTy .data [] .string) 208 281 | _ => none 209 282 210 283 def builtinValue? (name : Name) : Option Value := ··· 213 286 | "httpGet" => some .builtinHttpGet 214 287 | "readFileNickel" => some .builtinReadFileNickel 215 288 | "parseNickel" => some .builtinParseNickel 289 + | "parseJson" => some .builtinParseJson 216 290 | "get" => some .builtinDataGet 217 291 | "at" => some .builtinDataAt 218 292 | "asInt" => some .builtinDataAsInt 219 293 | "asString" => some .builtinDataAsString 220 294 | "asBool" => some .builtinDataAsBool 295 + | "toJson" => some .builtinDataToJson 296 + | "toNickel" => some .builtinDataToNickel 221 297 | _ => none 222 298 223 299 mutual ··· 241 317 let source ← expectString argVal 242 318 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalString source) 243 319 pure (.data (← parseRenderedData rendered)) 320 + | .builtinParseJson => do 321 + let source ← expectString argVal 322 + let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalJsonString source) 323 + pure (.data (← parseRenderedData rendered)) 244 324 | .builtinDataGet => do 245 325 let term ← expectData argVal 246 326 pure (.builtinDataGetField term) ··· 281 361 match term with 282 362 | .bool b => pure (.bool b) 283 363 | _ => throw (.typeError "asBool expects a boolean") 364 + | .builtinDataToJson => do 365 + let term ← expectData argVal 366 + pure (.string (renderJsonData term)) 367 + | .builtinDataToNickel => do 368 + let term ← expectData argVal 369 + pure (.string (renderNickelData term)) 284 370 | _ => 285 371 match fnVal, argVal with 286 372 | .data (.record fields), .string key => ··· 305 391 | .int n => pure (.int n) 306 392 | .bool b => pure (.bool b) 307 393 | .string s => pure (.string s) 394 + | .null => pure (.data .null) 308 395 | .var name => 309 396 match env.lookup name with 310 397 | some v => pure v ··· 312 399 match builtinValue? name with 313 400 | some v => pure v 314 401 | none => throw (.unboundVariable name) 402 + | .arrayE items => do 403 + let values ← items.mapM (eval env) 404 + pure (.data (.array (← values.mapM valueToData))) 405 + | .recordE fields => do 406 + let fields' ← fields.mapM (fun (name, value) => do 407 + let value' ← eval env value 408 + pure (name, (← valueToData value'))) 409 + pure (.data (.record fields')) 315 410 | .add lhs rhs => do 316 411 let l ← expectInt (← eval env lhs) 317 412 let r ← expectInt (← eval env rhs) ··· 367 462 applyValue fnVal argVal 368 463 end 369 464 370 - partial def renderData : Data → String 371 - | .null => "null" 372 - | .bool b => toString b 373 - | .int n => toString n 374 - | .string s => s!"\"{s}\"" 375 - | .array xs => "[" ++ String.intercalate ", " (xs.map renderData) ++ "]" 376 - | .record fields => 377 - let rendered := fields.map (fun (k, v) => s!"{k} = {renderData v}") 378 - "{ " ++ String.intercalate ", " rendered ++ " }" 465 + def renderData : Data → String := renderNickelData 379 466 380 467 def renderValue : Value → String 381 468 | .int n => toString n ··· 390 477 | .builtinHttpGet => "<builtin:httpGet>" 391 478 | .builtinReadFileNickel => "<builtin:readFileNickel>" 392 479 | .builtinParseNickel => "<builtin:parseNickel>" 480 + | .builtinParseJson => "<builtin:parseJson>" 393 481 | .builtinDataGet => "<builtin:get>" 394 482 | .builtinDataGetField _ => "<builtin:getField>" 395 483 | .builtinDataAt => "<builtin:at>" ··· 397 485 | .builtinDataAsInt => "<builtin:asInt>" 398 486 | .builtinDataAsString => "<builtin:asString>" 399 487 | .builtinDataAsBool => "<builtin:asBool>" 488 + | .builtinDataToJson => "<builtin:toJson>" 489 + | .builtinDataToNickel => "<builtin:toNickel>" 400 490 | .closure _ _ _ => "<closure>" 401 491 402 492 abbrev TyEnv := List (Name × Ty) ··· 451 541 | _ => none 452 542 453 543 unsafe def evalConstData? (env : List (Name × Data)) : Expr → Option Data 544 + | .null => some .null 454 545 | .string s => some (.string s) 455 546 | .int n => some (.int n) 456 547 | .bool b => some (.bool b) 457 548 | .var name => env.lookup name 549 + | .arrayE items => do 550 + some (.array (← items.mapM (evalConstData? env))) 551 + | .recordE fields => do 552 + some (.record (← fields.mapM (fun (name, value) => do 553 + let value' ← evalConstData? env value 554 + pure (name, value')))) 458 555 | .letE name value body => do 459 556 let value' ← evalConstData? env value 460 557 evalConstData? ((name, value') :: env) body ··· 476 573 | .error _ => none 477 574 | .error _ => none 478 575 | _ => none 576 + | .var "parseJson" => 577 + let source ← evalConstData? env arg 578 + match source with 579 + | .string s => 580 + match unsafeIO (NickelHost.evalJsonString s) with 581 + | .ok rendered => 582 + match Nickel.parse rendered with 583 + | .ok term => some (Data.ofNickel term) 584 + | .error _ => none 585 + | .error _ => none 586 + | _ => none 587 + | .var "httpGet" => 588 + let url ← evalConstData? env arg 589 + match url with 590 + | .string s => 591 + match unsafeIO (Http.httpGet s) with 592 + | .ok body => some (.string body) 593 + | .error _ => none 594 + | _ => none 479 595 | .var "readFileNickel" => 480 596 let path ← evalConstData? env arg 481 597 match path with ··· 510 626 | .int _ => pure (pureJudgment .int) 511 627 | .bool _ => pure (pureJudgment .bool) 512 628 | .string _ => pure (pureJudgment .string) 629 + | .null => pure (pureJudgment .dataNull) 513 630 | .var name => 514 631 match env.lookup name with 515 632 | some ty => pure (pureJudgment ty) ··· 517 634 match builtinType? name with 518 635 | some ty => pure (pureJudgment ty) 519 636 | none => throw (.unboundVariable name) 637 + | .arrayE items => do 638 + let itemJs ← items.mapM (inferType env) 639 + let dataTys ← itemJs.mapM (fun j => 640 + match j.ty with 641 + | .int => pure .dataInt 642 + | .bool => pure .dataBool 643 + | .string => pure .dataString 644 + | .data => pure .data 645 + | .dataInt => pure .dataInt 646 + | .dataBool => pure .dataBool 647 + | .dataString => pure .dataString 648 + | .dataNull => pure .dataNull 649 + | .dataArray ty => pure (.dataArray ty) 650 + | .dataRecord fields => pure (.dataRecord fields) 651 + | ty => throw (.mismatch .data ty)) 652 + let itemTy := 653 + match dataTys with 654 + | [] => .data 655 + | first :: rest => if rest.all (· == first) then first else .data 656 + pure { 657 + ty := .dataArray itemTy 658 + effects := itemJs.foldl (fun acc j => acc.union j.effects) [] 659 + } 660 + | .recordE fields => do 661 + let fieldJs ← fields.mapM (fun (name, value) => do pure (name, ← inferType env value)) 662 + let fieldTys ← fieldJs.mapM (fun (name, j) => do 663 + let ty ← match j.ty with 664 + | .int => pure .dataInt 665 + | .bool => pure .dataBool 666 + | .string => pure .dataString 667 + | .data => pure .data 668 + | .dataInt => pure .dataInt 669 + | .dataBool => pure .dataBool 670 + | .dataString => pure .dataString 671 + | .dataNull => pure .dataNull 672 + | .dataArray ty => pure (.dataArray ty) 673 + | .dataRecord fields => pure (.dataRecord fields) 674 + | ty => throw (.mismatch .data ty) 675 + pure (name, ty, j.effects)) 676 + pure { 677 + ty := .dataRecord (fieldTys.map (fun (name, ty, _) => (name, ty))) 678 + effects := fieldTys.foldl (fun acc (_, _, effects) => acc.union effects) [] 679 + } 520 680 | .add lhs rhs 521 681 | .sub lhs rhs 522 682 | .mul lhs rhs => do ··· 617 777 | .error _ => .data 618 778 | .var "parseNickel", _, .data => 619 779 match evalConstData? [] (.app fn arg) with 620 - | some data => dataType data 780 + | some data => refineKnownDataTy (dataType data) 781 + | none => .data 782 + | .var "parseJson", _, .data => 783 + match evalConstData? [] (.app fn arg) with 784 + | some data => refineKnownDataTy (dataType data) 621 785 | none => .data 622 786 | .var "readFileNickel", _, .data => 623 787 match evalConstData? [] (.app fn arg) with 624 - | some data => dataType data 788 + | some data => refineKnownDataTy (dataType data) 625 789 | none => .data 626 790 | .var "asInt", _, .int => 627 791 match argJ.ty with

+1

Mlang/NickelHost.lean

View file

··· 2 2 3 3 @[extern "mlang_nickel_eval_string"] opaque evalString (source : @& String) : IO String 4 4 @[extern "mlang_nickel_eval_file_string"] opaque evalFile (path : @& String) : IO String 5 + @[extern "mlang_json_eval_string"] opaque evalJsonString (source : @& String) : IO String 5 6 6 7 end Mlang.NickelHost

+70 -1

Mlang/Parser.lean

View file

··· 9 9 | ident : String → Token 10 10 | lparen : Token 11 11 | rparen : Token 12 + | lbracket : Token 13 + | rbracket : Token 14 + | lbrace : Token 15 + | rbrace : Token 12 16 | semicolon : Token 13 17 | comma : Token 14 18 | colon : Token ··· 28 32 | kwTry : Token 29 33 | kwWith : Token 30 34 | kwPmap : Token 35 + | kwNull : Token 31 36 deriving Repr, BEq, Inhabited 32 37 33 38 inductive ParseError where ··· 49 54 isIdentStart c || isDigit c 50 55 51 56 def isAtomStart : Token → Bool 52 - | .int _ | .bool _ | .string _ | .ident _ | .lparen => true 57 + | .int _ | .bool _ | .string _ | .ident _ | .lparen | .lbracket | .lbrace | .kwNull => true 53 58 | _ => false 54 59 55 60 partial def spanChars (p : Char → Bool) : List Char → List Char × List Char ··· 78 83 | "try" => .kwTry 79 84 | "with" => .kwWith 80 85 | "pmap" => .kwPmap 86 + | "null" => .kwNull 81 87 | "true" => .bool true 82 88 | "false" => .bool false 83 89 | _ => .ident name ··· 127 133 pure (tok :: toks) 128 134 | '(', _ => do pure (.lparen :: (← lexChars cs)) 129 135 | ')', _ => do pure (.rparen :: (← lexChars cs)) 136 + | '[', _ => do pure (.lbracket :: (← lexChars cs)) 137 + | ']', _ => do pure (.rbracket :: (← lexChars cs)) 138 + | '{', _ => do pure (.lbrace :: (← lexChars cs)) 139 + | '}', _ => do pure (.rbrace :: (← lexChars cs)) 130 140 | ';', _ => do pure (.semicolon :: (← lexChars cs)) 131 141 | ',', _ => do pure (.comma :: (← lexChars cs)) 132 142 | ':', _ => do pure (.colon :: (← lexChars cs)) ··· 143 153 lexChars input.toList 144 154 145 155 abbrev ParserState := List Token 156 + 157 + inductive ReplCommand where 158 + | bind : Name → Expr → ReplCommand 159 + | evalProgram : List Expr → ReplCommand 160 + deriving Repr, Inhabited 146 161 147 162 def expectToken (expected : Token) : ParserState → ParseM ParserState 148 163 | tok :: rest => ··· 292 307 pure (fn, tokens) 293 308 | [] => pure (fn, []) 294 309 310 + partial def parseArrayItems (items : List Expr) : ParserState → ParseM (Expr × ParserState) 311 + | .rbracket :: rest => pure (.arrayE items.reverse, rest) 312 + | .comma :: rest => do 313 + let (item, rest) ← parseExpr rest 314 + parseArrayItems (item :: items) rest 315 + | tok :: _ => throw (.unexpectedToken s!"expected ',' or ']', got {reprStr tok}") 316 + | [] => throw (.unexpectedEof "unterminated array") 317 + 318 + partial def parseArray : ParserState → ParseM (Expr × ParserState) 319 + | .rbracket :: rest => pure (.arrayE [], rest) 320 + | tokens => do 321 + let (first, rest) ← parseExpr tokens 322 + parseArrayItems [first] rest 323 + 324 + partial def parseFieldKey : ParserState → ParseM (String × ParserState) 325 + | .ident name :: rest => pure (name, rest) 326 + | .string name :: rest => pure (name, rest) 327 + | tok :: _ => throw (.unexpectedToken s!"expected field key, got {reprStr tok}") 328 + | [] => throw (.unexpectedEof "expected field key") 329 + 330 + partial def parseRecordFields (fields : List (String × Expr)) : ParserState → ParseM (Expr × ParserState) 331 + | .rbrace :: rest => pure (.recordE fields.reverse, rest) 332 + | .comma :: rest => do 333 + let (name, rest) ← parseFieldKey rest 334 + let rest ← expectToken .eq rest 335 + let (value, rest) ← parseExpr rest 336 + parseRecordFields ((name, value) :: fields) rest 337 + | tok :: _ => throw (.unexpectedToken s!"expected ',' or '}}', got {reprStr tok}") 338 + | [] => throw (.unexpectedEof "unterminated record") 339 + 340 + partial def parseRecord : ParserState → ParseM (Expr × ParserState) 341 + | .rbrace :: rest => pure (.recordE [], rest) 342 + | tokens => do 343 + let (name, rest) ← parseFieldKey tokens 344 + let rest ← expectToken .eq rest 345 + let (value, rest) ← parseExpr rest 346 + parseRecordFields [(name, value)] rest 347 + 295 348 partial def parseAtom : ParserState → ParseM (Expr × ParserState) 296 349 | .int n :: rest => pure (.int n, rest) 297 350 | .bool b :: rest => pure (.bool b, rest) 298 351 | .string s :: rest => pure (.string s, rest) 352 + | .kwNull :: rest => pure (.null, rest) 299 353 | .ident name :: rest => pure (.var name, rest) 354 + | .lbracket :: rest => parseArray rest 355 + | .lbrace :: rest => parseRecord rest 300 356 | .lparen :: rest => do 301 357 let (expr, rest) ← parseExpr rest 302 358 let rest ← expectToken .rparen rest ··· 320 376 def parseProgram (input : String) : ParseM (List Expr) := do 321 377 let tokens ← lex input 322 378 parseProgramTokens tokens 379 + 380 + def parseReplCommand (input : String) : ParseM ReplCommand := do 381 + let tokens ← lex input 382 + match tokens with 383 + | .kwLet :: .ident name :: .eq :: rest => 384 + match parseExpr rest with 385 + | .ok (value, []) => pure (.bind name value) 386 + | _ => 387 + let program ← parseProgramTokens tokens 388 + pure (.evalProgram program) 389 + | _ => 390 + let program ← parseProgramTokens tokens 391 + pure (.evalProgram program) 323 392 324 393 def parse (input : String) : ParseM Expr := do 325 394 let program ← parseProgram input

+28 -2

README.md

View file

··· 64 64 | expr - expr 65 65 | expr * expr 66 66 | expr expr 67 + | [expr, ...] 68 + | { key = expr, ... } 69 + | null 67 70 | (expr) 68 71 | true | false | 123 | "text" | name 69 72 ··· 72 75 type ::= Int | Bool | String | Data | List | Result | Error | type -> type | (type) 73 76 ``` 74 77 78 + Inside the REPL, there is also a top-level binding form: 79 + 80 + ```text 81 + repl ::= let name = expr 82 + ``` 83 + 84 + Bare REPL bindings persist across later entries, so you can write: 85 + 86 + ```mlang 87 + let x = 42 88 + x + 1 89 + ``` 90 + 75 91 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: 76 92 77 93 - `httpGet : String -> String ! {IO, Error}` 94 + - `parseJson : String -> Data ! {Error}` 78 95 79 96 - `get : Data -> String -> Data ! {Error}` 80 97 - `at : Data -> Int -> Data ! {Error}` 81 98 - `asInt : Data -> Int ! {Error}` 82 99 - `asString : Data -> String ! {Error}` 83 100 - `asBool : Data -> Bool ! {Error}` 101 + - `toJson : Data -> String` 102 + - `toNickel : Data -> String` 84 103 85 104 `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. 86 105 `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 114 96 115 Non-integer numeric Nickel values are not supported yet by `mlang`'s `Data` model. 97 116 117 + Native `Data` literals are also supported directly in `mlang`: 118 + 119 + ```mlang 120 + { answer = 42, flags = [true, false], note = "ok", empty = null } 121 + ``` 122 + 123 + Fields and array elements may be `Int`, `Bool`, `String`, or existing `Data` expressions. 124 + 98 125 `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. 99 126 100 127 There is also a thread-first form that desugars statically to nested application: ··· 110 137 => get x "answer" 111 138 ``` 112 139 113 - 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. 140 + 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. 114 141 115 142 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). 116 143 ··· 118 145 119 146 ## Next steps 120 147 121 - - persist top-level bindings across REPL entries 122 148 - add recursive functions 123 149 - add algebraic data types and pattern matching 124 150 - compile to a bytecode VM or another backend

+8

examples/samples.mlg

View file

··· 5 5 readFile "examples/sample.ncl"; 6 6 readFileNickel "examples/sample.ncl"; 7 7 parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"; 8 + parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"; 9 + { answer = 42, flags = [true, false], note = "ok", empty = null }; 10 + toJson (parseNickel "{ answer = 42, flags = [true, false], note = \"ok\" }"); 11 + toJson (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"empty\":null}"); 12 + toJson { answer = 42, flags = [true, false], note = "ok", empty = null }; 13 + toNickel (parseJson "{\"answer\":42,\"flags\":[true,false],\"note\":\"ok\",\"odd key\":null}"); 8 14 get (parseNickel "{ answer = 42, flags = [true, false] }") "answer"; 15 + get (parseJson "{\"answer\":42,\"flags\":[true,false]}") "answer"; 16 + get { answer = 42, flags = [true, false] } "answer"; 9 17 at (get (parseNickel "{ flags = [true, false] }") "flags") 1; 10 18 -> "examples/sample.ncl" readFileNickel (get "answer"); 11 19 -> "{ flags = [true, false] }" parseNickel (get "flags") (at 1);

+45

native/mlang_http/src/lib.rs

View file

··· 68 68 render_json_value(&value) 69 69 } 70 70 71 + fn json_to_data_string(source: &str) -> Result<String, String> { 72 + let value: serde_json::Value = 73 + serde_json::from_str(source).map_err(|err| format!("{err}"))?; 74 + render_json_value(&value) 75 + } 76 + 71 77 fn alloc_c_string(s: String) -> *mut c_char { 72 78 CString::new(s) 73 79 .unwrap_or_else(|_| CString::new("string contained interior NUL").unwrap()) ··· 211 217 } 212 218 } 213 219 } 220 + 221 + #[no_mangle] 222 + pub extern "C" fn mlang_json_eval( 223 + source: *const c_char, 224 + out_body: *mut *mut c_char, 225 + out_error: *mut *mut c_char, 226 + ) -> i32 { 227 + if source.is_null() || out_body.is_null() || out_error.is_null() { 228 + return 0; 229 + } 230 + unsafe { 231 + *out_body = ptr::null_mut(); 232 + *out_error = ptr::null_mut(); 233 + } 234 + let source = unsafe { CStr::from_ptr(source) }; 235 + let source = match source.to_str() { 236 + Ok(source) => source, 237 + Err(err) => { 238 + unsafe { 239 + *out_error = alloc_c_string(format!("invalid JSON source UTF-8: {err}")); 240 + } 241 + return 0; 242 + } 243 + }; 244 + match json_to_data_string(source) { 245 + Ok(rendered) => { 246 + unsafe { 247 + *out_body = alloc_c_string(rendered); 248 + } 249 + 1 250 + } 251 + Err(err) => { 252 + unsafe { 253 + *out_error = alloc_c_string(format!("JSON parse error: {err}")); 254 + } 255 + 0 256 + } 257 + } 258 + }

+9

native/mlang_http_ffi.c

View file

··· 6 6 extern uint8_t mlang_http_get_body(const char *url, char **out_body, char **out_error); 7 7 extern uint8_t mlang_nickel_eval(const char *source, char **out_body, char **out_error); 8 8 extern uint8_t mlang_nickel_eval_file(const char *path, char **out_body, char **out_error); 9 + extern uint8_t mlang_json_eval(const char *source, char **out_body, char **out_error); 9 10 extern void mlang_http_string_free(char *ptr); 10 11 extern lean_obj_res lean_mk_io_user_error(lean_obj_arg msg); 11 12 ··· 65 66 uint8_t ok = mlang_nickel_eval_file(lean_string_cstr(path), &body, &error); 66 67 return wrap_string_result(ok, body, error); 67 68 } 69 + 70 + LEAN_EXPORT lean_obj_res mlang_json_eval_string(b_lean_obj_arg source, lean_obj_arg world) { 71 + (void)world; 72 + char *body = NULL; 73 + char *error = NULL; 74 + uint8_t ok = mlang_json_eval(lean_string_cstr(source), &body, &error); 75 + return wrap_string_result(ok, body, error); 76 + }

+49 -1

native/mlang_repl/src/main.rs

View file

··· 33 33 } 34 34 } 35 35 36 + fn parse_bare_let_binding(input: &str) -> Option<(&str, &str)> { 37 + let rest = input.strip_prefix("let ")?; 38 + let eq_idx = rest.find('=')?; 39 + let name = rest[..eq_idx].trim(); 40 + if name.is_empty() 41 + || !name 42 + .chars() 43 + .all(|c| c == '_' || c.is_ascii_alphanumeric()) 44 + || !name 45 + .chars() 46 + .next() 47 + .is_some_and(|c| c == '_' || c.is_ascii_alphabetic()) 48 + { 49 + return None; 50 + } 51 + 52 + let value = rest[eq_idx + 1..].trim(); 53 + if value.is_empty() || input.contains(';') { 54 + return None; 55 + } 56 + 57 + Some((name, value)) 58 + } 59 + 60 + fn render_repl_input(prelude: &[String], input: &str) -> String { 61 + let body = match parse_bare_let_binding(input) { 62 + Some((name, value)) => format!("let {name} = {value} in {name}"), 63 + None => input.to_owned(), 64 + }; 65 + 66 + if prelude.is_empty() { 67 + body 68 + } else { 69 + let mut rendered = prelude 70 + .iter() 71 + .rev() 72 + .fold(body, |acc, binding| format!("{binding} in {acc}")); 73 + rendered.shrink_to_fit(); 74 + rendered 75 + } 76 + } 77 + 36 78 fn main() -> ExitCode { 37 79 let root = match repo_root() { 38 80 Ok(root) => root, ··· 56 98 }; 57 99 58 100 println!("mlang REPL. enter :quit to exit."); 101 + let mut prelude: Vec<String> = Vec::new(); 59 102 loop { 60 103 match rl.readline("mlang> ") { 61 104 Ok(line) => { ··· 67 110 return ExitCode::SUCCESS; 68 111 } 69 112 let _ = rl.add_history_entry(input); 70 - let _ = eval(&binary, input); 113 + let rendered = render_repl_input(&prelude, input); 114 + if eval(&binary, &rendered).is_ok() { 115 + if let Some((name, value)) = parse_bare_let_binding(input) { 116 + prelude.push(format!("let {name} = {value}")); 117 + } 118 + } 71 119 } 72 120 Err(ReadlineError::Interrupted) | Err(ReadlineError::Eof) => { 73 121 println!();

Configure Feed

Configure Feed