Skip to content

GitLab

why3
why3
Commit ee99af04 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

Parser: admit qualifiers M.() in types and patterns 

Also fix the suboptimal handling of casts in "returns { }".
parent 68a92927
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1628 additions and 1576 deletions
src/parser/handcrafted.messages
View file @ ee99af04
This diff is collapsed.
src/parser/parser.mly
View file @ ee99af04
......@@ -112,13 +112,25 @@
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 rec case (loc, pfl) = match pfl with
| [{ pat_desc = Ptree.Pparen p; pat_loc = loc}, f] -> case (loc, [p,f])
| [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] -> f
| [{ pat_desc = Ptree.Pvar { id_str = "result" } }, f] -> f
| [{ pat_desc = Ptree.Pvar id }, f] ->
{ term_desc = Tlet (id, rt loc, f); term_loc = loc }
| _ -> { term_desc = Tcase (rt loc, pfl); 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 *)
......@@ -457,6 +469,10 @@ ty:
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 }
......@@ -605,7 +621,7 @@ single_term_:
{ let re_pat pat d = { pat with pat_desc = d } in
let cast t ty = { t with term_desc = Tcast (t,ty) } in
let rec unfold d p = match p.pat_desc with
| Pparen p -> unfold d p
| 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)
......@@ -651,7 +667,7 @@ term_dot_:
| o = oppref ; a = term_dot { Tidapp (Qident o, [a]) }
| term_sub_ { $1 }
term_block:
term_block_:
| BEGIN term END { $2.term_desc }
| LEFTPAR term RIGHTPAR { $2.term_desc }
| BEGIN END { Ttuple [] }
......@@ -660,8 +676,8 @@ term_block:
| 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_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]) }
......@@ -852,7 +868,7 @@ single_expr_:
| _ -> Pghost pat) in
let pat = if $2 then push $4 else $4 in
let rec unfold gh d p = match p.pat_desc with
| Pparen p -> unfold gh d p
| 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)
......@@ -971,14 +987,14 @@ expr_arg_:
| TRUE { Etrue }
| FALSE { Efalse }
| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) }
| expr_sub { $1 }
| expr_sub_ { $1 }
expr_dot_:
| lqualid { Eident $1 }
| o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) }
| expr_sub { $1 }
| expr_sub_ { $1 }
expr_block:
expr_block_:
| BEGIN single_spec spec seq_expr END
{ Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $4) }
| BEGIN single_spec spec END
......@@ -991,15 +1007,15 @@ expr_block:
| LEFTBRC field_list1(expr) RIGHTBRC { Erecord $2 }
| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC { Eupdate ($2, $4) }
expr_pure:
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_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
......@@ -1171,6 +1187,10 @@ pat_arg_:
| UNDERSCORE { Pwild }
| attrs(lident_nq) { Pvar (add_model_trace_attr $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 }
......
src/parser/ptree.ml
View file @ ee99af04
......@@ -32,6 +32,7 @@ type pty =
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTarrow of pty * pty
| PTscope of qualid * pty
| PTparen of pty
| PTpure of pty
......@@ -53,8 +54,9 @@ and pat_desc =
| Pas of pattern * ident * ghost
| Por of pattern * pattern
| Pcast of pattern * pty
| Pghost of pattern
| Pscope of qualid * pattern
| Pparen of pattern
| Pghost of pattern
(*s Logical terms and formulas *)
......
src/parser/typing.ml
View file @ ee99af04
......@@ -105,23 +105,23 @@ let find_prog_symbol_ns ns p =
(** Parsing types *)
let ty_of_pty ns pty =
let rec get_ty = function
| PTtyvar {id_str = x} ->
ty_var (tv_of_string x)
| PTtyapp (q, tyl) ->
let ts = find_tysymbol_ns ns q in
let tyl = List.map get_ty tyl in
Loc.try2 ~loc:(qloc q) ty_app ts tyl
| PTtuple tyl ->
let s = its_tuple (List.length tyl) in
ty_app s.its_ts (List.map get_ty tyl)
| PTarrow (ty1, ty2) ->
ty_func (get_ty ty1) (get_ty ty2)
| PTpure ty | PTparen ty ->
get_ty ty
in
get_ty pty
let rec ty_of_pty ns = function
| PTtyvar {id_str = x} ->
ty_var (tv_of_string x)
| PTtyapp (q, tyl) ->
let ts = find_tysymbol_ns ns q in
let tyl = List.map (ty_of_pty ns) tyl in
Loc.try2 ~loc:(qloc q) ty_app ts tyl
| PTtuple tyl ->
let s = its_tuple (List.length tyl) in
ty_app s.its_ts (List.map (ty_of_pty ns) tyl)
| PTarrow (ty1, ty2) ->
ty_func (ty_of_pty ns ty1) (ty_of_pty ns ty2)
| PTscope (q, ty) ->
let ns = import_namespace ns (string_list_of_qualid q) in
ty_of_pty ns ty
| PTpure ty | PTparen ty ->
ty_of_pty ns ty
let dty_of_pty ns pty =
Dterm.dty_of_ty (ty_of_pty ns pty)
......@@ -156,10 +156,14 @@ let parse_record ~loc ns km get_val fl =
let rec dpattern ns km { pat_desc = desc; pat_loc = loc } =
match desc with
| Ptree.Pparen p -> dpattern ns km p
| Ptree.Pscope (q,p) ->
let ns = import_namespace ns (string_list_of_qualid q) in
dpattern ns km p
| _ -> (* creative indentation ahead *)
Dterm.dpattern ~loc (match desc with
| Ptree.Pparen _
| Ptree.Pscope _ -> assert false (* never *)
| Ptree.Pwild -> DPwild
| Ptree.Pparen _ -> assert false (* never *)
| Ptree.Pvar x -> DPvar (create_user_id x)
| Ptree.Papp (q,pl) ->
let pl = List.map (dpattern ns km) pl in
......@@ -422,25 +426,25 @@ let find_special muc test nm q =
end
| _ -> Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q
let ity_of_pty muc pty =
let rec get_ity = function
| PTtyvar {id_str = x} ->
ity_var (tv_of_string x)
| PTtyapp (q, tyl) ->
let s = find_itysymbol_ns (get_namespace muc) q in
let tyl = List.map get_ity tyl in
Loc.try3 ~loc:(qloc q) ity_app s tyl []
| PTtuple tyl ->
ity_tuple (List.map get_ity tyl)
| PTarrow (ty1, ty2) ->
ity_func (get_ity ty1) (get_ity ty2)
| PTpure ty ->
ity_purify (get_ity ty)
| PTparen ty ->
get_ity ty
in
get_ity pty
let rec ity_of_pty muc = function
| PTtyvar {id_str = x} ->
ity_var (tv_of_string x)
| PTtyapp (q, tyl) ->
let s = find_itysymbol muc q in
let tyl = List.map (ity_of_pty muc) tyl in
Loc.try3 ~loc:(qloc q) ity_app s tyl []
| PTtuple tyl ->
ity_tuple (List.map (ity_of_pty muc) tyl)
| PTarrow (ty1, ty2) ->
ity_func (ity_of_pty muc ty1) (ity_of_pty muc ty2)
| PTpure ty ->
ity_purify (ity_of_pty muc ty)
| PTscope (q, ty) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
ity_of_pty muc ty
| PTparen ty ->
ity_of_pty muc ty
let dity_of_pty muc pty =
Dexpr.dity_of_ity (ity_of_pty muc pty)
......@@ -499,10 +503,15 @@ let rec dpattern muc gh { pat_desc = desc; pat_loc = loc } =
match desc with
| Ptree.Pparen p -> dpattern muc gh p
| Ptree.Pghost p -> dpattern muc true p
| Ptree.Pscope (q,p) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
dpattern muc gh p
| _ -> (* creative indentation ahead *)
Dexpr.dpattern ~loc (match desc with
| Ptree.Pparen _ | Ptree.Pscope _
| Ptree.Pghost _ -> assert false (* never *)
| Ptree.Pwild -> DPwild
| Ptree.Pparen _ | Ptree.Pghost _ -> assert false
| Ptree.Pvar x -> DPvar (create_user_id x, gh)
| Ptree.Papp (q,pl) ->
DPapp (find_constructor muc q, List.map (dpattern muc gh) pl)
......@@ -557,23 +566,34 @@ let dpre muc pl lvm old =
List.map dpre pl
let dpost muc ql lvm old ity =
let rec dpost (loc,pfl) = match pfl with
| [{ pat_desc = Ptree.Pparen p; pat_loc = loc}, f] ->
dpost (loc, [p,f])
| [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
let v = create_pvsymbol (id_fresh "result") ity in
v, Loc.try3 ~loc type_fmla muc lvm old f
| [{ pat_desc = Ptree.Pvar id }, f] ->
let v = create_pvsymbol (create_user_id id) ity in
let lvm = Mstr.add id.id_str v lvm in
v, Loc.try3 ~loc type_fmla muc lvm old f
| _ ->
let v = create_pvsymbol (id_fresh "result") ity in
let i = { id_str = "(null)"; id_loc = loc; id_ats = [] } in
let t = { term_desc = Tident (Qident i); term_loc = loc } in
let f = { term_desc = Ptree.Tcase (t, pfl); term_loc = loc } in
let lvm = Mstr.add "(null)" v lvm in
v, Loc.try3 ~loc type_fmla muc lvm old f in
let mk_case loc pfl =
let v = create_pvsymbol (id_fresh "result") ity in
let i = { id_str = "(null)"; id_loc = loc; id_ats = [] } in
let t = { term_desc = Tident (Qident i); term_loc = loc } in
let f = { term_desc = Ptree.Tcase (t, pfl); term_loc = loc } in
let lvm = Mstr.add "(null)" v lvm in
v, Loc.try3 ~loc type_fmla muc lvm old f in
let dpost (loc,pfl) = match pfl with
| [pat, f] ->
let rec unfold p = match p.pat_desc with
| Ptree.Pparen p | Ptree.Pscope (_,p) -> unfold p
| Ptree.Pcast (p,pty) ->
let ty = ty_of_ity (ity_of_pty muc pty) in
Loc.try2 ~loc:p.pat_loc ty_equal_check (ty_of_ity ity) ty;
unfold p
| Ptree.Ptuple [] ->
Loc.try2 ~loc:p.pat_loc ity_equal_check ity ity_unit;
unfold { p with pat_desc = Ptree.Pwild }
| Ptree.Pwild ->
let v = create_pvsymbol (id_fresh "result") ity in
v, Loc.try3 ~loc type_fmla muc lvm old f
| Ptree.Pvar id ->
let v = create_pvsymbol (create_user_id id) ity in
let lvm = Mstr.add id.id_str v lvm in
v, Loc.try3 ~loc type_fmla muc lvm old f
| _ -> mk_case loc pfl in
unfold pat
| _ -> mk_case loc pfl in
List.map dpost ql
let dxpost muc ql lvm xsm old =
......@@ -1107,7 +1127,7 @@ let add_types muc tdl =
Hstr.add hts x itd.itd_its; Hstr.add htd x itd
and parse ~loc ~alias ~alg pty =
let rec down = function
let rec down muc = function
| PTtyvar id ->
ity_var (tv_of_string id.id_str)
| PTtyapp (q,tyl) ->
......@@ -1127,12 +1147,16 @@ let add_types muc tdl =
Hstr.find hts x
| _ ->
find_itysymbol muc q in
Loc.try3 ~loc:(qloc q) ity_app s (List.map down tyl) []
| PTtuple tyl -> ity_tuple (List.map down tyl)
| PTarrow (ty1,ty2) -> ity_func (down ty1) (down ty2)
| PTpure ty -> ity_purify (down ty)
| PTparen ty -> down ty in
down pty in
Loc.try3 ~loc:(qloc q) ity_app s (List.map (down muc) tyl) []
| PTtuple tyl -> ity_tuple (List.map (down muc) tyl)
| PTarrow (ty1,ty2) -> ity_func (down muc ty1) (down muc ty2)
| PTpure ty -> ity_purify (down muc ty)
| PTscope (q,ty) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
down muc ty
| PTparen ty -> down muc ty in
down muc pty in
Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment