Commit 77d2322b authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

nettoyage lexer et parser

parent 092ca94c
......@@ -67,7 +67,9 @@ COQVER = @COQVER@
GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \
src/parser/lexer.ml src/output/driver_lexer.ml \
src/output/driver_parser.mli src/output/driver_parser.ml
src/output/driver_parser.mli src/output/driver_parser.ml \
src/programs/pgm_lexer.ml src/programs/pgm_parser.mli \
src/programs/pgm_parser.ml
# main targets
##############
......@@ -149,7 +151,7 @@ test: bin/why.byte
# programs
##########
PGM_CMO := pgm_main.cmo
PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_main.cmo
PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) \
......
......@@ -33,3 +33,5 @@ val string : Lexing.lexbuf -> string
val report : Format.formatter -> error -> unit
val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
val remove_leading_plus : string -> string
......@@ -42,60 +42,36 @@
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[ "absurd", ABSURD;
[
"and", AND;
"as", AS;
"assert", ASSERT;
"axiom", AXIOM;
"begin", BEGIN;
"check", CHECK;
"clone", CLONE;
"do", DO;
"done", DONE;
"else", ELSE;
"else", ELSE;
"end", END;
"exception", EXCEPTION;
"exists", EXISTS;
"export", EXPORT;
"external", EXTERNAL;
"false", FALSE;
"for", FOR;
"forall", FORALL;
"fun", FUN;
"goal", GOAL;
"if", IF;
"import", IMPORT;
"in", IN;
"inductive", INDUCTIVE;
"invariant", INVARIANT;
"lemma", LEMMA;
"let", LET;
"logic", LOGIC;
"match", MATCH;
"namespace", NAMESPACE;
"not", NOT;
"of", OF;
"or", OR;
"parameter", PARAMETER;
"prop", PROP;
"raise", RAISE;
"raises", RAISES;
"reads", READS;
"rec", REC;
"ref", REF;
"returns", RETURNS;
"then", THEN;
"theory", THEORY;
"true", TRUE;
"try", TRY;
"type", TYPE;
"unit", UNIT;
"use", USE;
"variant", VARIANT;
"void", VOID;
"while", WHILE;
"with", WITH;
"writes", WRITES ]
]
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
......@@ -123,8 +99,6 @@
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'
......@@ -166,7 +140,7 @@ rule token = parse
| (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)) }
{ FLOAT (RConstDecimal (i, f, Util.option_map remove_leading_plus e)) }
| '0' ['x' 'X'] ((hexadigit* as i) '.' (hexadigit+ as f)
|(hexadigit+ as i) '.' (hexadigit* as f)
|(hexadigit+ as i) ("" as f))
......@@ -214,18 +188,8 @@ rule token = parse
{ LEFTB }
| "}"
{ RIGHTB }
| "{{"
{ LEFTBLEFTB }
| "}}"
{ RIGHTBRIGHTB }
| "|"
{ BAR }
| "||"
{ BARBAR }
| "&&"
{ AMPAMP }
| "=>"
{ BIGARROW }
| "\""
{ STRING (string lexbuf) }
| eof
......
......@@ -42,56 +42,6 @@
let prefix s = "prefix " ^ s
let postfix s = "postfix " ^ s
(***
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 */
......@@ -101,21 +51,34 @@
%token <string> OP0 OP1 OP2 OP3
%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 CHECK CLONE COLON COLONEQUAL COMMA DO
%token DONE DOT ELSE END EOF EQUAL
%token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI
%token FUN GOAL
%token IF IMPORT IN INCLUDE INDUCTIVE INVARIANT
%token LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA
%token LET LOGIC LRARROW MATCH
%token NAMESPACE NOT OF OR PARAMETER PROP
%token QUOTE RAISE RAISES READS REC REF RETURNS RIGHTB RIGHTBRIGHTB
/* keywords */
%token AND AS AXIOM
%token CLONE
%token ELSE END EXISTS EXPORT FALSE FORALL
%token GOAL
%token IF IMPORT IN INDUCTIVE LEMMA
%token LET LOGIC MATCH
%token NAMESPACE NOT OR
%token THEN THEORY TRUE TYPE
%token USE WITH
/* symbols */
%token ARROW AT
%token BANG BAR
%token COLON COLONEQUAL COMMA
%token DOT EQUAL
%token LEFTB LEFTPAR LEFTSQ
%token LRARROW
%token QUOTE RIGHTB
%token RIGHTPAR RIGHTSQ
%token SEMICOLON
%token THEN THEORY TRUE TRY TYPE UNDERSCORE
%token UNIT USE VARIANT VOID WHILE WITH WRITES
%token UNDERSCORE
%token EOF
/* Precedences */
......@@ -138,8 +101,8 @@
%left COLONEQUAL
%right prec_quant
%right ARROW LRARROW
%right OR BARBAR
%right AND AMPAMP
%right OR
%right AND
%right NOT
%right prec_if
%left EQUAL OP0
......@@ -567,333 +530,3 @@ subst:
| GOAL qualid { CSgoal $2 }
;
/******* programs **************************************************
qualid_ident:
| IDENT { $1, None }
| IDENT AT { $1, Some "" }
| IDENT AT IDENT { $1, Some $3 }
;
list0_ident_sep_comma:
| /* epsilon * / { [] }
| list1_ident_sep_comma { $1 }
;
decl:
| INCLUDE STRING
{ Include (loc_i 2,$2) }
| LET ident EQUAL expr
{ Program (loc_i 2,$2, $4) }
| LET ident binders EQUAL list0_bracket_assertion expr
{ Program (loc_i 2,$2, locate (Slam ($3, $5, force_function_post $6))) }
| LET REC recfun
{ let (loc,p) = $3 in Program (loc,rec_name p, locate p) }
| EXCEPTION ident
{ Exception (loc (), $2, None) }
| EXCEPTION ident OF primitive_type
{ Exception (loc (), $2, Some $4) }
| external_ PARAMETER list1_ident_sep_comma COLON type_v
{ Parameter (loc_i 3, $1, $3, $5) }
type_v:
| simple_type_v ARROW type_c
{ PVarrow ([Ident.anonymous, $1], $3) }
| ident COLON simple_type_v ARROW type_c
{ PVarrow ([($1, $3)], $5) }
| simple_type_v
{ $1 }
;
simple_type_v:
| primitive_type ARRAY { PVref (PPTexternal ([$1], Ident.farray, loc_i 2)) }
| primitive_type REF { PVref $1 }
| primitive_type { PVpure $1 }
| LEFTPAR type_v RIGHTPAR { $2 }
;
type_c:
| LEFTB opt_assertion RIGHTB result effects LEFTB opt_post_condition RIGHTB
{ let id,v = $4 in
{ pc_result_name = id; pc_result_type = v;
pc_effect = $5; pc_pre = list_of_some $2; pc_post = $7 } }
| type_v
{ ptype_c_of_v $1 }
;
result:
| RETURNS ident COLON type_v { $2, $4 }
| type_v { Ident.result, $1 }
;
effects:
| opt_reads opt_writes opt_raises
{ { pe_reads = $1; pe_writes = $2; pe_raises = $3 } }
;
opt_reads:
| /* epsilon * / { [] }
| READS list0_ident_sep_comma { $2 }
;
opt_writes:
| /* epsilon * / { [] }
| WRITES list0_ident_sep_comma { $2 }
;
opt_raises:
| /* epsilon * / { [] }
| RAISES list0_ident_sep_comma { $2 }
;
opt_assertion:
| /* epsilon * / { None }
| assertion { Some $1 }
;
assertion:
| lexpr
{ { pa_name = Anonymous; pa_value = $1; pa_loc = loc () } }
| lexpr AS ident
{ { pa_name = Name $3; pa_value = $1; pa_loc = loc () } }
;
opt_post_condition:
| /* epsilon * / { None }
| post_condition { Some $1 }
;
post_condition:
| assertion
{ $1, [] }
| assertion BAR list1_exn_condition_sep_bar
{ $1, $3 }
| BAR list1_exn_condition_sep_bar
{ Format.eprintf "%awarning: no postcondition; false inserted@\n"
Loc.report_position (loc ());
(* if Options.werror then exit 1; *)
({ pa_name = Anonymous; pa_value = mk_pp PPfalse; pa_loc = loc () }, $2) }
;
bracket_assertion:
| LEFTB assertion RIGHTB { $2 }
;
list1_bracket_assertion:
| bracket_assertion { [$1] }
| bracket_assertion list1_bracket_assertion { $1 :: $2 }
;
list0_bracket_assertion:
| /* epsilon * / { [] }
| LEFTB RIGHTB { [] }
| list1_bracket_assertion { $1 }
;
list1_exn_condition_sep_bar:
| exn_condition { [$1] }
| exn_condition BAR list1_exn_condition_sep_bar { $1 :: $3 }
;
exn_condition:
| ident BIGARROW assertion { $1,$3 }
;
expr:
| simple_expr %prec prec_simple
{ $1 }
| ident COLONEQUAL expr
{ locate
(Sapp (locate (Sapp (locate (Svar Ident.ref_set),
locate_i 1 (Svar $1))),
$3)) }
| ident LEFTSQ expr RIGHTSQ COLONEQUAL expr
{ locate
(Sapp (locate
(Sapp (locate
(Sapp (locate (Svar Ident.array_set),
locate_i 1 (Svar $1))),
$3)),
$6)) }
| IF expr THEN expr ELSE expr
{ locate (Sif ($2, $4, $6)) }
| IF expr THEN expr %prec prec_no_else
{ locate (Sif ($2, $4, locate (Sconst ConstUnit))) }
| WHILE expr DO invariant_variant expr DONE
{ (* syntactic suget for
try loop { invariant variant } if b then e else raise Exit
with Exit -> void end *)
let inv,var = $4 in
locate
(Stry
(locate
(Sloop (inv, var,
locate
(Sif ($2, $5,
locate (Sraise (exit_exn, None, None)))))),
[((exit_exn, None), locate (Sconst ConstUnit))])) }
| IDENT COLON expr
{ locate (Slabel ($1, $3)) }
| LET ident EQUAL expr IN expr
{ locate (Sletin ($2, $4, $6)) }
| LET ident EQUAL REF expr IN expr
{ locate (Sletref ($2, $5, $7)) }
| FUN binders ARROW list0_bracket_assertion expr %prec prec_fun
{ locate (Slam ($2, $4, force_function_post $5)) }
| LET ident binders EQUAL list0_bracket_assertion expr IN expr
{ let b = force_function_post ~warn:true $6 in
locate (Sletin ($2, locate (Slam ($3, $5, b)), $8)) }
| LET REC recfun %prec prec_letrec
{ let _loc,p = $3 in locate p }
| LET REC recfun IN expr
{ let _loc,p = $3 in locate (Sletin (rec_name p, locate p, $5)) }
| RAISE ident opt_cast
{ locate (Sraise ($2, None, $3)) }
| RAISE LEFTPAR ident expr RIGHTPAR opt_cast
{ locate (Sraise ($3, Some $4 , $6)) }
| TRY expr WITH bar_ list1_handler_sep_bar END
{ locate (Stry ($2, $5)) }
| ABSURD opt_cast
{ locate (Sabsurd $2) }
| simple_expr list1_simple_expr %prec prec_app
{ locate (app $1 $2) }
| expr BARBAR expr
{ locate (Slazy_or ($1, $3))
(* let ptrue = locate (Sconst (ConstBool true)) in
locate (Sif ($1, ptrue, $3)) *) }
| expr AMPAMP expr
{ locate (Slazy_and ($1, $3))
(* let pf = locate (Sconst (ConstBool false)) in
locate (Sif ($1, $3, pf)) *) }
| NOT expr
{ locate (Snot $2)
(* let pf = locate (Sconst (ConstBool false)) in
let pt = locate (Sconst (ConstBool true)) in
locate (Sif ($2, pf, pt)) *) }
| expr relation_id expr %prec prec_relation
{ bin_op $2 $1 $3 }
| expr PLUS expr
{ bin_op (loc_i 2, Ident.t_add) $1 $3 }
| expr MINUS expr
{ bin_op (loc_i 2, Ident.t_sub) $1 $3 }
| expr TIMES expr
{ bin_op (loc_i 2, Ident.t_mul) $1 $3 }
| expr SLASH expr
{ bin_op (loc_i 2, Ident.t_div) $1 $3 }
| expr PERCENT expr
{ bin_op (loc_i 2, Ident.t_mod_int) $1 $3 }
| MINUS expr %prec uminus
{ un_op (loc_i 1, Ident.t_neg) $2 }
| expr SEMICOLON expr
{ locate (Sseq ($1, $3)) }
| ASSERT list1_bracket_assertion SEMICOLON expr
{ locate (Sassert (`ASSERT,$2, $4)) }
| CHECK list1_bracket_assertion SEMICOLON expr
{ locate (Sassert (`CHECK,$2, $4)) }
| expr LEFTB post_condition RIGHTB
{ locate (Spost ($1, $3, Transparent)) }
| expr LEFTBLEFTB post_condition RIGHTBRIGHTB
{ locate (Spost ($1, $3, Opaque)) }
;
simple_expr:
| ident %prec prec_ident
{ locate (Svar $1) }
| INTEGER
{ locate (Sconst (ConstInt $1)) }
| FLOAT
{ let f = $1 in locate (Sconst (ConstFloat f)) }
| VOID
{ locate (Sconst ConstUnit) }
| TRUE
{ locate (Sconst (ConstBool true)) }
| FALSE
{ locate (Sconst (ConstBool false)) }
| BANG ident
{ locate (Sderef $2) }
| ident LEFTSQ expr RIGHTSQ
{ locate
(Sapp (locate (Sapp (locate (Svar Ident.array_get),
locate_i 1 (Svar $1))),
$3)) }
| LEFTSQ type_c RIGHTSQ
{ locate (Sany $2) }
| LEFTPAR expr RIGHTPAR
{ $2 }
| BEGIN expr END
{ $2 }
;
relation_id:
| LT { loc (), Ident.t_lt }
| LE { loc (), Ident.t_le }
| GT { loc (), Ident.t_gt }
| GE { loc (), Ident.t_ge }
| EQUAL { loc (), Ident.t_eq }
| NOTEQ { loc (), Ident.t_neq }
;
list1_simple_expr:
| simple_expr %prec prec_simple { [$1] }
| simple_expr list1_simple_expr { $1 :: $2 }
;
list1_handler_sep_bar:
| handler { [$1] }
| handler BAR list1_handler_sep_bar { $1 :: $3 }
;
handler:
| ident ARROW expr { (($1, None), $3) }
| ident ident ARROW expr { (($1, Some $2), $4) }
;
opt_cast:
| /* epsilon * / { None }
| COLON type_v { Some $2 }
;
invariant_variant:
| /* epsilon * / { None, None }
| LEFTB opt_invariant RIGHTB { $2, None }
| LEFTB opt_invariant VARIANT variant RIGHTB { $2, Some $4 }
;
opt_invariant:
| /* epsilon * / { None }
| INVARIANT assertion { Some $2 }
;
recfun:
| ident binders COLON type_v opt_variant EQUAL
list0_bracket_assertion expr %prec prec_recfun
{ (loc_i 1),Srec ($1, $2, $4, $5, $7, force_function_post $8) }
;
opt_variant:
| LEFTB VARIANT variant RIGHTB { Some $3 }
| /* epsilon * / { None }
;
variant:
| lexpr FOR ident { ($1, $3) }
| lexpr { ($1, Ident.t_zwf_zero) }
;
binders:
| list1_binder { List.flatten $1 }
;
list1_binder:
| binder { [$1] }
| binder list1_binder { $1 :: $2 }
;
binder:
| LEFTPAR RIGHTPAR
{ [Ident.anonymous, PVpure PPTunit] }
| LEFTPAR list1_ident_sep_comma COLON type_v RIGHTPAR
{ List.map (fun s -> (s, $4)) $2 }
;
****/
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
{
open Lexing
open Lexer
open Term
open Pgm_parser
let keywords = Hashtbl.create 97
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[ "absurd", ABSURD;
"and", AND;
"as", AS;
"assert", ASSERT;
"begin", BEGIN;
"check", CHECK;
"do", DO;
"done", DONE;