-
Notifications
You must be signed in to change notification settings - Fork 0
/
convertor.sml
82 lines (76 loc) · 2.38 KB
/
convertor.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
structure Convertor =
struct
structure G = Gallina;
open Annotation
open ConvertorProgram
infix @@;
fun convert'(source : string) : G.sentence list =
let
val ((J, B_BIND), (B_STAT, B_DYN), s) = Sml.lib()
val parseArgs = (J, B_BIND)
val elabArgs = (J, B_BIND, B_STAT)
val (J', program) = Sml.parse1 parseArgs (NONE, source)
val B_STAT' = Program.elabProgram true (B_STAT, program)
val s' = ref s
val B_DYN' = Program.evalProgram true ((s', B_DYN), program)
val infixEnv = VIdMap.difference(J', J);
(* val p @@ _ = program;
val Program p = p;
val (p, _) = p;
val p @@ _ = p;
val STRDECTopDec p = p;
val (p, _) = p;
val p @@ _ = p;
val DECStrDec p = p;
val p @@ a = p;
*)
in
program2sents (program, infixEnv)
end
fun convert(source: string): G.sentence list =
let
val ins = TextIO.openIn source
fun loop ins =
case TextIO.inputLine ins of
SOME line => line :: loop ins
| NONE => []
val codeList = (loop ins before TextIO.closeIn ins)
val code = String.concat codeList ^ ";"
in
convert' code
end
(* Functions for debugging *)
fun getAST(source: string) =
let
val ins = TextIO.openIn source
fun loop ins =
case TextIO.inputLine ins of
SOME line => line :: loop ins
| NONE => []
val codeList = loop ins before TextIO.closeIn ins
val source = String.concat codeList
val ((J, B_BIND), _, _) = Sml.lib()
val parseArgs = (J, B_BIND)
val (J', program) = Sml.parse1 parseArgs (NONE, source)
in
program
end
fun getElabAST(source: string) =
let
val ins = TextIO.openIn source
fun loop ins =
case TextIO.inputLine ins of
SOME line => line :: loop ins
| NONE => []
val codeList = loop ins before TextIO.closeIn ins
val source = String.concat codeList
val ((J, B_BIND), (B_STAT, B_DYN), s) = Sml.lib()
val parseArgs = (J, B_BIND)
val (J', program) = Sml.parse1 parseArgs (NONE, source)
val B_STAT' = Program.elabProgram true (B_STAT, program)
val s' = ref s
val B_DYN' = Program.evalProgram true ((s', B_DYN), program)
in
program
end
end