From 28f7bd0e93a186fe8e30a73662db9ad55f72508d Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Fri, 21 Jun 2024 16:49:09 +0800 Subject: [PATCH 01/12] Clone necessary files to start modifying parser --- src/sleek/README.md | 0 src/sleek/lexer_sleek.mll | 292 +++++ src/sleek/parser_sleek.mly | 169 +++ src/sleek/parser_sleek_common.mly | 1644 +++++++++++++++++++++++++++++ src/sleek/ptree_sleek.ml | 469 ++++++++ 5 files changed, 2574 insertions(+) create mode 100644 src/sleek/README.md create mode 100644 src/sleek/lexer_sleek.mll create mode 100644 src/sleek/parser_sleek.mly create mode 100644 src/sleek/parser_sleek_common.mly create mode 100644 src/sleek/ptree_sleek.ml diff --git a/src/sleek/README.md b/src/sleek/README.md new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/sleek/lexer_sleek.mll b/src/sleek/lexer_sleek.mll new file mode 100644 index 0000000000..ddee9fe57f --- /dev/null +++ b/src/sleek/lexer_sleek.mll @@ -0,0 +1,292 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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 Parser_tokens + + let keywords = Hashtbl.create 97 + let () = + List.iter (fun (x,y) -> Hashtbl.add keywords x y) Keywords.keyword_tokens + + let warn_inexistent_file = + Loc.register_warning "inexistent_file" "Warn about inexistent file in source location" + + let resolve_file orig_file file = + try + Sysutil.resolve_from_paths [Filename.dirname orig_file] file + with + | e -> + Loc.warning warn_inexistent_file "inexistent file in source location: %a" Exn_printer.exn_printer e; + file +} + +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 | quote* dec_sep)* quote* +let lident = ['a'-'z' '_'] suffix +let uident = ['A'-'Z'] suffix + +let core_suffix = quote 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* "]" + { let file = + Option.map (resolve_file Lexing.(lexbuf.lex_curr_p.pos_fname)) file + in + Lexlib.update_loc lexbuf file (int_of_string line) (int_of_string char); + token lexbuf } + | "[#" space* "\"" ([^ '\010' '\013' '"' ]* as file) "\"" + space* (dec+ as bline) space* (dec+ as bchar) space* + space* (dec+ as eline) space* (dec+ as echar) space* "]" + { let file = resolve_file Lexing.(lexbuf.lex_curr_p.pos_fname) file in + POSITION (Loc.user_position file (int_of_string bline) + (int_of_string bchar) (int_of_string eline) (int_of_string echar)) } + | "[@" space* ([^ ' ' '\n' ']']+ (' '+ [^ ' ' '\n' ']']+)* as lbl) space* ']' + { Lexlib.adjust_pos_utf8 lexbuf lbl; + ATTRIBUTE lbl } + | '\n' + { Lexing.new_line lexbuf; token lexbuf } + | space+ + { token lexbuf } + | '_' + { 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:(Option.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:(Option.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 } + | "->" + { ARROW } + | "->'" + { Lexlib.backjump lexbuf 1; ARROW } + | "<-" + { LARROW } + | "<->" + { LRARROW } + | "&&" + { AMPAMP } + | "||" + { BARBAR } + | "/\\" + { AND } + | "\\/" + { OR } + | "." + { DOT } + | ".." + { DOTDOT } + | "&" + { AMP } + | "|" + { BAR } + | "<" + { LT } + | ">" + { GT } + | "<>" + { LTGT } + | "=" + { EQUAL } + | "=>" + { EQUALARROW } + | "-" + { 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 } + | "[|" + { LEFTSQBAR } + | "|]" + { BARRIGHTSQ } + | 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 } + | "\"" + { let start_p = lexbuf.Lexing.lex_start_p in + let start_pos = lexbuf.Lexing.lex_start_pos in + let s = Lexlib.string lexbuf in + lexbuf.Lexing.lex_start_p <- start_p; + lexbuf.Lexing.lex_start_pos <- start_pos; + STRING s } + | eof + { EOF } + | _ as c + { Lexlib.illegal_character c lexbuf } + +{ + + 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.pp_print_string fmt "syntax error" + | Error (Some s) -> Format.fprintf fmt "syntax error: %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 = 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 checkpoint = + let text = Lexing.lexeme lb in + let fname = lb.Lexing.lex_curr_p.Lexing.pos_fname in + (* TODO/FIXME: ad-hoc fix for TryWhy3/Str incompatibility *) + let s = if Strings.has_prefix "/trywhy3_input." fname + then None + else Report.report text !last checkpoint 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 + + open Wstdlib + open Ident + open Theory + open Pmodule + + let parse_term lb = + build_parsing_function Parser.Incremental.term_eof lb + + let parse_expr lb = + build_parsing_function Parser.Incremental.expr_eof lb + + let parse_decl lb = build_parsing_function Parser.Incremental.decl_eof lb + + let parse_term_list lb = build_parsing_function Parser.Incremental.term_comma_list_eof lb + + let parse_qualid lb = build_parsing_function Parser.Incremental.qualid_eof lb + + let parse_list_ident lb = build_parsing_function Parser.Incremental.ident_comma_list_eof lb + + let parse_list_qualid lb = build_parsing_function Parser.Incremental.qualid_comma_list_eof lb + + let parse_mlw_file lb = build_parsing_function Parser.Incremental.mlw_file_parsing_only lb + + let read_channel env path file c = + let lb = Lexing.from_channel c in + Loc.set_file file lb; + Typing.open_file env path; + let mm = + try + build_parsing_function Parser.Incremental.mlw_file lb + with + e -> ignore (Typing.discard_file ()); raise e + in + if path = [] && Debug.test_flag debug then begin + let print_m _ m = Format.eprintf "%a@\n@." print_module m in + let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in + Mid.iter print_m (Mstr.fold add_m mm Mid.empty) + end; + mm + + let whyml_format = "whyml" + + let () = Env.register_format mlw_language whyml_format ["mlw";"why"] + read_channel ~desc:"WhyML@ programming@ and@ specification@ language" + +} diff --git a/src/sleek/parser_sleek.mly b/src/sleek/parser_sleek.mly new file mode 100644 index 0000000000..552b42ee71 --- /dev/null +++ b/src/sleek/parser_sleek.mly @@ -0,0 +1,169 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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. *) +(* *) +(********************************************************************) + +%{ + +%} + +(* Entry points *) + +%start mlw_file +%start mlw_file_parsing_only +%start term_eof +%start expr_eof +%start decl_eof +%start qualid_eof +%start qualid_comma_list_eof +%start term_comma_list_eof +%start ident_comma_list_eof + + +%% + +(* parsing of a single term or a single decl *) + +term_eof: +| term EOF { $1 } + +expr_eof: +| seq_expr EOF { $1 } + +decl_eof: +| pure_decl EOF { $1 } +| prog_decl EOF { $1 } + +(* Parsing of a list of qualified identifiers for the ITP *) + +qualid_eof: +| qualid EOF { $1 } + +qualid_comma_list_eof: +| comma_list1(qualid) EOF { $1 } + +ident_comma_list_eof: +| comma_list1(ident) EOF { $1 } + +term_comma_list_eof: +| comma_list1(single_term) EOF { $1 } +(* we use single_term to avoid conflict with tuples, that + do not need parentheses *) + + +(* Modules and scopes *) + +mlw_file: +| EOF +| mlw_module mlw_module_no_decl* EOF + { Typing.close_file () } +| module_decl module_decl_no_head* EOF + { let loc = floc $startpos($3) $endpos($3) in + Typing.close_module loc; Typing.close_file () } + +mlw_file_parsing_only: +| EOF { (Modules([])) } +| mlw_module_parsing_only mlw_module_no_decl_parsing_only* EOF { (Modules( [$1] @ $2)) } +| module_decl_parsing_only module_decl_no_head_parsing_only* EOF { (Decls( [$1] @ $2)) } + + +mlw_module: +| module_head module_decl_no_head* END + { Typing.close_module (floc $startpos($3) $endpos($3)) } + +mlw_module_parsing_only: +| module_head_parsing_only module_decl_no_head_parsing_only* END { ($1,$2) } + +module_head: +| THEORY attrs(uident_nq) { Typing.open_module $2 } +| MODULE attrs(uident_nq) intf = option(preceded(COLON, tqualid)) + { Typing.open_module ?intf $2 } + +scope_head: +| SCOPE boption(IMPORT) attrs(uident_nq) + { Typing.open_scope (floc $startpos $endpos) $3; $2 } + +module_decl: +| scope_head module_decl* END + { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 } +| IMPORT uqualid + { Typing.add_decl (floc $startpos $endpos) (Dimport($2)) } +| d = pure_decl | d = prog_decl | d = meta_decl + { Typing.add_decl (floc $startpos $endpos) d } +| use_clone { () } + +module_decl_parsing_only: +| scope_head_parsing_only module_decl_parsing_only* END + { let loc,import,qid = $1 in (Dscope(loc,import,qid,$2))} +| IMPORT uqualid { (Dimport $2) } +| d = pure_decl | d = prog_decl | d = meta_decl { d } +| use_clone_parsing_only { $1 } + +(* Do not open inside another module *) + +mlw_module_no_decl: +| SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } +| mlw_module + { $1 } + +mlw_module_no_decl_parsing_only: +| SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } +| mlw_module_parsing_only + { $1 } + +module_decl_no_head: +| THEORY | MODULE + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } +| module_decl + { $1 } + +module_decl_no_head_parsing_only: +| THEORY | MODULE + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } +| module_decl_parsing_only + { $1 } + + +(* Use and clone *) + +use_clone: +| USE EXPORT tqualid + { let loc = floc $startpos $endpos in + let decl = Ptree.Duseexport $3 in + Typing.add_decl loc decl + } +| CLONE EXPORT tqualid clone_subst + { let loc = floc $startpos $endpos in + let decl = Ptree.Dcloneexport(loc,$3,$4) in + Typing.add_decl loc decl + } +| USE boption(IMPORT) m_as_list = comma_list1(use_as) + { let loc = floc $startpos $endpos in + let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in + let import = $2 in + if import && not exists_as then Loc.warning ~loc warn_redundant_import + "the keyword `import' is redundant here and can be omitted"; + let decl = Ptree.Duseimport(loc,import,m_as_list) in + Typing.add_decl loc decl + } +| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst + { let loc = floc $startpos $endpos in + let import = $2 in + let as_opt = $4 in + if import && as_opt = None then Loc.warning ~loc warn_redundant_import + "the keyword `import' is redundant here and can be omitted"; + let decl = Ptree.Dcloneimport(loc,import,$3,as_opt,$5) in + Typing.add_decl loc decl + } diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly new file mode 100644 index 0000000000..ae91f120fb --- /dev/null +++ b/src/sleek/parser_sleek_common.mly @@ -0,0 +1,1644 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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. *) +(* *) +(********************************************************************) + +(* Important note: this is not a complete grammar, but a common part + to be used as "Menhir library". See details on Menhir manual, + Section 5.1 "Splitting specifications over multiple files" + See also there for the meaning of "%public" + +*) + +%{ + open Pstree + + let floc s e = Loc.extract (s,e) + + let add_attr id l = (* id.id_ats is usually nil *) + { id with id_ats = List.rev_append id.id_ats l } + + let id_anonymous loc = { id_str = "_"; id_ats = []; id_loc = loc } + + let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e } + + let get_op q s e = Qident (mk_id (Ident.op_get q) s e) + let upd_op q s e = Qident (mk_id (Ident.op_update q) s e) + let cut_op q s e = Qident (mk_id (Ident.op_cut q) s e) + let rcut_op q s e = Qident (mk_id (Ident.op_rcut q) s e) + let lcut_op q s e = Qident (mk_id (Ident.op_lcut q) s e) + + let mk_pat d s e = { pat_desc = d; pat_loc = floc s e } + let mk_term d s e = { term_desc = d; term_loc = floc s e } + let mk_expr d s e = { expr_desc = d; expr_loc = floc s e } + + let variant_union v1 v2 = match v1, v2 with + | _, [] -> v1 + | [], _ -> v2 + | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc + "multiple `variant' clauses are not allowed" + + let empty_sleek_spec = "" + + let empty_spec = { + sp_pre = []; + sp_post = []; + sp_xpost = []; + sp_reads = []; + sp_writes = []; + sp_alias = []; + sp_variant = []; + sp_checkrw = false; + sp_diverge = false; + sp_partial = false; + } + + let spec_union s1 s2 = { + sp_pre = s1.sp_pre @ s2.sp_pre; + sp_post = s1.sp_post @ s2.sp_post; + sp_xpost = s1.sp_xpost @ s2.sp_xpost; + sp_reads = s1.sp_reads @ s2.sp_reads; + sp_writes = s1.sp_writes @ s2.sp_writes; + sp_alias = s1.sp_alias @ s2.sp_alias; + sp_variant = variant_union s1.sp_variant s2.sp_variant; + sp_checkrw = s1.sp_checkrw || s2.sp_checkrw; + sp_diverge = s1.sp_diverge || s2.sp_diverge; + sp_partial = s1.sp_partial || s2.sp_partial; + } + + let break_id = "'Break" + let continue_id = "'Continue" + let return_id = "'Return" + + let apply_return pat sp = + let apply = function + | loc, [{pat_desc = Pvar {id_str = "result"; id_loc = l}}, f] + when Loc.equal loc l -> loc, [pat, f] + | post -> post in + match pat.pat_desc with + | Pwild -> sp + | _ -> { sp with sp_post = List.map apply sp.sp_post } + + type partial = + | Regular + | Partial + | Ghost + + let ghost part = (part = Ghost) + + let apply_partial_sp part sp = + if part <> Partial then sp else + { sp with sp_partial = true } + + let apply_partial part e = + if part <> Partial then e else + let ed = match e.expr_desc with + | Efun (_::_ as bl, op, p, m, s, ex) -> + Efun (bl, op, p, m, apply_partial_sp part s, ex) + | Eany (_::_ as pl, rsk, op, p, m, s) -> + Eany (pl, rsk, op, p, m, apply_partial_sp part s) + | _ -> + Loc.errorm ~loc:e.expr_loc + "this expression cannot be declared partial" in + { e with expr_desc = ed } + + let we_attr = Ident.create_attribute "expl:witness existence" + + let pre_of_any any_loc ty ql = + if ql = [] then [] else + let ri loc = { id_str = "result"; id_loc = loc; id_ats = [] } in + let rt loc = { term_desc = Tident (Qident (ri loc)); term_loc = loc } in + let cast t ty = { t with term_desc = Tcast (t,ty) } in + let case (loc, pfl) = + let mk_t d = { term_desc = d; term_loc = loc } in + match pfl with + | [pat, f] -> + let rec unfold d p = match p.pat_desc with + | Pparen p | Pscope (_,p) -> unfold d p + | Pcast (p,ty) -> unfold (cast d ty) p + | Ptuple [] -> unfold (cast d (PTtuple [])) + { p with pat_desc = Pwild } + | Pvar { id_str = "result" } | Pwild -> + begin match d.term_desc with + | Tident (Qident _) -> f (* no type casts on d *) + | _ -> mk_t (Tlet (id_anonymous p.pat_loc, d, f)) + end + | Pvar id -> mk_t (Tlet (id, d, f)) + | _ -> mk_t (Tcase (d, pfl)) in + unfold (rt loc) pat + | _ -> mk_t (Tcase (rt loc, pfl)) in + let mk_t desc = { term_desc = desc; term_loc = any_loc } in + let rec join ql = match ql with + | [] -> assert false (* never *) + | [q] -> case q + | q::ql -> mk_t (Tbinop (case q, Dterm.DTand_asym, join ql)) in + let id = add_attr (ri any_loc) [ATstr Ity.break_attr] in + let bl = [any_loc, Some id, false, Some ty] in + let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in + [mk_t (Tattr (ATstr we_attr, p))] + + let double_ref {id_loc = loc} = + Loc.errorm ~loc "this variable is already a reference" + + let set_ref id = + List.iter (function + | ATstr a when Ident.attr_equal a Pmodule.ref_attr -> + double_ref id + | _ -> ()) id.id_ats; + { id with id_ats = ATstr Pmodule.ref_attr :: id.id_ats } + + let set_ref_opt loc r = function + | id when not r -> id + | Some id -> Some (set_ref id) + | None -> Loc.errorm ~loc "anonymous parameters cannot be references" + + let binder_of_id id = + if id.id_str = "ref" then Loc.error ~loc:id.id_loc Error; + (* TODO: recognize and fail on core idents *) + Some id + + let lq_as_ref = function + | Qident {id_str = "ref"} -> () + | _ -> raise Error + + let error_param loc = + Loc.errorm ~loc "cannot determine the type of the parameter" + + let error_loc loc = Loc.error ~loc Error + + let warn_redundant_import = + Loc.register_warning "redundant import" "Warn about redundant import" + + let () = Exn_printer.register (fun fmt exn -> match exn with + | Error -> Format.fprintf fmt "syntax error %s" (Parser_messages.message 1) + | _ -> raise exn) + + let core_ident_error = format_of_string + "Symbol %s cannot be user-defined. User-defined symbol cannot use ' \ + before a letter. You can only use ' followed by _ or a number." + + let name_term id_opt def t = + let name = Option.fold ~some:(fun id -> id.id_str) ~none:def id_opt in + let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in + { term_loc = t.term_loc; term_desc = Tattr (attr, t) } + + let re_pat pat d = { pat with pat_desc = d } + + let rec simplify_let_pattern ?loc kind d pat e = + let cast e ty = { e with expr_desc = Ecast (e,ty) } in + let rec unfold gh d p = match p.pat_desc with + | Pparen p | Pscope (_,p) -> unfold gh d p + | Pghost p -> unfold true d p + | Pcast (p,ty) -> unfold gh (cast d ty) p + | Ptuple [] -> unfold gh (cast d (PTtuple [])) (re_pat p Pwild) + | Pvar id -> Elet (id, gh, kind, d, e) + | Pwild -> Elet (id_anonymous p.pat_loc, gh, kind, d, e) + | _ when kind = Expr.RKnone -> Ematch (d, [pat, e], []) + | _ -> Loc.errorm ?loc "illegal kind qualifier" in + unfold false d pat + + let rec reduce_fun_lit f l default = + match default, l with + | Some t, [] -> t + | None , [x] -> f x (snd x) + | _ , x :: xs -> f x (reduce_fun_lit f xs default) + | None , [] -> assert false (* should not happen *) + + (* if tl = [] then default <> None *) + let term_fun_lit loc_begin loc_end (tl,default) = + let id_str = if tl = [] then "_" else "x'x" in + let id_var = { id_str; id_ats = []; id_loc = loc_begin } in + let var = { term_desc = Tident (Qident id_var); term_loc = loc_begin } in + (* if x = ... then ... else if x = .. then ... else ... *) + let add_term (t1,t2) t = + let eq_id = { id_str = Ident.op_equ; id_ats = []; + id_loc = t1.term_loc } in + let v_eq_t1 = Tinfix (var,eq_id,t1) in + let v_eq_t1 = { term_desc = v_eq_t1; term_loc = t1.term_loc } in + { term_desc = Tif (v_eq_t1,t2,t); + term_loc = Loc.join t1.term_loc t.term_loc} in + let ifte = reduce_fun_lit add_term tl default in + (* fun x -> if x ... *) + let binder = (loc_begin, Some id_var, false, None) in + let desc = Ptree.Tquant (Dterm.DTlambda, [binder], [], ifte) in + let t = { term_desc = desc; term_loc = Loc.join loc_begin loc_end } in + Ptree.Tattr (Ptree.ATstr Ident.funlit, t) + + (* if el = [] then default <> None *) + let expr_fun_lit loc_begin loc_end (el,default) = + let lit_loc = Loc.join loc_begin loc_end in + let var id expr_loc = {expr_desc = Eident (Qident id); expr_loc} in + let id ?(id_ats=[]) id_str id_loc = { id_str; id_ats; id_loc } in + let var_of_string ?(id_ats=[]) nm loc = var (id ~id_ats nm loc) loc in + let proxy_atr = ATstr Ident.proxy_attr in + (* proxy vars for the literal domain/range expressions *) + let domain_ranga_vars i (e1,e2) = + let i = string_of_int i in + var_of_string ~id_ats:[proxy_atr] ("d'i" ^ i) e1.expr_loc, + var_of_string ~id_ats:[proxy_atr] ("r'i" ^ i) e2.expr_loc in + let el_proxies = List.mapi domain_ranga_vars el in + let default_proxy = + Option.map (fun d -> + var_of_string ~id_ats:[proxy_atr] "def'e" d.expr_loc) default in + (* fun x -> if ... *) + let fun_id_var = id (if el = [] then "_" else "x'x") loc_begin in + let fun_var = var fun_id_var loc_begin in + let add_expr (e1,e2) e = + let eq_id = { id_str = Ident.op_equ; id_ats = []; + id_loc = e1.expr_loc } in + let v_eq_e1 = Einfix (fun_var,eq_id,e1) in + let v_eq_e1 = { expr_desc = v_eq_e1; expr_loc = e1.expr_loc } in + { expr_desc = Eif (v_eq_e1,e2,e); + expr_loc = Loc.join e1.expr_loc e.expr_loc } in + let ifte = reduce_fun_lit add_expr el_proxies default_proxy in + let binder = (loc_begin, Some fun_id_var, false, None) in + let pattern = { pat_desc = Ptree.Pvar fun_id_var; + pat_loc = loc_begin } in + let spec = { sp_pre = []; sp_post = []; sp_xpost = []; sp_reads = []; + sp_writes = []; sp_alias = []; sp_variant = []; + sp_checkrw = false; sp_diverge = false; sp_partial = false } in + let efun = Ptree.Efun ([binder], None, pattern, Ity.MaskVisible, spec, ifte) in + let efun = { expr_desc = efun; expr_loc = lit_loc } in + (* let d1 = e1 in + let r1 = e2 in + let ... in + fun x -> if x = d1 then r1 else ... *) + let e2id e = match e with + | {expr_desc = Eident (Qident id)} -> id | _ -> assert false in + let mk_let e (d,r) (e1,e2) = + let expr_desc = Elet (e2id r,false,Expr.RKnone,e2,e) in + let e = {expr_desc; expr_loc = lit_loc} in + let expr_desc = Elet (e2id d,false,Expr.RKnone,e1,e) in + {expr_desc; expr_loc = lit_loc} in + let elets = List.fold_left2 mk_let efun el_proxies el in + (* let def = e_default in ... *) + let e = match default, default_proxy with + | Some e, Some d -> + let expr_desc = Elet (e2id d,false,Expr.RKnone,e,elets) in + {expr_desc; expr_loc = lit_loc} + | _ -> elets + in + Ptree.Eattr (Ptree.ATstr Ident.funlit, e) + +%} + +(* Tokens *) + +%token LIDENT CORE_LIDENT UIDENT CORE_UIDENT +%token INTEGER +%token OP1 OP2 OP3 OP4 OPPREF +%token REAL +%token STRING +%token ATTRIBUTE +%token POSITION +%token QUOTE_LIDENT +%token RIGHTSQ_QUOTE (* ]'' *) +%token RIGHTPAR_QUOTE (* )'spec *) +%token RIGHTPAR_USCORE (* )_spec *) + +(* keywords *) + +%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT +%token ELSE END EPSILON EXISTS EXPORT FALSE FLOAT FORALL FUNCTION +%token GOAL IF IMPORT IN INDUCTIVE LEMMA +%token LET MATCH META NOT PREDICATE RANGE SCOPE +%token SO THEN THEORY TRUE TYPE USE WITH + +(* program keywords *) + +%token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK +%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR +%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD PARTIAL +%token PRIVATE PURE RAISE RAISES READS REF REC REQUIRES +%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES + +(* symbols *) + +%token AND ARROW EQUALARROW +%token AMP BAR +%token COLON COMMA +%token DOT DOTDOT EQUAL LT GT LTGT MINUS +%token LEFTPAR LEFTSQ LEFTSQBAR +%token LARROW LRARROW OR +%token RIGHTPAR RIGHTSQ BARRIGHTSQ +%token UNDERSCORE + +%token EOF + +(* program symbols *) + +%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON + +(* Precedences *) + +%nonassoc below_SEMI +%nonassoc SEMICOLON +%nonassoc LET VAL EXCEPTION +%nonassoc prec_no_else +%nonassoc DOT ELSE RETURN +%nonassoc prec_no_spec +%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT +%nonassoc below_LARROW +%nonassoc LARROW +%nonassoc below_COMMA +%nonassoc COMMA +%nonassoc AS +%nonassoc GHOST +%nonassoc prec_attr +%nonassoc COLON (* weaker than -> because of t: a -> b *) +%right ARROW LRARROW BY SO +%right OR BARBAR +%right AND AMPAMP +%nonassoc NOT +%right EQUAL LTGT LT GT OP1 +%nonassoc AT OLD +%left OP2 MINUS +%left OP3 +%left OP4 +%nonassoc prec_prefix_op +%nonassoc INTEGER REAL (* stronger than MINUS *) +%nonassoc LEFTSQ +%nonassoc OPPREF + +(* + +No entry points here, see `parser.mly` + +The implicit/shared entry points are `module_head_parsing_only`, +`scope_head_parsing_only` and `use_clone_parsing_only` + +See also `plugins/cfg/cfg_parser.mly` + +*) + +%% + +%public module_head_parsing_only: +| THEORY attrs(uident_nq) { $2 } +| MODULE attrs(uident_nq) { $2 } + +%public scope_head_parsing_only: +| SCOPE boption(IMPORT) attrs(uident_nq) + { let loc = floc $startpos $endpos in (loc, $2, $3) } + +%public use_clone_parsing_only: +| USE EXPORT tqualid + { (Duseexport $3) } +| CLONE EXPORT tqualid clone_subst + { let loc = floc $startpos $endpos in + (Dcloneexport (loc,$3, $4)) } +| USE boption(IMPORT) m_as_list = comma_list1(use_as) + { let loc = floc $startpos $endpos in + let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in + if $2 && not exists_as then Loc.warning ~loc warn_redundant_import + "the keyword `import' is redundant here and can be omitted"; + (Duseimport (loc, $2, m_as_list)) } +| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst + { let loc = floc $startpos $endpos in + if $2 && $4 = None then Loc.warning ~loc warn_redundant_import + "the keyword `import' is redundant here and can be omitted"; + (Dcloneimport (loc, $2, $3, $4, $5)) } + +%public use_as: +| n = tqualid q = option(preceded(AS, uident)) { (n, q) } + +%public clone_subst: +| (* epsilon *) { [] } +| WITH comma_list1(single_clone_subst) { $2 } + +single_clone_subst: +| TYPE qualid ty_var* EQUAL ty { CStsym ($2,$3,$5) } +| TYPE qualid { CStsym ($2, [], PTtyapp ($2, [])) } +| CONSTANT qualid EQUAL qualid { CSfsym ($2,$4) } +| CONSTANT qualid { CSfsym ($2,$2) } +| FUNCTION qualid EQUAL qualid { CSfsym ($2,$4) } +| FUNCTION qualid { CSfsym ($2,$2) } +| PREDICATE qualid EQUAL qualid { CSpsym ($2,$4) } +| PREDICATE qualid { CSpsym ($2,$2) } +| VAL qualid EQUAL qualid { CSvsym ($2,$4) } +| VAL qualid { CSvsym ($2,$2) } +| EXCEPTION qualid EQUAL qualid { CSxsym ($2,$4) } +| EXCEPTION qualid { CSxsym ($2,$2) } +| AXIOM qualid { CSaxiom ($2) } +| LEMMA qualid { CSlemma ($2) } +| GOAL qualid { CSgoal ($2) } +| AXIOM DOT { CSprop (Decl.Paxiom) } +| LEMMA DOT { CSprop (Decl.Plemma) } +| GOAL DOT { CSprop (Decl.Pgoal) } + +(* Meta declarations *) + +%public meta_decl: +| META sident LEFTPAR RIGHTPAR { Dmeta ($2, []) } +| META sident comma_list1(meta_arg) { Dmeta ($2, $3) } + +meta_arg: +| TYPE ty { Mty $2 } +| CONSTANT qualid { Mfs $2 } +| FUNCTION qualid { Mfs $2 } +| PREDICATE qualid { Mps $2 } +| AXIOM qualid { Max $2 } +| LEMMA qualid { Mlm $2 } +| GOAL qualid { Mgl $2 } +| VAL qualid { Mval $2 } +| STRING { Mstr $1 } +| INTEGER { Mint (Number.to_small_integer $1) } + +(* Theory declarations *) + +%public pure_decl: +| TYPE with_list1(type_decl) { Dtype $2 } +| CONSTANT constant_decl { Dlogic [$2] } +| FUNCTION function_decl with_logic_decl* { Dlogic ($2::$3) } +| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) } +| INDUCTIVE with_list1(inductive_decl) { Dind (Decl.Ind, $2) } +| COINDUCTIVE with_list1(inductive_decl) { Dind (Decl.Coind, $2) } +| AXIOM attrs(ident_nq) COLON term { Dprop (Decl.Paxiom, { $2 with id_ats = (Ptree.ATstr Ident.useraxiom_attr)::$2.id_ats; }, $4) } +| LEMMA attrs(ident_nq) COLON term { Dprop (Decl.Plemma, $2, $4) } +| GOAL attrs(ident_nq) COLON term { Dprop (Decl.Pgoal, $2, $4) } + +(* Type declarations *) + +type_decl: +| attrs(lident_nq) ty_var* typedefn type_invariant* type_witness + { let (vis, mut), def = $3 in + { td_ident = $1; td_params = $2; + td_vis = vis; td_mut = mut; + td_inv = $4; td_wit = $5; td_def = def; + td_loc = floc $startpos $endpos } } + +type_witness: +| (* epsilon *) { None } +| BY expr { Some $2 } + +ty_var: +| attrs(quote_lident) { $1 } + +typedefn: +| (* epsilon *) + { (Abstract, false), TDrecord [] } +| EQUAL vis_mut bar_list1(type_case) + { $2, TDalgebraic $3 } +| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC + { $2, TDrecord $4 } +| EQUAL vis_mut ty + { $2, TDalias $3 } +(* FIXME: allow negative bounds *) +| EQUAL LT RANGE int_constant int_constant GT + { (Public, false), TDrange ($4, $5) } +| EQUAL LT FLOAT INTEGER INTEGER GT + { (Public, false), + TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) } + +int_constant: +| INTEGER { $1.Number.il_int } +| MINUS INTEGER { BigInt.minus ($2.Number.il_int) } + +vis_mut: +| (* epsilon *) { Public, false } +| MUTABLE { Public, true } +| abstract { $1, false } +| abstract MUTABLE { $1, true } +| MUTABLE abstract { $2, true } + +abstract: +| PRIVATE { Private } +| ABSTRACT { Abstract } + +type_field: +| field_modifiers ref_amp_id cast + { let mut, ghs = $1 and rff, id = $2 in + let ty = if rff then PTref [$3] else $3 in + { f_ident = id; f_mutable = mut; f_ghost = ghs; + f_pty = ty; f_loc = floc $startpos $endpos } } + +%inline field_modifiers: +| (* epsilon *) { false, false } +| MUTABLE { true, false } +| GHOST { false, true } +| GHOST MUTABLE { true, true } +| MUTABLE GHOST { true, true } + +(* we have to use lqualid instead of REF after field_modifiers + to avoid a conflict with ty. However, if the given lqualid + is not REF, then we want to fail as soon as possible: either + at AMP, if it occurs after the lqualid, or else at COLON. *) +ref_amp_id: +| lq_as_ref AMP attrs(lident_nq) { true, double_ref $3 } +| lq_as_ref_id attr* { true, add_attr $1 $2 } +| AMP attrs(lident_nq) { false, set_ref $2 } +| attrs(lident_nq) { false, $1 } + +lq_as_ref: lqualid { lq_as_ref $1 } +lq_as_ref_id: lqualid lident_nq { lq_as_ref $1; set_ref $2 } + +type_case: +| attrs(uident_nq) params { floc $startpos $endpos, $1, $2 } + +(* Logic declarations *) + +constant_decl: +| attrs(lident_rich) cast preceded(EQUAL,term)? + { { ld_ident = $1; + ld_params = []; ld_type = Some $2; + ld_def = $3; ld_loc = floc $startpos $endpos } } + +function_decl: +| attrs(lident_rich) params cast preceded(EQUAL,term)? + { { ld_ident = $1; ld_params = $2; ld_type = Some $3; + ld_def = $4; ld_loc = floc $startpos $endpos } } + +predicate_decl: +| attrs(lident_rich) params preceded(EQUAL,term)? + { { ld_ident = $1; ld_params = $2; ld_type = None; + ld_def = $3; ld_loc = floc $startpos $endpos } } + +with_logic_decl: +| WITH attrs(lident_rich) params cast? preceded(EQUAL,term)? + { { ld_ident = $2; ld_params = $3; ld_type = $4; + ld_def = $5; ld_loc = floc $startpos $endpos } } + +(* Inductive declarations *) + +inductive_decl: +| attrs(lident_rich) params ind_defn + { { in_ident = $1; in_params = $2; + in_def = $3; in_loc = floc $startpos $endpos } } + +ind_defn: +| (* epsilon *) { [] } +| EQUAL bar_list1(ind_case) { $2 } + +ind_case: +| attrs(ident_nq) COLON term { floc $startpos $endpos, $1, $3 } + +(* Type expressions *) + +%public ty: +| ty_arg { $1 } +| lqualid ty_arg+ { PTtyapp ($1, $2) } +| ty ARROW ty { PTarrow ($1, $3) } + +ty_arg: +| lqualid { PTtyapp ($1, []) } +| quote_lident { PTtyvar $1 } +| uqualid DOT ty_block { PTscope ($1, $3) } +| ty_block { $1 } + +ty_block: +| LEFTPAR comma_list2(ty) RIGHTPAR { PTtuple $2 } +| LEFTPAR RIGHTPAR { PTtuple [] } +| LEFTPAR ty RIGHTPAR { PTparen $2 } +| LEFTBRC ty RIGHTBRC { PTpure $2 } + +cast: +| COLON ty { $2 } + +(* Parameters and binders *) + +(* [param] and [binder] below must have the same grammar + and raise [Error] in the same cases. Interpretaion of + single-standing untyped [Qident]'s is different: [param] + treats them as type expressions, [binder], as parameter + names, whose type must be inferred. *) + +params: param* { List.concat $1 } + +params1: param+ { List.concat $1 } + +%public binders: binder+ { List.concat $1 } + +param: +| special_binder + { error_param (floc $startpos $endpos) } +| lident_nq attr+ + { error_param (floc $startpos $endpos) } +| ty_arg + { [floc $startpos $endpos, None, false, $1] } +| LEFTPAR GHOST ty RIGHTPAR + { [floc $startpos $endpos, None, true, $3] } +| LEFTPAR binder_vars_rest RIGHTPAR + { match snd $2 with [l,_] -> error_param l + | _ -> error_loc (floc $startpos($3) $endpos($3)) } +| LEFTPAR GHOST binder_vars_rest RIGHTPAR + { match snd $3 with [l,_] -> error_param l + | _ -> error_loc (floc $startpos($4) $endpos($4)) } +| LEFTPAR binder_vars cast RIGHTPAR + { let r = fst $2 in let ty = if r then PTref [$3] else $3 in + List.map (fun (l,i) -> l, set_ref_opt l r i, false, ty) (snd $2) } +| LEFTPAR GHOST binder_vars cast RIGHTPAR + { let r = fst $3 in let ty = if r then PTref [$4] else $4 in + List.map (fun (l,i) -> l, set_ref_opt l r i, true, ty) (snd $3) } + +%public binder: +| special_binder + { let l,i = $1 in [l, i, false, None] } +| lident_nq attr+ + { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] } +| ty_arg + { match $1 with + | PTparen (PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])])) -> + [floc $startpos $endpos, binder_of_id (set_ref id), false, None] + | PTtyapp (Qident id, []) + | PTparen (PTtyapp (Qident id, [])) -> + [floc $startpos $endpos, binder_of_id id, false, None] + | _ -> [floc $startpos $endpos, None, false, Some $1] } +| LEFTPAR GHOST ty RIGHTPAR + { match $3 with + | PTtyapp (Qident {id_str="ref"}, [PTtyapp (Qident id, [])]) -> + [floc $startpos $endpos, binder_of_id (set_ref id), true, None] + | PTtyapp (Qident id, []) -> + [floc $startpos $endpos, binder_of_id id, true, None] + | _ -> [floc $startpos $endpos, None, true, Some $3] } +| LEFTPAR binder_vars_rest RIGHTPAR + { match snd $2 with [l,i] -> [l, set_ref_opt l (fst $2) i, false, None] + | _ -> error_loc (floc $startpos($3) $endpos($3)) } +| LEFTPAR GHOST binder_vars_rest RIGHTPAR + { match snd $3 with [l,i] -> [l, set_ref_opt l (fst $3) i, true, None] + | _ -> error_loc (floc $startpos($4) $endpos($4)) } +| LEFTPAR binder_vars cast RIGHTPAR + { let r = fst $2 in let ty = if r then PTref [$3] else $3 in + List.map (fun (l,i) -> l, set_ref_opt l r i, false, Some ty) (snd $2) } +| LEFTPAR GHOST binder_vars cast RIGHTPAR + { let r = fst $3 in let ty = if r then PTref [$4] else $4 in + List.map (fun (l,i) -> l, set_ref_opt l r i, true, Some ty) (snd $3) } + +binder_vars: +| binder_vars_head { fst $1, match snd $1 with + | [] -> raise Error + | bl -> List.rev bl } +| binder_vars_rest { $1 } + +binder_vars_rest: +| binder_vars_head attr+ binder_var* + { let l2 = floc $startpos($2) $endpos($2) in + fst $1, List.rev_append (match snd $1 with + | (l, Some id) :: bl -> + (Loc.join l l2, Some (add_attr id $2)) :: bl + | _ -> error_loc l2) $3 } +| binder_vars_head special_binder binder_var* + { fst $1, List.rev_append (snd $1) ($2 :: $3) } +| special_binder binder_var* + { false, $1 :: $2 } + +binder_vars_head: +| ty { + let of_id id = id.id_loc, binder_of_id id in + let push acc = function + | PTtyapp (Qident id, []) -> of_id id :: acc + | _ -> raise Error in + match $1 with + | PTtyapp (Qident {id_str = "ref"}, l) -> + true, List.fold_left push [] l + | PTtyapp (Qident id, l) -> + false, List.fold_left push [of_id id] l + | _ -> raise Error } + +binder_var: +| attrs(lident_nq) { floc $startpos $endpos, Some $1 } +| special_binder { $1 } + +special_binder: +| UNDERSCORE { floc $startpos $endpos, None } +| AMP attrs(lident_nq) { floc $startpos $endpos, Some (set_ref $2) } + +(* Logical terms *) + +mk_term(X): d = X { mk_term d $startpos $endpos } + +%public term: +| single_term %prec below_COMMA { $1 } +| single_term COMMA term_ + { mk_term (Ttuple ($1::$3)) $startpos $endpos } + +term_: +| single_term %prec below_COMMA { [$1] } +| single_term COMMA term_ { $1::$3 } + +%public single_term: t = mk_term(single_term_) { t } + +single_term_: +| term_arg_ + { match $1 with (* break the infix relation chain *) + | Tinfix (l,o,r) -> Tinnfix (l,o,r) + | Tbinop (l,o,r) -> Tbinnop (l,o,r) + | d -> d } +| NOT single_term + { Tnot $2 } +| OLD single_term + { Tat ($2, mk_id Dexpr.old_label $startpos($1) $endpos($1)) } +| single_term AT uident + { Tat ($1, $3) } +| prefix_op single_term %prec prec_prefix_op + { Tidapp (Qident $1, [$2]) } +| minus_numeral + { Tconst $1 } +| l = single_term ; o = bin_op ; r = single_term + { Tbinop (l, o, r) } +| l = single_term ; o = infix_op_1 ; r = single_term + { Tinfix (l, o, r) } +| l = single_term ; o = infix_op_234 ; r = single_term + { Tidapp (Qident o, [l; r]) } +| term_arg located(term_arg)+ + { let join f (a,_,e) = mk_term (Tapply (f,a)) $startpos e in + (List.fold_left join $1 $2).term_desc } +| IF term THEN term ELSE term + { Tif ($2, $4, $6) } +| LET pattern EQUAL term IN term + { let cast t ty = { t with term_desc = Tcast (t,ty) } in + let rec unfold d p = match p.pat_desc with + | Pparen p | Pscope (_,p) -> unfold d p + | Pcast (p,ty) -> unfold (cast d ty) p + | Ptuple [] -> unfold (cast d (PTtuple [])) (re_pat p Pwild) + | Pvar id -> Tlet (id, d, $6) + | Pwild -> Tlet (id_anonymous p.pat_loc, d, $6) + | _ -> Tcase (d, [$2, $6]) in + unfold $4 $2 } +| LET attrs(lident_op_nq) EQUAL term IN term + { Tlet ($2, $4, $6) } +| LET attrs(lident_nq) mk_term(lam_defn) IN term + { Tlet ($2, $3, $5) } +| LET attrs(lident_op_nq) mk_term(lam_defn) IN term + { Tlet ($2, $3, $5) } +| MATCH term WITH match_cases(term) END + { Tcase ($2, $4) } +| quant comma_list1(quant_vars) triggers DOT term + { let l = List.concat $2 in + Tquant ($1, l, $3, $5) } +| FUN binders ARROW term + { Tquant (Dterm.DTlambda, $2, [], $4) } +| EPSILON + { Loc.errorm "Epsilon terms are currently not supported in WhyML" } +| attr single_term %prec prec_attr + { Tattr ($1, $2) } +| single_term cast + { Tcast ($1, $2) } + +lam_defn: +| binders EQUAL term { Tquant (Dterm.DTlambda, $1, [], $3) } + +term_arg: mk_term(term_arg_) { $1 } +term_dot: mk_term(term_dot_) { $1 } + +term_arg_: +| qualid { Tident $1 } +| AMP qualid { Tasref $2 } +| numeral { Tconst $1 } +| STRING { Tconst (Constant.ConstStr $1) } +| TRUE { Ttrue } +| FALSE { Tfalse } +| o = oppref ; a = term_arg { Tidapp (Qident o, [a]) } +| term_sub_ { $1 } +| LEFTSQBAR term_fun_lit BARRIGHTSQ + { let loc_begin = floc $startpos($1) $endpos($1) in + let loc_end = floc $startpos($3) $endpos($3) in + term_fun_lit loc_begin loc_end $2 } + +term_dot_: +| lqualid { Tident $1 } +| o = oppref ; a = term_dot { Tidapp (Qident o, [a]) } +| term_sub_ { $1 } + +term_block_: +| BEGIN term END { $2.term_desc } +| LEFTPAR term RIGHTPAR { $2.term_desc } +| BEGIN END { Ttuple [] } +| LEFTPAR RIGHTPAR { Ttuple [] } +| LEFTBRC field_list1(term) RIGHTBRC { Trecord $2 } +| LEFTBRC term_arg WITH field_list1(term) RIGHTBRC { Tupdate ($2,$4) } + +term_sub_: +| term_block_ { $1 } +| uqualid DOT mk_term(term_block_) { Tscope ($1, $3) } +| term_dot DOT lqualid_rich { Tidapp ($3,[$1]) } +| term_arg LEFTSQ term rightsq + { Tidapp (get_op $4 $startpos($2) $endpos($2), [$1;$3]) } +| term_arg LEFTSQ term LARROW term rightsq + { Tidapp (upd_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) } +| term_arg LEFTSQ term DOTDOT term rightsq + { Tidapp (cut_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) } +| term_arg LEFTSQ term DOTDOT rightsq + { Tidapp (rcut_op $5 $startpos($2) $endpos($2), [$1;$3]) } +| term_arg LEFTSQ DOTDOT term rightsq + { Tidapp (lcut_op $5 $startpos($2) $endpos($2), [$1;$4]) } + +term_fun_lit: +| mapping_list_with_default(term) { $1 } +| semicolon_list1(term) + { let mk_index_pair i t = + let const = Constant.int_const ~il_kind:Number.ILitDec (BigInt.of_int i) in + let tconst = {term_desc = Tconst const; term_loc = t.term_loc} in + tconst, t in + List.mapi mk_index_pair $1, None } + +field_list1(X): +| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl } + +match_cases(X): +| cl = bar_list1(match_case(X)) { cl } + +%public match_case(X): +| mc = separated_pair(pattern, ARROW, X) { mc } + +quant_vars: +| binder_var+ cast? { List.map (fun (l,i) -> l, i, false, $2) $1 } + +triggers: +| (* epsilon *) { [] } +| LEFTSQ separated_nonempty_list(BAR,comma_list1(single_term)) RIGHTSQ { $2 } + +%inline bin_op: +| ARROW { Dterm.DTimplies } +| LRARROW { Dterm.DTiff } +| OR { Dterm.DTor } +| BARBAR { Dterm.DTor_asym } +| AND { Dterm.DTand } +| AMPAMP { Dterm.DTand_asym } +| BY { Dterm.DTby } +| SO { Dterm.DTso } + +quant: +| FORALL { Dterm.DTforall } +| EXISTS { Dterm.DTexists } + +minus_numeral: +| MINUS INTEGER { Constant.(ConstInt (Number.neg_int $2)) } +| MINUS REAL { Constant.(ConstReal (Number.neg_real $2))} + +%public numeral: +| INTEGER { Constant.ConstInt $1 } +| REAL { Constant.ConstReal $1 } + +(* Program declarations *) + +%public prog_decl: +| VAL ghost kind attrs(lident_rich) mk_expr(fun_decl) + { Dlet ($4, ghost $2, $3, apply_partial $2 $5) } +| VAL ghost kind sym_binder mk_expr(const_decl) + { Dlet ($4, ghost $2, $3, apply_partial $2 $5) } +| VAL ghost REF ref_binder mk_expr(const_decl) + { let rf = mk_expr Eref $startpos($3) $endpos($3) in + let ee = { $5 with expr_desc = Eapply (rf, $5) } in + Dlet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee) } +| LET ghost kind attrs(lident_rich) mk_expr(fun_defn) + { Dlet ($4, ghost $2, $3, apply_partial $2 $5) } +| LET ghost kind sym_binder const_defn + { Dlet ($4, ghost $2, $3, apply_partial $2 $5) } +| LET ghost REF ref_binder const_defn + { let rf = mk_expr Eref $startpos($3) $endpos($3) in + let ee = { $5 with expr_desc = Eapply (rf, $5) } in + Dlet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee) } +| LET REC with_list1(rec_defn) + { Drec $3 } +| EXCEPTION attrs(uident_nq) + { Dexn ($2, PTtuple [], Ity.MaskVisible) } +| EXCEPTION attrs(uident_nq) return + { Dexn ($2, fst $3, snd $3) } + +ghost: +| (* epsilon *) { Regular } +| PARTIAL { Partial } +| GHOST { Ghost } +| GHOST PARTIAL +| PARTIAL GHOST { Loc.errorm ~loc:(floc $startpos $endpos) + "Ghost functions cannot be partial" } + +kind: +| (* epsilon *) { Expr.RKnone } +| FUNCTION { Expr.RKfunc } +| CONSTANT { Expr.RKfunc } +| PREDICATE { Expr.RKpred } +| LEMMA { Expr.RKlemma } + +(* Function definitions *) + +rec_defn: +| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr + { let pat, ty, mask = $5 in + let spec = apply_return pat (spec_union $6 $8) in + let id = mk_id return_id $startpos($7) $endpos($7) in + let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in + $3, ghost $1, $2, $4, ty, pat, mask, apply_partial_sp $1 spec, e } + +fun_defn: +| binders return_opt spec EQUAL spec seq_expr + { let pat, ty, mask = $2 in + let spec = apply_return pat (spec_union $3 $5) in + let id = mk_id return_id $startpos($4) $endpos($4) in + let e = { $6 with expr_desc = Eoptexn (id, mask, $6) } in + Efun ($1, ty, pat, mask, spec, e) } + +fun_decl: +| params1 return_opt spec + { let pat, ty, mask = $2 in + Eany ($1, Expr.RKnone, ty, pat, mask, apply_return pat $3) } + +const_decl: +| return_opt spec + { let pat, ty, mask = $1 in + Eany ([], Expr.RKnone, ty, pat, mask, apply_return pat $2) } + +const_defn: +| cast EQUAL seq_expr { { $3 with expr_desc = Ecast ($3, $1) } } +| EQUAL seq_expr { $2 } + +(* Program expressions *) + +mk_expr(X): d = X { mk_expr d $startpos $endpos } + +%public seq_expr: +| contract_expr %prec below_SEMI { $1 } +| contract_expr SEMICOLON { $1 } +| contract_expr SEMICOLON seq_expr + { mk_expr (Esequence ($1, $3)) $startpos $endpos } + +%public contract_expr: +| assign_expr %prec prec_no_spec { $1 } +| assign_expr single_spec spec + { let p = mk_pat Pwild $startpos $endpos in + let d = Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, $1) in + let d = Eattr (ATstr Vc.wb_attr, mk_expr d $startpos $endpos) in + mk_expr d $startpos $endpos } + +assign_expr: +| expr %prec below_LARROW { $1 } +| expr LARROW expr + { let loc = floc $startpos $endpos in + let rec down attrs assgns ll rl = match ll, rl with + | ({expr_desc = Eident q} as e1)::ll, e2::rl -> + let e1 = {e1 with expr_desc = Easref q} in + down attrs ((e1, None, e2) :: assgns) ll rl + | {expr_desc = Eidapp (q, [e1])}::ll, e2::rl -> + down attrs ((e1, Some q, e2) :: assgns) ll rl + | {expr_desc = Eidapp (Qident id, [_;_]); expr_loc = loc}::_, _::_ -> + begin match Ident.sn_decode id.id_str with + | Ident.SNget _ -> Loc.errorm ~loc + "Parallel array assignments are not allowed" + | _ -> Loc.errorm ~loc + "Invalid left expression in an assignment" + end + | {expr_desc = Eattr (attr, e)}::ll, rl -> + down (attr::attrs) assgns (e::ll) rl + | {expr_loc = loc}::_, _::_ -> Loc.errorm ~loc + "Invalid left expression in an assignment" + | [], [] -> + let attr e a = Eattr (a, {expr_desc = e; expr_loc = loc}) in + List.fold_left attr (Eassign (List.rev assgns)) attrs + | _ -> Loc.errorm ~loc "Invalid parallel assignment" + in + let d = match $1.expr_desc, $3.expr_desc with + | Eidapp (Qident id, [e1;e2]), _ -> + begin match Ident.sn_decode id.id_str with + | Ident.SNget q -> + Eidapp (Qident {id with id_str = Ident.op_set q}, [e1;e2;$3]) + | _ -> Loc.errorm ~loc:$1.expr_loc + "Invalid left expression in an assignment" + end + | Etuple ll, Etuple rl -> down [] [] ll rl + | Etuple _, _ -> Loc.errorm ~loc "Invalid parallel assignment" + | _, _ -> down [] [] [$1] [$3] in + { expr_desc = d; expr_loc = loc } } + +expr: +| single_expr %prec below_COMMA { $1 } +| single_expr COMMA expr_list1 + { mk_expr (Etuple ($1::$3)) $startpos $endpos } + +expr_list1: +| single_expr %prec below_COMMA { [$1] } +| single_expr COMMA expr_list1 { $1::$3 } + +single_expr: e = mk_expr(single_expr_) { e } + +single_expr_: +| expr_arg_ + { match $1 with (* break the infix relation chain *) + | Einfix (l,o,r) -> Einnfix (l,o,r) | d -> d } +| single_expr AMPAMP single_expr + { Eand ($1, $3) } +| single_expr BARBAR single_expr + { Eor ($1, $3) } +| NOT single_expr + { Enot $2 } +| prefix_op single_expr %prec prec_prefix_op + { Eidapp (Qident $1, [$2]) } +| minus_numeral + { Econst $1 } +| l = single_expr ; o = infix_op_1 ; r = single_expr + { Einfix (l,o,r) } +| l = single_expr ; o = infix_op_234 ; r = single_expr + { Eidapp (Qident o, [l;r]) } +| expr_arg located(expr_arg)+ + { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in + (List.fold_left join $1 $2).expr_desc } +| IF seq_expr THEN contract_expr ELSE contract_expr + { Eif ($2, $4, $6) } +| IF seq_expr THEN contract_expr %prec prec_no_else + { Eif ($2, $4, mk_expr (Etuple []) $startpos $endpos) } +| LET ghost kind let_pattern EQUAL seq_expr IN seq_expr + { let rec push pat = re_pat pat (match pat.pat_desc with + | Ptuple (p::pl) -> Ptuple (push p :: pl) + | Pcast (p,ty) -> Pcast (push p, ty) + | Pas (p,v,g) -> Pas (push p, v, g) + | Por (p,q) -> Por (push p, q) + | _ -> Pghost pat) in + let pat = if ghost $2 then push $4 else $4 in + let loc = floc $startpos($3) $endpos($3) in + simplify_let_pattern ~loc $3 (apply_partial $2 $6) pat $8 } +| LET ghost kind attrs(lident_op_nq) const_defn IN seq_expr + { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } +| LET ghost kind attrs(lident_nq) mk_expr(fun_defn) IN seq_expr + { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } +| LET ghost kind attrs(lident_op_nq) mk_expr(fun_defn) IN seq_expr + { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } +| LET ghost REF ref_binder const_defn IN seq_expr + { let rf = mk_expr Eref $startpos($3) $endpos($3) in + let ee = { $5 with expr_desc = Eapply (rf, $5) } in + Elet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee, $7) } +| LET REC with_list1(rec_defn) IN seq_expr + { Erec ($3, $5) } +| FUN binders spec ARROW spec seq_expr + { let id = mk_id return_id $startpos($4) $endpos($4) in + let e = { $6 with expr_desc = Eoptexn (id, Ity.MaskVisible, $6) } in + let p = mk_pat Pwild $startpos $endpos in + Efun ($2, None, p, Ity.MaskVisible, spec_union $3 $5, e) } +| ANY return_named spec + { let pat, ty, mask = $2 in + let loc = floc $startpos $endpos in + let spec = apply_return pat $3 in + if spec.sp_writes <> [] then Loc.errorm ~loc + "this expression should not produce side effects"; + if spec.sp_xpost <> [] then Loc.errorm ~loc + "this expression should not raise exceptions"; + if spec.sp_alias <> [] then Loc.errorm ~loc + "this expression cannot have alias restrictions"; + if spec.sp_diverge || spec.sp_partial then Loc.errorm ~loc + "this expression must terminate"; + let pre = pre_of_any loc ty spec.sp_post in + let spec = { spec with sp_pre = spec.sp_pre @ pre } in + let p = mk_pat Pwild $startpos $endpos in + Eany ([], Expr.RKnone, Some ty, p, mask, spec) } +| VAL ghost kind attrs(lident_rich) mk_expr(fun_decl) IN seq_expr + { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } +| VAL ghost kind sym_binder mk_expr(const_decl) IN seq_expr + { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } +| VAL ghost REF ref_binder mk_expr(const_decl) IN seq_expr + { let rf = mk_expr Eref $startpos($3) $endpos($3) in + let ee = { $5 with expr_desc = Eapply (rf, $5) } in + Elet ($4, ghost $2, Expr.RKnone, apply_partial $2 ee, $7) } +| MATCH seq_expr WITH ext_match_cases END + { let bl, xl = $4 in + let bl = if bl = [] then + [mk_pat Pwild $startpos($3) $endpos($3), + mk_expr Eabsurd $startpos($3) $endpos($3)] else bl in + Ematch ($2, bl, xl) } +| EXCEPTION attrs(uident) IN seq_expr + { Eexn ($2, PTtuple [], Ity.MaskVisible, $4) } +| EXCEPTION attrs(uident) return IN seq_expr + { Eexn ($2, fst $3, snd $3, $5) } +| LABEL id = attrs(uident) IN e = seq_expr + { let cont e = + let id = { id with id_str = id.id_str ^ continue_id } in + { e with expr_desc = Eoptexn (id, Ity.MaskVisible, e) } in + let rec over_loop e = { e with expr_desc = over_loop_desc e } + and over_loop_desc e = match e.expr_desc with + | Escope (q, e1) -> Escope (q, over_loop e1) + | Eattr (l, e1) -> Eattr (l, over_loop e1) + | Ecast (e1, t) -> Ecast (over_loop e1, t) + | Eghost e1 -> Eghost (over_loop e1) + | Esequence (e1, e2) -> Esequence (over_loop e1, e2) + | Eoptexn (id, mask, e1) -> Eoptexn (id, mask, over_loop e1) + | Ewhile (e1, inv, var, e2) -> + let e = { e with expr_desc = Ewhile (e1, inv, var, cont e2) } in + let id = { id with id_str = id.id_str ^ break_id } in + Eoptexn (id, Ity.MaskVisible, e) + | Efor (i, ef, dir, et, inv, e1) -> + let e = { e with expr_desc = Efor (i,ef,dir,et,inv,cont e1) } in + let id = { id with id_str = id.id_str ^ break_id } in + Eoptexn (id, Ity.MaskVisible, e) + | d -> d in + Elabel (id, over_loop e) } +| WHILE seq_expr DO loop_annotation loop_body DONE + { let id_b = mk_id break_id $startpos($3) $endpos($3) in + let id_c = mk_id continue_id $startpos($3) $endpos($3) in + let e = { $5 with expr_desc = Eoptexn (id_c, Ity.MaskVisible, $5) } in + let e = mk_expr (Ewhile ($2, fst $4, snd $4, e)) $startpos $endpos in + Eoptexn (id_b, Ity.MaskVisible, e) } +| FOR var_binder EQUAL seq_expr for_dir seq_expr DO invariant* loop_body DONE + { let id_b = mk_id break_id $startpos($7) $endpos($7) in + let id_c = mk_id continue_id $startpos($7) $endpos($7) in + let e = { $9 with expr_desc = Eoptexn (id_c, Ity.MaskVisible, $9) } in + let e = mk_expr (Efor ($2, $4, $5, $6, $8, e)) $startpos $endpos in + Eoptexn (id_b, Ity.MaskVisible, e) } +| FOR pattern IN seq_expr WITH uqualid iterator + DO loop_annotation loop_body DONE + { let id_b = mk_id break_id $startpos($8) $endpos($8) in + let id_c = mk_id continue_id $startpos($8) $endpos($8) in + let mk d = mk_expr d $startpos $endpos in + let q s = Qdot ($6, mk_id s $startpos($6) $endpos($6)) in + let next = mk (Eidapp (q "next", [mk (Eident (Qident $7))])) in + let e = mk (simplify_let_pattern Expr.RKnone next $2 $10) in + let e = { e with expr_desc = Eoptexn (id_c, Ity.MaskVisible, e) } in + let e = mk (Ewhile (mk Etrue, fst $9, snd $9, e)) in + let e = mk (Eoptexn (id_b, Ity.MaskVisible, e)) in + let unit = mk_expr (Etuple []) $startpos($10) $endpos($10) in + let e = mk (Ematch (e, [], [q "Done", None, unit])) in + let create = mk (Eidapp (q "create", [$4])) in + Elet ($7, false, Expr.RKnone, create, e) } +| ABSURD + { Eabsurd } +| RAISE uqualid expr_arg? + { Eraise ($2, $3) } +| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR + { Eraise ($3, $4) } +| RETURN ioption(contract_expr) + { let id = mk_id return_id $startpos($1) $endpos($1) in + Eraise (Qident id, $2) } +| BREAK ioption(uident) + { let id = match $2 with + | Some id -> { id with id_str = id.id_str ^ break_id } + | None -> mk_id break_id $startpos($1) $endpos($1) in + Eraise (Qident id, None) } +| CONTINUE ioption(uident) + { let id = match $2 with + | Some id -> { id with id_str = id.id_str ^ continue_id } + | None -> mk_id continue_id $startpos($1) $endpos($1) in + Eraise (Qident id, None) } +| TRY seq_expr WITH bar_list1(exn_handler) END + { Ematch ($2, [], $4) } +| GHOST single_expr + { Eghost $2 } +| assertion_kind option(ident_nq) LEFTBRC term RIGHTBRC + { Eassert (snd $1, name_term $2 (fst $1) $4) } +| attr single_expr %prec prec_attr + { Eattr ($1, $2) } +| single_expr cast + { Ecast ($1, $2) } + +expr_arg: e = mk_expr(expr_arg_) { e } +expr_dot: e = mk_expr(expr_dot_) { e } + +expr_arg_: +| qualid { Eident $1 } +| AMP qualid { Easref $2 } +| numeral { Econst $1 } +| STRING { Econst (Constant.ConstStr $1) } +| TRUE { Etrue } +| FALSE { Efalse } +| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) } +| expr_sub_ { $1 } +| LEFTSQBAR expr_fun_lit BARRIGHTSQ + { let loc_begin = floc $startpos($1) $endpos($1) in + let loc_end = floc $startpos($3) $endpos($3) in + expr_fun_lit loc_begin loc_end $2 } + +expr_fun_lit: +| mapping_list_with_default(expr) { $1 } +| semicolon_list1(expr) + { let mk_index_pair i e = + let const = Constant.int_const ~il_kind:Number.ILitDec (BigInt.of_int i) in + let econst = {expr_desc = Econst const; expr_loc = e.expr_loc} in + econst, e in + List.mapi mk_index_pair $1, None } + +expr_dot_: +| lqualid { Eident $1 } +| o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) } +| expr_sub_ { $1 } + +expr_block_: +| BEGIN single_spec spec seq_expr END + { let p = mk_pat Pwild $startpos $endpos in + Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, $4) } +| BEGIN single_spec spec END + { let e = mk_expr (Etuple []) $startpos $endpos in + let p = mk_pat Pwild $startpos $endpos in + Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, e) } +| BEGIN seq_expr END { $2.expr_desc } +| LEFTPAR seq_expr RIGHTPAR { $2.expr_desc } +| BEGIN END { Etuple [] } +| LEFTPAR RIGHTPAR { Etuple [] } +| LEFTBRC field_list1(expr) RIGHTBRC { Erecord $2 } +| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC { Eupdate ($2, $4) } + +expr_pure_: +| LEFTBRC qualid RIGHTBRC { Eidpur $2 } +| uqualid DOT LEFTBRC ident RIGHTBRC { Eidpur (Qdot ($1, $4)) } + +expr_sub_: +| expr_block_ { $1 } +| expr_pure_ { $1 } +| uqualid DOT mk_expr(expr_block_) { Escope ($1, $3) } +| expr_dot DOT mk_expr(expr_pure_) { Eapply ($3, $1) } +| expr_dot DOT lqualid_rich { Eidapp ($3, [$1]) } +| PURE LEFTBRC term RIGHTBRC { Epure $3 } +| expr_arg LEFTSQ expr rightsq + { Eidapp (get_op $4 $startpos($2) $endpos($2), [$1;$3]) } +| expr_arg LEFTSQ expr LARROW expr rightsq + { Eidapp (upd_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) } +| expr_arg LEFTSQ expr DOTDOT expr rightsq + { Eidapp (cut_op $6 $startpos($2) $endpos($2), [$1;$3;$5]) } +| expr_arg LEFTSQ expr DOTDOT rightsq + { Eidapp (rcut_op $5 $startpos($2) $endpos($2), [$1;$3]) } +| expr_arg LEFTSQ DOTDOT expr rightsq + { Eidapp (lcut_op $5 $startpos($2) $endpos($2), [$1;$4]) } + +loop_body: +| (* epsilon *) { mk_expr (Etuple []) $startpos $endpos } +| seq_expr { $1 } + +loop_annotation: +| (* epsilon *) + { [], [] } +| invariant loop_annotation + { let inv, var = $2 in $1 :: inv, var } +| variant loop_annotation + { let inv, var = $2 in inv, variant_union $1 var } + +iterator: +| (* epsilon *) { mk_id "it" $startpos $endpos} +| AS lident { $2 } + +ext_match_cases: +| ioption(BAR) ext_match_cases1 { $2 } + +ext_match_cases1: +| match_case(seq_expr) ext_match_cases0 { let bl,xl = $2 in $1::bl, xl } +| EXCEPTION exn_handler ext_match_cases0 { let bl,xl = $3 in bl, $2::xl } + +ext_match_cases0: +| (* epsilon *) { [], [] } +| BAR ext_match_cases1 { $2 } + +exn_handler: +| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 } + +%public assertion_kind: +| ASSERT { "Assert", Expr.Assert } +| ASSUME { "Assume", Expr.Assume } +| CHECK { "Check", Expr.Check } + +for_dir: +| TO { Expr.To } +| DOWNTO { Expr.DownTo } + +(* Specification *) + +%public spec: +| (* epsilon *) %prec prec_no_spec { empty_spec } +| single_spec spec { spec_union $1 $2 } + +single_spec: +| REQUIRES option(ident_nq) LEFTBRC term RIGHTBRC + { { empty_spec with sp_pre = [name_term $2 "Requires" $4] } } +| ENSURES option(ident_nq) LEFTBRC ensures RIGHTBRC + { let bindings = List.map (fun (p, t) -> p, name_term $2 "Ensures" t) $4 in + { empty_spec with sp_post = [floc $startpos($4) $endpos($4), bindings] } } +| RETURNS LEFTBRC match_cases(term) RIGHTBRC + { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } } +| RAISES LEFTBRC bar_list1(raises) RIGHTBRC + { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } } +| READS LEFTBRC comma_list0(lqualid) RIGHTBRC + { { empty_spec with sp_reads = $3; sp_checkrw = true } } +| WRITES LEFTBRC comma_list0(single_term) RIGHTBRC + { { empty_spec with sp_writes = $3; sp_checkrw = true } } +| ALIAS LEFTBRC comma_list0(alias) RIGHTBRC + { { empty_spec with sp_alias = $3; sp_checkrw = true } } +| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC + { { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } } +| DIVERGES + { { empty_spec with sp_diverge = true } } +| variant + { { empty_spec with sp_variant = $1 } } + +alias: +| single_term WITH single_term { $1, $3 } + +ensures: +| term + { let id = mk_id "result" $startpos $endpos in + [mk_pat (Pvar id) $startpos $endpos, $1] } + +raises: +| uqualid ARROW term + { $1, Some (mk_pat (Ptuple []) $startpos($1) $endpos($1), $3) } +| uqualid pat_arg ARROW term + { $1, Some ($2, $4) } + +xsymbol: +| uqualid { $1, None } + +invariant: +| INVARIANT option(ident_nq) LEFTBRC term RIGHTBRC + { name_term $2 "LoopInvariant" $4 } + +type_invariant: +| INVARIANT option(ident_nq) LEFTBRC term RIGHTBRC + { name_term $2 "TypeInvariant" $4 } + +variant: +| VARIANT option(ident_nq) LEFTBRC comma_list1(single_variant) RIGHTBRC + { List.map (fun (t,r) -> (name_term $2 "Variant" t,r)) $4 } + +single_variant: +| single_term preceded(WITH,lqualid)? { $1, $2 } + +return_opt: +| (* epsilon *) { mk_pat Pwild $startpos $endpos, None, Ity.MaskVisible } +| COLON return_named { let pat, ty, mask = $2 in pat, Some ty, mask } + +%public return_named: +| LEFTPAR ret_cast RIGHTPAR + { $2 } +| LEFTPAR comma_list2(ret_cast) RIGHTPAR + { mk_pat (Ptuple (List.map (fun (pat,_,_) -> pat) $2)) $startpos $endpos, + PTtuple (List.map (fun (_,ty,_) -> ty) $2), + Ity.MaskTuple (List.map (fun (_,_,mask) -> mask) $2) } +| return + { let ty, mask = $1 in mk_pat Pwild $startpos $endpos, ty, mask } + +ret_cast: +| ret_ident cast { $1, $2, Ity.MaskVisible } +| GHOST ret_ident cast { $2, $3, Ity.MaskGhost } + +ret_ident: +| id = attrs(lident_nq) + { let ats = ATstr Dterm.attr_w_unused_var_no :: id.id_ats in + mk_pat (Pvar {id with id_ats = ats}) $startpos $endpos } +| UNDERSCORE + { mk_pat (Pvar (id_anonymous (floc $startpos $endpos))) $startpos $endpos } + +return: +| ty { $1, Ity.MaskVisible } +| GHOST ty { $2, Ity.MaskGhost } +| LEFTPAR GHOST ty RIGHTPAR { $3, Ity.MaskGhost } +| LEFTPAR ret_ghost RIGHTPAR { PTtuple (fst $2), Ity.MaskTuple (snd $2) } + +ret_ghost: +| ty COMMA GHOST ty { [$1; $4], [Ity.MaskVisible; Ity.MaskGhost] } +| ty COMMA ret_ghost { $1::fst $3, Ity.MaskVisible::snd $3 } +| GHOST ty COMMA ret_rest { $2::fst $4, Ity.MaskGhost::snd $4 } + +ret_rest: +| ty COMMA ret_rest { $1::fst $3, Ity.MaskVisible::snd $3 } +| GHOST ty COMMA ret_rest { $2::fst $4, Ity.MaskGhost::snd $4 } +| ty { [$1], [Ity.MaskVisible] } +| GHOST ty { [$2], [Ity.MaskGhost] } + +(* Patterns *) + +mk_pat(X): X { mk_pat $1 $startpos $endpos } + +pattern: mk_pat(pattern_) { $1 } +pat_arg: mk_pat(pat_arg_) { $1 } + +pattern_: +| pat_conj_ { $1 } +| mk_pat(pat_conj_) BAR pattern { Por ($1,$3) } + +pat_conj_: +| pat_uni_ { $1 } +| comma_list2(mk_pat(pat_uni_)) { Ptuple $1 } + +pat_uni_: +| pat_arg_ { $1 } +| uqualid pat_arg+ { Papp ($1,$2) } +| GHOST mk_pat(pat_uni_) { Pghost $2 } +| mk_pat(pat_uni_) AS boption(GHOST) var_binder + { Pas ($1,$4,$3) } +| mk_pat(pat_uni_) cast { Pcast ($1,$2) } + +pat_arg_: +| UNDERSCORE { Pwild } +| var_binder { Pvar $1 } +| uqualid { Papp ($1,[]) } +| uqualid DOT mk_pat(pat_block_) { Pscope ($1,$3) } +| pat_block_ { $1 } + +pat_block_: +| LEFTPAR RIGHTPAR { Ptuple [] } +| LEFTPAR pattern RIGHTPAR { Pparen $2 } +| LEFTBRC field_list1(pattern) RIGHTBRC { Prec $2 } + +(* let-patterns cannot start with "ghost" *) + +let_pattern: mk_pat(let_pattern_) { $1 } + +let_pattern_: +| let_pat_conj_ { $1 } +| mk_pat(let_pat_conj_) BAR pattern { Por ($1,$3) } + +let_pat_conj_: +| let_pat_uni_ { $1 } +| mk_pat(let_pat_uni_) COMMA comma_list1(mk_pat(pat_uni_)) + { Ptuple ($1::$3) } + +let_pat_uni_: +| pat_arg_ { $1 } +| uqualid pat_arg+ { Papp ($1,$2) } +| mk_pat(let_pat_uni_) AS boption(GHOST) var_binder + { Pas ($1,$4,$3) } +| mk_pat(let_pat_uni_) cast { Pcast ($1,$2) } + +(* One-variable binders *) + +sym_binder: (* let and val without parameters *) +| attrs(lident_rich) { $1 } +| AMP attrs(lident_nq) { set_ref $2 } + +var_binder: (* pattern variables *) +| attrs(lident_nq) { $1 } +| AMP attrs(lident_nq) { set_ref $2 } + +ref_binder: (* let ref and val ref *) +| attrs(lident_nq) { set_ref $1 } +| AMP attrs(lident_nq) { double_ref $2 } + +(* Qualified idents *) + +%public qualid: +| ident { Qident $1 } +| uqualid DOT ident { Qdot ($1, $3) } + +%public uqualid: +| uident { Qident $1 } +| uqualid DOT uident { Qdot ($1, $3) } + +lqualid: +| lident { Qident $1 } +| uqualid DOT lident { Qdot ($1, $3) } + +lqualid_rich: +| lident { Qident $1 } +| lident_op { Qident $1 } +| uqualid DOT lident { Qdot ($1, $3) } +| uqualid DOT lident_op { Qdot ($1, $3) } + +%public tqualid: +| uident { Qident $1 } +| squalid DOT uident { Qdot ($1, $3) } + +squalid: +| sident { Qident $1 } +| squalid DOT sident { Qdot ($1, $3) } + +(* Idents *) + +%public ident: +| uident { $1 } +| lident { $1 } +| lident_op { $1 } + +%public ident_nq: +| uident_nq { $1 } +| lident_nq { $1 } +| lident_op_nq { $1 } + +%public lident_rich: +| lident_nq { $1 } +| lident_op_nq { $1 } + +%public uident: +| UIDENT { mk_id $1 $startpos $endpos } +| CORE_UIDENT { mk_id $1 $startpos $endpos } + +%public uident_nq: +| UIDENT { mk_id $1 $startpos $endpos } +| CORE_UIDENT { let loc = floc $startpos($1) $endpos($1) in + Loc.errorm ~loc core_ident_error $1 } + +%public lident: +| LIDENT { mk_id $1 $startpos $endpos } +| lident_keyword { mk_id $1 $startpos $endpos } +| CORE_LIDENT { mk_id $1 $startpos $endpos } +| REF { mk_id "ref" $startpos $endpos } +(* we don't put REF in lident_keyword, because we do not + want it in lident_nq, not even with an error message. + This avoids a conflict in "let ref x = ...". *) + +%public lident_nq: +| LIDENT { mk_id $1 $startpos $endpos } +| lident_keyword { mk_id $1 $startpos $endpos } +| CORE_LIDENT { let loc = floc $startpos($1) $endpos($1) in + Loc.errorm ~loc core_ident_error $1 } + +lident_keyword: +| RANGE { "range" } +| FLOAT { "float" } + +sident: +| lident { $1 } +| uident { $1 } +| STRING { mk_id $1 $startpos $endpos } +(* TODO: we can add all keywords and save on quotes *) + +quote_lident: +| QUOTE_LIDENT { mk_id $1 $startpos $endpos } + +(* Symbolic operation names *) + +lident_op: +| LEFTPAR lident_op_str RIGHTPAR + { mk_id $2 $startpos($2) $endpos($2) } +| LEFTPAR lident_op_str RIGHTPAR_USCORE + { mk_id ($2^$3) $startpos $endpos } +| LEFTPAR lident_op_str RIGHTPAR_QUOTE + { mk_id ($2^$3) $startpos $endpos } + +lident_op_nq: +| LEFTPAR lident_op_str RIGHTPAR + { mk_id $2 $startpos($2) $endpos($2) } +| LEFTPAR lident_op_str RIGHTPAR_USCORE + { mk_id ($2^$3) $startpos $endpos } +| LEFTPAR lident_op_str RIGHTPAR_QUOTE + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "Symbol (%s)%s cannot be user-defined" $2 $3 } + +lident_op_str: +| op_symbol { Ident.op_infix $1 } +| op_symbol UNDERSCORE { Ident.op_prefix $1 } +| MINUS UNDERSCORE { Ident.op_prefix "-" } +| EQUAL { Ident.op_infix "=" } +| MINUS { Ident.op_infix "-" } +| OPPREF UNDERSCORE? { Ident.op_prefix $1 } +| LEFTSQ rightsq { Ident.op_get $2 } +| LEFTSQ rightsq LARROW { Ident.op_set $2 } +| LEFTSQ LARROW rightsq { Ident.op_update $3 } +| LEFTSQ DOTDOT rightsq { Ident.op_cut $3 } +| LEFTSQ UNDERSCORE DOTDOT rightsq { Ident.op_rcut $4 } +| LEFTSQ DOTDOT UNDERSCORE rightsq { Ident.op_lcut $4 } + +rightsq: +| RIGHTSQ { "" } +| RIGHTSQ_QUOTE { $1 } + +op_symbol: +| OP1 { $1 } +| OP2 { $1 } +| OP3 { $1 } +| OP4 { $1 } +| LT { "<" } +| GT { ">" } + +%inline oppref: +| o = OPPREF { mk_id (Ident.op_prefix o) $startpos $endpos } + +prefix_op: +| op_symbol { mk_id (Ident.op_prefix $1) $startpos $endpos } +| MINUS { mk_id (Ident.op_prefix "-") $startpos $endpos } + +%inline infix_op_1: +| o = OP1 { mk_id (Ident.op_infix o) $startpos $endpos } +| EQUAL { mk_id (Ident.op_infix "=") $startpos $endpos } +| LTGT { mk_id (Ident.op_infix "<>") $startpos $endpos } +| LT { mk_id (Ident.op_infix "<") $startpos $endpos } +| GT { mk_id (Ident.op_infix ">") $startpos $endpos } + +%inline infix_op_234: +| o = OP2 { mk_id (Ident.op_infix o) $startpos $endpos } +| o = OP3 { mk_id (Ident.op_infix o) $startpos $endpos } +| o = OP4 { mk_id (Ident.op_infix o) $startpos $endpos } +| MINUS { mk_id (Ident.op_infix "-") $startpos $endpos } + +(* Attributes and position markers *) + +%public attrs(X): X attr* { add_attr $1 $2 } + +%public attr: +| ATTRIBUTE { ATstr (Ident.create_attribute $1) } +| POSITION { ATpos $1 } + +(* Miscellaneous *) + +bar_list1(X): +| ioption(BAR) ; xl = separated_nonempty_list(BAR, X) { xl } + +%public with_list1(X): +| separated_nonempty_list(WITH, X) { $1 } + +comma_list2(X): +| X COMMA comma_list1(X) { $1 :: $3 } + +%public comma_list1(X): +| separated_nonempty_list(COMMA, X) { $1 } + +comma_list0(X): +| xl = separated_list(COMMA, X) { xl } + +%public semicolon_list1(X): +| x = X ; ioption(SEMICOLON) { [x] } +| x = X ; SEMICOLON ; xl = semicolon_list1(X) { x :: xl } + +located(X): X { $1, $startpos, $endpos } + +mapping_list_with_default(X): +| UNDERSCORE EQUALARROW X option(SEMICOLON) { [], Some $3 } +| X EQUALARROW X option(SEMICOLON) { [$1, $3], None } +| X EQUALARROW X SEMICOLON mapping_list_with_default(X) + { let l,d = $5 in ($1, $3) :: l, d } diff --git a/src/sleek/ptree_sleek.ml b/src/sleek/ptree_sleek.ml new file mode 100644 index 0000000000..51b0ab402c --- /dev/null +++ b/src/sleek/ptree_sleek.ml @@ -0,0 +1,469 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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. *) +(* *) +(********************************************************************) + +(** {1 Parse trees} + +The module provides datatypes for WhyML parse trees. + +These datatypes are produced by the WhyML parser module [Parser]. + +They can be alternatively produced via OCaml code, and processed later + on by typing module [Typing]. See also Section 4.9. "ML Programs" + of the documentation. + +*) + +open Mysexplib.Std [@@warning "-33"] + +(** {2 Identifiers and attributes} *) + +(** attributes, with a specific case for a source location *) +type attr = + | ATstr of Ident.attribute + | ATpos of Loc.position +[@@deriving sexp] + +(** identifiers, with attributes and a source location *) +type ident = { + id_str : string; + id_ats : attr list; + id_loc : Loc.position; +} +[@@deriving sexp] + +(** qualified identifiers *) +type qualid = + | Qident of ident + | Qdot of qualid * ident +[@@deriving sexp] + +(** {2 Types} *) + +(** type expressions *) +type pty = + | PTtyvar of ident + (** type variable *) + | PTtyapp of qualid * pty list + (** type constructor, possibly with arguments, e.g., [int], [list bool], etc. *) + | PTtuple of pty list + (** tuples, e.g., [(int,bool)] *) + | PTref of pty list + (** reference type, e.g., [ref int], as used by the "auto-dereference" + mechanism (See manual Section 13.1. "Release Notes for version + 1.2: new syntax for auto-dereference") *) + | PTarrow of pty * pty + (** arrow type, e.g., [int -> bool] *) + | PTscope of qualid * pty + (** opening scope locally, e.g., [M.((list t,u))] *) + | PTparen of pty + (** parenthesised type *) + | PTpure of pty + (** purify a type *) +[@@deriving sexp] + + +(** {2 Patterns} *) + +(** "ghost" modifier *) +type ghost = bool +[@@deriving sexp] + +(** Patterns, equipped with a source location *) +type pattern = { + pat_desc : pat_desc; + pat_loc : Loc.position; +} + +and pat_desc = + | Pwild + (** wildcard, that is "_" *) + | Pvar of ident + (** variable as a pattern *) + | Papp of qualid * pattern list + (** constructor pattern, e.g., [Cons(x,y)] *) + | Prec of (qualid * pattern) list + (** record pattern *) + | Ptuple of pattern list + (** tuple pattern *) + | Pas of pattern * ident * ghost + (** as-pattern, e.g., [Cons(x,y) as z] *) + | Por of pattern * pattern + (** or-pattern [p1 | p2] *) + | Pcast of pattern * pty + (** type cast *) + | Pscope of qualid * pattern + (** open scope locally *) + | Pparen of pattern + (** parenthesised pattern *) + | Pghost of pattern + (** explicitly ghost pattern *) +[@@deriving sexp] + + +(** {2 Logical terms and formulas} *) + +(** binder as 4-uple [(loc,id,ghost,type)] to represent "ghost? id? : + type?". [id] and [type] cannot be [None] at the same time *) +type binder = Loc.position * ident option * ghost * pty option +[@@deriving sexp] + +(** parameter as 4-uple [(loc,id,ghost,type)] to represent + "ghost? id? : type". *) +type param = Loc.position * ident option * ghost * pty +[@@deriving sexp] + +(** Terms, equipped with a source location *) +type term = { + term_desc : term_desc; + term_loc : Loc.position; +} + +and term_desc = + | Ttrue + (** the true proposition *) + | Tfalse + (** the false proposition *) + | Tconst of Constant.constant + (** constant literals *) + | Tident of qualid + (** identifiers *) + | Tasref of qualid + (** identifier as reference, e.g., [&x] (See manual Section + 13.1. "Release Notes for version 1.2: new syntax for + auto-dereference") *) + | Tidapp of qualid * term list + (** (first-order) application of a logic identifier to a list of terms *) + | Tapply of term * term + (** curried application, of a term to a term *) + | Tinfix of term * ident * term + (** application of a binary operation in an infix fashion, allowing chaining. + For example, [Tinfix(t1,"<=",Tinfix(t2,"<",t3))] denotes + [t1 <= t2 /\ t2 < t3] *) + | Tinnfix of term * ident * term + (** application of a binary operation in an infix style, but without chaining *) + | Tbinop of term * Dterm.dbinop * term + (** application of a binary logic connective, in an infix fashion, allowing + chaining. For example, [Tbinop(p1,"<->",Tbinop(p2,"<->",p3))] denotes + [(p1 <-> p2) /\ (p2 <-> p3)] *) + | Tbinnop of term * Dterm.dbinop * term + (** application of a binary logic connective, but without chaining *) + | Tnot of term + (** logic negation *) + | Tif of term * term * term + (** if-expression *) + | Tquant of Dterm.dquant * binder list * term list list * term + (** quantified formulas. The third argument is a list of triggers. *) + | Teps of ident * pty * term + (** [Teps(x,ty,f)] denotes the epsilon term "any [x] of type [ty] + that satisfies [f]". Use with caution since if there is no such + [x] satisfying [f], then it acts like introducing an inconsistent + axiom. (As a matter of fact, this is the reason why there is no + concrete syntax for such epsilon-terms.) *) + | Tattr of attr * term + (** term annotated with an attribute *) + | Tlet of ident * term * term + (** let-expression *) + | Tcase of term * (pattern * term) list + (** pattern-matching *) + | Tcast of term * pty + (** type casting *) + | Ttuple of term list + (** tuples *) + | Trecord of (qualid * term) list + (** record expressions *) + | Tupdate of term * (qualid * term) list + (** record update expression *) + | Tscope of qualid * term + (** local scope *) + | Tat of term * ident + (** "at" modifier. The "old" modifier is a particular case with + the identifier [Dexpr.old_label] *) + +[@@deriving sexp] + +(** {2 Program expressions} *) + +(** Loop invariant or type invariant *) +type invariant = term list +[@@deriving sexp] + +(** Variant for both loops and recursive functions. The option + identifier is an optional ordering predicate *) +type variant = (term * qualid option) list +[@@deriving sexp] + +(** Precondition *) +type pre = term +[@@deriving sexp] + +(** Normal postconditions *) +type post = Loc.position * (pattern * term) list +[@@deriving sexp] + +(** Exceptional postconditions *) +type xpost = Loc.position * (qualid * (pattern * term) option) list +[@@deriving sexp] + +(** Sleek contract *) +type sleek_spec = string + +(** Contract *) +type spec = { + sp_pre : pre list; (** preconditions *) + sp_post : post list; (** normal postconditions *) + sp_xpost : xpost list; (** exceptional postconditions *) + sp_reads : qualid list; (** "reads" clause *) + sp_writes : term list; (** "writes" clause *) + sp_alias : (term * term) list; (** "alias" clause *) + sp_variant : variant; (** variant for recursive functions *) + sp_checkrw : bool; (** should the reads and writes clauses be checked against the given body? *) + sp_diverge : bool; (** may the function diverge? *) + sp_partial : bool; (** is the function partial? *) +} +[@@deriving sexp] + +(** Expressions, equipped with a source location *) +type expr = { + expr_desc : expr_desc; + expr_loc : Loc.position; + } + +(** Expression kinds *) +and expr_desc = + | Eref + (** built-in operator [ref] for auto-dereference syntax. (See manual Section + 13.1. "Release Notes for version 1.2: new syntax for + auto-dereference") *) + | Etrue + (** Boolean literal [True] *) + | Efalse + (** Boolean literal [False] *) + | Econst of Constant.constant + (** Constant literals *) + | Eident of qualid + (** Variable identifier *) + | Easref of qualid + (** identifier as reference, e.g., [&x] (See manual Section + 13.1. "Release Notes for version 1.2: new syntax for + auto-dereference") *) + | Eidapp of qualid * expr list + (** Uncurried application of a function identifier to a list of arguments *) + | Eapply of expr * expr + (** Curried application *) + | Einfix of expr * ident * expr + (** application of a binary function identifier, in an infix fashion, allowing + chaining, e.g., [Einfix(e1,"<=",Einfix(e2,"<",e3))] denotes + [e1 <= e2 && e2 < e3] *) + | Einnfix of expr * ident * expr + (** application of a binary function, but without chaining *) + | Elet of ident * ghost * Expr.rs_kind * expr * expr + (** [let ... in ...] expression *) + | Erec of fundef list * expr + (** Local definition of function(s), possibly mutually recursive *) + | Efun of binder list * pty option * pattern * Ity.mask * spec * sleek_spec * expr + (** Anonymous function *) + | Eany of param list * Expr.rs_kind * pty option * pattern * Ity.mask * spec * sleek_spec + (** "any params : ty ": abstract expression with a specification, + generating a VC for existence *) + | Etuple of expr list + (** Tuple of expressions *) + | Erecord of (qualid * expr) list + (** Record expression, e.g., [{f=e1; g=e2; ...}] *) + | Eupdate of expr * (qualid * expr) list + (** Record update, e.g., [{e with f=e1; ...}] *) + | Eassign of (expr * qualid option * expr) list + (** Assignment, of a mutable variable (no qualid given) or of a record field (qualid + given). Assignments are possibly in parallel, e.g., [x.f, y.g, z <- e1, e2, e3] *) + | Esequence of expr * expr + (** Sequence of two expressions, the first one being supposed of type unit *) + | Eif of expr * expr * expr + (** [if e1 then e2 else e3] expression *) + | Ewhile of expr * invariant * variant * expr + (** [while] loop with annotations *) + | Eand of expr * expr + (** lazy conjunction *) + | Eor of expr * expr + (** lazy disjunction *) + | Enot of expr + (** Boolean negation *) + | Ematch of expr * reg_branch list * exn_branch list + (** match expression, including both regular patterns and exception + patterns (those lists cannot be both empty) *) + | Eabsurd + (** [absurd] statement to mark unreachable branches *) + | Epure of term + (** turns a logical term into a pure expression, e.g., [pure { t }] *) + | Eidpur of qualid + (** promotes a logic symbol in programs, e.g., [{f}] or [M.{f}] *) + | Eraise of qualid * expr option + (** raise an exception, possibly with an argument *) + | Eexn of ident * pty * Ity.mask * expr + (** local declaration of an exception, e.g., [let exception E in e] *) + | Eoptexn of ident * Ity.mask * expr + (** local declaration of an exception, implicitly captured. Used by Why3 for handling + [return], [break], and [continue] *) + | Efor of ident * expr * Expr.for_direction * expr * invariant * expr + (** "for" loops *) + | Eassert of Expr.assertion_kind * term + (** [assert], [assume], and [check] expressions *) + | Escope of qualid * expr + (** open scope locally, e.g., [M.(e)] *) + | Elabel of ident * expr + (** introduction of a label, e.g., [label L in e] *) + | Ecast of expr * pty + (** cast an expression to a given type, e.g., [(e:ty)] *) + | Eghost of expr + (** forces an expression to be ghost, e.g., [ghost e] *) + | Eattr of attr * expr + (** attach an attribute to an expression *) + +(** A regular match branch *) +and reg_branch = pattern * expr + +(** An exception match branch *) +and exn_branch = qualid * pattern option * expr + +(** Local function definition *) +and fundef = ident * ghost * Expr.rs_kind * + binder list * pty option * pattern * Ity.mask * spec * sleek_spec * expr +[@@deriving sexp] + +(** {2 Declarations} *) + +(** record fields *) +type field = { + f_loc : Loc.position; + f_ident : ident; + f_pty : pty; + f_mutable : bool; + f_ghost : bool +} +[@@deriving sexp] + +(** Type definition body *) +type type_def = + | TDalias of pty + (** alias type *) + | TDalgebraic of (Loc.position * ident * param list) list + (** algebraic type *) + | TDrecord of field list + (** record type *) + | TDrange of BigInt.t * BigInt.t + (** integer type in given range *) + | TDfloat of int * int + (** floating-point type with given exponent and precision *) +[@@deriving sexp] + +(** The different kinds of visibility *) +type visibility = Public | Private | Abstract (** = Private + ghost fields *) +[@@deriving sexp] + +(** A type declaration *) +type type_decl = { + td_loc : Loc.position; + td_ident : ident; + td_params : ident list; + td_vis : visibility; (** visibility, for records only *) + td_mut : bool; (** mutability, for records or abstract types *) + td_inv : invariant; (** invariant, for records only *) + td_wit : expr option; (** witness for the invariant *) + td_def : type_def; +} +[@@deriving sexp] + +(** A single declaration of a function or predicate *) +type logic_decl = { + ld_loc : Loc.position; + ld_ident : ident; + ld_params : param list; + ld_type : pty option; + ld_def : term option; +} +[@@deriving sexp] + +(** A single declaration of an inductive predicate *) +type ind_decl = { + in_loc : Loc.position; + in_ident : ident; + in_params : param list; + in_def : (Loc.position * ident * term) list; +} +[@@deriving sexp] + +(** Arguments of "meta" declarations *) +type metarg = + | Mty of pty + | Mfs of qualid + | Mps of qualid + | Max of qualid + | Mlm of qualid + | Mgl of qualid + | Mval of qualid + | Mstr of string + | Mint of int +[@@deriving sexp] + +(** The possible "clone" substitution elements *) +type clone_subst = + | CStsym of qualid * ident list * pty + | CSfsym of qualid * qualid + | CSpsym of qualid * qualid + | CSvsym of qualid * qualid + | CSxsym of qualid * qualid + | CSprop of Decl.prop_kind + | CSaxiom of qualid + | CSlemma of qualid + | CSgoal of qualid +[@@deriving sexp] + +(** top-level declarations *) +type decl = + | Dtype of type_decl list + (** Type declaration *) + | Dlogic of logic_decl list + (** Collection of "function"s and "predicate"s, mutually recursively declared *) + | Dind of Decl.ind_sign * ind_decl list + (** An inductive or co-inductive predicate *) + | Dprop of Decl.prop_kind * ident * term + (** Propositions: "lemma" or "goal" or "axiom" *) + | Dlet of ident * ghost * Expr.rs_kind * expr + (** Global program variable *) + | Drec of fundef list + (** Program functions, mutually recursively defined *) + | Dexn of ident * pty * Ity.mask + (** Declaration of global exceptions *) + | Dmeta of ident * metarg list + (** Declaration of a "meta" *) + | Dcloneexport of Loc.position * qualid * clone_subst list + (** "clone export" *) + | Duseexport of qualid + (** "use export" *) + | Dcloneimport of Loc.position * bool * qualid * ident option * clone_subst list + (** "clone import ... as ..." *) + | Duseimport of Loc.position * bool * (qualid * ident option) list + (** "use import ... as ..." *) + | Dimport of qualid + (** "import" *) + | Dscope of Loc.position * bool * ident * decl list + (** "scope" *) +[@@deriving sexp] + +let sexp_of_mlw_file _ = assert false [@@warning "-32"] +let mlw_file_of_sexp _ = assert false [@@warning "-32"] +(* default values if the line below does not produce anything, i.e., + when ppx_sexp_conv is not installed *) + +type mlw_file = + | Modules of (ident * decl list) list + (** a list of modules containing lists of declarations *) + | Decls of decl list + (** a list of declarations outside any module *) +[@@deriving sexp] From cf64dbd86aab85f95bc689757b881d3da4a959cf Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 13:52:26 +0800 Subject: [PATCH 02/12] Add support for sleek spec in the lexer --- src/sleek/lexer_sleek.mll | 15 +++- src/sleek/lexlib_sleek.mli | 1 + src/sleek/lexlib_sleek.mll | 40 ++++++++++ src/sleek/parser_sleek_tokens.ml | 129 +++++++++++++++++++++++++++++++ 4 files changed, 181 insertions(+), 4 deletions(-) create mode 100644 src/sleek/lexlib_sleek.mli create mode 100644 src/sleek/lexlib_sleek.mll create mode 100644 src/sleek/parser_sleek_tokens.ml diff --git a/src/sleek/lexer_sleek.mll b/src/sleek/lexer_sleek.mll index ddee9fe57f..738b943d22 100644 --- a/src/sleek/lexer_sleek.mll +++ b/src/sleek/lexer_sleek.mll @@ -10,7 +10,7 @@ (********************************************************************) { - open Parser_tokens + open Parser_sleek_tokens let keywords = Hashtbl.create 97 let () = @@ -118,6 +118,13 @@ rule token = parse { REAL (Number.real_literal ~radix:16 ~neg:false ~int:i ~frac:f ~exp:(Option.map Lexlib.remove_leading_plus e)) } | "(*)" { Lexlib.backjump lexbuf 2; LEFTPAR } + | "(*sleek" + { let start_p = lexbuf.Lexing.lex_start_p in + let start_pos = lexbuf.Lexing.lex_start_pos in + let sleek_spec = Lexlib_sleek.sleek_spec lexbuf in + lexbuf.Lexing.lex_start_p <- start_p; + lexbuf.Lexing.lex_start_pos <- start_pos; + SLEEK_SPEC sleek_spec } | "(*" { Lexlib.comment lexbuf; token lexbuf } | "'" (lalpha suffix as id) @@ -284,9 +291,9 @@ rule token = parse end; mm - let whyml_format = "whyml" + let whyml_sleek_format = "whyml_sleek" - let () = Env.register_format mlw_language whyml_format ["mlw";"why"] - read_channel ~desc:"WhyML@ programming@ and@ specification@ language" + let () = Env.register_format mlw_language whyml_format ["mlws"] + read_channel ~desc:"WhyML@ programming@ and@ specification@ language@ with@ Sleek" } diff --git a/src/sleek/lexlib_sleek.mli b/src/sleek/lexlib_sleek.mli new file mode 100644 index 0000000000..99e8e521d0 --- /dev/null +++ b/src/sleek/lexlib_sleek.mli @@ -0,0 +1 @@ +val sleek_spec : Lexing.lexbuf -> string diff --git a/src/sleek/lexlib_sleek.mll b/src/sleek/lexlib_sleek.mll new file mode 100644 index 0000000000..7c86e4f2bd --- /dev/null +++ b/src/sleek/lexlib_sleek.mll @@ -0,0 +1,40 @@ +{ + exception UnterminatedSleekSpec + + let () = Exn_printer.register (fun fmt e -> match e with + | UnterminatedSleekSpec -> Format.pp_print_string fmt "unterminated sleek spec" + | _ -> raise e) + + let loc lb = Loc.extract (lb.lex_start_p, lb.lex_curr_p) + + (* TODO: implement proper support for utf8 + let utf8_extra_bytes = function + | '\000'..'\127' -> 0 + | '\192'..'\223' -> 1 + | '\224'..'\239' -> 2 + | '\240'..'\247' -> 3 + | _ -> -1 + + let adjust_pos lexbuf n = + let pos = lexbuf.lex_curr_p in + lexbuf.lex_curr_p <- { pos with pos_cnum = pos.pos_cnum - n }; + lexbuf.lex_abs_pos <- lexbuf.lex_abs_pos - n + *) +} + +(* this should be quite similar to string *) +rule sleek_spec buf = parse + | "*)" + { Buffer.contents buf } + | eof + { raise (Loc.Located (loc lexbuf, UnterminatedSleekSpec)) } + | _ as c + { (* let n = utf8_extra_bytes c in + if n > 0 then adjust_pos lexbuf n; *) + Buffer.add_char buf c; + sleek_spec buf lexbuf } + +{ + let sleek_spec lexbuf = + sleek_spec (Buffer.create 128) lexbuf +} diff --git a/src/sleek/parser_sleek_tokens.ml b/src/sleek/parser_sleek_tokens.ml new file mode 100644 index 0000000000..4dc38d059a --- /dev/null +++ b/src/sleek/parser_sleek_tokens.ml @@ -0,0 +1,129 @@ + +type token = + | WRITES + | WITH + | WHILE + | VARIANT + | VAL + | USE + | UNDERSCORE + | UIDENT of (string) + | TYPE + | TRY + | TRUE + | TO + | THEORY + | THEN + | STRING of (string) + | SO + | SEMICOLON + | SCOPE + | RIGHTSQ_QUOTE of (string) + | RIGHTSQ + | RIGHTPAR_USCORE of (string) + | RIGHTPAR_QUOTE of (string) + | RIGHTPAR + | RIGHTBRC + | RETURNS + | RETURN + | REQUIRES + | REF + | REC + | REAL of (Number.real_constant) + | READS + | RANGE + | RAISES + | RAISE + | QUOTE_LIDENT of (string) + | PURE + | PRIVATE + | PREDICATE + | POSITION of (Loc.position) + | PARTIAL + | OR + | OPPREF of (string) + | OP4 of (string) + | OP3 of (string) + | OP2 of (string) + | OP1 of (string) + | OLD + | NOT + | MUTABLE + | MODULE + | MINUS + | META + | MATCH + | LTGT + | LT + | LRARROW + | LIDENT of (string) + | LET + | LEMMA + | LEFTSQBAR + | LEFTSQ + | LEFTPAR + | LEFTBRC + | LARROW + | LABEL + | INVARIANT + | INTEGER of (Number.int_constant) + | INDUCTIVE + | IN + | IMPORT + | IF + | GT + | GOAL + | GHOST + | FUNCTION + | FUN + | FORALL + | FOR + | FLOAT + | FALSE + | EXPORT + | EXISTS + | EXCEPTION + | EQUALARROW + | EQUAL + | EPSILON + | EOF + | ENSURES + | END + | ELSE + | DOWNTO + | DOTDOT + | DOT + | DONE + | DO + | DIVERGES + | CORE_UIDENT of (string) + | CORE_LIDENT of (string) + | CONTINUE + | CONSTANT + | COMMA + | COLON + | COINDUCTIVE + | CLONE + | CHECK + | BY + | BREAK + | BEGIN + | BARRIGHTSQ + | BARBAR + | BAR + | AXIOM + | ATTRIBUTE of (string) + | AT + | ASSUME + | ASSERT + | AS + | ARROW + | ANY + | AND + | AMPAMP + | AMP + | ALIAS + | ABSURD + | ABSTRACT + (* Support for Sleek *) + | SLEEK_SPEC of string From 7a1b45f11ba4df73536a62d26efdeaf98e5ebdae Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 14:02:02 +0800 Subject: [PATCH 03/12] Update imports: use *_sleek instead --- src/sleek/lexer_sleek.mll | 24 ++++++++++++------------ src/sleek/parser_sleek_common.mly | 14 +++++++------- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/sleek/lexer_sleek.mll b/src/sleek/lexer_sleek.mll index 738b943d22..bde9ebd741 100644 --- a/src/sleek/lexer_sleek.mll +++ b/src/sleek/lexer_sleek.mll @@ -217,8 +217,8 @@ rule token = parse { - let debug = Debug.register_info_flag "print_modules" - ~desc:"Print@ program@ modules@ after@ typechecking." + let debug = Debug.register_info_flag "print_sleek_modules" + ~desc:"Print@ program@ modules@ @with @Sleek@ spec@ after@ typechecking." exception Error of string option @@ -232,7 +232,7 @@ rule token = parse 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 = Parser.MenhirInterpreter in + let module I = Parser_sleek.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 @@ -257,22 +257,22 @@ rule token = parse open Pmodule let parse_term lb = - build_parsing_function Parser.Incremental.term_eof lb + build_parsing_function Parser_sleek.Incremental.term_eof lb let parse_expr lb = - build_parsing_function Parser.Incremental.expr_eof lb + build_parsing_function Parser_sleek.Incremental.expr_eof lb - let parse_decl lb = build_parsing_function Parser.Incremental.decl_eof lb + let parse_decl lb = build_parsing_function Parser_sleek.Incremental.decl_eof lb - let parse_term_list lb = build_parsing_function Parser.Incremental.term_comma_list_eof lb + let parse_term_list lb = build_parsing_function Parser_sleek.Incremental.term_comma_list_eof lb - let parse_qualid lb = build_parsing_function Parser.Incremental.qualid_eof lb + let parse_qualid lb = build_parsing_function Parser_sleek.Incremental.qualid_eof lb - let parse_list_ident lb = build_parsing_function Parser.Incremental.ident_comma_list_eof lb + let parse_list_ident lb = build_parsing_function Parser_sleek.Incremental.ident_comma_list_eof lb - let parse_list_qualid lb = build_parsing_function Parser.Incremental.qualid_comma_list_eof lb + let parse_list_qualid lb = build_parsing_function Parser_sleek.Incremental.qualid_comma_list_eof lb - let parse_mlw_file lb = build_parsing_function Parser.Incremental.mlw_file_parsing_only lb + let parse_mlw_file lb = build_parsing_function Parser_sleek.Incremental.mlw_file_parsing_only lb let read_channel env path file c = let lb = Lexing.from_channel c in @@ -280,7 +280,7 @@ rule token = parse Typing.open_file env path; let mm = try - build_parsing_function Parser.Incremental.mlw_file lb + build_parsing_function Parser_sleek.Incremental.mlw_file lb with e -> ignore (Typing.discard_file ()); raise e in diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index ae91f120fb..ce1248b521 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -17,7 +17,7 @@ *) %{ - open Pstree + open Ptree_sleek let floc s e = Loc.extract (s,e) @@ -226,9 +226,9 @@ let ifte = reduce_fun_lit add_term tl default in (* fun x -> if x ... *) let binder = (loc_begin, Some id_var, false, None) in - let desc = Ptree.Tquant (Dterm.DTlambda, [binder], [], ifte) in + let desc = Ptree_sleek.Tquant (Dterm.DTlambda, [binder], [], ifte) in let t = { term_desc = desc; term_loc = Loc.join loc_begin loc_end } in - Ptree.Tattr (Ptree.ATstr Ident.funlit, t) + Ptree_sleek.Tattr (Ptree_sleek.ATstr Ident.funlit, t) (* if el = [] then default <> None *) let expr_fun_lit loc_begin loc_end (el,default) = @@ -258,12 +258,12 @@ expr_loc = Loc.join e1.expr_loc e.expr_loc } in let ifte = reduce_fun_lit add_expr el_proxies default_proxy in let binder = (loc_begin, Some fun_id_var, false, None) in - let pattern = { pat_desc = Ptree.Pvar fun_id_var; + let pattern = { pat_desc = Ptree_sleek.Pvar fun_id_var; pat_loc = loc_begin } in let spec = { sp_pre = []; sp_post = []; sp_xpost = []; sp_reads = []; sp_writes = []; sp_alias = []; sp_variant = []; sp_checkrw = false; sp_diverge = false; sp_partial = false } in - let efun = Ptree.Efun ([binder], None, pattern, Ity.MaskVisible, spec, ifte) in + let efun = Ptree_sleek.Efun ([binder], None, pattern, Ity.MaskVisible, spec, ifte) in let efun = { expr_desc = efun; expr_loc = lit_loc } in (* let d1 = e1 in let r1 = e2 in @@ -284,7 +284,7 @@ {expr_desc; expr_loc = lit_loc} | _ -> elets in - Ptree.Eattr (Ptree.ATstr Ident.funlit, e) + Ptree_sleek.Eattr (Ptree_sleek.ATstr Ident.funlit, e) %} @@ -459,7 +459,7 @@ meta_arg: | PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) } | INDUCTIVE with_list1(inductive_decl) { Dind (Decl.Ind, $2) } | COINDUCTIVE with_list1(inductive_decl) { Dind (Decl.Coind, $2) } -| AXIOM attrs(ident_nq) COLON term { Dprop (Decl.Paxiom, { $2 with id_ats = (Ptree.ATstr Ident.useraxiom_attr)::$2.id_ats; }, $4) } +| AXIOM attrs(ident_nq) COLON term { Dprop (Decl.Paxiom, { $2 with id_ats = (Ptree_sleek.ATstr Ident.useraxiom_attr)::$2.id_ats; }, $4) } | LEMMA attrs(ident_nq) COLON term { Dprop (Decl.Plemma, $2, $4) } | GOAL attrs(ident_nq) COLON term { Dprop (Decl.Pgoal, $2, $4) } From 607993257b9d5df69a903677d806440bfbce123b Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 15:17:06 +0800 Subject: [PATCH 04/12] Augment Efun constructor with another component: sleek_spec Currently, we only support sleek spec for top-level function definition. In other occurences of Efun, an empty sleek spec is used a placeholder for now. --- src/sleek/parser_sleek_common.mly | 43 ++++++++++++++++++------------- 1 file changed, 25 insertions(+), 18 deletions(-) diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index ce1248b521..882f19afd1 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -43,7 +43,7 @@ | [], _ -> v2 | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc "multiple `variant' clauses are not allowed" - + let empty_sleek_spec = "" let empty_spec = { @@ -99,8 +99,8 @@ let apply_partial part e = if part <> Partial then e else let ed = match e.expr_desc with - | Efun (_::_ as bl, op, p, m, s, ex) -> - Efun (bl, op, p, m, apply_partial_sp part s, ex) + | Efun (_::_ as bl, op, p, m, s, ss, ex) -> + Efun (bl, op, p, m, apply_partial_sp part s, ss, ex) | Eany (_::_ as pl, rsk, op, p, m, s) -> Eany (pl, rsk, op, p, m, apply_partial_sp part s) | _ -> @@ -260,10 +260,9 @@ let binder = (loc_begin, Some fun_id_var, false, None) in let pattern = { pat_desc = Ptree_sleek.Pvar fun_id_var; pat_loc = loc_begin } in - let spec = { sp_pre = []; sp_post = []; sp_xpost = []; sp_reads = []; - sp_writes = []; sp_alias = []; sp_variant = []; - sp_checkrw = false; sp_diverge = false; sp_partial = false } in - let efun = Ptree_sleek.Efun ([binder], None, pattern, Ity.MaskVisible, spec, ifte) in + let spec = empty_spec in + let sleek_spec = empty_sleek_spec in + let efun = Ptree_sleek.Efun ([binder], None, pattern, Ity.MaskVisible, spec, sleek_spec, ifte) in let efun = { expr_desc = efun; expr_loc = lit_loc } in (* let d1 = e1 in let r1 = e2 in @@ -302,6 +301,10 @@ %token RIGHTPAR_QUOTE (* )'spec *) %token RIGHTPAR_USCORE (* )_spec *) +(* sleek spec *) + +%token SLEEK_SPEC + (* keywords *) %token AS AXIOM BY CLONE COINDUCTIVE CONSTANT @@ -927,12 +930,13 @@ rec_defn: $3, ghost $1, $2, $4, ty, pat, mask, apply_partial_sp $1 spec, e } fun_defn: -| binders return_opt spec EQUAL spec seq_expr - { let pat, ty, mask = $2 in - let spec = apply_return pat (spec_union $3 $5) in - let id = mk_id return_id $startpos($4) $endpos($4) in - let e = { $6 with expr_desc = Eoptexn (id, mask, $6) } in - Efun ($1, ty, pat, mask, spec, e) } +| sleek_spec binders return_opt spec EQUAL spec seq_expr + { let pat, ty, mask = $3 in + let spec = apply_return pat (spec_union $4 $6) in + let id = mk_id return_id $startpos($5) $endpos($5) in + let e = { $7 with expr_desc = Eoptexn (id, mask, $7) } in + let sleek_spec = $1 in + Efun ($2, ty, pat, mask, spec, sleek_spec, e) } fun_decl: | params1 return_opt spec @@ -958,11 +962,11 @@ mk_expr(X): d = X { mk_expr d $startpos $endpos } | contract_expr SEMICOLON seq_expr { mk_expr (Esequence ($1, $3)) $startpos $endpos } -%public contract_expr: +%public contract_expr: (* TODO: do we need to augment this rule with sleek spec? *) | assign_expr %prec prec_no_spec { $1 } | assign_expr single_spec spec { let p = mk_pat Pwild $startpos $endpos in - let d = Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, $1) in + let d = Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, empty_sleek_spec, $1) in let d = Eattr (ATstr Vc.wb_attr, mk_expr d $startpos $endpos) in mk_expr d $startpos $endpos } @@ -1067,7 +1071,7 @@ single_expr_: { let id = mk_id return_id $startpos($4) $endpos($4) in let e = { $6 with expr_desc = Eoptexn (id, Ity.MaskVisible, $6) } in let p = mk_pat Pwild $startpos $endpos in - Efun ($2, None, p, Ity.MaskVisible, spec_union $3 $5, e) } + Efun ($2, None, p, Ity.MaskVisible, spec_union $3 $5, empty_sleek_spec, e) } | ANY return_named spec { let pat, ty, mask = $2 in let loc = floc $startpos $endpos in @@ -1215,11 +1219,11 @@ expr_dot_: expr_block_: | BEGIN single_spec spec seq_expr END { let p = mk_pat Pwild $startpos $endpos in - Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, $4) } + Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, empty_sleek_spec, $4) } | BEGIN single_spec spec END { let e = mk_expr (Etuple []) $startpos $endpos in let p = mk_pat Pwild $startpos $endpos in - Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, e) } + Efun ([], None, p, Ity.MaskVisible, spec_union $2 $3, empty_sleek_spec, e) } | BEGIN seq_expr END { $2.expr_desc } | LEFTPAR seq_expr RIGHTPAR { $2.expr_desc } | BEGIN END { Etuple [] } @@ -1290,6 +1294,9 @@ for_dir: (* Specification *) +sleek_spec: +| (* TODO *) + %public spec: | (* epsilon *) %prec prec_no_spec { empty_spec } | single_spec spec { spec_union $1 $2 } From 3c483cdb1034ac5c5f05ee30155448097a33c5f7 Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 15:23:16 +0800 Subject: [PATCH 05/12] Augment Eany constructor with sleek_spec Currently, we only support sleek spec at fun_decl and const_decl. --- src/sleek/parser_sleek_common.mly | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index 882f19afd1..8421941b85 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -101,8 +101,8 @@ let ed = match e.expr_desc with | Efun (_::_ as bl, op, p, m, s, ss, ex) -> Efun (bl, op, p, m, apply_partial_sp part s, ss, ex) - | Eany (_::_ as pl, rsk, op, p, m, s) -> - Eany (pl, rsk, op, p, m, apply_partial_sp part s) + | Eany (_::_ as pl, rsk, op, p, m, s, ss) -> + Eany (pl, rsk, op, p, m, apply_partial_sp part s, ss) | _ -> Loc.errorm ~loc:e.expr_loc "this expression cannot be declared partial" in @@ -939,14 +939,14 @@ fun_defn: Efun ($2, ty, pat, mask, spec, sleek_spec, e) } fun_decl: -| params1 return_opt spec - { let pat, ty, mask = $2 in - Eany ($1, Expr.RKnone, ty, pat, mask, apply_return pat $3) } +| sleek_spec params1 return_opt spec + { let pat, ty, mask = $3 in + Eany ($2, Expr.RKnone, ty, pat, mask, apply_return pat $4, $1) } const_decl: -| return_opt spec - { let pat, ty, mask = $1 in - Eany ([], Expr.RKnone, ty, pat, mask, apply_return pat $2) } +| sleek_spec return_opt spec + { let pat, ty, mask = $2 in + Eany ([], Expr.RKnone, ty, pat, mask, apply_return pat $3, $1) } const_defn: | cast EQUAL seq_expr { { $3 with expr_desc = Ecast ($3, $1) } } @@ -1087,7 +1087,7 @@ single_expr_: let pre = pre_of_any loc ty spec.sp_post in let spec = { spec with sp_pre = spec.sp_pre @ pre } in let p = mk_pat Pwild $startpos $endpos in - Eany ([], Expr.RKnone, Some ty, p, mask, spec) } + Eany ([], Expr.RKnone, Some ty, p, mask, spec, empty_sleek_spec) } | VAL ghost kind attrs(lident_rich) mk_expr(fun_decl) IN seq_expr { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) } | VAL ghost kind sym_binder mk_expr(const_decl) IN seq_expr From 2cec05a17b07f5eb1d915b356102e407cac6a6cd Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 15:27:50 +0800 Subject: [PATCH 06/12] Augment fundef tuple with sleek_spec component --- src/sleek/parser_sleek_common.mly | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index 8421941b85..bfe6bc56bf 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -922,12 +922,13 @@ kind: (* Function definitions *) rec_defn: -| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr - { let pat, ty, mask = $5 in - let spec = apply_return pat (spec_union $6 $8) in - let id = mk_id return_id $startpos($7) $endpos($7) in - let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in - $3, ghost $1, $2, $4, ty, pat, mask, apply_partial_sp $1 spec, e } +| sleek_spec ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr + { let pat, ty, mask = $6 in + let spec = apply_return pat (spec_union $7 $9) in + let id = mk_id return_id $startpos($8) $endpos($8) in + let e = { $10 with expr_desc = Eoptexn (id, mask, $10) } in + let sleek_spec = $1 in + $4, ghost $2, $3, $5, ty, pat, mask, apply_partial_sp $2 spec, sleek_spec, e } fun_defn: | sleek_spec binders return_opt spec EQUAL spec seq_expr From 2ea99e8d98993eca6b6c77362466c3cde609603f Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 15:33:35 +0800 Subject: [PATCH 07/12] Use a trivial implementation for sleek spec --- src/sleek/parser_sleek_common.mly | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index bfe6bc56bf..71fc77150a 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -345,6 +345,12 @@ %nonassoc LET VAL EXCEPTION %nonassoc prec_no_else %nonassoc DOT ELSE RETURN + +(* Sleek *) +%nonassoc prec_no_sleek_spec +%nonassoc SLEEK_SPEC +(* Sleek *) + %nonassoc prec_no_spec %nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT %nonassoc below_LARROW @@ -1295,8 +1301,9 @@ for_dir: (* Specification *) -sleek_spec: -| (* TODO *) +sleek_spec: (* TODO: change the representation of sleek spec *) +| (* epsilon *) %prec prec_no_sleek_spec { empty_sleek_spec } +| SLEEK_SPEC { $1 } %public spec: | (* epsilon *) %prec prec_no_spec { empty_spec } From 07b73d345a9a5872e4889e9e625abfa4efeb07af Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Mon, 24 Jun 2024 15:55:31 +0800 Subject: [PATCH 08/12] Add interface files for lexer and parser --- src/sleek/lexer_sleek.mli | 34 +++++++++++++++++++++ src/sleek/parser_sleek.mli | 61 ++++++++++++++++++++++++++++++++++++++ src/sleek/parser_sleek.mly | 25 ++++++++-------- 3 files changed, 108 insertions(+), 12 deletions(-) create mode 100644 src/sleek/lexer_sleek.mli create mode 100644 src/sleek/parser_sleek.mli diff --git a/src/sleek/lexer_sleek.mli b/src/sleek/lexer_sleek.mli new file mode 100644 index 0000000000..28a7575915 --- /dev/null +++ b/src/sleek/lexer_sleek.mli @@ -0,0 +1,34 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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. *) +(* *) +(********************************************************************) + +val parse_term : Lexing.lexbuf -> Ptree_sleek.term + +val parse_expr : Lexing.lexbuf -> Ptree_sleek.expr + +val parse_decl : Lexing.lexbuf -> Ptree_sleek.decl + +val parse_term_list: Lexing.lexbuf -> Ptree_sleek.term list + +val parse_qualid: Lexing.lexbuf -> Ptree_sleek.qualid + +val parse_list_qualid: Lexing.lexbuf -> Ptree_sleek.qualid list + +val parse_list_ident: Lexing.lexbuf -> Ptree_sleek.ident list + +(* TODO: mlws file instead of mlw file *) +val parse_mlw_file: Lexing.lexbuf -> Ptree_sleek.mlw_file + +(* TODO: no longer return Pmodule.mlw_file *) +val read_channel: Env.env -> Env.pathname -> string -> in_channel -> + Pmodule.mlw_file + +(* Name of the registered format for whyml *) +val whyml_sleek_format: Env.fformat diff --git a/src/sleek/parser_sleek.mli b/src/sleek/parser_sleek.mli new file mode 100644 index 0000000000..ea4b4847b1 --- /dev/null +++ b/src/sleek/parser_sleek.mli @@ -0,0 +1,61 @@ + +(* The type of tokens. *) + +type token = Parser_sleek_tokens.token + +(* This exception is raised by the monolithic API functions. *) + +exception Error + +(* The monolithic API. *) + +val term_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.term) + +val term_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.term list) + +val qualid_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.qualid) + +val qualid_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.qualid list) + +val mlw_file_parsing_only: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.mlw_file) + +val mlw_file: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Pmodule.pmodule Wstdlib.Mstr.t) + +val ident_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.ident list) + +val expr_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.expr) + +val decl_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.decl) + +module MenhirInterpreter : sig + + (* The incremental API. *) + + include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE + with type token = token + +end + +(* The entry point(s) to the incremental API. *) + +module Incremental : sig + + val term_eof: Lexing.position -> (Ptree_sleek.term) MenhirInterpreter.checkpoint + + val term_comma_list_eof: Lexing.position -> (Ptree_sleek.term list) MenhirInterpreter.checkpoint + + val qualid_eof: Lexing.position -> (Ptree_sleek.qualid) MenhirInterpreter.checkpoint + + val qualid_comma_list_eof: Lexing.position -> (Ptree_sleek.qualid list) MenhirInterpreter.checkpoint + + val mlw_file_parsing_only: Lexing.position -> (Ptree_sleek.mlw_file) MenhirInterpreter.checkpoint + + val mlw_file: Lexing.position -> (Pmodule.pmodule Wstdlib.Mstr.t) MenhirInterpreter.checkpoint + + val ident_comma_list_eof: Lexing.position -> (Ptree_sleek.ident list) MenhirInterpreter.checkpoint + + val expr_eof: Lexing.position -> (Ptree_sleek.expr) MenhirInterpreter.checkpoint + + val decl_eof: Lexing.position -> (Ptree_sleek.decl) MenhirInterpreter.checkpoint + +end diff --git a/src/sleek/parser_sleek.mly b/src/sleek/parser_sleek.mly index 552b42ee71..87637540ac 100644 --- a/src/sleek/parser_sleek.mly +++ b/src/sleek/parser_sleek.mly @@ -16,15 +16,16 @@ (* Entry points *) %start mlw_file -%start mlw_file_parsing_only -%start term_eof -%start expr_eof -%start decl_eof -%start qualid_eof -%start qualid_comma_list_eof -%start term_comma_list_eof -%start ident_comma_list_eof +%start mlw_file_parsing_only +%start term_eof +%start expr_eof +%start decl_eof +%start qualid_eof +%start qualid_comma_list_eof +%start term_comma_list_eof +%start ident_comma_list_eof +(* TODO: replace side effect of functions *) %% @@ -141,12 +142,12 @@ module_decl_no_head_parsing_only: use_clone: | USE EXPORT tqualid { let loc = floc $startpos $endpos in - let decl = Ptree.Duseexport $3 in + let decl = Ptree_sleek.Duseexport $3 in Typing.add_decl loc decl } | CLONE EXPORT tqualid clone_subst { let loc = floc $startpos $endpos in - let decl = Ptree.Dcloneexport(loc,$3,$4) in + let decl = Ptree_sleek.Dcloneexport(loc,$3,$4) in Typing.add_decl loc decl } | USE boption(IMPORT) m_as_list = comma_list1(use_as) @@ -155,7 +156,7 @@ use_clone: let import = $2 in if import && not exists_as then Loc.warning ~loc warn_redundant_import "the keyword `import' is redundant here and can be omitted"; - let decl = Ptree.Duseimport(loc,import,m_as_list) in + let decl = Ptree_sleek.Duseimport(loc,import,m_as_list) in Typing.add_decl loc decl } | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst @@ -164,6 +165,6 @@ use_clone: let as_opt = $4 in if import && as_opt = None then Loc.warning ~loc warn_redundant_import "the keyword `import' is redundant here and can be omitted"; - let decl = Ptree.Dcloneimport(loc,import,$3,as_opt,$5) in + let decl = Ptree_sleek.Dcloneimport(loc,import,$3,as_opt,$5) in Typing.add_decl loc decl } From d318a5382da289da42cab5dd1c04597a26ccf8a5 Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Tue, 25 Jun 2024 13:47:24 +0800 Subject: [PATCH 09/12] Try to update build script for sleek --- Makefile.in | 29 ++++++++- src/sleek/lexer_sleek.mli | 4 +- src/sleek/lexer_sleek.mll | 4 +- src/sleek/parser_sleek.mly | 118 +++++++++++++++++++------------------ 4 files changed, 92 insertions(+), 63 deletions(-) diff --git a/Makefile.in b/Makefile.in index 900d6ca39f..2dd4eb1511 100644 --- a/Makefile.in +++ b/Makefile.in @@ -222,6 +222,7 @@ GENERATED = # Why3 library ############## +# sleek support LIBGENERATED = \ src/util/config.ml \ src/util/rc.ml src/util/lexlib.ml src/util/mysexplib.ml \ @@ -235,7 +236,11 @@ LIBGENERATED = \ src/driver/driver_lexer.ml \ src/driver/sexp.ml \ src/session/compress.ml src/session/xml.ml \ - src/session/strategy_parser.ml + src/session/strategy_parser.ml \ + src/sleek/lexer_sleek.ml \ + src/sleek/lexlib_sleek.ml \ + src/sleek/parser_sleek_tokens.mli src/sleek/parser_sleek_tokens.ml \ + src/sleek/parser_sleek.mli src/sleek/parser_sleek.ml \ LIB_UTIL = exn_printer mysexplib config bigInt mlmpfr_wrapper util opt lists strings \ pp extmap extset exthtbl weakhtbl diffmap hcpt \ @@ -303,8 +308,12 @@ LIB_SESSION = compress xml termcode session_itp \ server_utils itp_communication \ itp_server json_util unix_scheduler +# sleek support +LIB_SLEEK = lexer_sleek lexlib_sleek parser_sleek_tokens parser_sleek ptree_sleek + LIB_CMIONLY = driver/driver_ast +# sleek support LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \ $(addprefix src/core/, $(LIB_CORE)) \ $(addprefix src/driver/, $(LIB_DRIVER)) \ @@ -315,9 +324,11 @@ LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \ $(addprefix src/parser/, $(LIB_PARSER)) \ $(addprefix src/transform/, $(LIB_TRANSFORM)) \ $(addprefix src/printer/, $(LIB_PRINTER)) \ - $(addprefix src/session/, $(LIB_SESSION)) + $(addprefix src/session/, $(LIB_SESSION)) \ + $(addprefix src/sleek/, $(LIB_SLEEK)) -LIBDIRS = util core driver mlw extract parser transform printer session +# sleek support +LIBDIRS = util core driver mlw extract parser transform printer session sleek ifeq (@enable_infer@,yes) LIBDIRS += infer @@ -339,6 +350,8 @@ $(LIBCMX): OFLAGS += -for-pack Why3 $(LIBDEP): $(LIBGENERATED) +# TODO: sleek support for ptree_sleek? + src/parser/ptree.cmx src/parser/ptree.cmo: FLAGS += -w -70 src/util/mysexplib.cmx src/util/mysexplib.cmo: FLAGS += -w -70 @@ -2107,6 +2120,16 @@ pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.m $(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser $^ $(HIDE)for f in plugins/cfg/cfg_parser.mli plugins/cfg/cfg_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done +# sleek support +src/s%eek/parser_sleek_tokens.ml src/s%eek/parser_sleek_tokens.mli: src/sleek/sleek_parser_common.mly + $(SHOW) 'Menhir $^' + $(HIDE)$(MENHIR) --base src/sleek/parser_sleek_tokens --only-tokens $^ + +src/s%eek/parser_sleek.ml src/s%eek/parser_sleek.mli: src/sleek/parser_sleek_common.mly src/sleek/parser_sleek.mly + $(SHOW) 'Menhir $^' + $(HIDE)$(MENHIR) --table --explain --strict --base src/sleek/parser_sleek \ + --external-tokens Parser_sleek_tokens $^ + %.ml %.mli: %.mly $(SHOW) 'Menhir $<' $(HIDE)$(MENHIR) --table --explain --strict $< diff --git a/src/sleek/lexer_sleek.mli b/src/sleek/lexer_sleek.mli index 28a7575915..2cdc961c27 100644 --- a/src/sleek/lexer_sleek.mli +++ b/src/sleek/lexer_sleek.mli @@ -27,8 +27,8 @@ val parse_list_ident: Lexing.lexbuf -> Ptree_sleek.ident list val parse_mlw_file: Lexing.lexbuf -> Ptree_sleek.mlw_file (* TODO: no longer return Pmodule.mlw_file *) -val read_channel: Env.env -> Env.pathname -> string -> in_channel -> - Pmodule.mlw_file +(* val read_channel: Env.env -> Env.pathname -> string -> in_channel -> + Pmodule.mlw_file *) (* Name of the registered format for whyml *) val whyml_sleek_format: Env.fformat diff --git a/src/sleek/lexer_sleek.mll b/src/sleek/lexer_sleek.mll index bde9ebd741..6b5145c3ce 100644 --- a/src/sleek/lexer_sleek.mll +++ b/src/sleek/lexer_sleek.mll @@ -274,7 +274,7 @@ rule token = parse let parse_mlw_file lb = build_parsing_function Parser_sleek.Incremental.mlw_file_parsing_only lb - let read_channel env path file c = + (* let read_channel env path file c = let lb = Lexing.from_channel c in Loc.set_file file lb; Typing.open_file env path; @@ -289,7 +289,7 @@ rule token = parse let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in Mid.iter print_m (Mstr.fold add_m mm Mid.empty) end; - mm + mm *) let whyml_sleek_format = "whyml_sleek" diff --git a/src/sleek/parser_sleek.mly b/src/sleek/parser_sleek.mly index 87637540ac..6081bb128b 100644 --- a/src/sleek/parser_sleek.mly +++ b/src/sleek/parser_sleek.mly @@ -15,7 +15,7 @@ (* Entry points *) -%start mlw_file +// %start mlw_file %start mlw_file_parsing_only %start term_eof %start expr_eof @@ -60,13 +60,13 @@ term_comma_list_eof: (* Modules and scopes *) -mlw_file: -| EOF -| mlw_module mlw_module_no_decl* EOF - { Typing.close_file () } -| module_decl module_decl_no_head* EOF - { let loc = floc $startpos($3) $endpos($3) in - Typing.close_module loc; Typing.close_file () } +// mlw_file: +// | EOF +// | mlw_module mlw_module_no_decl* EOF + // { Typing.close_file () } +// | module_decl module_decl_no_head* EOF + // { let loc = floc $startpos($3) $endpos($3) in + // Typing.close_module loc; Typing.close_file () } mlw_file_parsing_only: | EOF { (Modules([])) } @@ -76,95 +76,101 @@ mlw_file_parsing_only: mlw_module: | module_head module_decl_no_head* END - { Typing.close_module (floc $startpos($3) $endpos($3)) } + // { Typing.close_module (floc $startpos($3) $endpos($3)) } mlw_module_parsing_only: -| module_head_parsing_only module_decl_no_head_parsing_only* END { ($1,$2) } +| module_head_parsing_only module_decl_no_head_parsing_only* END + { ($1, $2) } module_head: -| THEORY attrs(uident_nq) { Typing.open_module $2 } +| THEORY attrs(uident_nq) + // { Typing.open_module $2 } | MODULE attrs(uident_nq) intf = option(preceded(COLON, tqualid)) - { Typing.open_module ?intf $2 } + // { Typing.open_module ?intf $2 } scope_head: | SCOPE boption(IMPORT) attrs(uident_nq) - { Typing.open_scope (floc $startpos $endpos) $3; $2 } + // { Typing.open_scope (floc $startpos $endpos) $3; $2 } module_decl: | scope_head module_decl* END - { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 } + // { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 } | IMPORT uqualid - { Typing.add_decl (floc $startpos $endpos) (Dimport($2)) } + // { Typing.add_decl (floc $startpos $endpos) (Dimport($2)) } | d = pure_decl | d = prog_decl | d = meta_decl - { Typing.add_decl (floc $startpos $endpos) d } -| use_clone { () } + // { Typing.add_decl (floc $startpos $endpos) d } +| use_clone + // { () } module_decl_parsing_only: | scope_head_parsing_only module_decl_parsing_only* END - { let loc,import,qid = $1 in (Dscope(loc,import,qid,$2))} -| IMPORT uqualid { (Dimport $2) } -| d = pure_decl | d = prog_decl | d = meta_decl { d } -| use_clone_parsing_only { $1 } + { let loc, import, qid = $1 in (Dscope(loc, import, qid, $2)) } +| IMPORT uqualid + { (Dimport $2) } +| d = pure_decl | d = prog_decl | d = meta_decl + { d } +| use_clone_parsing_only + { $1 } (* Do not open inside another module *) mlw_module_no_decl: | SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl - { let loc = floc $startpos $endpos in - Loc.errorm ~loc "trying to open a module inside another module" } + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } | mlw_module - { $1 } + { $1 } mlw_module_no_decl_parsing_only: | SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl - { let loc = floc $startpos $endpos in - Loc.errorm ~loc "trying to open a module inside another module" } + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } | mlw_module_parsing_only - { $1 } + { $1 } module_decl_no_head: | THEORY | MODULE - { let loc = floc $startpos $endpos in + { let loc = floc $startpos $endpos in Loc.errorm ~loc "trying to open a module inside another module" } | module_decl - { $1 } + { $1 } module_decl_no_head_parsing_only: | THEORY | MODULE - { let loc = floc $startpos $endpos in - Loc.errorm ~loc "trying to open a module inside another module" } + { let loc = floc $startpos $endpos in + Loc.errorm ~loc "trying to open a module inside another module" } | module_decl_parsing_only - { $1 } + { $1 } (* Use and clone *) use_clone: | USE EXPORT tqualid - { let loc = floc $startpos $endpos in - let decl = Ptree_sleek.Duseexport $3 in - Typing.add_decl loc decl - } + // { let loc = floc $startpos $endpos in + // let decl = Ptree_sleek.Duseexport $3 in + // Typing.add_decl loc decl + // } | CLONE EXPORT tqualid clone_subst - { let loc = floc $startpos $endpos in - let decl = Ptree_sleek.Dcloneexport(loc,$3,$4) in - Typing.add_decl loc decl - } + // { let loc = floc $startpos $endpos in + // let decl = Ptree_sleek.Dcloneexport(loc,$3,$4) in + // Typing.add_decl loc decl + // } | USE boption(IMPORT) m_as_list = comma_list1(use_as) - { let loc = floc $startpos $endpos in - let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in - let import = $2 in - if import && not exists_as then Loc.warning ~loc warn_redundant_import - "the keyword `import' is redundant here and can be omitted"; - let decl = Ptree_sleek.Duseimport(loc,import,m_as_list) in - Typing.add_decl loc decl - } + // { let loc = floc $startpos $endpos in + // let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in + // let import = $2 in + // if import && not exists_as then Loc.warning ~loc warn_redundant_import + // "the keyword `import' is redundant here and can be omitted"; + // let decl = Ptree_sleek.Duseimport(loc,import,m_as_list) in + // Typing.add_decl loc decl + // } | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst - { let loc = floc $startpos $endpos in - let import = $2 in - let as_opt = $4 in - if import && as_opt = None then Loc.warning ~loc warn_redundant_import - "the keyword `import' is redundant here and can be omitted"; - let decl = Ptree_sleek.Dcloneimport(loc,import,$3,as_opt,$5) in - Typing.add_decl loc decl - } + // { let loc = floc $startpos $endpos in + // let import = $2 in + // let as_opt = $4 in + // if import && as_opt = None then Loc.warning ~loc warn_redundant_import + // "the keyword `import' is redundant here and can be omitted"; + // let decl = Ptree_sleek.Dcloneimport(loc,import,$3,as_opt,$5) in + // Typing.add_decl loc decl + // } From 6cf5408f2d8b1107901516da4c0ad648b9f29b6d Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Wed, 26 Jun 2024 13:34:26 +0800 Subject: [PATCH 10/12] Modify build file to support sleek parser It finally works... --- .gitignore | 9 ++ Makefile.in | 8 +- genmake.sh | 5 ++ src/sleek/keywords_sleek.ml | 110 ++++++++++++++++++++++++ src/sleek/keywords_sleek.mli | 15 ++++ src/sleek/lexer_sleek.mll | 34 +++----- src/sleek/lexlib_sleek.mll | 2 + src/sleek/parser_sleek.mli | 61 -------------- src/sleek/parser_sleek.mly | 133 +++++++++++++++--------------- src/sleek/parser_sleek_common.mly | 65 +++++++-------- src/sleek/parser_sleek_tokens.ml | 129 ----------------------------- src/sleek/ptree_sleek.ml | 1 + 12 files changed, 254 insertions(+), 318 deletions(-) create mode 100755 genmake.sh create mode 100644 src/sleek/keywords_sleek.ml create mode 100644 src/sleek/keywords_sleek.mli delete mode 100644 src/sleek/parser_sleek.mli delete mode 100644 src/sleek/parser_sleek_tokens.ml diff --git a/.gitignore b/.gitignore index c550c66ebc..36f3ee3e6e 100644 --- a/.gitignore +++ b/.gitignore @@ -319,3 +319,12 @@ trywhy3.tar.gz # Opam _opam/ + +# /src/sleek/ +/src/sleek/lexer_sleek.ml +/src/sleek/parser_sleek.ml +/src/sleek/parser_sleek.mli +/src/sleek/parser_sleek.conflicts +/src/sleek/lexlib_sleek.ml +/src/sleek/parser_sleek_tokens.ml +/src/sleek/parser_sleek_tokens.mli diff --git a/Makefile.in b/Makefile.in index 2dd4eb1511..9fd14f7043 100644 --- a/Makefile.in +++ b/Makefile.in @@ -240,7 +240,7 @@ LIBGENERATED = \ src/sleek/lexer_sleek.ml \ src/sleek/lexlib_sleek.ml \ src/sleek/parser_sleek_tokens.mli src/sleek/parser_sleek_tokens.ml \ - src/sleek/parser_sleek.mli src/sleek/parser_sleek.ml \ + src/sleek/parser_sleek.mli src/sleek/parser_sleek.ml LIB_UTIL = exn_printer mysexplib config bigInt mlmpfr_wrapper util opt lists strings \ pp extmap extset exthtbl weakhtbl diffmap hcpt \ @@ -309,7 +309,9 @@ LIB_SESSION = compress xml termcode session_itp \ itp_server json_util unix_scheduler # sleek support -LIB_SLEEK = lexer_sleek lexlib_sleek parser_sleek_tokens parser_sleek ptree_sleek +LIB_SLEEK = \ + ptree_sleek lexlib_sleek parser_sleek_tokens parser_sleek \ + keywords_sleek lexer_sleek LIB_CMIONLY = driver/driver_ast @@ -2121,7 +2123,7 @@ pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.m $(HIDE)for f in plugins/cfg/cfg_parser.mli plugins/cfg/cfg_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done # sleek support -src/s%eek/parser_sleek_tokens.ml src/s%eek/parser_sleek_tokens.mli: src/sleek/sleek_parser_common.mly +src/s%eek/parser_sleek_tokens.ml src/s%eek/parser_sleek_tokens.mli: src/sleek/parser_sleek_common.mly $(SHOW) 'Menhir $^' $(HIDE)$(MENHIR) --base src/sleek/parser_sleek_tokens --only-tokens $^ diff --git a/genmake.sh b/genmake.sh new file mode 100755 index 0000000000..353ce085d8 --- /dev/null +++ b/genmake.sh @@ -0,0 +1,5 @@ +#!/bin/sh -eux + +autoconf +./configure --enable-local --disable-ide --disable-web-ide --disable-coq-libs --disable-pvs-libs --disable-isabelle-libs --disable-doc --disable-emacs-compilation + diff --git a/src/sleek/keywords_sleek.ml b/src/sleek/keywords_sleek.ml new file mode 100644 index 0000000000..09437cd894 --- /dev/null +++ b/src/sleek/keywords_sleek.ml @@ -0,0 +1,110 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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 Parser_sleek_tokens + +(* keep the following files synchronized: + + doc/ext/why3.py + plugins/cfg/cfg_lexer.mll + share/emacs/why3.el + share/vim/syntax/why3.vim + src/trywhy3/mode-why3.js +*) + +let plain = [ + "abstract", ABSTRACT; + "absurd", ABSURD; + "alias", ALIAS; + "any", ANY; + "as", AS; + "assert", ASSERT; + "assume", ASSUME; + "at", AT; + "axiom", AXIOM; + "begin", BEGIN; + "break", BREAK; + "by", BY; + "check", CHECK; + "clone", CLONE; + "coinductive", COINDUCTIVE; + "constant", CONSTANT; + "continue", CONTINUE; + "diverges", DIVERGES; + "do", DO; + "done", DONE; + "downto", DOWNTO; + "else", ELSE; + "end", END; + "ensures", ENSURES; + "epsilon", EPSILON; + "exception", EXCEPTION; + "exists", EXISTS; + "export", EXPORT; + "false", FALSE; + "for", FOR; + "forall", FORALL; + "fun", FUN; + "function", FUNCTION; + "ghost", GHOST; + "goal", GOAL; + "if", IF; + "import", IMPORT; + "in", IN; + "inductive", INDUCTIVE; + "invariant", INVARIANT; + "label", LABEL; + "lemma", LEMMA; + "let", LET; + "match", MATCH; + "meta", META; + "module", MODULE; + "mutable", MUTABLE; + "not", NOT; + "old", OLD; + "partial", PARTIAL; + "predicate", PREDICATE; + "private", PRIVATE; + "pure", PURE; + "raise", RAISE; + "raises", RAISES; + "reads", READS; + "rec", REC; + "requires", REQUIRES; + "return", RETURN; + "returns", RETURNS; + "scope", SCOPE; + "so", SO; + "then", THEN; + "theory", THEORY; + "to", TO; + "true", TRUE; + "try", TRY; + "type", TYPE; + "use", USE; + "val", VAL; + "variant", VARIANT; + "while", WHILE; + "with", WITH; + "writes", WRITES; + ] + +let contextual = [ + "float", FLOAT; + "range", RANGE; + "ref", REF; + ] + +let keyword_tokens = + plain @ contextual + +let keywords = + List.map fst plain diff --git a/src/sleek/keywords_sleek.mli b/src/sleek/keywords_sleek.mli new file mode 100644 index 0000000000..f697939adc --- /dev/null +++ b/src/sleek/keywords_sleek.mli @@ -0,0 +1,15 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2023 -- Inria - CNRS - Paris-Saclay 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. *) +(* *) +(********************************************************************) + +val keyword_tokens: (string * Parser_sleek.token) list + +(* does not include contextual tokens *) +val keywords: string list diff --git a/src/sleek/lexer_sleek.mll b/src/sleek/lexer_sleek.mll index 6b5145c3ce..3d1490702b 100644 --- a/src/sleek/lexer_sleek.mll +++ b/src/sleek/lexer_sleek.mll @@ -14,7 +14,7 @@ let keywords = Hashtbl.create 97 let () = - List.iter (fun (x,y) -> Hashtbl.add keywords x y) Keywords.keyword_tokens + List.iter (fun (x,y) -> Hashtbl.add keywords x y) Keywords_sleek.keyword_tokens let warn_inexistent_file = Loc.register_warning "inexistent_file" "Warn about inexistent file in source location" @@ -216,10 +216,6 @@ rule token = parse { Lexlib.illegal_character c lexbuf } { - - let debug = Debug.register_info_flag "print_sleek_modules" - ~desc:"Print@ program@ modules@ @with @Sleek@ spec@ after@ typechecking." - exception Error of string option let () = Exn_printer.register (fun fmt exn -> match exn with @@ -238,16 +234,10 @@ rule token = parse I.lexer_lexbuf_to_supplier (fun x -> let t = token x in last := t; t) lb and succeed t = t and fail checkpoint = - let text = Lexing.lexeme lb in - let fname = lb.Lexing.lex_curr_p.Lexing.pos_fname in - (* TODO/FIXME: ad-hoc fix for TryWhy3/Str incompatibility *) - let s = if Strings.has_prefix "/trywhy3_input." fname - then None - else Report.report text !last checkpoint 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 + Loc.with_location (fun _x -> raise (Error None)) lb in I.loop_handle succeed fail supplier checkpoint @@ -274,26 +264,24 @@ rule token = parse let parse_mlw_file lb = build_parsing_function Parser_sleek.Incremental.mlw_file_parsing_only lb - (* let read_channel env path file c = + let read_channel env path file c = let lb = Lexing.from_channel c in Loc.set_file file lb; - Typing.open_file env path; - let mm = - try - build_parsing_function Parser_sleek.Incremental.mlw_file lb - with - e -> ignore (Typing.discard_file ()); raise e + let _ = try + build_parsing_function Parser_sleek.Incremental.mlw_file_parsing_only lb + with + e -> ignore (Typing.discard_file ()); raise e in - if path = [] && Debug.test_flag debug then begin + (* if path = [] && Debug.test_flag debug then begin let print_m _ m = Format.eprintf "%a@\n@." print_module m in let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in Mid.iter print_m (Mstr.fold add_m mm Mid.empty) - end; - mm *) + end; *) + Wstdlib.Mstr.empty let whyml_sleek_format = "whyml_sleek" - let () = Env.register_format mlw_language whyml_format ["mlws"] + let () = Env.register_format mlw_language whyml_sleek_format ["mlws"] read_channel ~desc:"WhyML@ programming@ and@ specification@ language@ with@ Sleek" } diff --git a/src/sleek/lexlib_sleek.mll b/src/sleek/lexlib_sleek.mll index 7c86e4f2bd..a0e4d79f06 100644 --- a/src/sleek/lexlib_sleek.mll +++ b/src/sleek/lexlib_sleek.mll @@ -1,4 +1,6 @@ { + open Lexing + exception UnterminatedSleekSpec let () = Exn_printer.register (fun fmt e -> match e with diff --git a/src/sleek/parser_sleek.mli b/src/sleek/parser_sleek.mli deleted file mode 100644 index ea4b4847b1..0000000000 --- a/src/sleek/parser_sleek.mli +++ /dev/null @@ -1,61 +0,0 @@ - -(* The type of tokens. *) - -type token = Parser_sleek_tokens.token - -(* This exception is raised by the monolithic API functions. *) - -exception Error - -(* The monolithic API. *) - -val term_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.term) - -val term_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.term list) - -val qualid_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.qualid) - -val qualid_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.qualid list) - -val mlw_file_parsing_only: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.mlw_file) - -val mlw_file: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Pmodule.pmodule Wstdlib.Mstr.t) - -val ident_comma_list_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.ident list) - -val expr_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.expr) - -val decl_eof: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Ptree_sleek.decl) - -module MenhirInterpreter : sig - - (* The incremental API. *) - - include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE - with type token = token - -end - -(* The entry point(s) to the incremental API. *) - -module Incremental : sig - - val term_eof: Lexing.position -> (Ptree_sleek.term) MenhirInterpreter.checkpoint - - val term_comma_list_eof: Lexing.position -> (Ptree_sleek.term list) MenhirInterpreter.checkpoint - - val qualid_eof: Lexing.position -> (Ptree_sleek.qualid) MenhirInterpreter.checkpoint - - val qualid_comma_list_eof: Lexing.position -> (Ptree_sleek.qualid list) MenhirInterpreter.checkpoint - - val mlw_file_parsing_only: Lexing.position -> (Ptree_sleek.mlw_file) MenhirInterpreter.checkpoint - - val mlw_file: Lexing.position -> (Pmodule.pmodule Wstdlib.Mstr.t) MenhirInterpreter.checkpoint - - val ident_comma_list_eof: Lexing.position -> (Ptree_sleek.ident list) MenhirInterpreter.checkpoint - - val expr_eof: Lexing.position -> (Ptree_sleek.expr) MenhirInterpreter.checkpoint - - val decl_eof: Lexing.position -> (Ptree_sleek.decl) MenhirInterpreter.checkpoint - -end diff --git a/src/sleek/parser_sleek.mly b/src/sleek/parser_sleek.mly index 6081bb128b..750ddb604a 100644 --- a/src/sleek/parser_sleek.mly +++ b/src/sleek/parser_sleek.mly @@ -63,44 +63,43 @@ term_comma_list_eof: // mlw_file: // | EOF // | mlw_module mlw_module_no_decl* EOF - // { Typing.close_file () } +// { Typing.close_file () } // | module_decl module_decl_no_head* EOF - // { let loc = floc $startpos($3) $endpos($3) in - // Typing.close_module loc; Typing.close_file () } +// { let loc = floc $startpos($3) $endpos($3) in +// Typing.close_module loc; Typing.close_file () } mlw_file_parsing_only: | EOF { (Modules([])) } | mlw_module_parsing_only mlw_module_no_decl_parsing_only* EOF { (Modules( [$1] @ $2)) } | module_decl_parsing_only module_decl_no_head_parsing_only* EOF { (Decls( [$1] @ $2)) } - -mlw_module: -| module_head module_decl_no_head* END - // { Typing.close_module (floc $startpos($3) $endpos($3)) } +// mlw_module: +// | module_head module_decl_no_head* END +// { Typing.close_module (floc $startpos($3) $endpos($3)) } mlw_module_parsing_only: | module_head_parsing_only module_decl_no_head_parsing_only* END { ($1, $2) } -module_head: -| THEORY attrs(uident_nq) - // { Typing.open_module $2 } -| MODULE attrs(uident_nq) intf = option(preceded(COLON, tqualid)) - // { Typing.open_module ?intf $2 } - -scope_head: -| SCOPE boption(IMPORT) attrs(uident_nq) - // { Typing.open_scope (floc $startpos $endpos) $3; $2 } - -module_decl: -| scope_head module_decl* END - // { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 } -| IMPORT uqualid - // { Typing.add_decl (floc $startpos $endpos) (Dimport($2)) } -| d = pure_decl | d = prog_decl | d = meta_decl - // { Typing.add_decl (floc $startpos $endpos) d } -| use_clone - // { () } +// module_head: +// | THEORY attrs(uident_nq) +// { Typing.open_module $2 } +// | MODULE attrs(uident_nq) intf = option(preceded(COLON, tqualid)) +// { Typing.open_module ?intf $2 } + +// scope_head: +// | SCOPE boption(IMPORT) attrs(uident_nq) +// { Typing.open_scope (floc $startpos $endpos) $3; $2 } + +// module_decl: +// | scope_head module_decl* END +// { Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 } +// | IMPORT uqualid +// { Typing.add_decl (floc $startpos $endpos) (Dimport($2)) } +// | d = pure_decl | d = prog_decl | d = meta_decl +// { Typing.add_decl (floc $startpos $endpos) d } +// | use_clone +// { () } module_decl_parsing_only: | scope_head_parsing_only module_decl_parsing_only* END @@ -114,12 +113,12 @@ module_decl_parsing_only: (* Do not open inside another module *) -mlw_module_no_decl: -| SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl - { let loc = floc $startpos $endpos in - Loc.errorm ~loc "trying to open a module inside another module" } -| mlw_module - { $1 } +// mlw_module_no_decl: +// | SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl +// { let loc = floc $startpos $endpos in +// Loc.errorm ~loc "trying to open a module inside another module" } +// | mlw_module +// { $1 } mlw_module_no_decl_parsing_only: | SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl @@ -128,12 +127,12 @@ mlw_module_no_decl_parsing_only: | mlw_module_parsing_only { $1 } -module_decl_no_head: -| THEORY | MODULE - { let loc = floc $startpos $endpos in - Loc.errorm ~loc "trying to open a module inside another module" } -| module_decl - { $1 } +// module_decl_no_head: +// | THEORY | MODULE +// { let loc = floc $startpos $endpos in +// Loc.errorm ~loc "trying to open a module inside another module" } +// | module_decl +// { $1 } module_decl_no_head_parsing_only: | THEORY | MODULE @@ -145,32 +144,32 @@ module_decl_no_head_parsing_only: (* Use and clone *) -use_clone: -| USE EXPORT tqualid - // { let loc = floc $startpos $endpos in - // let decl = Ptree_sleek.Duseexport $3 in - // Typing.add_decl loc decl - // } -| CLONE EXPORT tqualid clone_subst - // { let loc = floc $startpos $endpos in - // let decl = Ptree_sleek.Dcloneexport(loc,$3,$4) in - // Typing.add_decl loc decl - // } -| USE boption(IMPORT) m_as_list = comma_list1(use_as) - // { let loc = floc $startpos $endpos in - // let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in - // let import = $2 in - // if import && not exists_as then Loc.warning ~loc warn_redundant_import - // "the keyword `import' is redundant here and can be omitted"; - // let decl = Ptree_sleek.Duseimport(loc,import,m_as_list) in - // Typing.add_decl loc decl - // } -| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst - // { let loc = floc $startpos $endpos in - // let import = $2 in - // let as_opt = $4 in - // if import && as_opt = None then Loc.warning ~loc warn_redundant_import - // "the keyword `import' is redundant here and can be omitted"; - // let decl = Ptree_sleek.Dcloneimport(loc,import,$3,as_opt,$5) in - // Typing.add_decl loc decl - // } +// use_clone: +// | USE EXPORT tqualid +// { let loc = floc $startpos $endpos in +// let decl = Ptree_sleek.Duseexport $3 in +// Typing.add_decl loc decl +// } +// | CLONE EXPORT tqualid clone_subst +// { let loc = floc $startpos $endpos in +// let decl = Ptree_sleek.Dcloneexport(loc,$3,$4) in +// Typing.add_decl loc decl +// } +// | USE boption(IMPORT) m_as_list = comma_list1(use_as) +// { let loc = floc $startpos $endpos in +// let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in +// let import = $2 in +// if import && not exists_as then Loc.warning ~loc warn_redundant_import +// "the keyword `import' is redundant here and can be omitted"; +// let decl = Ptree_sleek.Duseimport(loc,import,m_as_list) in +// Typing.add_decl loc decl +// } +// | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst +// { let loc = floc $startpos $endpos in +// let import = $2 in +// let as_opt = $4 in +// if import && as_opt = None then Loc.warning ~loc warn_redundant_import +// "the keyword `import' is redundant here and can be omitted"; +// let decl = Ptree_sleek.Dcloneimport(loc,import,$3,as_opt,$5) in +// Typing.add_decl loc decl +// } diff --git a/src/sleek/parser_sleek_common.mly b/src/sleek/parser_sleek_common.mly index 71fc77150a..2b1b2e0731 100644 --- a/src/sleek/parser_sleek_common.mly +++ b/src/sleek/parser_sleek_common.mly @@ -46,6 +46,8 @@ let empty_sleek_spec = "" + let sleek_spec_union s1 s2 = s1 ^ s2 + let empty_spec = { sp_pre = []; sp_post = []; @@ -172,9 +174,6 @@ let error_loc loc = Loc.error ~loc Error - let warn_redundant_import = - Loc.register_warning "redundant import" "Warn about redundant import" - let () = Exn_printer.register (fun fmt exn -> match exn with | Error -> Format.fprintf fmt "syntax error %s" (Parser_messages.message 1) | _ -> raise exn) @@ -346,11 +345,6 @@ %nonassoc prec_no_else %nonassoc DOT ELSE RETURN -(* Sleek *) -%nonassoc prec_no_sleek_spec -%nonassoc SLEEK_SPEC -(* Sleek *) - %nonassoc prec_no_spec %nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT %nonassoc below_LARROW @@ -401,18 +395,17 @@ See also `plugins/cfg/cfg_parser.mly` { (Duseexport $3) } | CLONE EXPORT tqualid clone_subst { let loc = floc $startpos $endpos in - (Dcloneexport (loc,$3, $4)) } + (Dcloneexport (loc,$3, $4)) + } | USE boption(IMPORT) m_as_list = comma_list1(use_as) { let loc = floc $startpos $endpos in let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in - if $2 && not exists_as then Loc.warning ~loc warn_redundant_import - "the keyword `import' is redundant here and can be omitted"; - (Duseimport (loc, $2, m_as_list)) } + (Duseimport (loc, $2, m_as_list)) + } | CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst { let loc = floc $startpos $endpos in - if $2 && $4 = None then Loc.warning ~loc warn_redundant_import - "the keyword `import' is redundant here and can be omitted"; - (Dcloneimport (loc, $2, $3, $4, $5)) } + (Dcloneimport (loc, $2, $3, $4, $5)) + } %public use_as: | n = tqualid q = option(preceded(AS, uident)) { (n, q) } @@ -928,32 +921,34 @@ kind: (* Function definitions *) rec_defn: -| sleek_spec ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr - { let pat, ty, mask = $6 in - let spec = apply_return pat (spec_union $7 $9) in +| ghost kind attrs(lident_rich) binders return_opt sleek_spec spec EQUAL sleek_spec spec seq_expr + { let pat, ty, mask = $5 in + let spec = apply_return pat (spec_union $7 $10) in let id = mk_id return_id $startpos($8) $endpos($8) in - let e = { $10 with expr_desc = Eoptexn (id, mask, $10) } in - let sleek_spec = $1 in - $4, ghost $2, $3, $5, ty, pat, mask, apply_partial_sp $2 spec, sleek_spec, e } + let e = { $11 with expr_desc = Eoptexn (id, mask, $11) } in + let sleek_spec = sleek_spec_union $6 $9 in + $3, ghost $1, $2, $4, ty, pat, mask, apply_partial_sp $1 spec, sleek_spec, e + } fun_defn: -| sleek_spec binders return_opt spec EQUAL spec seq_expr - { let pat, ty, mask = $3 in - let spec = apply_return pat (spec_union $4 $6) in +| binders return_opt sleek_spec spec EQUAL sleek_spec spec seq_expr + { let pat, ty, mask = $2 in + let spec = apply_return pat (spec_union $4 $7) in let id = mk_id return_id $startpos($5) $endpos($5) in - let e = { $7 with expr_desc = Eoptexn (id, mask, $7) } in - let sleek_spec = $1 in - Efun ($2, ty, pat, mask, spec, sleek_spec, e) } + let e = { $8 with expr_desc = Eoptexn (id, mask, $8) } in + let sleek_spec = sleek_spec_union $3 $6 in + Efun ($1, ty, pat, mask, spec, sleek_spec, e) + } fun_decl: -| sleek_spec params1 return_opt spec - { let pat, ty, mask = $3 in - Eany ($2, Expr.RKnone, ty, pat, mask, apply_return pat $4, $1) } +| params1 return_opt sleek_spec spec + { let pat, ty, mask = $2 in + Eany ($1, Expr.RKnone, ty, pat, mask, apply_return pat $4, $3) } const_decl: -| sleek_spec return_opt spec - { let pat, ty, mask = $2 in - Eany ([], Expr.RKnone, ty, pat, mask, apply_return pat $3, $1) } +| return_opt sleek_spec spec + { let pat, ty, mask = $1 in + Eany ([], Expr.RKnone, ty, pat, mask, apply_return pat $3, $2) } const_defn: | cast EQUAL seq_expr { { $3 with expr_desc = Ecast ($3, $1) } } @@ -1302,8 +1297,8 @@ for_dir: (* Specification *) sleek_spec: (* TODO: change the representation of sleek spec *) -| (* epsilon *) %prec prec_no_sleek_spec { empty_sleek_spec } -| SLEEK_SPEC { $1 } +| (* epsilon *) { empty_sleek_spec } +| SLEEK_SPEC { $1 } %public spec: | (* epsilon *) %prec prec_no_spec { empty_spec } diff --git a/src/sleek/parser_sleek_tokens.ml b/src/sleek/parser_sleek_tokens.ml deleted file mode 100644 index 4dc38d059a..0000000000 --- a/src/sleek/parser_sleek_tokens.ml +++ /dev/null @@ -1,129 +0,0 @@ - -type token = - | WRITES - | WITH - | WHILE - | VARIANT - | VAL - | USE - | UNDERSCORE - | UIDENT of (string) - | TYPE - | TRY - | TRUE - | TO - | THEORY - | THEN - | STRING of (string) - | SO - | SEMICOLON - | SCOPE - | RIGHTSQ_QUOTE of (string) - | RIGHTSQ - | RIGHTPAR_USCORE of (string) - | RIGHTPAR_QUOTE of (string) - | RIGHTPAR - | RIGHTBRC - | RETURNS - | RETURN - | REQUIRES - | REF - | REC - | REAL of (Number.real_constant) - | READS - | RANGE - | RAISES - | RAISE - | QUOTE_LIDENT of (string) - | PURE - | PRIVATE - | PREDICATE - | POSITION of (Loc.position) - | PARTIAL - | OR - | OPPREF of (string) - | OP4 of (string) - | OP3 of (string) - | OP2 of (string) - | OP1 of (string) - | OLD - | NOT - | MUTABLE - | MODULE - | MINUS - | META - | MATCH - | LTGT - | LT - | LRARROW - | LIDENT of (string) - | LET - | LEMMA - | LEFTSQBAR - | LEFTSQ - | LEFTPAR - | LEFTBRC - | LARROW - | LABEL - | INVARIANT - | INTEGER of (Number.int_constant) - | INDUCTIVE - | IN - | IMPORT - | IF - | GT - | GOAL - | GHOST - | FUNCTION - | FUN - | FORALL - | FOR - | FLOAT - | FALSE - | EXPORT - | EXISTS - | EXCEPTION - | EQUALARROW - | EQUAL - | EPSILON - | EOF - | ENSURES - | END - | ELSE - | DOWNTO - | DOTDOT - | DOT - | DONE - | DO - | DIVERGES - | CORE_UIDENT of (string) - | CORE_LIDENT of (string) - | CONTINUE - | CONSTANT - | COMMA - | COLON - | COINDUCTIVE - | CLONE - | CHECK - | BY - | BREAK - | BEGIN - | BARRIGHTSQ - | BARBAR - | BAR - | AXIOM - | ATTRIBUTE of (string) - | AT - | ASSUME - | ASSERT - | AS - | ARROW - | ANY - | AND - | AMPAMP - | AMP - | ALIAS - | ABSURD - | ABSTRACT - (* Support for Sleek *) - | SLEEK_SPEC of string diff --git a/src/sleek/ptree_sleek.ml b/src/sleek/ptree_sleek.ml index 51b0ab402c..2dca2c89dc 100644 --- a/src/sleek/ptree_sleek.ml +++ b/src/sleek/ptree_sleek.ml @@ -214,6 +214,7 @@ type xpost = Loc.position * (qualid * (pattern * term) option) list (** Sleek contract *) type sleek_spec = string +[@@deriving sexp] (** Contract *) type spec = { From b2ca3d5cada4d7a32c6553077a9b1c4afe64b688 Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Wed, 26 Jun 2024 14:41:47 +0800 Subject: [PATCH 11/12] Modify build script for 'why3pp_sleek' --- Makefile.in | 35 +++++++++++++++++++++++++++++++++++ src/tools/why3pp_sleek.ml | 6 ++++++ src/tools/why3pp_sleek.mli | 0 3 files changed, 41 insertions(+) create mode 100644 src/tools/why3pp_sleek.ml create mode 100644 src/tools/why3pp_sleek.mli diff --git a/Makefile.in b/Makefile.in index 9fd14f7043..8faf6e20f7 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1588,6 +1588,41 @@ install-bin:: install_local:: bin/why3pp.$(SHAREDBEST) +# sleek support +################# +# why3pp_sleek # +################# + +PP_SLEEK_FILES = why3pp_sleek +PP_SLEEK_MODULES = $(addprefix src/tools/, $(PP_SLEEK_FILES)) + +PP_SLEEK_DEP = $(addsuffix .dep, $(PP_SLEEK_MODULES)) +PP_SLEEK_CMO = $(addsuffix .cmo, $(PP_SLEEK_MODULES)) +PP_SLEEK_CMX = $(addsuffix .cmx, $(PP_SLEEK_MODULES)) + +$(PP_SLEEK_DEP) $(PP_SLEEK_CMO) $(PP_SLEEK_CMX): INCLUDES += -I src/tools + +# build targets + +byte: bin/why3pp_sleek.cma +opt: bin/why3pp_sleek.cmxs + +bin/why3pp_sleek.cmxs: $(PP_SLEEK_CMX) +bin/why3pp_sleek.cma: $(PP_SLEEK_CMO) + +# depend and clean targets + +MAKEINC += $(PP_SLEEK_DEP) + +uninstall-bin:: + rm -f $(TOOLDIR)/why3pp_sleek.$(SHAREDBEST) + +install-bin:: + $(MKDIR_P) $(TOOLDIR) + $(INSTALL_DATA) bin/why3pp_sleek.$(SHAREDBEST) $(TOOLDIR) + +install_local:: bin/why3pp_sleek.$(SHAREDBEST) + ######### # why3doc ######### diff --git a/src/tools/why3pp_sleek.ml b/src/tools/why3pp_sleek.ml new file mode 100644 index 0000000000..5d468d95dd --- /dev/null +++ b/src/tools/why3pp_sleek.ml @@ -0,0 +1,6 @@ +open Format +open Why3 +open Wstdlib + +let () = + eprintf "why3pp_sleek: handle input file@." diff --git a/src/tools/why3pp_sleek.mli b/src/tools/why3pp_sleek.mli new file mode 100644 index 0000000000..e69de29bb2 From 2ade73ea0c956e8dffe79c555d7859210d2a6f81 Mon Sep 17 00:00:00 2001 From: VietAnh1010 Date: Wed, 26 Jun 2024 15:39:37 +0800 Subject: [PATCH 12/12] why3pp_sleek: print sexp of file with sleek spec --- src/tools/why3pp_sleek.ml | 36 ++++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/src/tools/why3pp_sleek.ml b/src/tools/why3pp_sleek.ml index 5d468d95dd..383c48d387 100644 --- a/src/tools/why3pp_sleek.ml +++ b/src/tools/why3pp_sleek.ml @@ -1,6 +1,38 @@ open Format open Why3 -open Wstdlib + +let usage_msg = "\nParse the given file, then display the AST in Sexp format" +let opt_file = ref None +let option_list = [] + +let add_opt_file file = opt_file := Some file + +let _, _ = + eprintf "why3pp_sleek.ml: initialize args@."; + Whyconf.Args.initialize option_list add_opt_file usage_msg + +let parse_mlw_file filename = + let c = if filename = "-" then stdin else open_in filename in + let lexbuf = Lexing.from_channel c in + Loc.set_file filename lexbuf; + let mlw_file = Lexer_sleek.parse_mlw_file lexbuf in + if filename <> "-" then + close_in c; + mlw_file +let handle_no_file () = + Whyconf.Args.exit_with_usage usage_msg + +let handle_file file = + let mlw_file = parse_mlw_file file in + let sexp = Why3.Ptree_sleek.sexp_of_mlw_file mlw_file in + Mysexplib.output std_formatter sexp let () = - eprintf "why3pp_sleek: handle input file@." + eprintf "why3pp_sleek: handle input file@."; + try + match !opt_file with + | None -> handle_no_file () + | Some file -> handle_file file + with e when not (Debug.test_flag Debug.stack_trace) -> + eprintf "%a@." Exn_printer.exn_printer e; + exit 1