Skip to content
GitLab
Commit c60caecb authored by Mário Pereira's avatar Mário Pereira
Browse files

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system

parents 7e641725 232875b5
Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ c60caecb
......@@ -86,7 +86,6 @@ why3.conf
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
/bin/style.css
# /doc/
/doc/version.tex
......@@ -123,9 +122,10 @@ why3.conf
/doc/apidoc/
/doc/stdlibdoc/
/doc/texput.log
/doc/q.log
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
......@@ -133,7 +133,6 @@ why3.conf
# /lib/why3/
/lib/why3/META
/lib/why3-cpulimit
# /lib/ocaml/
/lib/ocaml/why3__BigInt_compat.ml
......
src/core/dterm.ml
View file @ c60caecb
......@@ -235,6 +235,7 @@ let dty_unify_app ls unify (l1: 'a list) (l2: dty list) =
try List.iter2 unify l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l1))
(* FIXME: can we convert every use of dty_unify_app to this one? *)
let dty_unify_app_map ls unify (l1: 'a list) (l2: dty list) =
try List.map2 unify l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l1))
......@@ -274,6 +275,7 @@ let dpattern ?loc node =
dty, Mstr.singleton n dty
| DPapp (ls,dpl) ->
let dtyl, dty = specialize_cs ls in
(* FIXME: ignore (dty_unify_app_map ...) ? *)
dty_unify_app ls dpat_expected_type dpl dtyl;
let join n _ _ = raise (DuplicateVar n) in
let add acc dp = Mstr.union join acc dp.dp_vars in
......@@ -296,31 +298,25 @@ let dpattern ?loc node =
let slab_coercion = Slab.singleton Pretty.label_coercion
let apply_coercion ~loc l dt =
let apply_coercion l ({dt_loc = loc} as dt) =
let apply dt ls =
let (dtyl, dty) = specialize_ls ls in
let dtl = [dt] in
List.iter2 dterm_expected_type dtl dtyl;
let dt = { dt_node = DTapp (ls, dtl); dt_dty = dty; dt_loc = loc } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } in
let dtyl, dty = specialize_ls ls in
dterm_expected_type dt (List.hd dtyl);
let dt = { dt_node = DTapp (ls, [dt]); dt_dty = dty; dt_loc = loc } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } in
List.fold_left apply dt l
(* coercions using just head tysymbols without type arguments: *)
(* TODO: this can be improved *)
let rec ts_of_dty = function
| Dvar { contents = Dval (Duty { ty_node = (Tyapp (ts, _)) })} ->
ts
| Dvar { contents = Dval dty } ->
ts_of_dty dty
| Dvar { contents = Dind _ } ->
let tv = create_tvsymbol (id_fresh "xi") in
raise (UndefinedTypeVar tv)
| Dapp (ts, _) ->
ts
| Duty { ty_node = (Tyapp (ts, _)) } ->
ts
| Duty { ty_node = Tyvar tv } ->
raise (UndefinedTypeVar tv)
| Dvar {contents = Dval dty} ->
ts_of_dty dty
| Dvar {contents = Dind _}
| Duty {ty_node = Tyvar _} ->
raise Exit
| Duty {ty_node = Tyapp (ts,_)}
| Dapp (ts,_) ->
ts
let ts_of_dty = function
| Some dt_dty -> ts_of_dty dt_dty
......@@ -332,8 +328,8 @@ let dterm_expected tuc dt dty =
if (ts_equal ts1 ts2) then dt
else
let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts2 in
apply_coercion ~loc:dt.dt_loc crc dt
with Not_found | UndefinedTypeVar _ -> dt
apply_coercion crc dt
with Not_found | Exit -> dt
let dterm_expected_dterm tuc dt dty =
let dt = dterm_expected tuc dt (Some dty) in
......@@ -350,48 +346,51 @@ let dterm tuc ?loc node =
let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
match node with
| DTvar (_,dty) ->
mk_dty (Some dty)
mk_dty (Some dty)
| DTgvar vs ->
mk_dty (Some (dty_of_ty vs.vs_ty))
mk_dty (Some (dty_of_ty vs.vs_ty))
| DTconst (Number.ConstInt _) ->
mk_dty (Some dty_int)
mk_dty (Some dty_int)
| DTconst (Number.ConstReal _) ->
mk_dty (Some dty_real)
mk_dty (Some dty_real)
| DTapp (ls, dtl) when ls_equal ls ps_equ ->
let dtyl, dty = specialize_ls ls in
let dtl = dty_unify_app_map ls (dterm_expected_dterm tuc) (List.rev dtl) dtyl in
{ dt_node = DTapp (ls, List.rev dtl);
dt_dty = dty;
dt_loc = loc }
let dtyl, dty = specialize_ls ls in
let dtl = dty_unify_app_map ls
(dterm_expected_dterm tuc) (List.rev dtl) dtyl in
{ dt_node = DTapp (ls, List.rev dtl);
dt_dty = dty;
dt_loc = loc }
| DTapp (ls, dtl) ->
let dtyl, dty = specialize_ls ls in
{ dt_node = DTapp (ls, dty_unify_app_map ls (dterm_expected_dterm tuc) dtl dtyl);
dt_dty = dty;
dt_loc = loc }
let dtyl, dty = specialize_ls ls in
{ dt_node = DTapp (ls,
dty_unify_app_map ls (dterm_expected_dterm tuc) dtl dtyl);
dt_dty = dty;
dt_loc = loc }
| DTfapp ({dt_dty = Some res} as dt1,dt2) ->
let rec not_arrow = function
| Dvar {contents = Dval dty} -> not_arrow dty
| Duty {ty_node = Tyapp (ts,_)}
| Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
| Dvar _ -> false | _ -> true in
if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
"This term has type %a,@ it cannot be applied" print_dty res;
let dtyl, dty = specialize_ls fs_func_app in
dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
mk_dty dty
let rec not_arrow = function
| Dvar {contents = Dval dty} -> not_arrow dty
| Duty {ty_node = Tyapp (ts,_)}
| Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
| Dvar _ -> false | _ -> true in
if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
"This term has type %a,@ it cannot be applied" print_dty res;
let dtyl, dty = specialize_ls fs_func_app in
(* FIXME: why no conversion here? *)
dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
mk_dty dty
| DTfapp ({dt_dty = None; dt_loc = loc},_) ->
Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
| DTif (df,dt1,dt2) ->
let df = dfmla_expected_dterm tuc df in
dexpr_expected_type dt2 dt1.dt_dty;
{ dt_node = DTif (df, dt1, dt2);
dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty;
dt_loc = loc }
let df = dfmla_expected_dterm tuc df in
dexpr_expected_type dt2 dt1.dt_dty;
{ dt_node = DTif (df, dt1, dt2);
dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty;
dt_loc = loc }
| DTlet (dt,_,df) ->
ignore (dty_of_dterm dt);
mk_dty df.dt_dty
ignore (dty_of_dterm dt);
mk_dty df.dt_dty
| DTcase (_,[]) ->
raise EmptyCase
raise EmptyCase
| DTcase (dt,(dp1,df1)::bl) ->
dterm_expected_type dt dp1.dp_dty;
let check (dp,df) =
......@@ -401,15 +400,15 @@ let dterm tuc ?loc node =
let is_fmla (_,df) = df.dt_dty = None in
if List.exists is_fmla bl then mk_dty None else mk_dty df1.dt_dty
| DTeps (_,dty,df) ->
dfmla_expected_type df;
mk_dty (Some dty)
dfmla_expected_type df;
mk_dty (Some dty)
| DTquant (DTlambda,vl,_,df) ->
let res = Opt.get_def dty_bool df.dt_dty in
let app (_,l,_) r = Dapp (ts_func,[l;r]) in
mk_dty (Some (List.fold_right app vl res))
let res = Opt.get_def dty_bool df.dt_dty in
let app (_,l,_) r = Dapp (ts_func,[l;r]) in
mk_dty (Some (List.fold_right app vl res))
| DTquant ((DTforall|DTexists),_,_,df) ->
dfmla_expected_type df;
mk_dty None
dfmla_expected_type df;
mk_dty None
| DTbinop (_,df1,df2) ->
dfmla_expected_type df1;
dfmla_expected_type df2;
......@@ -422,13 +421,13 @@ let dterm tuc ?loc node =
always replace [true] by [True] and [false] by [False], so that
there is no need to count these constructs as "formulas" which
require explicit if-then-else conversion to bool *)
mk_dty (Some dty_bool)
mk_dty (Some dty_bool)
| DTcast (dt,ty) ->
let dty = dty_of_ty ty in
dterm_expected_dterm tuc dt dty
let dty = dty_of_ty ty in
dterm_expected_dterm tuc dt dty
| DTuloc (dt,_)
| DTlabel (dt,_) ->
mk_dty (dt.dt_dty)
mk_dty (dt.dt_dty)
in Loc.try1 ?loc (dterm_node loc) node
(** Final stage *)
......
src/core/theory.ml
View file @ c60caecb
......@@ -153,11 +153,11 @@ type theory = {
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
th_crcmap : Coercion.t; (* coercions *)
}
and tdecl = {
......@@ -257,13 +257,13 @@ type theory_uc = {
uc_name : ident;
uc_path : string list;
uc_decls : tdecl list;
uc_crcmap : Coercion.t;
uc_prefix : string list;
uc_import : namespace list;
uc_export : namespace list;
uc_known : known_map;
uc_local : Sid.t;
uc_used : Sid.t;
uc_crcmap : Coercion.t;
}
exception CloseTheory
......@@ -273,13 +273,13 @@ let empty_theory n p = {
uc_name = id_register n;
uc_path = p;
uc_decls = [];
uc_crcmap = Coercion.empty;
uc_prefix = [];
uc_import = [empty_ns];
uc_export = [empty_ns];
uc_known = Mid.empty;
uc_local = Sid.empty;
uc_used = Sid.empty;
uc_crcmap = Coercion.empty;
}
let close_theory uc = match uc.uc_export with
......@@ -287,11 +287,11 @@ let close_theory uc = match uc.uc_export with
{ th_name = uc.uc_name;
th_path = uc.uc_path;
th_decls = List.rev uc.uc_decls;
th_crcmap = uc.uc_crcmap;
th_export = e;
th_known = uc.uc_known;
th_local = uc.uc_local;
th_used = uc.uc_used;
th_crcmap = uc.uc_crcmap }
th_used = uc.uc_used }
| _ -> raise CloseTheory
let get_namespace uc = List.hd uc.uc_import
......@@ -350,8 +350,9 @@ let add_tdecl uc td = match td.td_node with
| Clone (_,sm) -> known_clone uc.uc_known sm;
{ uc with uc_decls = td :: uc.uc_decls }
| Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion ->
known_meta uc.uc_known al;
{ uc with uc_crcmap = Coercion.add uc.uc_crcmap ls }
known_meta uc.uc_known al;
(* FIXME: shouldn't we add the meta to the theory? *)
{ uc with uc_crcmap = Coercion.add uc.uc_crcmap ls }
| Meta (_,al) -> known_meta uc.uc_known al;
{ uc with uc_decls = td :: uc.uc_decls }
......
src/core/theory.mli
View file @ c60caecb
......@@ -84,11 +84,11 @@ type theory = private {
th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
th_crcmap : Coercion.t (* coercions *)
}
and tdecl = private {
......@@ -122,14 +122,13 @@ type theory_uc = private {
uc_name : ident;
uc_path : string list;
uc_decls : tdecl list;
uc_crcmap : Coercion.t;
uc_prefix : string list;
uc_import : namespace list;
uc_export : namespace list;
uc_known : known_map;
uc_local : Sid.t;
uc_used : Sid.t;
uc_crcmap : Coercion.t;
}
val create_theory : ?path:string list -> preid -> theory_uc
......
src/mlw/dexpr.ml
View file @ c60caecb
......@@ -822,7 +822,7 @@ let effect_of_dspec dsp =
(* TODO: add warnings for empty postconditions (anywhere)
and empty exceptional postconditions (toplevel). *)
let check_spec inr dsp ecty ({e_loc = loc} as e) =
let bad_read reff eff = not (Spv.subset reff.eff_reads eff.eff_reads) in
let bad_read reff eff = not (Spv.subset reff.eff_reads eff.eff_reads) in
let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
weff.eff_writes eff.eff_writes) in
let bad_raise xeff eff = not (Sxs.subset xeff.eff_raises eff.eff_raises) in
......
src/mlw/eval_match.ml
View file @ c60caecb
......@@ -88,8 +88,9 @@ let is_fragile_projection ls =
(* Integer-indexed "pins" represent individual values whose
invariant may be broken. Fresh pins are assigned to values
from top to bottom, so that a lesser pin can never be reached
from a greater pin. Each pin is associated to a list of fresh
bottom-up, and the canonical representative pin in a UF class
is the minimal one. Thus, a greater pin can never be reached
from a lesser pin. Each pin is associated to a list of fresh
variables that correspond to "temporary fields". Committing
a pin means that we prove that the temporary fields satisfy
the invariant and then assume that the temporary fields are
......@@ -243,9 +244,6 @@ let rec cap_join uf c1 c2 = match c1, c2 with
| _ -> assert false
let cap_of_term kn uf pins caps t =
let cap_join_opt c cj = match cj with
| Some cj -> cap_join uf c cj
| None -> c in
let rec unroll t = function
| (pj,t0)::pjl ->
let t = t_app pj [t] t0.t_ty in
......@@ -279,7 +277,7 @@ let cap_of_term kn uf pins caps t =
| Tyapp (ts,tl) ->
find_constructors_ts kn ts, ts_match_args ts tl
| _ -> assert false in
let mk_branch cs fl =
let add_branch cs fl (bl, cj) =
let fdl = List.assq cs csl in
let mk_pat fd_ty fd = match fd with
| Some ls when ls_equal pj ls -> p0
......@@ -287,10 +285,8 @@ let cap_of_term kn uf pins caps t =
let pl = List.map2 mk_pat cs.ls_args fdl in
let c = find_projection_field pj fl fdl in
let t0, c = unwind t0 c pjl in
t_close_branch (pat_app cs pl ty) t0, c in
let add_branch cs fl (bl, cj) =
let b, c = mk_branch cs fl in
b::bl, Some (cap_join_opt c cj) in
let b = t_close_branch (pat_app cs pl ty) t0 in
b::bl, Some (Opt.fold (cap_join uf) c cj) in
let bl, c = Mls.fold add_branch css (bb, None) in
t_case t bl, Opt.get c
| R pjs, (pj,t0)::pjl ->
......@@ -337,14 +333,12 @@ let cap_of_term kn uf pins caps t =
t_label_copy t (t_let_close v t0 t1), c1
| Tcase (t0,bl) ->
let t0, c0 = down caps [] t0 in
let mk_branch b =
let add_branch b (bl, cj) =
let p, t1 = t_open_branch b in
let caps = add_pat uf caps c0 p in
let t1, c1 = down caps pjl t1 in
t_close_branch p t1, c1 in
let add_branch b (bl, cj) =
let b, c = mk_branch b in
b::bl, Some (cap_join_opt c cj) in
let t1, c = down caps pjl t1 in
let b = t_close_branch p t1 in
b::bl, Some (Opt.fold (cap_join uf) c cj) in
let bl, c = List.fold_right add_branch bl ([], None) in
t_label_copy t (t_case t0 bl), Opt.get c
| Teps tb ->
......@@ -369,6 +363,95 @@ let cap_of_term kn uf pins caps t =
in
down caps [] t
let uf_inter uf1 uf2 =
let uf1 = Mint.map (get_index uf1) uf1 in
let uf2 = Mint.map (get_index uf2) uf2 in
let inter n m1 m2 acc =
if m1 = m2 then acc else
let easy = if m1 < m2
then get_index uf1 m2 = m1
else get_index uf2 m1 = m2 in
if easy then acc else
let inner b = Some (match b with
| Some m -> min m n
| None -> n) in
let outer b = Some (match b with
| Some m -> Mint.change inner m2 m
| None -> Mint.singleton m2 n) in
Mint.change outer m1 acc in
let map = Mint.fold2_inter inter uf1 uf2 Mint.empty in
let inter n m1 m2 =
if m1 = m2 then Some m1 else
try let m = Mint.find m2 (Mint.find m1 map) in
if m = n then None else Some m
with Not_found -> Some (max m1 m2) in
Mint.inter inter uf1 uf2
let rec track kn uf pins caps pos f = match f.t_node with
| Tvar _ | Tconst _ | Teps _ -> assert false (* never *)
| Tapp (ls,[t1;t2]) when not pos && ls_equal ls ps_equ ->
assert false (* TODO *)
| _ when Slab.mem stop_split f.t_label ->
fst (cap_of_term kn uf pins caps f), uf
| Tapp _ ->
fst (cap_of_term kn uf pins caps f), uf
| Tif (f0,f1,f2) ->
let f0, _ = cap_of_term kn uf pins caps f0 in
let f1, uf1 = track kn uf pins caps pos f1 in
let f2, uf2 = track kn uf pins caps pos f2 in
t_label_copy f (t_if f0 f1 f2), uf_inter uf1 uf2
| Tlet (t0,fb) ->
let t0, c0 = cap_of_term kn uf pins caps t0 in
let v, f1 = t_open_bound fb in
let caps = add_cap v c0 caps in
let f1, uf = track kn uf pins caps pos f1 in
t_label_copy f (t_let_close v t0 f1), uf
| Tcase (t0,bl) ->
let t0, c0 = cap_of_term kn uf pins caps t0 in
let add_branch b (bl, ufj) =
let p, f1 = t_open_branch b in
let caps = add_pat uf caps c0 p in
let f1, uf1 = track kn uf pins caps pos f1 in
let b = t_close_branch p f1 in
b::bl, Some (Opt.fold uf_inter uf1 ufj) in
let bl, uf = List.fold_right add_branch bl ([], None) in
t_label_copy f (t_case t0 bl), Opt.get uf
| Tquant (q,fq) ->
let vl, tt, f0 = t_open_quant fq in
let down t = fst (cap_of_term kn uf pins caps t) in
let tt = List.map (List.map down) tt in
let valid = match q with
| Tforall -> not pos
| Texists -> pos in
let caps, pins =
if valid then caps, pins else
let add (caps, pins) v =
let c, pins = add_var kn pins v in
add_cap v c caps, pins in
List.fold_left add (caps, pins) vl in
let f0, uf = track kn uf pins caps pos f0 in
let f0 = t_quant q (t_close_quant vl tt f0) in
t_label_copy f f0, uf
| Tbinop (Tand,f1,f2) ->
let f1, uf1 = track kn uf pins caps pos f1 in
let f2, uf2 = track kn uf1 pins caps pos f2 in
t_label_copy f (t_and f1 f2), uf2
| Tbinop (Timplies,f1,f2) ->
let f1, uf1 = track kn uf pins caps (not pos) f1 in
let f2, _ = track kn uf1 pins caps pos f2 in
t_label_copy f (t_implies f1 f2), uf
| Tbinop (Tor,f1,f2) ->
let f1, uf1 = track kn uf pins caps pos f1 in
let f2, uf2 = track kn uf pins caps pos f2 in
t_label_copy f (t_or f1 f2), uf_inter uf1 uf2
| Tbinop (Tiff,_,_) ->
fst (cap_of_term kn uf pins caps f), uf
| Tnot f1 ->
let f1, _ = track kn uf pins caps (not pos) f1 in
t_label_copy f (t_not f1), uf
| Ttrue | Tfalse ->
f, uf
(* Part II - EvalMatch simplification *)
(* we destruct tuples, units, and singleton records *)
......
Supports Markdown
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