nandi.uk
This repository has no description
1import Mlang
2
3open Mlang
4
5def 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
21def renderResult (value : Value) (judgment : Judgment) : String :=
22 s!"{renderValue value} : {renderJudgment (refineJudgmentFromValue value judgment)}"
23
24unsafe 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
40unsafe def checkAndEvalWith (tyEnv : TyEnv) (env : Env) (source : String) : IO (Except String (List (Value × Judgment))) := do
41 match parseProgram source with
42 | .error err =>
43 pure (.error s!"parse error: {reprStr err}")
44 | .ok exprs => do
45 checkExprsWith tyEnv env exprs
46
47unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) :=
48 checkAndEvalWith [] [] source
49
50unsafe def runFile (path : String) : IO UInt32 := do
51 let source ← IO.FS.readFile path
52 match (← checkAndEval source) with
53 | .ok results =>
54 for (value, judgment) in results do
55 IO.println (renderResult value judgment)
56 pure 0
57 | .error msg =>
58 IO.eprintln s!"{path}: {msg}"
59 pure 1
60
61unsafe def runEval (source : String) : IO UInt32 := do
62 match (← checkAndEval source) with
63 | .ok results =>
64 for (value, judgment) in results do
65 IO.println (renderResult value judgment)
66 pure 0
67 | .error msg =>
68 IO.eprintln msg
69 pure 1
70
71unsafe def repl (tyEnv : TyEnv := []) (env : Env := []) : IO UInt32 := do
72 let stdin ← IO.getStdin
73 let line ← stdin.getLine
74 let input := (String.trimAscii line).toString
75 if input.isEmpty then
76 repl tyEnv env
77 else if input = ":quit" || input = ":q" then
78 pure 0
79 else do
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
107
108def printUsage : IO Unit := do
109 IO.println "usage:"
110 IO.println " mlang # start REPL"
111 IO.println " mlang --eval <src> # evaluate source from the command line"
112 IO.println " mlang <file> # run a semicolon-separated source file"
113 IO.println " mlang :quit # not valid; use inside REPL"
114
115unsafe def main (args : List String) : IO UInt32 := do
116 match args with
117 | [] =>
118 IO.println "mlang REPL. enter :quit to exit."
119 repl
120 | ["-h"] | ["--help"] =>
121 printUsage
122 pure 0
123 | ["--eval", source] =>
124 runEval source
125 | [path] =>
126 runFile path
127 | _ =>
128 printUsage
129 pure 1