Parsing signature files

3 files changed, 49 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