nandi.uk
This repository has no description
5.0 kB
143 lines
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 renderValueForJudgment (value : Value) (judgment : Judgment) : String :=
22 match judgment.ty, value with
23 | .decimal, .number (.exact q) => renderDecimal q
24 | .int, .number (.exact q) =>
25 if q.den = 1 then toString q.num else renderValue value
26 | _, _ => renderValue value
27
28def renderNumericStability (value : Value) (judgment : Judgment) : String :=
29 match judgment.ty with
30 | .number =>
31 s!" [rational={rationalStabilityOfValue value}, decimal={decimalStabilityOfValue value}]"
32 | _ => ""
33
34def renderResult (value : Value) (judgment : Judgment) : String :=
35 let refined := refineJudgmentFromValue value judgment
36 s!"{renderValueForJudgment value refined} : {renderJudgment refined}{renderNumericStability value refined}"
37
38unsafe def checkExprsWith (tyEnv : TyEnv) (env : Env) (exprs : List Expr) : IO (Except String (List (Value × Judgment))) := do
39 let rec loop (pending : List Expr) (acc : List (Value × Judgment)) : IO (Except String (List (Value × Judgment))) := do
40 match pending with
41 | [] => pure (.ok acc.reverse)
42 | expr :: rest =>
43 match inferType tyEnv expr with
44 | .error err =>
45 pure (.error s!"type error: {renderTypeError err}")
46 | .ok judgment =>
47 match (← (eval env expr).toIO') with
48 | .ok value =>
49 loop rest ((value, judgment) :: acc)
50 | .error err =>
51 pure (.error s!"runtime error: {reprStr err}")
52 loop exprs []
53
54unsafe def checkAndEvalWith (tyEnv : TyEnv) (env : Env) (source : String) : IO (Except String (List (Value × Judgment))) := do
55 match parseProgram source with
56 | .error err =>
57 pure (.error s!"parse error: {reprStr err}")
58 | .ok exprs => do
59 checkExprsWith tyEnv env exprs
60
61unsafe def checkAndEval (source : String) : IO (Except String (List (Value × Judgment))) :=
62 checkAndEvalWith [] [] source
63
64unsafe def runFile (path : String) : IO UInt32 := do
65 let source ← IO.FS.readFile path
66 match (← checkAndEval source) with
67 | .ok results =>
68 for (value, judgment) in results do
69 IO.println (renderResult value judgment)
70 pure 0
71 | .error msg =>
72 IO.eprintln s!"{path}: {msg}"
73 pure 1
74
75unsafe def runEval (source : String) : IO UInt32 := do
76 match (← checkAndEval source) with
77 | .ok results =>
78 for (value, judgment) in results do
79 IO.println (renderResult value judgment)
80 pure 0
81 | .error msg =>
82 IO.eprintln msg
83 pure 1
84
85unsafe def repl (tyEnv : TyEnv := []) (env : Env := []) : IO UInt32 := do
86 let stdin ← IO.getStdin
87 let line ← stdin.getLine
88 let input := (String.trimAscii line).toString
89 if input.isEmpty then
90 repl tyEnv env
91 else if input = ":quit" || input = ":q" then
92 pure 0
93 else do
94 match parseReplCommand input with
95 | .error err =>
96 IO.eprintln s!"parse error: {reprStr err}"
97 repl tyEnv env
98 | .ok command =>
99 match command with
100 | .bind name value =>
101 match inferType tyEnv value with
102 | .error err =>
103 IO.eprintln s!"type error: {renderTypeError err}"
104 repl tyEnv env
105 | .ok judgment =>
106 match (← (eval env value).toIO') with
107 | .error err =>
108 IO.eprintln s!"runtime error: {reprStr err}"
109 repl tyEnv env
110 | .ok boundValue =>
111 IO.println (renderResult boundValue judgment)
112 repl ((name, judgment.ty) :: tyEnv) ((name, boundValue) :: env)
113 | .evalProgram exprs =>
114 match (← checkExprsWith tyEnv env exprs) with
115 | .ok results =>
116 for (value, judgment) in results do
117 IO.println (renderResult value judgment)
118 | .error msg =>
119 IO.eprintln msg
120 repl tyEnv env
121
122def printUsage : IO Unit := do
123 IO.println "usage:"
124 IO.println " mlang # start REPL"
125 IO.println " mlang --eval <src> # evaluate source from the command line"
126 IO.println " mlang <file> # run a semicolon-separated source file"
127 IO.println " mlang :quit # not valid; use inside REPL"
128
129unsafe def main (args : List String) : IO UInt32 := do
130 match args with
131 | [] =>
132 IO.println "mlang REPL. enter :quit to exit."
133 repl
134 | ["-h"] | ["--help"] =>
135 printUsage
136 pure 0
137 | ["--eval", source] =>
138 runEval source
139 | [path] =>
140 runFile path
141 | _ =>
142 printUsage
143 pure 1