Lexer et Parser

Makefile.in

@@ -59,7 +59,7 @@ COQDEP = @COQDEP@
 COQLIB = "@COQLIB@"
 COQVER = @COQVER@
 
-GENERATED = src/version.ml 
+GENERATED = src/version.ml src/parser.mli src/parser.ml src/lexer.ml
 
 # main targets
 ##############
@@ -90,7 +90,8 @@ check: $(BINARY) $(PRELUDE)
 
 LIBCMO = lib/pp.cmo lib/loc.cmo
 
-CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo
+CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo \
+      src/parser.cmo src/lexer.cmo
 CMX = $(CMO:.cmo=.cmx)
 
 bin/why.opt: $(CMX) 

src/lexer.mll

+
+{
+  open Lexing
+  open Ptree
+  open Parser
+
+  let keywords = Hashtbl.create 97
+  let () = 
+    List.iter 
+      (fun (x,y) -> Hashtbl.add keywords x y)
+      [ "absurd", ABSURD;
+	"and", AND;
+        "array", ARRAY;
+	"as", AS;
+	"assert", ASSERT;
+	"axiom", AXIOM;
+	"begin", BEGIN;
+        "bool", BOOL;
+        "check", CHECK;
+	"do", DO;
+	"done", DONE;
+        "else", ELSE;
+	"end", END;
+	"exception", EXCEPTION; 
+	"exists", EXISTS;
+	"external", EXTERNAL;
+        "false", FALSE;
+	"for", FOR;
+	"forall", FORALL;
+	"fun", FUN;
+	"function", FUNCTION;
+	"goal", GOAL;
+	"if", IF;
+	"in", IN;
+	"include", INCLUDE;
+	"inductive", INDUCTIVE;
+	"int", INT;
+	"invariant", INVARIANT;
+	"let", LET;
+	"logic", LOGIC;
+	"match", MATCH;
+	"not", NOT;
+	"of", OF;
+	"or", OR;
+	"parameter", PARAMETER;
+	"predicate", PREDICATE;
+	"prop", PROP;
+	"raise", RAISE;
+	"raises", RAISES;
+	"reads", READS;
+	"real", REAL;
+	"rec", REC;
+	"ref", REF;
+	"returns", RETURNS;
+	"then", THEN;
+	"true", TRUE;
+	"try", TRY;
+	"type", TYPE;
+	"unit", UNIT;
+	"variant", VARIANT;
+	"void", VOID;
+	"while", WHILE;
+	"with", WITH;
+        "writes", WRITES ]
+	       
+  let newline lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <- 
+      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
+
+  let string_buf = Buffer.create 1024
+
+  exception Lexical_error of string
+
+  let char_for_backslash = function
+    | 'n' -> '\n'
+    | 't' -> '\t'
+    | c -> c
+
+  let update_loc lexbuf file line chars =
+    let pos = lexbuf.lex_curr_p in
+    let new_file = match file with None -> pos.pos_fname | Some s -> s in
+    lexbuf.lex_curr_p <- 
+      { pos with
+	  pos_fname = new_file;
+	  pos_lnum = int_of_string line;
+	  pos_bol = pos.pos_cnum - int_of_string chars;
+      }
+
+  let remove_leading_plus s =
+    let n = String.length s in 
+    if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s
+
+  let option_app f = function None -> None | Some x -> Some (f x)
+
+}
+
+let newline = '\n'
+let space = [' ' '\t' '\r']
+let alpha = ['a'-'z' 'A'-'Z']
+let letter = alpha | '_'
+let digit = ['0'-'9']
+let ident = letter (letter | digit | '\'')*
+let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
+(*
+let hexafloat = '0' ['x' 'X'] (hexadigit* '.' hexadigit+ | hexadigit+ '.' hexadigit* ) ['p' 'P'] ['-' '+']? digit+
+  *)
+
+rule token = parse
+  | "#" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
+    space* (digit+ as line) space* (digit+ as char) space* "#"
+      { update_loc lexbuf file line char; token lexbuf }
+  | newline 
+      { newline lexbuf; token lexbuf }
+  | space+  
+      { token lexbuf }
+  | ident as id  
+      { try Hashtbl.find keywords id with Not_found -> IDENT id }
+  | digit+ as s
+      { INTEGER s }
+  | (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)
+  | (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
+  | (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?
+      { FLOAT (RConstDecimal (i, f, option_app remove_leading_plus e)) }
+  | '0' ['x' 'X'] ((hexadigit* as i) '.' (hexadigit+ as f) 
+                  |(hexadigit+ as i) '.' (hexadigit* as f)
+		  |(hexadigit+ as i) ("" as f))
+    ['p' 'P'] (['-' '+']? digit+ as e)
+      { FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
+  | "(*"
+      { comment lexbuf; token lexbuf }
+  | "'"
+      { QUOTE }
+  | ","
+      { COMMA }
+  | "("
+      { LEFTPAR }
+  | ")"
+      { RIGHTPAR }
+  | "!"
+      { BANG }
+  | ":"
+      { COLON }
+  | ";"
+      { SEMICOLON }
+  | ":="
+      { COLONEQUAL }
+  | "->"
+      { ARROW }
+  | "<->"
+      { LRARROW }
+  | "="
+      { EQUAL }
+  | "<"
+      { LT }
+  | "<="
+      { LE }
+  | ">"
+      { GT }
+  | ">="
+      { GE }
+  | "<>"
+      { NOTEQ }
+  | "+"
+      { PLUS }
+  | "-"
+      { MINUS }
+  | "*"
+      { TIMES }
+  | "/"
+      { SLASH }
+  | "%"
+      { PERCENT }
+  | "@"
+      { AT }
+  | "."
+      { DOT }
+  | "["
+      { LEFTSQ }
+  | "]"
+      { RIGHTSQ }
+  | "{"
+      { LEFTB }
+  | "}"
+      { RIGHTB }
+  | "{{"
+      { LEFTBLEFTB }
+  | "}}"
+      { RIGHTBRIGHTB }
+  | "|"
+      { BAR }
+  | "||"
+      { BARBAR }
+  | "&&" 
+      { AMPAMP }
+  | "=>"
+      { BIGARROW }
+  | "\""
+      { Buffer.clear string_buf; string lexbuf }
+  | eof 
+      { EOF }
+  | _ as c
+      { raise (Lexical_error ("illegal character: " ^ String.make 1 c)) }
+
+and comment = parse
+  | "*)" 
+      { () }
+  | "(*" 
+      { comment lexbuf; comment lexbuf }
+  | newline 
+      { newline lexbuf; comment lexbuf }
+  | eof
+      { raise (Lexical_error "unterminated comment") }
+  | _ 
+      { comment lexbuf }
+
+and string = parse
+  | "\""
+      { STRING (Buffer.contents string_buf) }
+  | "\\" (_ as c)
+      { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
+  | newline 
+      { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
+  | eof
+      { raise (Lexical_error "unterminated string") }
+  | _ as c
+      { Buffer.add_char string_buf c; string lexbuf }
+
+
+
+{
+
+  let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
+
+  let with_location f lb =
+    try f lb with e -> raise (Loc.Located (loc lb, e))
+
+  let parse_lexpr = with_location (lexpr token)
+  let parse_logic_file = with_location (logic_file token)
+
+  let lexpr_of_string s = parse_lexpr (from_string s)
+}
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -j -C .. bin/why.byte"
+End: 
+*)
+

src/parser.mly

+
+%{
+
+  open Ptree
+  open Parsing
+
+  let loc () = (symbol_start_pos (), symbol_end_pos ())
+  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
+  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
+
+  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
+  let mk_pp d = mk_ppl (loc ()) d
+  let mk_pp_i i d = mk_ppl (loc_i i) d
+		    
+  let infix_ppl loc a i b = mk_ppl loc (PPinfix (a, i, b))
+  let infix_pp a i b = infix_ppl (loc ()) a i b
+
+  let prefix_ppl loc p a = mk_ppl loc (PPprefix (p, a))
+  let prefix_pp p a = prefix_ppl (loc ()) p a
+
+(***
+  let with_loc loc d = { pdesc = d; ploc = loc }
+  let locate d = with_loc (loc ()) d
+  let locate_i i d = with_loc (loc_i i) d
+
+  let rec_name = function Srec (x,_,_,_,_,_) -> x | _ -> assert false
+
+  let join (b,_) (_,e) = (b,e)
+
+  let rec app f = function
+    | [] -> 
+	assert false
+    | [a] -> 
+	Sapp (f, a)
+    | a :: l -> 
+	let loc = join f.ploc a.ploc in 
+	app (with_loc loc (Sapp (f, a))) l
+
+  let bin_op (loc_op,op) e1 e2 =
+    let f = with_loc loc_op (Svar op) in
+    let f_e1 = with_loc (join e1.ploc loc_op) (Sapp (f, e1)) in
+    locate (Sapp (f_e1, e2))
+      
+  let un_op (loc_op,op) e =
+    locate (app (with_loc loc_op (Svar op)) [e])
+
+  let ptype_c_of_v v =
+    { pc_result_name = Ident.result;
+      pc_result_type = v;
+      pc_effect = { pe_reads = []; pe_writes = []; pe_raises = [] };
+      pc_pre = []; 
+      pc_post = None }
+
+  let list_of_some = function None -> [] | Some x -> [x]
+
+  (*s ensures a postcondition for a function body *)
+
+  let force_function_post ?(warn=false) e = match e.pdesc with
+    | Spost _ -> 
+	e
+    | _ -> 
+       if warn then 
+	 Format.eprintf 
+	   "%ano postcondition for this function; true inserted@\n"
+	   Loc.report_position e.ploc; 
+       let q = 
+	 { pa_name = Anonymous; pa_value = mk_pp PPtrue; pa_loc = loc () }
+       in
+       { e with pdesc = Spost (e, (q, []), Transparent) }
+***)
+%}
+
+/* Tokens */ 
+
+%token <string> IDENT
+%token <string> INTEGER
+%token <Ptree.real_constant> FLOAT
+%token <string> STRING
+%token ABSURD AMPAMP AND ARRAY ARROW AS ASSERT AT AXIOM 
+%token BANG BAR BARBAR BEGIN 
+%token BIGARROW BOOL CHECK COLON COLONEQUAL COMMA DO DONE DOT ELSE END EOF EQUAL
+%token EXCEPTION EXISTS EXTERNAL FALSE FOR FORALL FPI FUN FUNCTION GE GOAL GT
+%token IF IN INCLUDE INDUCTIVE INT INVARIANT
+%token LE LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LET LOGIC LRARROW LT MATCH MINUS
+%token NOT NOTEQ OF OR PARAMETER PERCENT PLUS PREDICATE PROP 
+%token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB
+%token RIGHTPAR RIGHTSQ 
+%token SEMICOLON SLASH 
+%token THEN TIMES TRUE TRY TYPE UNIT VARIANT VOID WHILE WITH WRITES
+
+/* Precedences */
+
+%nonassoc prec_recfun
+%nonassoc prec_fun
+%left LEFTB LEFTBLEFTB
+%left prec_simple
+
+%left COLON 
+
+%left prec_letrec
+%left IN
+
+%right SEMICOLON
+
+%left prec_no_else
+%left ELSE
+
+%right prec_named
+%left COLONEQUAL
+%right prec_forall prec_exists
+%right ARROW LRARROW
+%right OR BARBAR
+%right AND AMPAMP
+%right NOT
+%right prec_if
+%left prec_relation EQUAL NOTEQ LT LE GT GE
+%left PLUS MINUS
+%left TIMES SLASH PERCENT
+%right uminus
+%left prec_app
+%left prec_ident
+%left LEFTSQ
+
+/* Entry points */
+
+%type <Ptree.lexpr> lexpr
+%start lexpr
+%type <Ptree.logic_file> logic_file
+%start logic_file
+%%
+
+logic_file:
+| list1_decl EOF 
+   { $1 }
+| EOF 
+   { [] }
+;
+
+list1_decl:
+| decl 
+   { [$1] }
+| decl list1_decl 
+   { $1 :: $2 }
+;
+
+decl:
+| external_ LOGIC list1_ident_sep_comma COLON logic_type
+   { Logic (loc_i 3, $1, $3, $5) }
+| AXIOM ident COLON lexpr
+   { Axiom (loc (), $2, $4) }
+| PREDICATE ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr
+   { Predicate_def (loc (), $2, $4, $7) }
+| INDUCTIVE ident COLON logic_type inddefn
+   { Inductive_def (loc (), $2, $4, $5) }
+| FUNCTION ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON 
+  primitive_type EQUAL lexpr
+   { Function_def (loc (), $2, $4, $7, $9) }
+| GOAL ident COLON lexpr
+   { Goal (loc (), $2, $4) }
+| EXTERNAL TYPE typedecl
+   { let loc, vl, id = $3 in TypeDecl (loc, true, vl, id) }
+| TYPE typedecl typedefn
+   { let loc, vl, id = $2 in $3 loc vl id }
+;
+
+typedecl:
+| ident
+    { (loc_i 1, [], $1) }
+| type_var ident
+    { (loc_i 2, [$1], $2) }
+| LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR ident
+    { (loc_i 6, $2 :: $4, $6) }
+;
+
+typedefn:
+| /* epsilon */
+    { fun loc vl id -> TypeDecl (loc, false, vl, id) }
+| EQUAL bar_ typecases typecont
+    { fun loc vl id -> AlgType ((loc, vl, id, $3) :: $4) }
+;
+
+typecont:
+| /* epsilon */
+    { [] }
+| AND typedecl EQUAL bar_ typecases typecont
+    { let loc, vl, id = $2 in (loc, vl, id, $5) :: $6 }
+;
+
+typecases:
+| typecase                { [$1] }
+| typecase BAR typecases  { $1::$3 }
+;
+
+typecase:
+| ident
+    { (loc_i 1,$1,[]) }
+| ident LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
+    { (loc_i 1,$1,$3) }
+;
+
+inddefn:
+| /* epsilon */       { [] }
+| EQUAL bar_ indcases { $3 }
+;
+
+indcases:
+| indcase               { [$1] }
+| indcase BAR indcases  { $1::$3 }
+;
+
+indcase:
+| ident COLON lexpr { (loc_i 1,$1,$3) }
+;
+
+primitive_type:
+| INT 
+   { PPTint }
+| BOOL 
+   { PPTbool }
+| REAL 
+   { PPTreal }
+| UNIT 
+   { PPTunit }
+| type_var 
+   { PPTvarid ($1, loc ()) }
+| ident 
+   { PPTexternal ([], $1, loc ()) }
+| primitive_type ident
+   { PPTexternal ([$1], $2, loc_i 2) }
+| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR ident
+   { PPTexternal ($2 :: $4, $6, loc_i 6) }
+/*
+| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
+   { match $2 with [p] -> p | _ -> raise Parse_error }
+*/
+;
+
+
+logic_type:
+| list0_primitive_type_sep_comma ARROW PROP
+   { PPredicate $1 }
+| PROP
+   { PPredicate [] }
+| list0_primitive_type_sep_comma ARROW primitive_type
+   { PFunction ($1, $3) }
+| primitive_type
+   { PFunction ([], $1) }
+;
+
+list0_primitive_type_sep_comma:
+| /* epsilon */                  { [] }
+| list1_primitive_type_sep_comma { $1 }
+;
+
+list1_primitive_type_sep_comma:
+| primitive_type                                      { [$1] }
+| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
+;
+
+list0_logic_binder_sep_comma:
+| /* epsilon */                { [] }
+| list1_logic_binder_sep_comma { $1 }
+;
+
+list1_logic_binder_sep_comma:
+| logic_binder                                    { [$1] }
+| logic_binder COMMA list1_logic_binder_sep_comma { $1 :: $3 }
+;
+
+logic_binder:
+| ident COLON primitive_type       
+    { (loc_i 1, $1, $3) }
+/***
+| ident COLON primitive_type ARRAY 
+    { (loc_i 1, $1, PPTexternal ([$3], Ident.farray, loc_i 3)) }
+***/
+;
+
+external_:
+| /* epsilon */ { false }
+| EXTERNAL      { true  }
+;
+
+lexpr:
+| lexpr ARROW lexpr 
+   { infix_pp $1 PPimplies $3 }
+| lexpr LRARROW lexpr 
+   { infix_pp $1 PPiff $3 }
+| lexpr OR lexpr 
+   { infix_pp $1 PPor $3 }
+| lexpr AND lexpr 
+   { infix_pp $1 PPand $3 }
+| NOT lexpr 
+   { prefix_pp PPnot $2 }
+| lexpr relation lexpr %prec prec_relation
+   { infix_pp $1 $2 $3 }
+| lexpr PLUS lexpr
+   { infix_pp $1 PPadd $3 }
+| lexpr MINUS lexpr
+   { infix_pp $1 PPsub $3 }
+| lexpr TIMES lexpr
+   { infix_pp $1 PPmul $3 }
+| lexpr SLASH lexpr
+   { infix_pp $1 PPdiv $3 }
+| lexpr PERCENT lexpr
+   { infix_pp $1 PPmod $3 }
+| MINUS lexpr %prec uminus
+   { prefix_pp PPneg $2 }
+/***
+| qualid_ident
+   { mk_pp (PPvar $1) }
+| qualid_ident LEFTPAR list1_lexpr_sep_comma RIGHTPAR
+   { mk_pp (PPapp ($1, $3)) }
+| qualid_ident LEFTSQ lexpr RIGHTSQ
+   { mk_pp (PPapp (Ident.access, [mk_pp_i 1 (PPvar $1); $3])) }
+***/
+| IF lexpr THEN lexpr ELSE lexpr %prec prec_if 
+   { mk_pp (PPif ($2, $4, $6)) }
+| FORALL list1_ident_sep_comma COLON primitive_type triggers 
+  DOT lexpr %prec prec_forall
+   { let rec mk = function
+       | [] -> assert false
+       | [id] -> mk_pp (PPforall (id, $4, $5, $7))
+       | id :: l -> mk_pp (PPforall (id, $4, [], mk l))
+     in
+     mk $2 }
+| EXISTS ident COLON primitive_type DOT lexpr %prec prec_exists
+   { mk_pp (PPexists ($2, $4, $6)) }
+| INTEGER
+   { mk_pp (PPconst (ConstInt $1)) }
+| FLOAT
+   { mk_pp (PPconst (ConstFloat $1)) }
+| TRUE
+   { mk_pp PPtrue }
+| FALSE
+   { mk_pp PPfalse }    
+/***
+| VOID
+   { mk_pp (PPconst ConstUnit) }
+***/
+| LEFTPAR lexpr RIGHTPAR
+   { $2 }
+| ident_or_string COLON lexpr %prec prec_named
+   { mk_pp (PPnamed ($1, $3)) }
+| LET ident EQUAL lexpr IN lexpr 
+   { mk_pp (PPlet ($2, $4, $6)) }
+| MATCH lexpr WITH bar_ match_cases END
+   { mk_pp (PPmatch ($2, $5)) }
+;
+
+match_cases:
+| match_case                  { [$1] }
+| match_case BAR match_cases  { $1::$3 }
+;
+
+match_case:
+| pattern ARROW lexpr { ($1,$3) }
+;
+