Commit a22db1ec authored by Andrei Paskevich's avatar Andrei Paskevich

small cleanups

parent b8d3a796
...@@ -86,7 +86,6 @@ why3.conf ...@@ -86,7 +86,6 @@ why3.conf
/bin/why3wc.opt /bin/why3wc.opt
/bin/why3wc.byte /bin/why3wc.byte
/bin/why3wc /bin/why3wc
/bin/style.css
# /doc/ # /doc/
/doc/version.tex /doc/version.tex
...@@ -123,9 +122,10 @@ why3.conf ...@@ -123,9 +122,10 @@ why3.conf
/doc/apidoc/ /doc/apidoc/
/doc/stdlibdoc/ /doc/stdlibdoc/
/doc/texput.log /doc/texput.log
/doc/q.log
# /lib # /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
/lib/why3cpulimit /lib/why3cpulimit
/lib/why3cpulimit.exe /lib/why3cpulimit.exe
/lib/why3server /lib/why3server
...@@ -133,7 +133,6 @@ why3.conf ...@@ -133,7 +133,6 @@ why3.conf
# /lib/why3/ # /lib/why3/
/lib/why3/META /lib/why3/META
/lib/why3-cpulimit
# /lib/ocaml/ # /lib/ocaml/
/lib/ocaml/why3__BigInt_compat.ml /lib/ocaml/why3__BigInt_compat.ml
......
...@@ -235,6 +235,7 @@ let dty_unify_app ls unify (l1: 'a list) (l2: dty list) = ...@@ -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 _ -> try List.iter2 unify l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l1)) 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) = let dty_unify_app_map ls unify (l1: 'a list) (l2: dty list) =
try List.map2 unify l1 l2 with Invalid_argument _ -> try List.map2 unify l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l1)) raise (BadArity (ls, List.length l1))
...@@ -274,6 +275,7 @@ let dpattern ?loc node = ...@@ -274,6 +275,7 @@ let dpattern ?loc node =
dty, Mstr.singleton n dty dty, Mstr.singleton n dty
| DPapp (ls,dpl) -> | DPapp (ls,dpl) ->
let dtyl, dty = specialize_cs ls in let dtyl, dty = specialize_cs ls in
(* FIXME: ignore (dty_unify_app_map ...) ? *)
dty_unify_app ls dpat_expected_type dpl dtyl; dty_unify_app ls dpat_expected_type dpl dtyl;
let join n _ _ = raise (DuplicateVar n) in let join n _ _ = raise (DuplicateVar n) in
let add acc dp = Mstr.union join acc dp.dp_vars in let add acc dp = Mstr.union join acc dp.dp_vars in
...@@ -296,31 +298,25 @@ let dpattern ?loc node = ...@@ -296,31 +298,25 @@ let dpattern ?loc node =
let slab_coercion = Slab.singleton Pretty.label_coercion 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 apply dt ls =
let (dtyl, dty) = specialize_ls ls in let dtyl, dty = specialize_ls ls in
let dtl = [dt] in dterm_expected_type dt (List.hd dtyl);
List.iter2 dterm_expected_type dtl dtyl; let dt = { dt_node = DTapp (ls, [dt]); dt_dty = dty; dt_loc = loc } in
let dt = { dt_node = DTapp (ls, dtl); dt_dty = dty; dt_loc = loc } in { dt with dt_node = DTlabel (dt, slab_coercion) } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } in
List.fold_left apply dt l List.fold_left apply dt l
(* coercions using just head tysymbols without type arguments: *) (* coercions using just head tysymbols without type arguments: *)
(* TODO: this can be improved *) (* TODO: this can be improved *)
let rec ts_of_dty = function let rec ts_of_dty = function
| Dvar { contents = Dval (Duty { ty_node = (Tyapp (ts, _)) })} -> | Dvar {contents = Dval dty} ->
ts ts_of_dty dty
| Dvar { contents = Dval dty } -> | Dvar {contents = Dind _}
ts_of_dty dty | Duty {ty_node = Tyvar _} ->
| Dvar { contents = Dind _ } -> raise Exit
let tv = create_tvsymbol (id_fresh "xi") in | Duty {ty_node = Tyapp (ts,_)}
raise (UndefinedTypeVar tv) | Dapp (ts,_) ->
| Dapp (ts, _) -> ts
ts
| Duty { ty_node = (Tyapp (ts, _)) } ->
ts
| Duty { ty_node = Tyvar tv } ->
raise (UndefinedTypeVar tv)
let ts_of_dty = function let ts_of_dty = function
| Some dt_dty -> ts_of_dty dt_dty | Some dt_dty -> ts_of_dty dt_dty
...@@ -332,8 +328,8 @@ let dterm_expected tuc dt dty = ...@@ -332,8 +328,8 @@ let dterm_expected tuc dt dty =
if (ts_equal ts1 ts2) then dt if (ts_equal ts1 ts2) then dt
else else
let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts2 in let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts2 in
apply_coercion ~loc:dt.dt_loc crc dt apply_coercion crc dt
with Not_found | UndefinedTypeVar _ -> dt with Not_found | Exit -> dt
let dterm_expected_dterm tuc dt dty = let dterm_expected_dterm tuc dt dty =
let dt = dterm_expected tuc dt (Some dty) in let dt = dterm_expected tuc dt (Some dty) in
...@@ -350,48 +346,51 @@ let dterm tuc ?loc node = ...@@ -350,48 +346,51 @@ let dterm tuc ?loc node =
let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
match node with match node with
| DTvar (_,dty) -> | DTvar (_,dty) ->
mk_dty (Some dty) mk_dty (Some dty)
| DTgvar vs -> | DTgvar vs ->
mk_dty (Some (dty_of_ty vs.vs_ty)) mk_dty (Some (dty_of_ty vs.vs_ty))
| DTconst (Number.ConstInt _) -> | DTconst (Number.ConstInt _) ->
mk_dty (Some dty_int) mk_dty (Some dty_int)
| DTconst (Number.ConstReal _) -> | DTconst (Number.ConstReal _) ->
mk_dty (Some dty_real) mk_dty (Some dty_real)
| DTapp (ls, dtl) when ls_equal ls ps_equ -> | DTapp (ls, dtl) when ls_equal ls ps_equ ->
let dtyl, dty = specialize_ls ls in let dtyl, dty = specialize_ls ls in
let dtl = dty_unify_app_map ls (dterm_expected_dterm tuc) (List.rev dtl) dtyl in let dtl = dty_unify_app_map ls
{ dt_node = DTapp (ls, List.rev dtl); (dterm_expected_dterm tuc) (List.rev dtl) dtyl in
dt_dty = dty; { dt_node = DTapp (ls, List.rev dtl);
dt_loc = loc } dt_dty = dty;
dt_loc = loc }
| DTapp (ls, dtl) -> | DTapp (ls, dtl) ->
let dtyl, dty = specialize_ls ls in let dtyl, dty = specialize_ls ls in
{ dt_node = DTapp (ls, dty_unify_app_map ls (dterm_expected_dterm tuc) dtl dtyl); { dt_node = DTapp (ls,
dt_dty = dty; dty_unify_app_map ls (dterm_expected_dterm tuc) dtl dtyl);
dt_loc = loc } dt_dty = dty;
dt_loc = loc }
| DTfapp ({dt_dty = Some res} as dt1,dt2) -> | DTfapp ({dt_dty = Some res} as dt1,dt2) ->
let rec not_arrow = function let rec not_arrow = function
| Dvar {contents = Dval dty} -> not_arrow dty | Dvar {contents = Dval dty} -> not_arrow dty
| Duty {ty_node = Tyapp (ts,_)} | Duty {ty_node = Tyapp (ts,_)}
| Dapp (ts,_) -> not (ts_equal ts Ty.ts_func) | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
| Dvar _ -> false | _ -> true in | Dvar _ -> false | _ -> true in
if not_arrow res then Loc.errorm ?loc:dt1.dt_loc if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
"This term has type %a,@ it cannot be applied" print_dty res; "This term has type %a,@ it cannot be applied" print_dty res;
let dtyl, dty = specialize_ls fs_func_app in let dtyl, dty = specialize_ls fs_func_app in
dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl; (* FIXME: why no conversion here? *)
mk_dty dty dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
mk_dty dty
| DTfapp ({dt_dty = None; dt_loc = loc},_) -> | 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) -> | DTif (df,dt1,dt2) ->
let df = dfmla_expected_dterm tuc df in let df = dfmla_expected_dterm tuc df in
dexpr_expected_type dt2 dt1.dt_dty; dexpr_expected_type dt2 dt1.dt_dty;
{ dt_node = DTif (df, dt1, dt2); { dt_node = DTif (df, dt1, dt2);
dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty; dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty;
dt_loc = loc } dt_loc = loc }
| DTlet (dt,_,df) -> | DTlet (dt,_,df) ->
ignore (dty_of_dterm dt); ignore (dty_of_dterm dt);
mk_dty df.dt_dty mk_dty df.dt_dty
| DTcase (_,[]) -> | DTcase (_,[]) ->
raise EmptyCase raise EmptyCase
| DTcase (dt,(dp1,df1)::bl) -> | DTcase (dt,(dp1,df1)::bl) ->
dterm_expected_type dt dp1.dp_dty; dterm_expected_type dt dp1.dp_dty;
let check (dp,df) = let check (dp,df) =
...@@ -401,15 +400,15 @@ let dterm tuc ?loc node = ...@@ -401,15 +400,15 @@ let dterm tuc ?loc node =
let is_fmla (_,df) = df.dt_dty = None in 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 if List.exists is_fmla bl then mk_dty None else mk_dty df1.dt_dty
| DTeps (_,dty,df) -> | DTeps (_,dty,df) ->
dfmla_expected_type df; dfmla_expected_type df;
mk_dty (Some dty) mk_dty (Some dty)
| DTquant (DTlambda,vl,_,df) -> | DTquant (DTlambda,vl,_,df) ->
let res = Opt.get_def dty_bool df.dt_dty in let res = Opt.get_def dty_bool df.dt_dty in
let app (_,l,_) r = Dapp (ts_func,[l;r]) in let app (_,l,_) r = Dapp (ts_func,[l;r]) in
mk_dty (Some (List.fold_right app vl res)) mk_dty (Some (List.fold_right app vl res))
| DTquant ((DTforall|DTexists),_,_,df) -> | DTquant ((DTforall|DTexists),_,_,df) ->
dfmla_expected_type df; dfmla_expected_type df;
mk_dty None mk_dty None
| DTbinop (_,df1,df2) -> | DTbinop (_,df1,df2) ->
dfmla_expected_type df1; dfmla_expected_type df1;
dfmla_expected_type df2; dfmla_expected_type df2;
...@@ -422,13 +421,13 @@ let dterm tuc ?loc node = ...@@ -422,13 +421,13 @@ let dterm tuc ?loc node =
always replace [true] by [True] and [false] by [False], so that always replace [true] by [True] and [false] by [False], so that
there is no need to count these constructs as "formulas" which there is no need to count these constructs as "formulas" which
require explicit if-then-else conversion to bool *) require explicit if-then-else conversion to bool *)
mk_dty (Some dty_bool) mk_dty (Some dty_bool)
| DTcast (dt,ty) -> | DTcast (dt,ty) ->
let dty = dty_of_ty ty in let dty = dty_of_ty ty in
dterm_expected_dterm tuc dt dty dterm_expected_dterm tuc dt dty
| DTuloc (dt,_) | DTuloc (dt,_)
| DTlabel (dt,_) -> | DTlabel (dt,_) ->
mk_dty (dt.dt_dty) mk_dty (dt.dt_dty)
in Loc.try1 ?loc (dterm_node loc) node in Loc.try1 ?loc (dterm_node loc) node
(** Final stage *) (** Final stage *)
......
...@@ -153,11 +153,11 @@ type theory = { ...@@ -153,11 +153,11 @@ type theory = {
th_name : ident; (* theory name *) th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *) th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *) th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *) th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *) th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *) th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *) th_used : Sid.t; (* used theories *)
th_crcmap : Coercion.t; (* coercions *)
} }
and tdecl = { and tdecl = {
...@@ -257,13 +257,13 @@ type theory_uc = { ...@@ -257,13 +257,13 @@ type theory_uc = {
uc_name : ident; uc_name : ident;
uc_path : string list; uc_path : string list;
uc_decls : tdecl list; uc_decls : tdecl list;
uc_crcmap : Coercion.t;
uc_prefix : string list; uc_prefix : string list;
uc_import : namespace list; uc_import : namespace list;
uc_export : namespace list; uc_export : namespace list;
uc_known : known_map; uc_known : known_map;
uc_local : Sid.t; uc_local : Sid.t;
uc_used : Sid.t; uc_used : Sid.t;
uc_crcmap : Coercion.t;
} }
exception CloseTheory exception CloseTheory
...@@ -273,13 +273,13 @@ let empty_theory n p = { ...@@ -273,13 +273,13 @@ let empty_theory n p = {
uc_name = id_register n; uc_name = id_register n;
uc_path = p; uc_path = p;
uc_decls = []; uc_decls = [];
uc_crcmap = Coercion.empty;
uc_prefix = []; uc_prefix = [];
uc_import = [empty_ns]; uc_import = [empty_ns];
uc_export = [empty_ns]; uc_export = [empty_ns];
uc_known = Mid.empty; uc_known = Mid.empty;
uc_local = Sid.empty; uc_local = Sid.empty;
uc_used = Sid.empty; uc_used = Sid.empty;
uc_crcmap = Coercion.empty;
} }
let close_theory uc = match uc.uc_export with let close_theory uc = match uc.uc_export with
...@@ -287,11 +287,11 @@ 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_name = uc.uc_name;
th_path = uc.uc_path; th_path = uc.uc_path;
th_decls = List.rev uc.uc_decls; th_decls = List.rev uc.uc_decls;
th_crcmap = uc.uc_crcmap;
th_export = e; th_export = e;
th_known = uc.uc_known; th_known = uc.uc_known;
th_local = uc.uc_local; th_local = uc.uc_local;
th_used = uc.uc_used; th_used = uc.uc_used }
th_crcmap = uc.uc_crcmap }
| _ -> raise CloseTheory | _ -> raise CloseTheory
let get_namespace uc = List.hd uc.uc_import let get_namespace uc = List.hd uc.uc_import
...@@ -350,8 +350,9 @@ let add_tdecl uc td = match td.td_node with ...@@ -350,8 +350,9 @@ let add_tdecl uc td = match td.td_node with
| Clone (_,sm) -> known_clone uc.uc_known sm; | Clone (_,sm) -> known_clone uc.uc_known sm;
{ uc with uc_decls = td :: uc.uc_decls } { uc with uc_decls = td :: uc.uc_decls }
| Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion -> | Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion ->
known_meta uc.uc_known al; known_meta uc.uc_known al;
{ uc with uc_crcmap = Coercion.add uc.uc_crcmap ls } (* 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; | Meta (_,al) -> known_meta uc.uc_known al;
{ uc with uc_decls = td :: uc.uc_decls } { uc with uc_decls = td :: uc.uc_decls }
......
...@@ -84,11 +84,11 @@ type theory = private { ...@@ -84,11 +84,11 @@ type theory = private {
th_name : ident; (* theory name *) th_name : ident; (* theory name *)
th_path : string list; (* environment qualifiers *) th_path : string list; (* environment qualifiers *)
th_decls : tdecl list; (* theory declarations *) th_decls : tdecl list; (* theory declarations *)
th_crcmap : Coercion.t; (* implicit coercions *)
th_export : namespace; (* exported namespace *) th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *) th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *) th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *) th_used : Sid.t; (* used theories *)
th_crcmap : Coercion.t (* coercions *)
} }
and tdecl = private { and tdecl = private {
...@@ -122,14 +122,13 @@ type theory_uc = private { ...@@ -122,14 +122,13 @@ type theory_uc = private {
uc_name : ident; uc_name : ident;
uc_path : string list; uc_path : string list;
uc_decls : tdecl list; uc_decls : tdecl list;
uc_crcmap : Coercion.t;
uc_prefix : string list; uc_prefix : string list;
uc_import : namespace list; uc_import : namespace list;
uc_export : namespace list; uc_export : namespace list;
uc_known : known_map; uc_known : known_map;
uc_local : Sid.t; uc_local : Sid.t;
uc_used : Sid.t; uc_used : Sid.t;
uc_crcmap : Coercion.t;
} }
val create_theory : ?path:string list -> preid -> theory_uc val create_theory : ?path:string list -> preid -> theory_uc
......
...@@ -822,7 +822,7 @@ let effect_of_dspec dsp = ...@@ -822,7 +822,7 @@ let effect_of_dspec dsp =
(* TODO: add warnings for empty postconditions (anywhere) (* TODO: add warnings for empty postconditions (anywhere)
and empty exceptional postconditions (toplevel). *) and empty exceptional postconditions (toplevel). *)
let check_spec inr dsp ecty ({e_loc = loc} as e) = 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) let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
weff.eff_writes eff.eff_writes) in weff.eff_writes eff.eff_writes) in
let bad_raise xeff eff = not (Sxs.subset xeff.eff_raises eff.eff_raises) in let bad_raise xeff eff = not (Sxs.subset xeff.eff_raises eff.eff_raises) 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