Mercurial > urweb

changeset 55:5c97b7cd912b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing signature files
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 11:04:10 -0400
parents a6e185c7c428
children d3cc191cb25f
files src/compiler.sig src/compiler.sml src/source_print.sig tests/split.lac tests/split.lig
diffstat 5 files changed, 53 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/compiler.sig	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/compiler.sig	Sun Jun 22 11:04:10 2008 -0400
@@ -31,6 +31,9 @@
 
     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
--- a/src/compiler.sml	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/compiler.sml	Sun Jun 22 11:04:10 2008 -0400
@@ -35,6 +35,46 @@
                          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 @@
         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
 
--- a/src/source_print.sig	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/source_print.sig	Sun Jun 22 11:04:10 2008 -0400
@@ -32,5 +32,6 @@
     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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/split.lac	Sun Jun 22 11:04:10 2008 -0400
@@ -0,0 +1,2 @@
+type t = int
+val x = 0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/split.lig	Sun Jun 22 11:04:10 2008 -0400
@@ -0,0 +1,2 @@
+type t
+val x : t