Commit b614cb92 authored by Andrei Paskevich's avatar Andrei Paskevich

clean up the interface of Denv and Typing

parent 32cdfb78
......@@ -674,8 +674,6 @@ let clone_export uc th inst =
let clone_theory add_td acc th inst =
clone_theory (cl_init th inst) add_td acc th inst
let create_clone = clone_theory (fun tdl td -> td :: tdl)
let create_null_clone th =
let sm = {
sm_ts = Mts.empty;
......
......@@ -170,8 +170,6 @@ val create_inst :
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
val create_clone : tdecl list -> theory -> th_inst -> tdecl list
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val create_null_clone : theory -> tdecl
......
......@@ -31,7 +31,6 @@ and type_var = {
type_var_loc : loc option;
}
let tyvar v = Tyvar v
let tyuvar tv = Tyuvar tv
let rec type_inst s ty = match ty.ty_node with
......@@ -49,11 +48,8 @@ let tyapp ts tyl = match ts.ts_def with
with Invalid_argument _ ->
Loc.errorm "this type expects %d parameters" (List.length ts.ts_args)
type dty = dty_view
let tvsymbol_of_type_var tv = tv.tvsymbol
let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
......@@ -67,16 +63,16 @@ let rec print_dty fmt = function
| Tyapp (s, l) ->
fprintf fmt "%s %a" s.ts_name.id_string (print_list space print_dty) l
let rec view_dty = function
| Tyvar { type_val = Some dty } -> view_dty dty
| dty -> dty
let create_ty_decl_var =
let t = ref 0 in
fun ?loc tv ->
incr t;
{ tag = !t; tvsymbol = tv; type_val = None; type_var_loc = loc }
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc tv)
let rec occurs v = function
| Tyvar { type_val = Some t } -> occurs v t
| Tyvar { tag = t; type_val = None } -> v.tag = t
......@@ -115,6 +111,10 @@ let rec ty_of_dty = function
| Tyapp (s, tl) ->
ty_app s (List.map ty_of_dty tl)
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar tv -> Tyuvar tv
| Ty.Tyapp (ts,tl) -> Tyapp (ts, List.map dty_of_ty tl)
type ident = Ptree.ident
type dpattern = { dp_node : dpattern_node; dp_ty : dty }
......
......@@ -16,29 +16,19 @@ open Theory
(** Destructive unification *)
type type_var
val find_type_var : loc:Ptree.loc -> type_var Htv.t -> tvsymbol -> type_var
val create_ty_decl_var : ?loc:Ptree.loc -> tvsymbol -> type_var
type dty
val tyvar : type_var -> dty
val tyuvar: tvsymbol -> dty
val tyapp : tysymbol -> dty list -> dty
type dty_view =
| Tyvar of type_var
| Tyuvar of tvsymbol
| Tyapp of tysymbol * dty list
val tyuvar : tvsymbol -> dty
val tyapp : tysymbol -> dty list -> dty
val view_dty : dty -> dty_view
val fresh_type_var : Ptree.loc -> dty
val unify : dty -> dty -> bool
val print_dty : Format.formatter -> dty -> unit
val ty_of_dty : dty -> ty
val dty_of_ty : ty -> dty
type ident = Ptree.ident
......@@ -91,10 +81,4 @@ val fmla : vsymbol Mstr.t -> dfmla -> term
(** Specialization *)
val specialize_ty : loc:Ptree.loc -> type_var Htv.t -> ty -> dty
val specialize_lsymbol : loc:Ptree.loc -> lsymbol -> dty list * dty option
(** exported for programs *)
val tvsymbol_of_type_var : type_var -> tvsymbol
......@@ -138,11 +138,6 @@ let rec string_list_of_qualid acc = function
| Qident id -> id.id :: acc
| Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p
let specialize_tysymbol loc p uc =
let sl = string_list_of_qualid [] p in
try ns_find_ts (get_namespace uc) sl
with Not_found -> error ~loc (UnboundType sl)
(* lazy declaration of tuples *)
let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
......@@ -152,18 +147,6 @@ let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
let rec dty uc = function
| PPTtyvar {id=x} ->
create_user_type_var x
| PPTtyapp (p, x) ->
let loc = qloc x in
let ts = specialize_tysymbol loc x uc in
let tyl = List.map (dty uc) p in
Loc.try2 loc tyapp ts tyl
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
tyapp ts (List.map (dty uc) tyl)
let find_ns get_id find p ns =
let loc = qloc p in
let sl = string_list_of_qualid [] p in
......@@ -202,6 +185,17 @@ let find_namespace_ns = find_ns get_dummy_id ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
*)
let rec dty uc = function
| PPTtyvar {id=x} ->
create_user_type_var x
| PPTtyapp (p, x) ->
let ts = find_tysymbol x uc in
let tyl = List.map (dty uc) p in
Loc.try2 (qloc x) tyapp ts tyl
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
tyapp ts (List.map (dty uc) tyl)
let specialize_lsymbol p uc =
let s = find_lsymbol p uc in
let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
......@@ -329,10 +323,6 @@ let check_pat_linearity p =
in
check p
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
tyvar (create_ty_decl_var ~loc tv)
let rec dpat uc env pat =
let env, n, ty = dpat_node pat.pat_loc uc env pat.pat_desc in
env, { dp_node = n; dp_ty = ty }
......@@ -442,9 +432,7 @@ and dterm_node ~localize loc uc env = function
Tvar x, ty
| PPvar x when env.gvars x <> None ->
let vs = Opt.get (env.gvars x) in
assert (ty_closed vs.vs_ty);
let ty = specialize_ty ~loc (Htv.create 0) vs.vs_ty in
Tgvar vs, ty
Tgvar vs, dty_of_ty vs.vs_ty
| PPvar x ->
(* 0-arity symbol (constant) *)
let s, tyl, ty = specialize_fsymbol x uc in
......@@ -1015,24 +1003,25 @@ let add_logics dl th =
let th = if defn = [] then th else add_logic_decl th defn in
th
let type_term uc denv env t =
let type_term uc gfn t =
let denv = denv_empty_with_globals gfn in
let t = dterm ~localize:(Some None) uc denv t in
term env t
term Mstr.empty t
let type_fmla uc denv env f =
let type_fmla uc gfn f =
let denv = denv_empty_with_globals gfn in
let f = dfmla ~localize:(Some None) uc denv f in
fmla env f
fmla Mstr.empty f
let add_prop k loc s f th =
let pr = create_prsymbol (create_user_id s) in
let f = type_fmla th denv_empty Mstr.empty f in
let f = type_fmla th (fun _ -> None) f in
Loc.try4 loc add_prop_decl th k pr f
let loc_of_id id = Opt.get id.Ident.id_loc
let add_inductives s dl th =
(* 1. create all symbols and make an environment with these symbols *)
let denv = denv_empty in
let psymbols = Hstr.create 17 in
let create_symbol th d =
let id = d.in_ident.id in
......@@ -1051,7 +1040,7 @@ let add_inductives s dl th =
let ps = Hstr.find psymbols id in
let clause (loc, id, f) =
Hstr.replace propsyms id.id loc;
let f = type_fmla th' denv Mstr.empty f in
let f = type_fmla th' (fun _ -> None) f in
create_prsymbol (create_user_id id), f
in
ps, List.map clause d.in_def
......
......@@ -27,8 +27,7 @@ val add_use_clone :
unit Env.library -> theory Mstr.t -> theory_uc ->
Loc.position -> Ptree.use_clone -> theory_uc
val close_namespace :
Loc.position -> bool -> theory_uc -> theory_uc
val close_namespace : Loc.position -> bool -> theory_uc -> theory_uc
val close_theory : theory Mstr.t -> theory_uc -> theory Mstr.t
......@@ -36,67 +35,23 @@ val open_file : unit Env.library -> Env.pathname -> Ptree.incremental
val close_file : unit -> theory Mstr.t
(******************************************************************************)
(** The following is exported for program typing (src/programs/pgm_typing.ml) *)
(******************************************************************************)
(***************************************************************************)
(** The following is exported for program typing (src/whyml/mlw_typing.ml) *)
(***************************************************************************)
val specialize_lsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty option
val create_user_tv : string -> tvsymbol
val specialize_fsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
val specialize_psymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list
val specialize_tysymbol :
Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol
val create_user_tv: string -> tvsymbol
val create_user_type_var : string -> Denv.dty
type denv
val denv_empty : denv
val denv_empty_with_globals : (Ptree.qualid -> vsymbol option) -> denv
val mem_var : string -> denv -> bool
val find_var : string -> denv -> Denv.dty
val add_var : string -> Denv.dty -> denv -> denv
val print_qualid : Format.formatter -> Ptree.qualid -> unit
val split_qualid : Ptree.qualid -> string list * string
val qloc : Ptree.qualid -> Loc.position
val type_term : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val type_fmla : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val find_ns :
('a -> Ident.ident) -> ('b -> string list -> 'a) -> Ptree.qualid -> 'b -> 'a
val dty : theory_uc -> Ptree.pty -> Denv.dty
val dterm : ?localize:(Ptree.loc option option) ->
theory_uc -> denv -> Ptree.lexpr -> Denv.dterm
val dfmla : ?localize:(Ptree.loc option option) ->
theory_uc -> denv -> Ptree.lexpr -> Denv.dfmla
val dpat : theory_uc -> denv -> Ptree.pattern -> denv * Denv.dpattern
val dpat_list :
theory_uc -> denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
val type_term :
theory_uc -> (Ptree.qualid -> vsymbol option) -> Ptree.lexpr -> term
val print_denv : Format.formatter -> denv -> unit
val print_qualid: Format.formatter -> Ptree.qualid -> unit
val type_fmla :
theory_uc -> (Ptree.qualid -> vsymbol option) -> Ptree.lexpr -> term
val split_qualid : Ptree.qualid -> string list * string
val string_list_of_qualid : string list -> Ptree.qualid -> string list
val qloc : Ptree.qualid -> Loc.position
val find_ns : ('a -> Ident.ident) ->
('b -> string list -> 'a) -> Ptree.qualid -> 'b -> 'a
val find_lsymbol : Ptree.qualid -> theory_uc -> lsymbol
(*
val is_projection : theory_uc -> lsymbol -> (tysymbol * lsymbol * int) option
(** [is_projection uc ls] returns
- [Some (ts, lsc, i)] if [ls] is the i-th projection of an
algebraic datatype [ts] with only one constructor [lcs]
- [None] otherwise *)
val list_fields: theory_uc ->
(Ptree.qualid * 'a) list -> tysymbol * lsymbol * (Ptree.loc * 'a) option list
(** check that the given fields all belong to the same record type
and do not appear several times *)
*)
val type_inst: theory_uc -> theory -> Ptree.clone_subst list -> th_inst
val type_inst : theory_uc -> theory -> Ptree.clone_subst list -> th_inst
......@@ -134,7 +134,7 @@ type number_support = {
let check_support support default do_it try_next v =
match support with
| Number_unsupported -> try_next v
| Number_default -> do_it (match default with Some d -> d | None -> assert false) v
| Number_default -> do_it (Opt.get default) v
| Number_custom f -> do_it f v
let force_support support do_it v =
......
......@@ -138,7 +138,8 @@ let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
(** Namespace lookup *)
let uc_find_ls uc p =
Typing.find_lsymbol p (get_theory uc)
let ns = Theory.get_namespace (get_theory uc) in
Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
let get_id_ts = function
| PT pt -> pt.its_pure.ts_name
......@@ -298,6 +299,12 @@ let find_global_vs uc p = try match uc_find_ps uc p with
| _ -> None
with _ -> None
let find_vs uc lvm p = match p with
| Qdot _ -> find_global_vs uc p
| Qident id ->
let ovs = Mstr.find_opt id.id lvm in
if ovs = None then find_global_vs uc p else ovs
let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
| Ptree.PPpwild ->
PPwild, create_type_variable (), denv
......@@ -666,7 +673,6 @@ type lenv = {
th_old : Theory.theory_uc;
let_vars : let_sym Mstr.t;
log_vars : vsymbol Mstr.t;
log_denv : Typing.denv;
}
let create_lenv uc = {
......@@ -675,7 +681,6 @@ let create_lenv uc = {
th_old = Theory.use_export (get_theory uc) Mlw_wp.th_mark_old;
let_vars = Mstr.empty;
log_vars = Mstr.empty;
log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
}
(* invariant handling *)
......@@ -770,13 +775,13 @@ let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar v -> Denv.tyuvar v
let create_variant lenv (t,r) =
let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
let t = Typing.type_term lenv.th_at (find_vs lenv.mod_uc lenv.log_vars) t in
count_term_tuples t;
check_at t;
t, r
let create_assert lenv f =
let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
let f = Typing.type_fmla lenv.th_at (find_vs lenv.mod_uc lenv.log_vars) f in
let f = t_label_add Split_goal.stop_split f in
count_term_tuples f;
check_at f;
......@@ -784,18 +789,17 @@ let create_assert lenv f =
let create_pre lenv fs = t_and_simp_l (List.map (create_assert lenv) fs)
let create_post lenv res dty pat f =
let log_vars, log_denv = match pat.pat_desc with
let create_post lenv res pat f =
let log_vars = match pat.pat_desc with
| Ptree.PPpvar { id = x } ->
Mstr.add x res lenv.log_vars,
Typing.add_var x dty lenv.log_denv
Mstr.add x res lenv.log_vars
| Ptree.PPptuple [] ->
Loc.try2 pat.pat_loc Ty.ty_equal_check res.vs_ty ty_unit;
lenv.log_vars, lenv.log_denv
lenv.log_vars
| Ptree.PPpwild ->
lenv.log_vars, lenv.log_denv
lenv.log_vars
| _ -> assert false in
let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
let f = Typing.type_fmla lenv.th_old (find_vs lenv.mod_uc log_vars) f in
let f = t_label_add Split_goal.stop_split f in
let f = remove_old f in
count_term_tuples f;
......@@ -803,14 +807,13 @@ let create_post lenv res dty pat f =
f
let create_post lenv ty fs =
let dty = dty_of_ty ty in
let rec get_name = function
| ({ pat_desc = Ptree.PPpvar { id = "(null)" }},_)::l -> get_name l
| ({ pat_desc = Ptree.PPpvar { id = x }},_)::_ -> x
| _::l -> get_name l
| [] -> "result" in
let res = create_vsymbol (id_fresh (get_name fs)) ty in
let post (pat,f) = create_post lenv res dty pat f in
let post (pat,f) = create_post lenv res pat f in
let f = t_and_simp_l (List.map post fs) in
Mlw_ty.create_post res f
......@@ -824,11 +827,9 @@ let add_local x lv lenv = match lv with
| LetA _ ->
{ lenv with let_vars = Mstr.add x lv lenv.let_vars }
| LetV pv ->
let dty = dty_of_ty pv.pv_vs.vs_ty in
{ lenv with
let_vars = Mstr.add x lv lenv.let_vars;
log_vars = Mstr.add x pv.pv_vs lenv.log_vars;
log_denv = Typing.add_var x dty lenv.log_denv }
log_vars = Mstr.add x pv.pv_vs lenv.log_vars }
let binders bl =
let binder (id, ghost, dity) =
......@@ -1276,10 +1277,11 @@ let add_type_invariant loc uc id params inv =
let _, tvl = Lists.map_fold_left add_tv Sstr.empty params in
let ty = ty_app its.its_pure (List.map ty_var tvl) in
let res = create_vsymbol (id_fresh x) ty in
let vars = Mstr.singleton x res in
let denv = Typing.add_var x (dty_of_ty ty) Typing.denv_empty in
let find = function
| Qident { id = id } when id = x -> Some res
| _ -> None in
let mk_inv f =
let f = Typing.type_fmla (get_theory uc) denv vars f in
let f = Typing.type_fmla (get_theory uc) find f in
t_label_add Split_goal.stop_split f in
let inv = List.map mk_inv inv in
let q = Mlw_ty.create_post res (t_and_simp_l inv) 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