From a22db1eca888a88d451bdae28e04c28ffd72fcf6 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Thu, 16 Feb 2017 15:33:35 +0100 Subject: [PATCH] small cleanups --- .gitignore | 5 +- src/core/dterm.ml | 127 ++++++++++++++++++++++---------------------- src/core/theory.ml | 15 +++--- src/core/theory.mli | 5 +- src/mlw/dexpr.ml | 2 +- 5 files changed, 76 insertions(+), 78 deletions(-) diff --git a/.gitignore b/.gitignore index a2e96969e..e37bbbd66 100644 --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/src/core/dterm.ml b/src/core/dterm.ml index 59dc51bf7..1f34a9079 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -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 *) diff --git a/src/core/theory.ml b/src/core/theory.ml index 3af56eac6..5d5c30f70 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -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 } diff --git a/src/core/theory.mli b/src/core/theory.mli index 018f67a5e..5487c0312 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -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 diff --git a/src/mlw/dexpr.ml b/src/mlw/dexpr.ml index 07fe65093..dcf9b723a 100644 --- a/src/mlw/dexpr.ml +++ b/src/mlw/dexpr.ml @@ -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 -- GitLab