summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/compiler.sig3
-rw-r--r--src/compiler.sml46
-rw-r--r--src/source_print.sig1
-rw-r--r--tests/split.lac2
-rw-r--r--tests/split.lig2
5 files changed, 53 insertions, 1 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index eac2c538..872ae0fc 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -31,6 +31,9 @@ signature COMPILER = sig
val compile : string -> unit
+ val parseLig : string -> Source.sgn_item list option
+ val testLig : string -> unit
+
val parse : string -> Source.file option
val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option
val explify : ElabEnv.env -> string -> Expl.file option
diff --git a/src/compiler.sml b/src/compiler.sml
index 8e011d8e..ddfa122a 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -35,6 +35,46 @@ structure LacwebP = Join(structure ParserData = LacwebLrVals.ParserData
structure Lex = Lex
structure LrParser = LrParser)
+fun parseLig filename =
+ let
+ val fname = OS.FileSys.tmpName ()
+ val outf = TextIO.openOut fname
+ val () = TextIO.output (outf, "sig\n")
+ val inf = TextIO.openIn filename
+ fun loop () =
+ case TextIO.inputLine inf of
+ NONE => ()
+ | SOME line => (TextIO.output (outf, line);
+ loop ())
+ val () = loop ()
+ val () = TextIO.closeIn inf
+ val () = TextIO.closeOut outf
+
+ val () = (ErrorMsg.resetErrors ();
+ ErrorMsg.resetPositioning filename)
+ val file = TextIO.openIn fname
+ fun get _ = TextIO.input file
+ fun parseerror (s, p1, p2) = ErrorMsg.errorAt' (p1, p2) s
+ val lexer = LrParser.Stream.streamify (Lex.makeLexer get)
+ val (absyn, _) = LacwebP.parse (30, lexer, parseerror, ())
+ in
+ TextIO.closeIn file;
+ if ErrorMsg.anyErrors () then
+ NONE
+ else
+ case absyn of
+ [(Source.DSgn ("?", (Source.SgnConst sgis, _)), _)] => SOME sgis
+ | _ => NONE
+ end
+ handle LrParser.ParseError => NONE
+
+fun testLig fname =
+ case parseLig fname of
+ NONE => ()
+ | SOME sgis =>
+ app (fn sgi => (Print.print (SourcePrint.p_sgn_item sgi);
+ print "\n")) sgis
+
(* The main parsing routine *)
fun parse filename =
let
@@ -50,7 +90,11 @@ fun parse filename =
if ErrorMsg.anyErrors () then
NONE
else
- SOME absyn
+ case absyn of
+ [(Source.DSgn ("?", _), _)] =>
+ (ErrorMsg.error "File starts with 'sig'";
+ NONE)
+ | _ => SOME absyn
end
handle LrParser.ParseError => NONE
diff --git a/src/source_print.sig b/src/source_print.sig
index c21d328a..72addfb7 100644
--- a/src/source_print.sig
+++ b/src/source_print.sig
@@ -32,5 +32,6 @@ signature SOURCE_PRINT = sig
val p_explicitness : Source.explicitness Print.printer
val p_con : Source.con Print.printer
val p_decl : Source.decl Print.printer
+ val p_sgn_item : Source.sgn_item Print.printer
val p_file : Source.file Print.printer
end
diff --git a/tests/split.lac b/tests/split.lac
new file mode 100644
index 00000000..0a855c5e
--- /dev/null
+++ b/tests/split.lac
@@ -0,0 +1,2 @@
+type t = int
+val x = 0
diff --git a/tests/split.lig b/tests/split.lig
new file mode 100644
index 00000000..d095f7c4
--- /dev/null
+++ b/tests/split.lig
@@ -0,0 +1,2 @@
+type t
+val x : t