diff options
| -rw-r--r-- | src/compiler.sig | 3 | ||||
| -rw-r--r-- | src/compiler.sml | 46 | ||||
| -rw-r--r-- | src/source_print.sig | 1 | ||||
| -rw-r--r-- | tests/split.lac | 2 | ||||
| -rw-r--r-- | tests/split.lig | 2 |
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 |