Commit 8f9a5016 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'ada_parser' into 'master'

Ada parser

See merge request !282
parents a41f82cb 627275d1
......@@ -446,6 +446,8 @@ PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/microc/mc_lexer.ml \
plugins/microc/mc_parser.ml plugins/microc/mc_parser.mli \
plugins/parser/dimacs.ml \
plugins/ada_terms/ada_lexer.ml \
plugins/ada_terms/ada_parser.ml plugins/ada_terms/ada_parser.mli
PLUG_PARSER = genequlin dimacs
PLUG_PRINTER =
......@@ -453,12 +455,14 @@ PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUG_MICROC = mc_ast mc_parser mc_lexer mc_main
PLUG_ADA = ada_nametable ada_parser ada_lexer ada_main
PLUGINS = genequlin dimacs tptp python microc
PLUGINS = genequlin dimacs tptp python microc ada
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
ADAMODULES = $(addprefix plugins/ada_terms/, $(PLUG_ADA))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
......@@ -469,6 +473,9 @@ PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
ADACMO = $(addsuffix .cmo, $(ADAMODULES))
ADACMX = $(addsuffix .cmx, $(ADAMODULES))
ifeq (@enable_hypothesis_selection@,yes)
PLUG_TRANSFORM += hypothesis_selection
PLUGINS += hypothesis_selection
......@@ -482,13 +489,14 @@ endif
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES)
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES) \
$(ADAMODULES)
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGDIRS = parser printer transform tptp python microc
PLUGDIRS = parser printer transform tptp python microc ada_terms
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
......@@ -525,6 +533,8 @@ lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
lib/plugins/microc.cmxs: $(MICROCCMX)
lib/plugins/microc.cmo: $(MICROCCMO)
lib/plugins/ada.cmxs: $(ADACMX)
lib/plugins/ada.cmo: $(ADACMO)
# depend and clean targets
......
......@@ -436,6 +436,7 @@ echo ""
echo "=== Checking replay (no prover) ==="
replay bench/replay
replay tests/ada_terms # TODO ada plugin only
replay examples/stdlib --merging-only
replay examples/bts --merging-only
replay examples/tests --merging-only
......
External printer for task/arguments parser for transformations
==============================================================
* Operators are printed the Ada way:
| Why3 | Ada |
|------|------------|
| `<>` | `/=` |
| `/\` | `and` |
| `\/` | `or` |
| `&&` | `and then` |
| `||` | `or else` |
* Attributes are printed and can be used:
Functions with attribute `name` (could be `syntax`) as `First` or `Last` are
printed as attributes:
| Why3 | Ada |
|:----------|----------:|
| `first A` | `A'First` |
| `last A` | `A'Last` |
* When the type is detected to be a Why3 record type: fields are printed in dot
notation: X.Y.Z
Also, parsed the same way for argument of transformations
* Quantifiers are printed in a close way to Ada:
| Why3 | Ada |
|-----------------|----------------------|
| `forall x.` | `for all x => ` |
| `exists x.` | `for some x => ` |
| `forall x:int.` | `for all x:int => ` |
| `exists x:int.` | `for some x:int => ` |
* Notation for Ada-like intervals for quantification:
| Why3 | Ada |
|------------------------------------|----------------------------|
| `forall x. x <= y and y <= z -> P` | `for all x in y .. z => P` |
* Ada arrays are recognized by the tool with attributes on the type and on the
getter functions such as:
`type __t [@syntax:array:elts] = { elts [@syntax:getter:elts] : int -> int; foo: bar}`
`function get [@syntax:getter:get] (a: __t) (i: int) : int = a.elts i`
This allows `elts` to be directly understood as an array access:
| Why3 | Ada |
|------------|--------|
| `get A I` | `A(I)` |
| `elts A I` | `A(I)` |
When parsing, `elts` is used as the default getter.
* Record type definitions are printed à la Ada:
| Why3 | Ada |
|------------------------------|---------------------|
| `type t = { F: r; G : bool}` | `type t is` |
| | ` record -- t'mk` |
| | ` F: r` |
| | ` g: bool` |
| | ` end record` |
* Bitvector/ <range 0 256> types/constant are printed with an Ada name:
| Why3 | Ada |
|------------------------------------|--------------------------|
| `type t [@name:M] = <range 0 256>` | `type M = <range 0 256>` |
| `(22:t)` | `(22:M)` |
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
{
open Why3
open Ada_parser
let keywords = Hashtbl.create 97
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[
"all", ALL; (* Ada specific *)
"and", AND; (* Ada specific *)
"as", AS;
"by", BY;
"else", ELSE;
"end", END;
"false", FALSE;
"float", FLOAT;
"for", FOR; (* Ada specific *)
"if", IF;
"in", IN;
"let", LET;
"match", MATCH;
"not", NOT;
"or", OR; (* Ada specific *)
"range", RANGE;
"so", SO;
"some", SOME; (* Ada specific *)
"then", THEN;
"true", TRUE;
"with", WITH;
(* programs *)
"at", AT;
"begin", BEGIN;
"fun", FUN;
"ghost", GHOST;
"old", OLD;
"ref", REF;
]
}
let space = [' ' '\t' '\r']
let quote = '\''
let bin = ['0' '1']
let oct = ['0'-'7']
let dec = ['0'-'9']
let hex = ['0'-'9' 'a'-'f' 'A'-'F']
let bin_sep = ['0' '1' '_']
let oct_sep = ['0'-'7' '_']
let dec_sep = ['0'-'9' '_']
let hex_sep = ['0'-'9' 'a'-'f' 'A'-'F' '_']
let lalpha = ['a'-'z']
let ualpha = ['A'-'Z']
let alpha = ['a'-'z' 'A'-'Z']
let suffix = (alpha | dec_sep)*
let lident = ['a'-'z' '_'] suffix
let uident = ['A'-'Z'] suffix
let core_suffix = alpha suffix
let core_lident = lident core_suffix+
let core_uident = uident core_suffix+
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* (dec+ as line) space* (dec+ as char) space* "]"
{ Lexlib.update_loc lexbuf file (int_of_string line) (int_of_string char);
token lexbuf }
| "[#" space* "\"" ([^ '\010' '\013' '"' ]* as file) "\""
space* (dec+ as line) space* (dec+ as bchar) space*
(dec+ as echar) space* "]"
{ POSITION (Loc.user_position file (int_of_string line)
(int_of_string bchar) (int_of_string echar)) }
| "[@" space* ([^ ' ' '\n' ']']+ (' '+ [^ ' ' '\n' ']']+)* as lbl) space* ']'
{ ATTRIBUTE lbl }
| '\n'
{ Lexing.new_line lexbuf; token lexbuf }
| space+
{ token lexbuf }
| quote { QUOTE }
| '_'
{ UNDERSCORE }
| lident as id
{ try Hashtbl.find keywords id with Not_found -> LIDENT id }
| core_lident as id
{ CORE_LIDENT id }
| uident as id
{ UIDENT id }
| core_uident as id
{ CORE_UIDENT id }
| dec dec_sep* as s
{ INTEGER Number.(int_literal ILitDec ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['x' 'X'] (hex hex_sep* as s)
{ INTEGER Number.(int_literal ILitHex ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['o' 'O'] (oct oct_sep* as s)
{ INTEGER Number.(int_literal ILitOct ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['b' 'B'] (bin bin_sep* as s)
{ INTEGER Number.(int_literal ILitBin ~neg:false (Lexlib.remove_underscores s)) }
| (dec+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER Number.(int_literal ILitDec ~neg:false i) }
| '0' ['x' 'X'] (hex+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER Number.(int_literal ILitHex ~neg:false i) }
| (dec+ as i) ("" as f) ['e' 'E'] (['-' '+']? dec+ as e)
| (dec+ as i) '.' (dec* as f) (['e' 'E'] (['-' '+']? dec+ as e))?
| (dec* as i) '.' (dec+ as f) (['e' 'E'] (['-' '+']? dec+ as e))?
{ REAL (Number.real_literal ~radix:10 ~neg:false ~int:i ~frac:f ~exp:(Opt.map Lexlib.remove_leading_plus e)) }
| '0' ['x' 'X'] (hex+ as i) ("" as f) ['p' 'P'] (['-' '+']? dec+ as e)
| '0' ['x' 'X'] (hex+ as i) '.' (hex* as f)
(['p' 'P'] (['-' '+']? dec+ as e))?
| '0' ['x' 'X'] (hex* as i) '.' (hex+ as f)
(['p' 'P'] (['-' '+']? dec+ as e))?
{ REAL (Number.real_literal ~radix:16 ~neg:false ~int:i ~frac:f ~exp:(Opt.map Lexlib.remove_leading_plus e)) }
| "(*)"
{ Lexlib.backjump lexbuf 2; LEFTPAR }
| "(*"
{ Lexlib.comment lexbuf; token lexbuf }
| "'" (lalpha suffix as id)
{ QUOTE_LIDENT id }
| ","
{ COMMA }
| "("
{ LEFTPAR }
| ")"
{ RIGHTPAR }
| "{"
{ LEFTBRC }
| "}"
{ RIGHTBRC }
| ":"
{ COLON }
| ";"
{ SEMICOLON }
| "=>"
{ DARROW }
| "->"
{ ARROW }
| "->'"
{ Lexlib.backjump lexbuf 1; ARROW }
| "<-"
{ LARROW }
| "<->"
{ LRARROW }
| "."
{ DOT }
| ".."
{ DOTDOT }
| "&"
{ AMP }
| "|"
{ BAR }
| "<"
{ LT }
| ">"
{ GT }
| "/="
{ LTGT } (* Ada specific *)
| "="
{ EQUAL }
| "-"
{ MINUS }
| "["
{ LEFTSQ }
| "]"
{ RIGHTSQ }
| "]" (quote+ as s)
{ RIGHTSQ_QUOTE s }
| ")" ('\'' alpha suffix core_suffix* as s)
{ RIGHTPAR_QUOTE s }
| ")" ('_' alpha suffix core_suffix* as s)
{ RIGHTPAR_USCORE s }
| op_char_pref op_char_4* quote* as s
{ OPPREF s }
| op_char_1234* op_char_1 op_char_1234* quote* as s
{ OP1 s }
| op_char_234* op_char_2 op_char_234* quote* as s
{ OP2 s }
| op_char_34* op_char_3 op_char_34* quote* as s
{ OP3 s }
| op_char_4+ as s
{ OP4 s }
| eof
{ EOF }
| _ as c
{ Lexlib.illegal_character c lexbuf }
{
open Why3
let debug = Debug.register_info_flag "print_modules"
~desc:"Print@ program@ modules@ after@ typechecking."
exception Error of string option
let () = Exn_printer.register (fun fmt exn -> match exn with
(* This ad hoc switch allows to not edit the automatically generated
handcrafted.messages in ad hoc ways. *)
| Error None -> Format.fprintf fmt "syntax error"
| Error (Some s) -> Format.fprintf fmt "syntax error:\n %s" s
| _ -> raise exn)
let build_parsing_function (parser_entry: Lexing.position -> 'a) lb =
(* This records the last token which was read (for error messages) *)
let last = ref EOF in
let module I = Ada_parser.MenhirInterpreter in
let checkpoint = parser_entry lb.Lexing.lex_curr_p
and supplier =
I.lexer_lexbuf_to_supplier (fun x -> let t = token x in last := t; t) lb
and succeed t = t
and fail _ =
let text = Lexing.lexeme lb in
(* TODO/FIXME: ad-hoc fix for TryWhy3/Str incompatibility *)
let s = (* TODO changed if Strings.has_prefix "/trywhy3_input." fname
then None
else Report.report text !last checkpoint*) Some text in
(* Typing.close_file is supposedly done at the end of the file in
parsing.mly. If there is a syntax error, we still need to close it (to
be able to reload). *)
Loc.with_location (fun _x -> raise (Error s)) lb
in
I.loop_handle succeed fail supplier checkpoint
let parse_term nt lb =
Ada_nametable.set_naming_table nt;
build_parsing_function Ada_parser.Incremental.term_eof lb
let parse_term_list nt lb =
Ada_nametable.set_naming_table nt;
build_parsing_function Ada_parser.Incremental.term_comma_list_eof lb
let parse_qualid lb = build_parsing_function Ada_parser.Incremental.qualid_eof lb
let parse_list_ident lb = build_parsing_function Ada_parser.Incremental.ident_comma_list_eof lb
let parse_list_qualid lb = build_parsing_function Ada_parser.Incremental.qualid_comma_list_eof lb
}
(* This is a very light parsing/printing of tasks example for Ada. .adb files
can be understood as whyml files. Then, in the ide, tasks are printed looking
like Ada code and arguments of transformations are parsed using the same
formalism.
*)
open Why3
let ada_format = "ada"
let () = Env.register_format Pmodule.mlw_language ada_format ["adb"]
Lexer.read_channel ~desc:"WhyML@ for@ Ada"
open Pretty
open Term
open Format
open Pp
let get_name ls =
Ident.(get_element_name ~attrs:ls.ls_name.id_attrs)
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
(* ada print_binop *)
let print_binop ~asym fmt = function
| Tand when asym -> fprintf fmt "and then"
| Tor when asym -> fprintf fmt "or else"
| Tand -> fprintf fmt "and"
| Tor -> fprintf fmt "or"
| Timplies -> fprintf fmt "->"
| Tiff -> fprintf fmt "<->"
let print_ty_arg print_any fmt ty =
fprintf fmt "@ %a" print_any (Pp_ty (ty, 2, false))
let print_constr print_any fmt (cs,pjl) =
let add_pj pj ty pjl = (pj,ty)::pjl in
let print_pj fmt (pj,ty) = match pj with
| Some ls ->
fprintf fmt "@ %a:@ %a"
print_any (Pp_ls ls)
print_any (Pp_ty (ty, 2, false))
| None -> print_ty_arg print_any fmt ty
in
fprintf fmt " -- %a%a@\n%a" print_any (Pp_cs cs)
print_any (Pp_id cs.ls_name)
(print_list Pp.newline print_pj)
(List.fold_right2 add_pj pjl cs.ls_args [])
let print_quant fmt = function
| Tforall -> fprintf fmt "for all"
| Texists -> fprintf fmt "for some"
(* Check the "syntax" attribute of the lsymbol and returns true if it is a
getter. *)
let is_getter fs =
Ident.(match get_element_syntax ~attrs:fs.ls_name.id_attrs with
| Is_getter name when name = fs.ls_name.id_string ->
true
| _ -> false
)
(* Register the transformations functions *)
let rec ada_ext_printer is_field print_any fmt a =
(* TODO complete this function *)
match a with
| Pp_term (t, pri) ->
begin match t.t_node with
| Tnot {t_node = Tapp (ls, [t1; t2]) } when ls_equal ls ps_equ ->
(* /= *)
fprintf fmt (protect_on (pri > 0) "@[%a /= %a@]")
(ada_ext_printer is_field print_any) (Pp_term (t1, 0))
(ada_ext_printer is_field print_any) (Pp_term (t2, 0))
| Tbinop (b, f1, f2) ->
(* and, or, and then, or else *)
let asym = Ident.Sattr.mem asym_split f1.t_attrs in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "@[%a %a@ %a@]")
(ada_ext_printer is_field print_any) (Pp_term (f1, (p + 1)))
(print_binop ~asym) b
(ada_ext_printer is_field print_any) (Pp_term (f2, p))
| Tapp (fs, [{t_node = Tapp (getter, [array]); _}; index])
when ls_equal fs Term.fs_func_app && is_getter getter ->
(* Array case: [|(get A) @ I|] to be printed as [|A (I)|] *)
fprintf fmt (protect_on (pri > 0) "@[%a (%a)@]")
(ada_ext_printer is_field print_any) (Pp_term (array, 0))
(ada_ext_printer is_field print_any) (Pp_term (index, 0))
| Tapp (getter, [array; index]) when is_getter getter ->
(* Array case: [|get A I|] to be printed as [|A (I)|] *)
fprintf fmt (protect_on (pri > 0) "@[%a (%a)@]")
(ada_ext_printer is_field print_any) (Pp_term (array, 0))
(ada_ext_printer is_field print_any) (Pp_term (index, 0))
| Tapp (fs, [r]) when is_field fs ->
(* Record field a.b.c *)
fprintf fmt "@[%a.%a@]"
(ada_ext_printer is_field print_any) (Pp_term (r, 7))
print_any (Pp_ls fs)
| Tapp (fs, [r])
when let s = get_name fs in s = Some "First" || s = Some "Last" ->
(* Printing of 'First and 'Last *)
fprintf fmt "@[%a'%a@]"
(ada_ext_printer is_field print_any) (Pp_term (r, 7))
print_any (Pp_ls fs)
| Tquant (q, fq) ->
let vl,tl,f = t_open_quant fq in
(* Specific case for : for all I in A .. B => P(I)
TODO: We recognize <= with its ident name: this could be improved
*)
begin match f.t_node, vl with
| Tbinop
(Timplies,
{t_node =
Tbinop (Tand,
{t_node =
Tapp (le1, [t1; {t_node = Tvar v1; _}]); _},
{t_node = Tapp (le2, [{t_node = Tvar v2; _}; t2]); _}
); _},
f2), [v3]
when le1.ls_name.Ident.id_string = "infix <=" &&
le2.ls_name.Ident.id_string = "infix <=" &&
Term.vs_equal v1 v2 && Term.vs_equal v2 v3 ->
fprintf fmt (protect_on (pri > 0) "@[<hov 1>%a %a%a in %a .. %a =>@ %a@]")
print_quant q
(print_list comma (fun fmt v -> print_any fmt (Pp_vs v))) vl
print_any (Pp_trigger tl)
(ada_ext_printer is_field print_any) (Pp_term (t1, 1))
(ada_ext_printer is_field print_any) (Pp_term (t2, 1))
(ada_ext_printer is_field print_any) (Pp_term (f2, 0));
print_any fmt (Pp_forget vl)
| _, _ ->
fprintf fmt (protect_on (pri > 0) "@[<hov 1>%a %a%a =>@ %a@]")
print_quant q
(print_list comma (fun fmt v -> print_any fmt (Pp_vs v))) vl
print_any (Pp_trigger tl)
(ada_ext_printer is_field print_any) (Pp_term (f, 0));
print_any fmt (Pp_forget vl)
end
| Tconst c ->
begin
match t.t_ty with
| Some {Ty.ty_node = Ty.Tyapp (ts,[])}
when Ty.ts_equal ts Ty.ts_int || Ty.ts_equal ts Ty.ts_real ->
Constant.print_def fmt c
| Some ty ->
(* TODO find a better way to print those *)
fprintf fmt "(%a:%a)" Constant.print_def c
print_any (Pp_ty (ty, 0, false))
| None -> assert false
end
| _ -> print_any fmt a
end
| Pp_decl (fst, ts, csl) ->
begin match csl with
| [_, pr_list] when List.for_all (fun x -> x <> None) pr_list &&
ts.Ty.ts_args = [] ->
fprintf fmt "@[<hov 2>%s %a%a is @\n record %a@\n end record@]"
(if fst then "type" else "with")
print_any (Pp_ts ts)
print_any (Pp_id ts.Ty.ts_name)
(print_list newline (print_constr print_any)) csl;
(print_any fmt) Pp_forget_tvs
| _ -> print_any fmt a
end
| _ -> print_any fmt a
let ada_ext_printer task =
(* First traverse the task to find fields of records, then use it during
printing. *)
let set_records =
let records_fields = Sls.empty in
let decls = Task.task_tdecls task in
List.fold_left Theory.(fun acc decl ->
match decl.td_node with
| Decl d ->
Decl.(begin match d.d_node with
| Ddata [_tys, [_cs_name, fields]] ->
(* Non recursive with only one constructor *)
List.fold_left (fun acc ls ->
if ls <> None then
Sls.add (Opt.get ls) acc
else
acc) acc fields
| _ -> acc
end)
| _ -> acc) records_fields decls
in
let is_record ls =
Sls.mem ls set_records
in
ada_ext_printer is_record
let () = Itp_server.add_registered_lang ada_format ada_ext_printer
let () = Args_wrapper.set_argument_parsing_functions ada_format
~parse_term:(fun nt lb -> Ada_lexer.parse_term nt lb)
~parse_term_list:(fun nt lb -> Ada_lexer.parse_term_list nt lb)
~parse_list_ident:(fun lb -> Ada_lexer.parse_list_ident lb)
~parse_qualid:(fun lb -> Ada_lexer.parse_qualid lb)
~parse_list_qualid:(fun lb -> Ada_lexer.parse_list_qualid lb)
open Why3
let naming_table_ref: Trans.naming_table option ref = ref None
let get_naming_table () =
match !naming_table_ref with
| None -> raise Not_found
| Some nt -> nt
let set_naming_table nt =
naming_table_ref := Some nt
(* If the string is recognized in the naming table as of an array type
(according to attribute "syntax" of said type) then returns the string