Mercurial > urweb

annotate src/lacweb.lex @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 9f89f0b00b84
children e86370850c30
rev   line source
adamc@1 1 (* Copyright (c) 2008, Adam Chlipala
adamc@1 2 * All rights reserved.
adamc@1 3 *
adamc@1 4 * Redistribution and use in source and binary forms, with or without
adamc@1 5 * modification, are permitted provided that the following conditions are met:
adamc@1 6 *
adamc@1 7 * - Redistributions of source code must retain the above copyright notice,
adamc@1 8 * this list of conditions and the following disclaimer.
adamc@1 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1 10 * this list of conditions and the following disclaimer in the documentation
adamc@1 11 * and/or other materials provided with the distribution.
adamc@1 12 * - The names of contributors may not be used to endorse or promote products
adamc@1 13 * derived from this software without specific prior written permission.
adamc@1 14 *
adamc@1 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@1 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@1 26 *)
adamc@1 27
adamc@1 28 (* Lexing info for Laconic/Web programs *)
adamc@1 29
adamc@1 30 type pos = int
adamc@1 31 type svalue = Tokens.svalue
adamc@1 32 type ('a,'b) token = ('a,'b) Tokens.token
adamc@1 33 type lexresult = (svalue,pos) Tokens.token
adamc@1 34
adamc@1 35 local
adamc@1 36 val commentLevel = ref 0
adamc@1 37 val commentPos = ref 0
adamc@1 38 in
adamc@1 39 fun enterComment pos =
adamc@1 40 (if !commentLevel = 0 then
adamc@1 41 commentPos := pos
adamc@1 42 else
adamc@1 43 ();
adamc@1 44 commentLevel := !commentLevel + 1)
adamc@1 45
adamc@1 46 fun exitComment () =
adamc@1 47 (ignore (commentLevel := !commentLevel - 1);
adamc@1 48 !commentLevel = 0)
adamc@1 49
adamc@1 50 fun eof () =
adamc@1 51 let
adamc@1 52 val pos = ErrorMsg.lastLineStart ()
adamc@1 53 in
adamc@1 54 if !commentLevel > 0 then
adamc@1 55 ErrorMsg.errorAt' (!commentPos, !commentPos) "Unterminated comment"
adamc@1 56 else
adamc@1 57 ();
adamc@1 58 Tokens.EOF (pos, pos)
adamc@1 59 end
adamc@1 60 end
adamc@1 61
adamc@14 62 val str = ref ([] : char list)
adamc@14 63 val strStart = ref 0
adamc@14 64
adamc@54 65 local
adamc@54 66 val initSig = ref false
adamc@54 67 val offset = ref 0
adamc@54 68 in
adamc@54 69
adamc@54 70 fun initialSig () = initSig := true
adamc@54 71
adamc@54 72 fun pos yypos = yypos - !offset
adamc@54 73
adamc@54 74 fun newline yypos =
adamc@54 75 if !initSig then
adamc@54 76 (initSig := false;
adamc@54 77 offset := yypos + 1)
adamc@54 78 else
adamc@54 79 ErrorMsg.newline (pos yypos)
adamc@54 80
adamc@54 81 end
adamc@54 82
adamc@54 83
adamc@1 84 %%
adamc@1 85 %header (functor LacwebLexFn(structure Tokens : Lacweb_TOKENS));
adamc@1 86 %full
adamc@14 87 %s COMMENT STRING;
adamc@1 88
adamc@48 89 id = [a-z_][A-Za-z0-9_']*;
adamc@48 90 cid = [A-Z][A-Za-z0-9_']*;
adamc@1 91 ws = [\ \t\012];
adamc@14 92 intconst = [0-9]+;
adamc@14 93 realconst = [0-9]+\.[0-9]*;
adamc@1 94
adamc@1 95 %%
adamc@1 96
adamc@54 97 <INITIAL> \n => (newline yypos;
adamc@1 98 continue ());
adamc@54 99 <COMMENT> \n => (newline yypos;
adamc@1 100 continue ());
adamc@1 101
adamc@1 102 <INITIAL> {ws}+ => (lex ());
adamc@1 103
adamc@1 104 <INITIAL> "(*" => (YYBEGIN COMMENT;
adamc@54 105 enterComment (pos yypos);
adamc@1 106 continue ());
adamc@54 107 <INITIAL> "*)" => (ErrorMsg.errorAt' (pos yypos, pos yypos) "Unbalanced comments";
adamc@1 108 continue ());
adamc@1 109
adamc@54 110 <COMMENT> "(*" => (enterComment (pos yypos);
adamc@1 111 continue ());
adamc@1 112 <COMMENT> "*)" => (if exitComment () then YYBEGIN INITIAL else ();
adamc@1 113 continue ());
adamc@1 114
adamc@54 115 <INITIAL> "\"" => (YYBEGIN STRING; strStart := pos yypos; str := []; continue());
adamc@14 116 <STRING> "\\\"" => (str := #"\"" :: !str; continue());
adamc@14 117 <STRING> "\"" => (YYBEGIN INITIAL;
adamc@54 118 Tokens.STRING (String.implode (List.rev (!str)), !strStart, pos yypos + 1));
adamc@54 119 <STRING> "\n" => (newline yypos;
adamc@14 120 str := #"\n" :: !str; continue());
adamc@14 121 <STRING> . => (str := String.sub (yytext, 0) :: !str; continue());
adamc@14 122
adamc@82 123 <INITIAL> "()" => (Tokens.UNIT (pos yypos, pos yypos + size yytext));
adamc@54 124 <INITIAL> "(" => (Tokens.LPAREN (pos yypos, pos yypos + size yytext));
adamc@54 125 <INITIAL> ")" => (Tokens.RPAREN (pos yypos, pos yypos + size yytext));
adamc@54 126 <INITIAL> "[" => (Tokens.LBRACK (pos yypos, pos yypos + size yytext));
adamc@54 127 <INITIAL> "]" => (Tokens.RBRACK (pos yypos, pos yypos + size yytext));
adamc@54 128 <INITIAL> "{" => (Tokens.LBRACE (pos yypos, pos yypos + size yytext));
adamc@54 129 <INITIAL> "}" => (Tokens.RBRACE (pos yypos, pos yypos + size yytext));
adamc@1 130
adamc@54 131 <INITIAL> "->" => (Tokens.ARROW (pos yypos, pos yypos + size yytext));
adamc@54 132 <INITIAL> "=>" => (Tokens.DARROW (pos yypos, pos yypos + size yytext));
adamc@54 133 <INITIAL> "++" => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext));
adamc@1 134
adamc@54 135 <INITIAL> "=" => (Tokens.EQ (pos yypos, pos yypos + size yytext));
adamc@54 136 <INITIAL> "," => (Tokens.COMMA (pos yypos, pos yypos + size yytext));
adamc@54 137 <INITIAL> ":::" => (Tokens.TCOLON (pos yypos, pos yypos + size yytext));
adamc@54 138 <INITIAL> "::" => (Tokens.DCOLON (pos yypos, pos yypos + size yytext));
adamc@54 139 <INITIAL> ":" => (Tokens.COLON (pos yypos, pos yypos + size yytext));
adamc@54 140 <INITIAL> "." => (Tokens.DOT (pos yypos, pos yypos + size yytext));
adamc@54 141 <INITIAL> "$" => (Tokens.DOLLAR (pos yypos, pos yypos + size yytext));
adamc@54 142 <INITIAL> "#" => (Tokens.HASH (pos yypos, pos yypos + size yytext));
adamc@54 143 <INITIAL> "__" => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext));
adamc@54 144 <INITIAL> "_" => (Tokens.UNDER (pos yypos, pos yypos + size yytext));
adamc@1 145
adamc@54 146 <INITIAL> "con" => (Tokens.CON (pos yypos, pos yypos + size yytext));
adamc@54 147 <INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
adamc@54 148 <INITIAL> "val" => (Tokens.VAL (pos yypos, pos yypos + size yytext));
adamc@54 149 <INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext));
adamc@67 150 <INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
adamc@1 151
adamc@54 152 <INITIAL> "structure" => (Tokens.STRUCTURE (pos yypos, pos yypos + size yytext));
adamc@54 153 <INITIAL> "signature" => (Tokens.SIGNATURE (pos yypos, pos yypos + size yytext));
adamc@54 154 <INITIAL> "struct" => (Tokens.STRUCT (pos yypos, pos yypos + size yytext));
adamc@54 155 <INITIAL> "sig" => (if yypos = 2 then initialSig () else (); Tokens.SIG (pos yypos, pos yypos + size yytext));
adamc@54 156 <INITIAL> "end" => (Tokens.END (pos yypos, pos yypos + size yytext));
adamc@54 157 <INITIAL> "functor" => (Tokens.FUNCTOR (pos yypos, pos yypos + size yytext));
adamc@54 158 <INITIAL> "where" => (Tokens.WHERE (pos yypos, pos yypos + size yytext));
adamc@54 159 <INITIAL> "extern" => (Tokens.EXTERN (pos yypos, pos yypos + size yytext));
adamc@58 160 <INITIAL> "include" => (Tokens.INCLUDE (pos yypos, pos yypos + size yytext));
adamc@58 161 <INITIAL> "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext));
adamc@30 162
adamc@54 163 <INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
adamc@54 164 <INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
adamc@82 165 <INITIAL> "Unit" => (Tokens.KUNIT (pos yypos, pos yypos + size yytext));
adamc@1 166
adamc@54 167 <INITIAL> {id} => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext));
adamc@54 168 <INITIAL> {cid} => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext));
adamc@1 169
adamc@14 170 <INITIAL> {intconst} => (case Int64.fromString yytext of
adamc@54 171 SOME x => Tokens.INT (x, pos yypos, pos yypos + size yytext)
adamc@54 172 | NONE => (ErrorMsg.errorAt' (pos yypos, pos yypos)
adamc@14 173 ("Expected int, received: " ^ yytext);
adamc@14 174 continue ()));
adamc@14 175 <INITIAL> {realconst} => (case Real64.fromString yytext of
adamc@54 176 SOME x => Tokens.FLOAT (x, pos yypos, pos yypos + size yytext)
adamc@54 177 | NONE => (ErrorMsg.errorAt' (pos yypos, pos yypos)
adamc@14 178 ("Expected float, received: " ^ yytext);
adamc@14 179 continue ()));
adamc@14 180
adamc@1 181 <COMMENT> . => (continue());
adamc@1 182
adamc@54 183 <INITIAL> . => (ErrorMsg.errorAt' (pos yypos, pos yypos)
adamc@1 184 ("illegal character: \"" ^ yytext ^ "\"");
adamc@1 185 continue ());