Commit 43b684d0 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: match expression is ghost if we look inside ghost fields

We store in every lsymbol a new integer field ls_constr,
equal to zero if the lsymbol is not a constructor, and equal
to the number of constructors of the lsymbol's type otherwise.
It is allowed to declare or define an lsymbol with ls_constr > 0
as an ordinary function (otherwise algebraic type elimination
wouldn't work - though we might still check this in theories),
but it is forbidden to use a wrong ls_constr in algebraic type
definitions.

The ghostness of a match expression is now determined as follows:

If at least one branch expression is ghost,
  then the match is ghost;
else if there is only one branch,
  then the match is not ghost;
else if the matched expression is ghost,
  then the match is ghost;
else if at least one pattern matches a ghost field
        against a constructor with ls_constr > 1
  then the match is ghost;
else
  the match is not ghost.

We do just enough to recognize obvious non-ghost cases, and
make no attempt to handle redundant matches or to detect
exhaustive or-patterns in subpatterns.
parent bb6734a1
module TestGhost
use import int.Int
use import list.List
use import ref.Ref
type t = { f1 : int; ghost f2 : (int,list int) }
let test1 (x: int) (y: t) =
ensures { result = y.f1 }
let r1 = ref x in
let _ = match y with
| { f1 = i; f2 = (_,Nil) } -> r1 := i
| _ -> ()
end in
!r1
end
......@@ -427,7 +427,7 @@ let rec tr_arith_constant dep t = match kind_of_term t with
| _ ->
raise NotArithConstant
let body_of_constant c =
let body_of_constant c =
if Reductionops.is_transparent (ConstKey c) then
CoqCompat.body_of_constant (Global.lookup_constant c)
else None
......@@ -534,6 +534,8 @@ and tr_global_ts dep env r =
let j = ith_mutual_inductive i j in
let ts = lookup_table global_ts (IndRef j) in
let tyj = Ty.ty_app ts (List.map Ty.ty_var ts.Ty.ts_args) in
let opaque = Ty.Stv.of_list ts.Ty.ts_args in
let constr = Array.length oib.mind_nf_lc in
let mk_constructor k _tyk = (* k-th constructor *)
let r = ConstructRef (j, k+1) in
let ty = Global.type_of_global r in
......@@ -548,7 +550,7 @@ and tr_global_ts dep env r =
let l, _ = decompose_arrows t in
let l = List.map (tr_type dep' tvm env) l in
let id = preid_of_id (Nametab.basename_of_global r) in
let ls = Term.create_lsymbol id l (Some tyj) in
let ls = Term.create_fsymbol ~opaque ~constr id l tyj in
add_table global_ls r (Some ls);
add_poly_arity ls vars;
ls, List.map (fun _ -> None) ls.ls_args
......
......@@ -423,19 +423,20 @@ let create_data_decl tdl =
let tss = List.fold_left add Sts.empty tdl in
let check_proj cs tyv s tya ls = match ls with
| None -> s
| Some ({ ls_args = [ptyv]; ls_value = Some ptya } as ls) ->
| Some ({ls_args = [ptyv]; ls_value = Some ptya; ls_constr = 0} as ls) ->
ty_equal_check tyv ptyv;
ty_equal_check tya ptya;
Sls.add_new (DuplicateRecordField (cs,ls)) ls s
| Some ls -> raise (BadRecordField ls)
in
let check_constr tys ty pjs (syms,news) (fs,pl) =
let check_constr tys ty cll pjs (syms,news) (fs,pl) =
ty_equal_check ty (Opt.get_exn (BadConstructor fs) fs.ls_value);
let fs_pjs =
try List.fold_left2 (check_proj fs ty) Sls.empty fs.ls_args pl
with Invalid_argument _ -> raise (BadConstructor fs) in
if not (Sls.equal pjs fs_pjs) then
raise (RecordFieldMissing (fs, Sls.choose (Sls.diff pjs fs_pjs)));
if fs.ls_constr <> cll then raise (BadConstructor fs);
let vs = ty_freevars Stv.empty ty in
let rec check seen ty = match ty.ty_node with
| Tyvar v when Stv.mem v vs -> ()
......@@ -451,6 +452,7 @@ let create_data_decl tdl =
syms, news_id news fs.ls_name
in
let check_decl (syms,news) (ts,cl) =
let cll = List.length cl in
if cl = [] then raise (EmptyAlgDecl ts);
if ts.ts_def <> None then raise (IllegalTypeAlias ts);
let news = news_id news ts.ts_name in
......@@ -458,7 +460,7 @@ let create_data_decl tdl =
(Opt.fold (fun s ls -> Sls.add ls s)) s pl) Sls.empty cl in
let news = Sls.fold (fun pj s -> news_id s pj.ls_name) pjs news in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
List.fold_left (check_constr ts ty pjs) (syms,news) cl
List.fold_left (check_constr ts ty cll pjs) (syms,news) cl
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
mk_decl (Ddata tdl) syms news
......
......@@ -21,7 +21,7 @@ module type Action = sig
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol
exception ConstructorExpected of lsymbol * ty
exception NonExhaustive of pattern list
module Compile (X : Action) = struct
......@@ -51,7 +51,7 @@ module Compile (X : Action) = struct
| Pas (p,_) -> populate acc p
| Por (p,q) -> populate (populate acc p) q
| Papp (fs,pl) when Sls.mem fs css -> Mls.add fs pl acc
| Papp (fs,_) -> raise (ConstructorExpected fs)
| Papp (fs,_) -> raise (ConstructorExpected (fs,ty))
in
let populate acc (pl,_) = populate acc (List.hd pl) in
List.fold_left populate Mls.empty rl
......
......@@ -22,7 +22,7 @@ module type Action = sig
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol
exception ConstructorExpected of lsymbol * ty
exception NonExhaustive of pattern list
module Compile (X : Action) : sig
......
......@@ -524,13 +524,16 @@ let () = Exn_printer.register
fprintf fmt "Not a function symbol: %a" print_ls ls
| Term.PredicateSymbolExpected ls ->
fprintf fmt "Not a predicate symbol: %a" print_ls ls
| Term.ConstructorExpected ls ->
fprintf fmt "Symbol %a is not a constructor"
print_ls ls
| Term.TermExpected t ->
fprintf fmt "Not a term: %a" print_term t
| Term.FmlaExpected t ->
fprintf fmt "Not a formula: %a" print_term t
| Pattern.ConstructorExpected ls ->
fprintf fmt "The symbol %a is not a constructor"
print_ls ls
| Pattern.ConstructorExpected (ls,ty) ->
fprintf fmt "Symbol %a is not a constructor of type %a"
print_ls ls print_ty ty
| Pattern.NonExhaustive pl ->
fprintf fmt "Pattern not covered by a match:@\n @[%a@]"
print_pat (List.hd pl)
......
......@@ -46,6 +46,7 @@ type lsymbol = {
ls_args : ty list;
ls_value : ty option;
ls_opaque : Stv.t;
ls_constr : int;
}
module Lsym = MakeMSHW (struct
......@@ -68,15 +69,20 @@ let check_opaque opaque args value =
let s = List.fold_left diff (Opt.fold diff opaque value) args in
if Stv.is_empty s then opaque else invalid_arg "Term.create_lsymbol"
let create_lsymbol ?(opaque=Stv.empty) name args value = {
let create_lsymbol ?(opaque=Stv.empty) ?(constr=0) name args value = {
ls_name = id_register name;
ls_args = args;
ls_value = value;
ls_opaque = check_opaque opaque args value;
ls_constr = if constr = 0 || (constr > 0 && value <> None)
then constr else invalid_arg "Term.create_lsymbol";
}
let create_fsymbol ?opaque nm al vl = create_lsymbol ?opaque nm al (Some vl)
let create_psymbol ?opaque nm al = create_lsymbol ?opaque nm al (None)
let create_fsymbol ?opaque ?constr nm al vl =
create_lsymbol ?opaque ?constr nm al (Some vl)
let create_psymbol ?opaque ?constr nm al =
create_lsymbol ?opaque ?constr nm al None
let ls_ty_freevars ls =
let acc = oty_freevars Stv.empty ls.ls_value in
......@@ -199,6 +205,7 @@ let pat_any pr pat =
exception BadArity of lsymbol * int * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
exception ConstructorExpected of lsymbol
let pat_app fs pl ty =
let s = match fs.ls_value with
......@@ -209,6 +216,7 @@ let pat_app fs pl ty =
ignore (try List.fold_left2 mtch s fs.ls_args pl
with Invalid_argument _ -> raise (BadArity
(fs, List.length fs.ls_args, List.length pl)));
if fs.ls_constr = 0 then raise (ConstructorExpected fs);
pat_app fs pl ty
let pat_as p v =
......@@ -793,8 +801,8 @@ let ps_equ =
let t_equ t1 t2 = ps_app ps_equ [t1; t2]
let t_neq t1 t2 = t_not (ps_app ps_equ [t1; t2])
let fs_bool_true = create_fsymbol (id_fresh "True") [] ty_bool
let fs_bool_false = create_fsymbol (id_fresh "False") [] ty_bool
let fs_bool_true = create_fsymbol ~constr:2 (id_fresh "True") [] ty_bool
let fs_bool_false = create_fsymbol ~constr:2 (id_fresh "False") [] ty_bool
let t_bool_true = fs_app fs_bool_true [] ty_bool
let t_bool_false = fs_app fs_bool_false [] ty_bool
......@@ -807,7 +815,7 @@ let fs_tuple = Hint.memo 17 (fun n ->
let tl = List.map ty_var ts.ts_args in
let ty = ty_app ts tl in
let id = id_fresh ("Tuple" ^ string_of_int n) in
let fs = create_fsymbol ~opaque id tl ty in
let fs = create_fsymbol ~opaque ~constr:1 id tl ty in
Hid.add fs_tuple_ids fs.ls_name n;
fs)
......
......@@ -39,6 +39,7 @@ type lsymbol = private {
ls_args : ty list;
ls_value : ty option;
ls_opaque : Stv.t;
ls_constr : int;
}
module Mls : Extmap.S with type key = lsymbol
......@@ -49,9 +50,14 @@ module Wls : Weakhtbl.S with type key = lsymbol
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol : ?opaque:Stv.t -> preid -> ty list -> ty option -> lsymbol
val create_fsymbol : ?opaque:Stv.t -> preid -> ty list -> ty -> lsymbol
val create_psymbol : ?opaque:Stv.t -> preid -> ty list -> lsymbol
val create_lsymbol :
?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty option -> lsymbol
val create_fsymbol :
?opaque:Stv.t -> ?constr:int -> preid -> ty list -> ty -> lsymbol
val create_psymbol :
?opaque:Stv.t -> ?constr:int -> preid -> ty list -> lsymbol
val ls_ty_freevars : lsymbol -> Stv.t
......@@ -63,6 +69,7 @@ exception UncoveredVar of vsymbol
exception BadArity of lsymbol * int * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
exception ConstructorExpected of lsymbol
(** {2 Patterns} *)
......
......@@ -505,9 +505,11 @@ let cl_find_ls cl ls =
else try Mls.find ls cl.ls_table
with Not_found ->
let opaque = ls.ls_opaque in
let constr = ls.ls_constr in
let id = id_clone ls.ls_name in
let ta' = List.map (cl_trans_ty cl) ls.ls_args in
let vt' = Opt.map (cl_trans_ty cl) ls.ls_value in
let ls' = create_lsymbol ~opaque (id_clone ls.ls_name) ta' vt' in
let ls' = create_lsymbol ~opaque ~constr id ta' vt' in
cl.ls_table <- Mls.add ls ls' cl.ls_table;
ls'
......
......@@ -763,6 +763,7 @@ let add_types dl th =
| TDalias _ -> abstr, algeb, ts::alias
| TDalgebraic cl ->
let ht = Hstr.create 17 in
let constr = List.length cl in
let opaque = Stv.of_list ts.ts_args in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let projection (_,id,_,_) fty = match id with
......@@ -784,7 +785,7 @@ let add_types dl th =
let tyl = param_tys th' pl in
let pjl = List.map2 projection pl tyl in
Hstr.replace csymbols id.id loc;
create_fsymbol ~opaque (create_user_id id) tyl ty, pjl
create_fsymbol ~opaque ~constr (create_user_id id) tyl ty, pjl
in
abstr, (ts, List.map constructor cl) :: algeb, alias
| TDrecord _ ->
......@@ -806,11 +807,11 @@ let add_types dl th =
let prepare_typedef td =
if td.td_model then
errorm ~loc:td.td_loc "model types are not allowed in the logic";
errorm ~loc:td.td_loc "model types are not allowed in pure theories";
if td.td_vis <> Public then
errorm ~loc:td.td_loc "logic types cannot be abstract or private";
errorm ~loc:td.td_loc "pure types cannot be abstract or private";
if td.td_inv <> [] then
errorm ~loc:td.td_loc "logic types cannot have invariants";
errorm ~loc:td.td_loc "pure types cannot have invariants";
match td.td_def with
| TDabstract | TDalgebraic _ | TDalias _ ->
td
......
......@@ -125,7 +125,7 @@ let create_data_decl tdl =
(* let syms = ref Sid.empty in *)
let news = ref Sid.empty in
let projections = Hstr.create 17 in (* id -> plsymbol *)
let build_constructor its res (id,al) =
let build_constructor its res cll (id,al) =
(* check well-formedness *)
let fds = List.map snd al in
let tvs = List.fold_right Stv.add its.its_ts.ts_args Stv.empty in
......@@ -141,7 +141,7 @@ let create_data_decl tdl =
List.iter check_arg fds;
(* build the constructor ps *)
let hidden = its.its_abst and rdonly = its.its_priv in
let cs = create_plsymbol ~hidden ~rdonly id fds res in
let cs = create_plsymbol ~hidden ~rdonly ~constr:cll id fds res in
news := news_id !news cs.pl_ls.ls_name;
(* build the projections, if any *)
let build_proj fd id =
......@@ -167,10 +167,11 @@ let create_data_decl tdl =
let build_type (its,cl) =
Hstr.clear projections;
news := news_id !news its.its_ts.ts_name;
let cll = List.length cl in
let tvl = List.map ity_var its.its_ts.ts_args in
let ity = ity_app its tvl its.its_regs in
let res = { fd_ity = ity; fd_ghost = false; fd_mut = None } in
its, List.map (build_constructor its res) cl, null_invariant its
its, List.map (build_constructor its res cll) cl, null_invariant its
in
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) Sid.empty !news
......
......@@ -48,7 +48,7 @@ let create_plsymbol_unsafe, restore_pl =
pl),
Wls.find ls_to_pls
let create_plsymbol ?(hidden=false) ?(rdonly=false) id args value =
let create_plsymbol ?(hidden=false) ?(rdonly=false) ?(constr=0) id args value =
let ty_of_field fd =
Opt.iter (fun r -> ity_equal_check fd.fd_ity r.reg_ity) fd.fd_mut;
ty_of_ity fd.fd_ity in
......@@ -56,7 +56,7 @@ let create_plsymbol ?(hidden=false) ?(rdonly=false) id args value =
let pure_value = ty_of_field value in
(* plsymbols are used for constructors and projections, which are safe *)
let opaque = List.fold_left ty_freevars Stv.empty (pure_value::pure_args) in
let ls = create_fsymbol ~opaque id pure_args pure_value in
let ls = create_fsymbol ~opaque ~constr id pure_args pure_value in
create_plsymbol_unsafe ls args value ~hidden ~rdonly
let ity_of_ty_opt ty = ity_of_ty (Opt.get_def ty_bool ty)
......@@ -138,6 +138,7 @@ type pre_ppattern =
let make_ppattern pp ?(ghost=false) ity =
let hv = Hstr.create 3 in
let gghost = ref false in
let find id ghost ity =
let nm = preid_name id in
try
......@@ -170,6 +171,9 @@ let make_ppattern pp ?(ghost=false) ity =
ppat_effect = eff_empty; }
| PPpapp (pls,ppl) ->
if pls.pl_hidden then raise (HiddenPLS pls);
if pls.pl_ls.ls_constr = 0 then
raise (Term.ConstructorExpected pls.pl_ls);
if ghost && pls.pl_ls.ls_constr > 1 then gghost := true;
let ityv = pls.pl_value.fd_ity in
let sbs = ity_match ity_subst_empty ityv ity in
let mtch arg pp =
......@@ -183,17 +187,20 @@ let make_ppattern pp ?(ghost=false) ity =
{ pp with ppat_effect = eff }
| _, _ -> pp in
let ppl = try List.map2 mtch pls.pl_args ppl with
| Not_found -> raise (Pattern.ConstructorExpected pls.pl_ls)
| Not_found -> raise (Term.ConstructorExpected pls.pl_ls)
| Invalid_argument _ -> raise (Term.BadArity
(pls.pl_ls, List.length pls.pl_args, List.length ppl)) in
make_app pls.pl_ls ppl ghost ity
| PPlapp (ls,ppl) ->
if ls.ls_constr = 0 then
raise (Term.ConstructorExpected ls);
if ghost && ls.ls_constr > 1 then gghost := true;
let ityv = ity_of_ty_opt ls.ls_value in
let sbs = ity_match ity_subst_empty ityv ity in
let mtch arg pp =
make ghost (ity_full_inst sbs (ity_of_ty arg)) pp in
let ppl = try List.map2 mtch ls.ls_args ppl with
| Not_found -> raise (Pattern.ConstructorExpected ls)
| Not_found -> raise (Term.ConstructorExpected ls)
| Invalid_argument _ -> raise (Term.BadArity
(ls,List.length ls.ls_args,List.length ppl)) in
make_app ls ppl ghost ity
......@@ -212,6 +219,8 @@ let make_ppattern pp ?(ghost=false) ity =
ppat_effect = pp.ppat_effect; }
in
let pp = make ghost ity pp in
let gh = pp.ppat_ghost || !gghost in
let pp = { pp with ppat_ghost = gh } in
Hstr.fold Mstr.add hv Mstr.empty, pp
(** program symbols *)
......@@ -636,16 +645,18 @@ let e_case e0 bl =
let bity = match bl with
| (_,e)::_ -> ity_of_expr e
| [] -> raise Term.EmptyCase in
let multi_br = List.length bl > 1 in
let rec branch ghost eff varm = function
| (pp,e)::bl ->
if pp.ppat_ghost <> e0.e_ghost then
if e0.e_ghost && not pp.ppat_ghost then
Loc.errorm "Non-ghost pattern in a ghost position";
ity_equal_check (ity_of_expr e0) pp.ppat_ity;
ity_equal_check (ity_of_expr e) bity;
let ghost = ghost || e.e_ghost in
let del_vs vs _ m = Mid.remove vs.vs_name m in
let bvarm = Mvs.fold del_vs pp.ppat_pattern.pat_vars e.e_varm in
let eff = eff_union (eff_union eff pp.ppat_effect) e.e_effect in
(* one-branch match is not ghost even if its pattern is ghost *)
let ghost = ghost || (multi_br && pp.ppat_ghost) || e.e_ghost in
branch ghost eff (varmap_union varm bvarm) bl
| [] ->
(* the cumulated effect of all branches, w/out e0 *)
......@@ -655,9 +666,7 @@ let e_case e0 bl =
let varm = add_e_vars e0 varm in
mk_expr (Ecase (e0,bl)) (VTvalue bity) ghost eff varm
in
(* a one-branch match may be not ghost even if the matched expr is *)
let ghost = match bl with [_] -> false | _ -> e0.e_ghost in
branch ghost eff_empty Mid.empty bl
branch false eff_empty Mid.empty bl
(* ghost *)
......
......@@ -42,7 +42,8 @@ type plsymbol = private {
val pl_equal : plsymbol -> plsymbol -> bool
val create_plsymbol :
?hidden:bool -> ?rdonly:bool -> preid -> field list -> field -> plsymbol
?hidden:bool -> ?rdonly:bool -> ?constr:int ->
preid -> field list -> field -> plsymbol
exception HiddenPLS of plsymbol
exception RdOnlyPLS of plsymbol
......
......@@ -1867,6 +1867,7 @@ let add_types ~wp uc tdl =
let mk_pure_decl ts csl =
let pjt = Hstr.create 3 in
let constr = List.length csl in
let opaque = Stv.of_list ts.ts_args in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let mk_proj (pj,fd) =
......@@ -1881,7 +1882,7 @@ let add_types ~wp uc tdl =
in
let mk_constr (id,pjl) =
let pjl = List.map mk_proj pjl in
let cs = create_fsymbol ~opaque id (List.map fst pjl) ty in
let cs = create_fsymbol ~opaque ~constr id (List.map fst pjl) ty in
cs, List.map snd pjl
in
List.map mk_constr csl
......
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