Commit f2e07804 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Parser & Ptree: continue refactoring

parent 23061646
......@@ -65,7 +65,7 @@ type incremental = {
(* start a module *)
let mk_ident ?(label=[]) ?(loc=Loc.dummy_position) s = {
id = s; id_lab=label; id_loc = loc
id_str = s; id_lab=label; id_loc = loc
}
let m = t.open_module (mk_ident "Program")
......@@ -93,11 +93,11 @@ let () = t.use_clone Loc.dummy_position (use_int_Int,None)
let mul_int = mk_qid ["Int";"infix *"]
let mk_lexpr p = { pp_loc = Loc.dummy_position;
pp_desc = p }
let mk_lexpr p = { term_loc = Loc.dummy_position;
term_desc = p }
let mk_const s =
mk_lexpr (PPconst(Number.ConstInt(Number.int_const_dec s)))
mk_lexpr (Tconst(Number.ConstInt(Number.int_const_dec s)))
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
......@@ -110,7 +110,7 @@ let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
*)
let d : pdecl =
let args =
[Loc.dummy_position,Some(mk_ident "_dummy"),false,Some(PPTtuple [])]
[Loc.dummy_position,Some(mk_ident "_dummy"),false,Some(PTtuple [])]
in
let spec = {
sp_pre = [];
......@@ -127,8 +127,8 @@ let d : pdecl =
let c6 = mk_const "6" in
let c7 = mk_const "7" in
let c42 = mk_const "42" in
let c6p7 = mk_lexpr (PPidapp(mul_int,[c6;c7])) in
let p = mk_lexpr (PPinfix(c6p7,mk_ident "infix =",c42)) in
let c6p7 = mk_lexpr (Tidapp(mul_int,[c6;c7])) in
let p = mk_lexpr (Tinfix(c6p7,mk_ident "infix =",c42)) in
mk_expr(Eassert(Aassert,p))
in
Dfun(mk_ident "f",Gnone,(args,None,body,spec))
......
This diff is collapsed.
......@@ -13,7 +13,7 @@
type loc = Loc.position
(*s Logical expressions (for both terms and predicates) *)
(*s Logical terms and formulas *)
type integer_constant = Number.integer_constant
type real_constant = Number.real_constant
......@@ -23,16 +23,20 @@ type label =
| Lstr of Ident.label
| Lpos of Loc.position
type pp_quant =
| PPforall | PPexists | PPlambda
type quant =
| Tforall | Texists | Tlambda
type pp_binop =
| PPand | PPand_asym | PPor | PPor_asym | PPimplies | PPiff
type binop =
| Tand | Tand_asym | Tor | Tor_asym | Timplies | Tiff
type pp_unop =
| PPnot
type unop =
| Tnot
type ident = { id : string; id_lab : label list; id_loc : loc }
type ident = {
id_str : string;
id_lab : label list;
id_loc : loc;
}
type qualid =
| Qident of ident
......@@ -41,59 +45,58 @@ type qualid =
type opacity = bool
type pty =
| PPTtyvar of ident * opacity
| PPTtyapp of qualid * pty list
| PPTtuple of pty list
| PPTarrow of pty * pty
| PPTparen of pty
| PTtyvar of ident * opacity
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTarrow of pty * pty
| PTparen of pty
type ghost = bool
type binder = loc * ident option * ghost * pty option
type param = loc * ident option * ghost * pty
type quvar = ident * pty option
type pattern =
{ pat_loc : loc; pat_desc : pat_desc }
type pattern = {
pat_desc : pat_desc;
pat_loc : loc;
}
and pat_desc =
| PPpwild
| PPpvar of ident
| PPpapp of qualid * pattern list
| PPprec of (qualid * pattern) list
| PPptuple of pattern list
| PPpor of pattern * pattern
| PPpas of pattern * ident
type lexpr =
{ pp_loc : loc; pp_desc : pp_desc }
and pp_desc =
| PPtrue
| PPfalse
| PPconst of constant
| PPident of qualid
| PPidapp of qualid * lexpr list
| PPapply of lexpr * lexpr
| PPinfix of lexpr * ident * lexpr
| PPinnfix of lexpr * ident * lexpr
| PPbinop of lexpr * pp_binop * lexpr
| PPunop of pp_unop * lexpr
| PPif of lexpr * lexpr * lexpr
| PPquant of pp_quant * quvar list * lexpr list list * lexpr
| PPnamed of label * lexpr
| PPlet of ident * lexpr * lexpr
| PPmatch of lexpr * (pattern * lexpr) list
| PPcast of lexpr * pty
| PPtuple of lexpr list
| PPrecord of (qualid * lexpr) list
| PPupdate of lexpr * (qualid * lexpr) list
| Pwild
| Pvar of ident
| Papp of qualid * pattern list
| Prec of (qualid * pattern) list
| Ptuple of pattern list
| Por of pattern * pattern
| Pas of pattern * ident
type term = {
term_desc : term_desc;
term_loc : loc;
}
(*s Declarations. *)
and term_desc =
| Ttrue
| Tfalse
| Tconst of constant
| Tident of qualid
| Tidapp of qualid * term list
| Tapply of term * term
| Tinfix of term * ident * term
| Tinnfix of term * ident * term
| Tbinop of term * binop * term
| Tunop of unop * term
| Tif of term * term * term
| Tquant of quant * binder list * term list list * term
| Tnamed of label * term
| Tlet of ident * term * term
| Tmatch of term * (pattern * term) list
| Tcast of term * pty
| Ttuple of term list
| Trecord of (qualid * term) list
| Tupdate of term * (qualid * term) list
type plogic_type =
| PPredicate of pty list
| PFunction of pty list * pty
(*s Declarations. *)
type use = {
use_theory : qualid;
......@@ -125,7 +128,7 @@ type type_def =
type visibility = Public | Private | Abstract
type invariant = lexpr list
type invariant = term list
type type_decl = {
td_loc : loc;
......@@ -142,35 +145,32 @@ type logic_decl = {
ld_ident : ident;
ld_params : param list;
ld_type : pty option;
ld_def : lexpr option;
ld_def : term option;
}
type ind_decl = {
in_loc : loc;
in_ident : ident;
in_params : param list;
in_def : (loc * ident * lexpr) list;
in_def : (loc * ident * term) list;
}
type prop_kind =
| Kaxiom | Klemma | Kgoal
type metarg =
| PMAty of pty
| PMAfs of qualid
| PMAps of qualid
| PMApr of qualid
| PMAstr of string
| PMAint of int
| Mty of pty
| Mfs of qualid
| Mps of qualid
| Mpr of qualid
| Mstr of string
| Mint of int
type use_clone = use * clone_subst list option
type decl =
| TypeDecl of type_decl list
| LogicDecl of logic_decl list
| IndDecl of Decl.ind_sign * ind_decl list
| PropDecl of prop_kind * ident * lexpr
| Meta of ident * metarg list
| Dtype of type_decl list
| Dlogic of logic_decl list
| Dind of Decl.ind_sign * ind_decl list
| Dprop of Decl.prop_kind * ident * term
| Dmeta of ident * metarg list
(* program files *)
......@@ -178,7 +178,7 @@ type assertion_kind = Aassert | Aassume | Acheck
type lazy_op = LazyAnd | LazyOr
type variant = lexpr * qualid option
type variant = term * qualid option
type loop_annotation = {
loop_invariant : invariant;
......@@ -187,24 +187,24 @@ type loop_annotation = {
type for_direction = To | Downto
type pre = lexpr
type post = loc * (pattern * lexpr) list
type xpost = loc * (qualid * pattern * lexpr) list
type pre = term
type post = loc * (pattern * term) list
type xpost = loc * (qualid * pattern * term) list
type spec = {
sp_pre : pre list;
sp_post : post list;
sp_xpost : xpost list;
sp_reads : qualid list;
sp_writes : lexpr list;
sp_writes : term list;
sp_variant : variant list;
sp_checkrw : bool;
sp_diverge : bool;
}
type type_v =
| Tpure of pty
| Tarrow of param list * type_c
| PTpure of pty
| PTfunc of param list * type_c
and type_c = type_v * spec
......@@ -238,7 +238,7 @@ and expr_desc =
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Ewhile of expr * loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Elazy of expr * lazy_op * expr
| Enot of expr
| Ematch of expr * (pattern * expr) list
| Eabsurd
......@@ -246,7 +246,7 @@ and expr_desc =
| Etry of expr * (qualid * pattern option * expr) list
| Efor of ident * expr * for_direction * expr * invariant * expr
(* annotations *)
| Eassert of assertion_kind * lexpr
| Eassert of assertion_kind * term
| Emark of ident * expr
| Ecast of expr * pty
| Eany of type_c
......
This diff is collapsed.
......@@ -51,8 +51,8 @@ val find_qualid :
type global_vs = Ptree.qualid -> vsymbol option
val type_term : theory_uc -> global_vs -> Ptree.lexpr -> term
val type_term : theory_uc -> global_vs -> Ptree.term -> term
val type_fmla : theory_uc -> global_vs -> Ptree.lexpr -> term
val type_fmla : theory_uc -> global_vs -> Ptree.term -> term
val type_inst : theory_uc -> theory -> Ptree.clone_subst list -> th_inst
......@@ -92,34 +92,34 @@ let uc_find_ls uc p =
let ity_of_pty ?(noop=true) uc pty =
let rec get_ty = function
| PPTtyvar ({id_loc = loc}, true) when noop ->
| PTtyvar ({id_loc = loc}, true) when noop ->
Loc.errorm ~loc "Opaqueness@ annotations@ are@ only@ \
allowed@ in@ the@ types@ of@ formal@ arguments"
| PPTtyvar ({id = x}, _) ->
| PTtyvar ({id_str = x}, _) ->
ity_var (tv_of_string x)
| PPTtyapp (q, tyl) ->
| PTtyapp (q, tyl) ->
let tyl = List.map get_ty tyl in
begin match uc_find_ts uc q with
| PT s -> Loc.try2 ~loc:(qloc q) ity_app_fresh s tyl
| TS s -> Loc.try2 ~loc:(qloc q) ity_pur s tyl
end
| PPTtuple tyl ->
| PTtuple tyl ->
let s = ts_tuple (List.length tyl) in
ity_pur s (List.map get_ty tyl)
| PPTarrow (ty1, ty2) ->
| PTarrow (ty1, ty2) ->
ity_pur ts_func [get_ty ty1; get_ty ty2]
| PPTparen ty ->
| PTparen ty ->
get_ty ty
in
get_ty pty
let rec opaque_tvs acc = function
| PPTtyvar (id, true) -> Stv.add (tv_of_string id.id) acc
| PPTtyvar (_, false) -> acc
| PPTtyapp (_, pl)
| PPTtuple pl -> List.fold_left opaque_tvs acc pl
| PPTarrow (ty1, ty2) -> opaque_tvs (opaque_tvs acc ty1) ty2
| PPTparen ty -> opaque_tvs acc ty
| PTtyvar (id, true) -> Stv.add (tv_of_string id.id_str) acc
| PTtyvar (_, false) -> acc
| PTtyapp (_, pl)
| PTtuple pl -> List.fold_left opaque_tvs acc pl
| PTarrow (ty1, ty2) -> opaque_tvs (opaque_tvs acc ty1) ty2
| PTparen ty -> opaque_tvs acc ty
(** typing program expressions *)
......@@ -168,16 +168,16 @@ let create_user_id = Typing.create_user_id
let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
Mlw_dexpr.dpattern ~loc (match desc with
| Ptree.PPpwild -> DPwild
| Ptree.PPpvar x -> DPvar (create_user_id x)
| Ptree.PPpapp (q,pl) ->
| Ptree.Pwild -> DPwild
| Ptree.Pvar x -> DPvar (create_user_id x)
| Ptree.Papp (q,pl) ->
begin match uc_find_ps uc q with
| PL s -> DPpapp (s, List.map (fun p -> dpattern uc p) pl)
| LS s -> DPlapp (s, List.map (fun p -> dpattern uc p) pl)
| _ -> Loc.errorm ~loc:(qloc q) "Not a constructor: %a" print_qualid q
end
| Ptree.PPprec [] -> raise Decl.EmptyRecord
| Ptree.PPprec ((q,_)::_ as fl) ->
| Ptree.Prec [] -> raise Decl.EmptyRecord
| Ptree.Prec ((q,_)::_ as fl) ->
let get_val _ _ = function
| Some p -> dpattern uc p
| None -> Mlw_dexpr.dpattern DPwild in
......@@ -186,11 +186,11 @@ let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
| LS _ -> let cs,fl = pure_record ~loc uc get_val fl in DPlapp (cs,fl)
| _ -> Loc.errorm ~loc:(qloc q) "Not a record field: %a" print_qualid q
end
| Ptree.PPptuple pl ->
| Ptree.Ptuple pl ->
let pl = List.map (fun p -> dpattern uc p) pl in
DPlapp (fs_tuple (List.length pl), pl)
| Ptree.PPpas (p, x) -> DPas (dpattern uc p, create_user_id x)
| Ptree.PPpor (p, q) -> DPor (dpattern uc p, dpattern uc q))
| Ptree.Pas (p, x) -> DPas (dpattern uc p, create_user_id x)
| Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q))
(* specifications *)
......@@ -211,7 +211,7 @@ let find_global_vs uc p = try match uc_find_ps uc p with
let find_local_vs uc lvm p = match p with
| Qdot _ -> find_global_vs uc p
| Qident id -> let ovs = Mstr.find_opt id.id lvm in
| Qident id -> let ovs = Mstr.find_opt id.id_str lvm in
if ovs = None then find_global_vs uc p else ovs
let check_at f0 =
......@@ -244,17 +244,17 @@ let dpre lenv pl lvm =
let dpost lenv ql lvm ty =
let dpost (loc,pfl) = match pfl with
| [{ pat_desc = Ptree.PPpwild | Ptree.PPptuple [] }, f] ->
| [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] ->
None, Loc.try3 ~loc type_fmla lenv.uc lenv.th_old lvm f
| [{ pat_desc = Ptree.PPpvar id }, f] ->
| [{ pat_desc = Ptree.Pvar id }, f] ->
let v = create_vsymbol (create_user_id id) ty in
let lvm = Mstr.add id.id v lvm in
let lvm = Mstr.add id.id_str v lvm in
Some v, Loc.try3 ~loc type_fmla lenv.uc lenv.th_old lvm f
| _ ->
let v = create_vsymbol (id_fresh "result") ty in
let i = { id = "(null)"; id_loc = loc; id_lab = [] } in
let t = { pp_desc = PPident (Qident i); pp_loc = loc } in
let f = { pp_desc = PPmatch (t, pfl); pp_loc = loc } in
let i = { id_str = "(null)"; id_loc = loc; id_lab = [] } in
let t = { term_desc = Tident (Qident i); term_loc = loc } in
let f = { term_desc = Tmatch (t, pfl); term_loc = loc } in
let lvm = Mstr.add "(null)" v lvm in
Some v, Loc.try3 ~loc type_fmla lenv.uc lenv.th_old lvm f
in
......@@ -332,9 +332,9 @@ let dbinder uc (_,id,gh,pty) = dbinder uc id gh pty
let rec dtype_c lenv (tyv, sp) = dtype_v lenv tyv, dspec lenv sp
and dtype_v lenv = function
| Tpure pty ->
| PTpure pty ->
DSpecV (dity_of_ity (ity_of_pty lenv.uc pty))
| Tarrow (bl,tyc) ->
| PTfunc (bl,tyc) ->
DSpecA (List.map (fun p -> dparam lenv.uc p) bl, dtype_c lenv tyc)
(* expressions *)
......@@ -379,8 +379,8 @@ let chainable_qualid uc p = match uc_find_ps uc p with
let chainable_op uc denv op =
(* non-bool -> non-bool -> bool *)
op.id = "infix =" || op.id = "infix <>" ||
match denv_get_opt denv op.id with
op.id_str = "infix =" || op.id_str = "infix <>" ||
match denv_get_opt denv op.id_str with
| Some (DEvar (_,t)) -> dvty_is_chainable t
| Some (DEgpsym ps) -> chainable_ps ps
| Some _ -> false (* can never happen *)
......@@ -427,7 +427,7 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
"unexpected exception symbol %a" print_xs xs
in
let qualid_app q el = match q with
| Qident {id = n} ->
| Qident {id_str = n} ->
(match denv_get_opt denv n with
| Some d -> expr_app d el
| None -> qualid_app q el)
......@@ -456,8 +456,8 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
DElsapp (fs_tuple (List.length el), el)
| Ptree.Einfix (e12, op2, e3)
| Ptree.Einnfix (e12, op2, e3) ->
let make_app de1 op de2 = if op.id = "infix <>" then
let oq = Qident { op with id = "infix =" } in
let make_app de1 op de2 = if op.id_str = "infix <>" then
let oq = Qident { op with id_str = "infix =" } in
(* FIXME: op.id_loc is wrong for the 2nd argument *)
let dt = qualid_app oq [(op.id_loc, de1); (op.id_loc, de2)] in
DEnot (Mlw_dexpr.dexpr ~loc dt)
......@@ -543,7 +543,7 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
DEif (e1, e2, e3)
| Ptree.Enot e1 ->
DEnot (dexpr lenv denv e1)
| Ptree.Elazy (op, e1, e2) ->
| Ptree.Elazy (e1, op, e2) ->
let op = match op with
| Ptree.LazyAnd -> DEand
| Ptree.LazyOr -> DEor in
......@@ -650,15 +650,15 @@ let add_type_invariant loc uc id params inv =
let x = "self" in
let its = match uc_find_ts uc (Qident id) with
| PT its when its.its_inv -> its
| _ -> Loc.errorm ~loc "type %s does not have an invariant" id.id in
let add_tv acc { id = id; id_loc = loc } =
| _ -> Loc.errorm ~loc "type %s does not have an invariant" id.id_str in
let add_tv acc { id_str = id; id_loc = loc } =
let e = Loc.Located (loc, DuplicateTypeVar id) in
Sstr.add_new e id acc, tv_of_string id in
let _, tvl = Lists.map_fold_left add_tv Sstr.empty params in
let ty = ty_app its.its_ts (List.map ty_var tvl) in
let res = create_vsymbol (id_fresh x) ty in
let find = function
| Qident { id = id } when id = x -> Some res
| Qident { id_str = id } when id = x -> Some res
| _ -> None in
let mk_inv f =
let f = Typing.type_fmla (get_theory uc) find f in
......@@ -673,10 +673,10 @@ let add_type_invariant loc uc id params inv =
Mlw_module.add_invariant uc its q
let look_for_loc tdl s =
let look_id loc id = if id.id = s then Some id.id_loc else loc in
let look_id loc id = if id.id_str = s then Some id.id_loc else loc in
let look_pj loc (_,id,_,_) = Opt.fold look_id loc id in
let look_cs loc (csloc,id,pjl) =
let loc = if id.id = s then Some csloc else loc in
let loc = if id.id_str = s then Some csloc else loc in
List.fold_left look_pj loc pjl in
let look_fl loc f = look_id loc f.f_ident in
let look loc d =
......@@ -690,7 +690,7 @@ let look_for_loc tdl s =
let add_types ~wp uc tdl =
let add m d =
let id = d.td_ident.id in
let id = d.td_ident.id_str in
Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d m in
let def = List.fold_left add Mstr.empty tdl in
......@@ -701,16 +701,16 @@ let add_types ~wp uc tdl =
| Some false -> Loc.errorm ~loc:d.td_loc "Cyclic type definition"
| None ->
let ts_seen seen = function
| Qident { id = x } ->
| Qident { id_str = x } ->
begin try cyc_visit x (Mstr.find x def) seen
with Not_found -> seen end
| _ -> seen in
let rec check seen = function
| PPTtyvar _ -> seen
| PPTparen ty -> check seen ty
| PPTarrow (ty1,ty2) -> check (check seen ty1) ty2
| PPTtyapp (q,tyl) -> List.fold_left check (ts_seen seen q) tyl
| PPTtuple tyl -> List.fold_left check seen tyl in
| PTtyvar _ -> seen
| PTparen ty -> check seen ty
| PTarrow (ty1,ty2) -> check (check seen ty1) ty2
| PTtyapp (q,tyl) -> List.fold_left check (ts_seen seen q) tyl
| PTtuple tyl -> List.fold_left check seen tyl in
let seen = match d.td_def with
| TDabstract | TDalgebraic _ | TDrecord _ -> seen
| TDalias ty -> check (Mstr.add x false seen) ty in
......@@ -724,18 +724,18 @@ let add_types ~wp uc tdl =
try Hstr.find impures x
with Not_found ->
let ts_imp = function
| Qident { id = x } when Mstr.mem x def -> imp_visit x
| Qident { id_str = x } when Mstr.mem x def -> imp_visit x
| q ->
begin match uc_find_ts uc q with
| PT _ -> true | TS _ -> false
end
in
let rec check = function
| PPTtyvar _ -> false
| PPTparen ty -> check ty
| PPTarrow (ty1,ty2) -> check ty1 || check ty2
| PPTtyapp (q,tyl) -> ts_imp q || List.exists check tyl
| PPTtuple tyl -> List.exists check tyl in
| PTtyvar _ -> false
| PTparen ty -> check ty
| PTarrow (ty1,ty2) -> check ty1 || check ty2
| PTtyapp (q,tyl) -> ts_imp q || List.exists check tyl
| PTtuple tyl -> List.exists check tyl in
Hstr.replace impures x false;
let imp =
let td = Mstr.find x def in
......@@ -762,7 +762,7 @@ let add_types ~wp uc tdl =
try Hstr.find mutables x
with Not_found ->
let ts_mut = function
| Qident { id = x } when Mstr.mem x def -> mut_visit x
| Qident { id_str = x } when Mstr.mem x def -> mut_visit x
| q ->
begin match uc_find_ts uc q with
| PT its -> its.its_regs <> [] || its.its_inv
......@@ -770,11 +770,11 @@ let add_types ~wp uc tdl =
end
in
let rec check = function
| PPTtyvar _ -> false
| PPTparen ty -> check ty
| PPTarrow (ty1,ty2) -> check ty1 || check ty2
| PPTtyapp (q,tyl) -> ts_mut q || List.exists check tyl
| PPTtuple tyl -> List.exists check tyl in
| PTtyvar _ -> false
| PTparen ty -> check ty
| PTarrow (ty1,ty2) -> check ty1 || check ty2
| PTtyapp (q,tyl) -> ts_mut q || List.exists check tyl
| PTtuple tyl -> List.exists check tyl in
Hstr.replace mutables x false;
let mut =
let td = Mstr.find x def in
......@@ -811,41 +811,45 @@ let add_types ~wp uc tdl =
with Not_found ->
let d = Mstr.find x def in
let add_tv acc id =
let e = Loc.Located (id.Ptree.id_loc, DuplicateTypeVar id.id) in
let tv = tv_of_string id.id in
Mstr.add_new e id.id tv acc in
let e = Loc.Located (id.Ptree.id_loc, DuplicateTypeVar id.id_str) in
let tv = tv_of_string id.id_str in
Mstr.add_new e id.id_str tv acc in
let vars = List.fold_left add_tv Mstr.empty d.td_params in
let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in
let vl = List.map (fun id -> Mstr.find id.id_str vars) d.td_params in
let id = Typing.create_user_id d.td_ident in