Skip to content

GitLab

why3
why3
Commit 6a159d62 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

programs are now parsed with src/parser/

parent 7d2eca12
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 88 additions and 1180 deletions
Makefile.in
View file @ 6a159d62
......@@ -282,10 +282,9 @@ install_no_local::
# Whyml
########
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_lexer.ml
PGMGENERATED =
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer \
PGM_FILES = pgm_ttree \
pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
modules/stdlib.mlw
View file @ 6a159d62
module Ref
{ use import programs.Prelude }
use import programs.Prelude
mutable type ref 'a model 'a
......
src/parser/lexer.mli
View file @ 6a159d62
......@@ -29,6 +29,8 @@ val parse_list0_decl :
val parse_lexpr : Lexing.lexbuf -> Ptree.lexpr
val parse_program_file : Lexing.lexbuf -> Ptree.program_file
(** other functions to be re-used in other lexers/parsers *)
val newline : Lexing.lexbuf -> unit
......
src/parser/lexer.mll
View file @ 6a159d62
......@@ -301,6 +301,8 @@ and string = parse
let parse_lexpr = with_location (lexpr_eof token)
let parse_program_file = with_location (program_file token)
let read_channel env file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
......
src/parser/parser.pre.mly
View file @ 6a159d62
......@@ -1144,6 +1144,7 @@ simple_type_c:
;
annotation:
| LEFTBRC RIGHTBRC { mk_pp PPtrue }
| LEFTBRC lexpr RIGHTBRC { $2 }
;
......
src/programs/pgm_lexer.mll deleted 100644 → 0
View file @ 7d2eca12
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* 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 Format
open Lexing
open Why
open Lexer
open Term
open Pgm_parser
exception UnterminatedLogic
exception IllegalCharacter of char
let () = Exn_printer.register (fun fmt exn -> match exn with
| UnterminatedLogic -> fprintf fmt "unterminated logic block"
| IllegalCharacter c -> fprintf fmt "illegal character %c" c
| Parsing.Parse_error -> fprintf fmt "syntax error"
| _ -> raise exn)
let keywords = Hashtbl.create 97
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[ "absurd", ABSURD;
"and", AND;
"any", ANY;
"as", AS;
"assert", ASSERT;
"assume", ASSUME;
"begin", BEGIN;
"check", CHECK;
"do", DO;
"done", DONE;
"downto", DOWNTO;
"else", ELSE;
"export", EXPORT;
"end", END;
"exception", EXCEPTION;
"for", FOR;
"fun", FUN;
"ghost", GHOST;
"if", IF;
"import", IMPORT;
"in", IN;
"invariant", INVARIANT;
"label", LABEL;
"let", LET;
"match", MATCH;
"model", MODEL;
"module", MODULE;
"mutable", MUTABLE;
"namespace", NAMESPACE;
"not", NOT;
"of", OF;
"parameter", PARAMETER;
"raise", RAISE;
"raises", RAISES;
"reads", READS;
"rec", REC;
"then", THEN;
"to", TO;
"try", TRY;
"type", TYPE;
"use", USE;
"variant", VARIANT;
"while", WHILE;
"with", WITH;
"writes", WRITES;
]
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 logic_start_loc = ref Loc.dummy_position
let logic_buffer = Buffer.create 1024
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
}
let newline = '\n'
let space = [' ' '\t' '\r']
let lalpha = ['a'-'z' '_']
let ualpha = ['A'-'Z']
let alpha = lalpha | ualpha
let digit = ['0'-'9']
let lident = lalpha (alpha | digit | '\'')*
let uident = ualpha (alpha | digit | '\'')*
let decimal_literal =
['0'-'9'] ['0'-'9' '_']*
let hex_literal =
'0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']*
let oct_literal =
'0' ['o' 'O'] ['0'-'7'] ['0'-'7' '_']*
let bin_literal =
'0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']*
let int_literal =
decimal_literal | hex_literal | oct_literal | bin_literal
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
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 }
| '_'
{ UNDERSCORE }
| lident as id
{ try Hashtbl.find keywords id with Not_found -> LIDENT id }
| uident as id
{ UIDENT id }
| int_literal 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))?
{ REAL (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))
['p' 'P'] (['-' '+']? digit+ as e)
{ REAL (RConstHexa (i, f, remove_leading_plus e)) }
| "(*)"
{ LEFTPAR_STAR_RIGHTPAR }
| "(*"
{ comment lexbuf; token lexbuf }
| "'"
{ QUOTE }
| "`"
{ BACKQUOTE }
| ","
{ COMMA }
| "("
{ LEFTPAR }
| ")"
{ RIGHTPAR }
| ":"
{ COLON }
| ";"
{ SEMICOLON }
| ":="
{ COLONEQUAL }
| "->"
{ ARROW }
| "="
{ EQUAL }
| "<>"
{ LTGT }
| "@"
{ AT }
| "."
{ DOT }
| "["
{ LEFTSQ }
| "]"
{ RIGHTSQ }
| "{"
{ logic_start_loc := loc lexbuf;
let s = logic lexbuf in
LOGIC ((fst !logic_start_loc, snd (loc lexbuf)), s) }
(* FIXME: allow newlines as well *)
| "{" space* "}"
{ LOGIC (loc lexbuf, "true") }
| "{{"
{ LEFTBLEFTB }
| "}}"
{ RIGHTBRIGHTB }
| "|"
{ BAR }
| "||"
{ BARBAR }
| "&&"
{ AMPAMP }
| op_char_pref op_char_4* as s
{ OPPREF s }
| op_char_1234* op_char_1 op_char_1234* as s
{ OP1 s }
| op_char_234* op_char_2 op_char_234* as s
{ OP2 s }
| op_char_34* op_char_3 op_char_34* as s
{ OP3 s }
| op_char_4+ as s
{ OP4 s }
| "\""
{ STRING (string lexbuf) }
| eof
{ EOF }
| _ as c
{ raise (IllegalCharacter c) }
and logic = parse
| "}"
{ let s = Buffer.contents logic_buffer in
Buffer.clear logic_buffer;
s }
| newline
{ newline lexbuf; Buffer.add_char logic_buffer '\n'; logic lexbuf }
| eof
{ raise (Loc.Located (!logic_start_loc, UnterminatedLogic)) }
| _ as c
{ Buffer.add_char logic_buffer c; logic lexbuf }
{
let parse_file = with_location (file token)
}
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
src/programs/pgm_main.ml
View file @ 6a159d62
......@@ -24,13 +24,14 @@ open Why
open Util
open Ident
open Ptree
open Pgm_ptree
open Pgm_module
let add_module ?(type_only=false) env penv lmod m =
let wp = not type_only in
let id = m.mod_name in
let uc = create_module (Ident.id_user id.id id.id_loc) in
let prelude = Env.find_theory env ["programs"] "Prelude" in
let uc = use_export_theory uc prelude in
let uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in
let m = close_module uc in
Mnm.add id.id m lmod
......@@ -38,7 +39,7 @@ let add_module ?(type_only=false) env penv lmod m =
let retrieve penv file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ml = Pgm_lexer.parse_file lb in
let ml = Lexer.parse_program_file lb in
if Debug.test_flag Typing.debug_parse_only then
Mnm.empty
else
......
src/programs/pgm_module.ml
View file @ 6a159d62
......@@ -175,24 +175,11 @@ let use_export uc m =
uc_th = Theory.use_export uc.uc_th m.m_th; }
| _ -> assert false
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
let use_export_theory uc th =
{ uc with uc_th = Theory.use_export uc.uc_th th }
let reloc loc lb =
lb.Lexing.lex_curr_p <- loc;
lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum + 1
let parse_string f loc s =
let lb = Lexing.from_string s in
reloc loc lb;
f lb
let logic_lexpr ((pos, _), s) =
parse_string Lexer.parse_lexpr pos s
let parse_logic_decls env ((loc, _), s) uc =
let parse = Lexer.parse_list0_decl env Theory.Mnm.empty uc.uc_th in
{ uc with uc_th = parse_string parse loc s }
let add_logic_pdecl env d uc =
{ uc with uc_th = Typing.add_decl env Theory.Mnm.empty uc.uc_th d }
......
src/programs/pgm_module.mli
View file @ 6a159d62
......@@ -40,6 +40,7 @@ val open_namespace : uc -> uc
val close_namespace : uc -> bool -> string option -> uc
val use_export : uc -> t -> uc
val use_export_theory : uc -> Theory.theory -> uc
(** insertion *)
......@@ -51,9 +52,7 @@ val add_mtsymbol : mtsymbol -> uc -> uc
val add_decl : Pgm_ttree.decl -> uc -> uc
val add_logic_decl : Decl.decl -> uc -> uc
(** TODO: *)
val parse_logic_decls : Env.env -> Loc.position * string -> uc -> uc
val logic_lexpr : Loc.position * string -> Ptree.lexpr
val add_logic_pdecl : Env.env -> Ptree.decl -> uc -> uc
(** exceptions *)
......
src/programs/pgm_parser.mly deleted 100644 → 0
View file @ 7d2eca12
This diff is collapsed.
src/programs/pgm_ptree.ml deleted 100644 → 0
View file @ 7d2eca12
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* 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 Why
type loc = Loc.position
type ident = Ptree.ident
type qualid = Ptree.qualid
type constant = Term.constant
type assertion_kind = Aassert | Aassume | Acheck
type lazy_op = LazyAnd | LazyOr
type logic = Loc.position * string
type lexpr = logic
type variant = lexpr * qualid
type loop_annotation = {
loop_invariant : lexpr option;
loop_variant : variant option;
}
type for_direction = To | Downto
type effect = {
pe_reads : qualid list;
pe_writes : qualid list;
pe_raises : qualid list;
}
type pre = lexpr
type post = lexpr * (qualid * lexpr) list
type type_v =
| Tpure of Ptree.pty
| Tarrow of binder list * type_c
and type_c =
{ pc_result_type : type_v;
pc_effect : effect;
pc_pre : pre;
pc_post : post; }
and binder = ident * type_v option
type expr = {
expr_desc : expr_desc;
expr_loc : loc;
}
and expr_desc =
(* lambda-calculus *)
| Econstant of constant
| Eident of qualid
| Eapply of expr * expr
| Efun of binder list * triple
| Elet of ident * expr * expr
| Eletrec of (ident * binder list * variant option * triple) list * expr
| Etuple of expr list
(* control *)
| Esequence of expr * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Ematch of expr * (Ptree.pattern * expr) list
| Eskip
| Eabsurd
| Eraise of qualid * expr option
| Etry of expr * (qualid * ident option * expr) list
| Efor of ident * expr * for_direction * expr * lexpr option * expr
(* annotations *)
| Eassert of assertion_kind * lexpr
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
| Eany of type_c
(* TODO: ghost *)
and triple = pre * expr * post
type decl =
| Dlet of ident * expr
| Dletrec of (ident * binder list * variant option * triple) list
| Dlogic of logic
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
(* modules *)
| Duse of qualid * Ptree.imp_exp * (*as:*) ident option
| Dnamespace of ident * (* import: *) bool * decl list
| Dmutable_type of ident * ident list * Ptree.pty option
type module_ = {
mod_name : ident;
mod_decl : decl list;
}
type file = module_ list
src/programs/pgm_ttree.ml
View file @ 6a159d62
......@@ -27,11 +27,11 @@ type ident = Ptree.ident
type constant = Term.constant
type assertion_kind = Pgm_ptree.assertion_kind
type assertion_kind = Ptree.assertion_kind
type lazy_op = Pgm_ptree.lazy_op
type lazy_op = Ptree.lazy_op
type for_direction = Pgm_ptree.for_direction
type for_direction = Ptree.for_direction
(*****************************************************************************)
(* phase 1: introduction of destructive types *)
......
src/programs/pgm_types.mli
View file @ 6a159d62
......@@ -29,7 +29,7 @@ val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty -> bool
val ts_arrow : tysymbol
(* program types *)
module rec T : sig
......
src/programs/pgm_typing.ml
View file @ 6a159d62
This diff is collapsed.
src/programs/pgm_typing.mli
View file @ 6a159d62
......@@ -24,7 +24,7 @@ val debug : Debug.flag
val decl :
wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Pgm_module.Mnm.t ->
Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
Pgm_module.uc -> Ptree.program_decl -> Pgm_module.uc
val print_post : Format.formatter -> Pgm_ttree.post -> unit
src/programs/pgm_wp.ml
View file @ 6a159d62
......@@ -74,7 +74,7 @@ let wp_forall v f =
(* utility functions for building WPs *)
let fresh_label env =
let ty = ty_app (find_ts env "label") [] in
let ty = ty_app (find_ts env "label_") [] in
create_vsymbol (id_fresh "label") ty
let wp_binder x f = match x.pv_tv with
......@@ -365,9 +365,9 @@ and wp_desc env e q = match e.expr_desc with
and I(v2+1) -> Q *)
let (res, q1), _ = q in
let gt, le, incr = match d with
| Pgm_ptree.To ->
| Ptree.To ->
find_ls env "infix >", find_ls env "infix <=", t_int_const "1"
| Pgm_ptree.Downto ->
| Ptree.Downto ->
find_ls env "infix <", find_ls env "infix >=", t_int_const "-1"
in
let v1_gt_v2 = f_app gt [t_var v1.pv_vs; t_var v2.pv_vs] in
......@@ -394,13 +394,13 @@ and wp_desc env e q = match e.expr_desc with
in
wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f)
| Eassert (Pgm_ptree.Aassert, f) ->
| Eassert (Ptree.Aassert, f) ->
let (_, q), _ = q in
wp_and f q
| Eassert (Pgm_ptree.Acheck, f) ->
| Eassert (Ptree.Acheck, f) ->
let (_, q), _ = q in
wp_and ~sym:true f q
| Eassert (Pgm_ptree.Aassume, f) ->
| Eassert (Ptree.Aassume, f) ->
let (_, q), _ = q in
wp_implies f q
| Elabel (lab, e1) ->
......
tests/test-pgm-jcf.mlw
View file @ 6a159d62
module P
{ use import programs.Prelude }
{ use import int.Int }
use import programs.Prelude
use import int.Int
use module export stdlib.Ref
use export module stdlib.Ref
let incr (r : ref int) : unit =
{}
{ }
set r (get r + 1)
{ r = old r + 1 }
(* parameter r : ref int *)
let f () =
{ true }
{ }
let r = ref 0 in
(* assert { r = 0 }; *)
incr r;
......
theories/programs.why
View file @ 6a159d62
theory Prelude
use export int.Int
use export bool.Bool
type unit = ()
logic ignore 'a : unit
(* type label *)
(* logic at 'a label : 'a *)
logic old 'a : 'a
type label_
logic at 'a label_ : 'a
logic old 'a : 'a
type exn
logic lt_nat (x y:int) = 0 <= y and x < y
(* logic lt_nat (x y:int) = 0 <= y and x < y *)
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment