Commit 454aaf47 authored by François Bobot's avatar François Bobot

guard : use select for reducing the quantifier on variable

parent 15eb1b44
......@@ -101,7 +101,7 @@ module Transform = struct
let vars,expr = open_ls_defn ldef in
let add v (vl,vm) =
let vs = Term.create_vsymbol (id_fresh "t") ty_type in
vs :: vl, Mtv.add v vs vm
vs :: vl, Mtv.add v (t_var vs) vm
in
let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
(match expr with
......
......@@ -65,12 +65,36 @@ module Transform = struct
List.fold_left2 ty_match2 s l1 l2
| _ -> assert false
(** type_of *)
let fs_type =
let alpha = ty_var (create_tvsymbol (id_fresh "a")) in
create_fsymbol (id_fresh "type_of") [alpha] ty_type
let app_type t = t_app fs_type [t] ty_type
(** rewrite a closed formula modulo its free typevars
using selection functions *)
let rec extract_tvar acc t ty = match ty.ty_node with
| Tyvar tvar when Mtv.mem tvar acc -> acc
| Tyvar tvar -> Mtv.add tvar t acc
| Tyapp (ts,tyl) ->
let fold acc ls_select ty =
extract_tvar acc (t_app ls_select [t] ty_type) ty in
List.fold_left2 fold acc (ls_selects_of_ts ts) tyl
let type_close_select tvs ts fn f =
let fold acc t = extract_tvar acc (app_type t) t.t_ty in
let tvm = List.fold_left fold Mtv.empty ts in
let tvs = Mtv.diff (const3 None) tvs tvm in
let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
let tvm' = Mtv.mapi (fun v () -> get_vs v) tvs in
let vl = Mtv.values tvm' in
let tvm' = Mtv.map t_var tvm' in
let tvm = Mtv.union (fun _ _ _ -> assert false) tvm tvm' in
f_forall_close_simp vl [] (fn tvm f)
let type_variable_only_in_value lsymbol =
let tvar_val = ty_freevars Stv.empty (of_option lsymbol.ls_value) in
let tvar_arg = List.fold_left ty_freevars Stv.empty lsymbol.ls_args in
......@@ -108,19 +132,25 @@ module Transform = struct
f_app (findL p) terms
| Fquant(q,b) ->
let vsl,trl,fmla,cb = f_open_quant_cb b in
let fmla = fmla_transform kept varM fmla in
let fmla2 = guard q kept varM fmla vsl in
(* TODO : how to modify the triggers? *)
let guard fmla vs =
if Sty.mem vs.vs_ty kept then fmla else
let g = f_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
f_implies g fmla in
let fmla2 = List.fold_left guard (fmla_transform kept varM fmla) vsl in
let trl = tr_map (term_transform kept varM)
(fmla_transform kept varM) trl in
f_quant q (cb vsl trl fmla2)
| _ -> (* otherwise : just traverse and translate *)
f_map (term_transform kept varM) (fmla_transform kept varM) f(* in *)
f_map (term_transform kept varM) (fmla_transform kept varM) f(* in *)
(* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)
and guard q kept varM fmla vsl =
let aux fmla vs =
if Sty.mem vs.vs_ty kept then fmla else
let g = f_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
match q with
| Fforall -> f_implies g fmla
| Fexists -> f_and g fmla in
List.fold_left aux fmla vsl
and args_transform kept varM lsymbol args ty =
(* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
let tv_to_ty = ty_match2 Mtv.empty (of_option lsymbol.ls_value) ty in
......@@ -132,6 +162,27 @@ module Transform = struct
let add _ ty acc = term_of_ty varM ty :: acc in
Mtv.fold add tv_to_ty args
and f_type_close_select kept f' =
let tvs = f_ty_freevars Stv.empty f' in
let rec trans fn acc f = match f.f_node with
| Fquant(Fforall as q,b) -> (* Exists same thing? *)
let vsl,trl,fmla,cb = f_open_quant_cb b in
let add acc vs = (t_var vs)::acc in
let acc = List.fold_left add acc vsl in
let fn varM f =
let fmla2 = guard q kept varM f vsl in
(* TODO : how to modify the triggers? *)
let trl = tr_map (term_transform kept varM)
(fmla_transform kept varM) trl in
fn varM (f_quant q (cb vsl trl fmla2))
in
let fn varM f = fn varM (fmla_transform kept varM f) in
type_close_select tvs acc fn fmla
| _ ->
let fn varM f = fn varM (fmla_transform kept varM f) in
type_close_select tvs acc fn f in
trans (fun _ f -> f) [] f'
let logic_guard kept acc lsymbol =
match lsymbol.ls_value with
| None -> acc
......@@ -139,7 +190,6 @@ module Transform = struct
| Some ty_val ->
let varl = List.map (fun v -> create_vsymbol (id_fresh "x") v)
lsymbol.ls_args in
let stv = ls_ty_freevars lsymbol in
let trans varM () =
let terms = List.map t_var varl in
let terms = args_transform kept varM lsymbol terms ty_val in
......@@ -153,7 +203,9 @@ module Transform = struct
let fmla = List.fold_left guard fmla varl in
f_forall_close_simp varl [] fmla
in
let fmla = Libencoding.type_close stv trans () in
let stv = ls_ty_freevars lsymbol in
let tl = List.rev_map (t_var) varl in
let fmla = type_close_select stv tl trans () in
Decl.create_prop_decl Paxiom
(create_prsymbol (id_clone lsymbol.ls_name)) fmla::acc
......@@ -169,7 +221,7 @@ module Transform = struct
let vars,expr = open_ls_defn ldef in
let add v (vl,vm) =
let vs = Term.create_vsymbol (id_fresh "t") ty_type in
vs :: vl, Mtv.add v vs vm
vs :: vl, Mtv.add v (t_var vs) vm
in
let vars,varM =
match lsymbol.ls_value with
......@@ -193,13 +245,13 @@ module Transform = struct
(** transform an inductive declaration *)
let ind_transform kept idl =
let iconv (pr,f) = pr, Libencoding.f_type_close (fmla_transform kept) f in
let iconv (pr,f) = pr, f_type_close_select kept f in
let conv (ls,il) = findL ls, List.map iconv il in
[Decl.create_ind_decl (List.map conv idl)]
(** transforms a proposition into another (mostly a substitution) *)
let prop_transform kept (prop_kind, prop_name, f) =
let quantified_fmla = Libencoding.f_type_close (fmla_transform kept) f in
let quantified_fmla = f_type_close_select kept f in
[Decl.create_prop_decl prop_kind prop_name quantified_fmla]
end
......@@ -207,7 +259,7 @@ end
(** {2 main part} *)
let decl kept d = match d.d_node with
| Dtype tdl -> d :: Libencoding.lsdecl_of_tydecl tdl
| Dtype tdl -> d :: Libencoding.lsdecl_of_tydecl_select tdl
| Dlogic ldl -> Transform.logic_transform kept ldl
| Dind idl -> Transform.ind_transform kept idl
| Dprop prop -> Transform.prop_transform kept prop
......
......@@ -37,18 +37,51 @@ let ls_of_ts = Wts.memoize 63 (fun ts ->
let args = List.map (const ty_type) ts.ts_args in
create_fsymbol (id_clone ts.ts_name) args ty_type)
(* function symbol selecting ty_type from ty_type^n *)
let ls_selects_of_ts = Wts.memoize 63 (fun ts ->
let create_select _ =
let preid = id_fresh ("select_"^ts.ts_name.id_string) in
create_fsymbol preid [ty_type] ty_type in
List.rev_map create_select ts.ts_args)
(** definition of the previous selecting functions *)
let ls_selects_def_of_ts acc ts =
let ls = ls_of_ts ts in
let ls_selects = ls_selects_of_ts ts in
let vars = List.rev_map
(fun _ -> create_vsymbol (id_fresh "x") ty_type) ls_selects
in
let tvars = List.map t_var vars in
let fmlas = List.rev_map2
(fun ls_select value ->
let t = t_app ls tvars ty_type in
let f = f_equ (t_app ls_select [t] ty_type) value in
let f = f_forall_close vars [] f in
f)
ls_selects tvars in
let create_props ls_select fmla =
let prsymbol = create_prsymbol (id_clone ls_select.ls_name) in
create_prop_decl Paxiom prsymbol fmla in
let props =
List.fold_left2 (fun acc x y -> create_props x y::acc)
acc ls_selects fmlas in
let add acc fs = create_logic_decl [fs,None] :: acc in
List.fold_left add props ls_selects
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
| Tyvar tv ->
t_var (Mtv.find tv tvmap)
Mtv.find tv tvmap
| Tyapp (ts,tl) ->
t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
(* rewrite a closed formula modulo its free typevars *)
let type_close tvs fn f =
let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
let tvm = Stv.fold (fun v m -> Mtv.add v (get_vs v) m) tvs Mtv.empty in
let vl = Mtv.fold (fun _ vs acc -> vs::acc) tvm [] in
let tvm = Mtv.mapi (fun v () -> get_vs v) tvs in
let vl = Mtv.values tvm in
let tvm = Mtv.map t_var tvm in
f_forall_close_simp vl [] (fn tvm f)
let f_type_close fn f =
......@@ -56,15 +89,28 @@ let f_type_close fn f =
type_close tvs fn f
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl tdl =
let add td acc = match td with
let lsdecl_of_tydecl acc td = match td with
| ts, Talgebraic _ ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
Printer.unsupportedType ty "no algebraic types at this point"
| { ts_def = Some _ }, _ -> acc
| ts, _ -> create_logic_decl [ls_of_ts ts, None] :: acc
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl_select tdl =
let add acc td = match td with
| ts, Talgebraic _ ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
Printer.unsupportedType ty "no algebraic types at this point"
| { ts_def = Some _ }, _ -> acc
| ts, _ -> ls_selects_def_of_ts acc ts
in
List.fold_right add tdl []
let defs = List.fold_left add [] tdl in
List.fold_left lsdecl_of_tydecl defs tdl
let lsdecl_of_tydecl tdl = List.fold_left lsdecl_of_tydecl [] tdl
(* convert a constant to a functional symbol of type ty_base *)
let ls_of_const ty_base =
......
......@@ -33,18 +33,24 @@ val d_ts_type : decl
(* function symbol mapping ty_type^n to ty_type *)
val ls_of_ts : tysymbol -> lsymbol
(* function symbol selecting ty_type from ty_type^n *)
val ls_selects_of_ts : tysymbol -> lsymbol list
(* convert a type to a term of type ty_type *)
val term_of_ty : vsymbol Mtv.t -> ty -> term
val term_of_ty : term Mtv.t -> ty -> term
(* rewrite a closed formula modulo the given free typevars *)
val type_close : Stv.t -> (vsymbol Mtv.t -> 'a -> fmla) -> 'a -> fmla
val type_close : Stv.t -> (term Mtv.t -> 'a -> fmla) -> 'a -> fmla
(* rewrite a closed formula modulo its free typevars *)
val f_type_close : (vsymbol Mtv.t -> fmla -> fmla) -> fmla -> fmla
val f_type_close : (term Mtv.t -> fmla -> fmla) -> fmla -> fmla
(* convert a type declaration to a list of lsymbol declarations *)
val lsdecl_of_tydecl : ty_decl list -> decl list
(* convert a type declaration to a list of lsymbol declarations *)
val lsdecl_of_tydecl_select : ty_decl list -> decl list
(* monomorphise wrt the base type, the set of kept types, and a symbol map *)
val d_monomorph : ty -> Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
......
......@@ -67,6 +67,8 @@ module type S =
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
val add_new : key -> 'a -> exn -> 'a t -> 'a t
val keys: 'a t -> key list
val values: 'a t -> 'a list
module type Set =
sig
......@@ -377,6 +379,13 @@ module Make(Ord: OrderedType) = struct
let bindings s =
bindings_aux [] s
let rec values_aux accu = function
Empty -> accu
| Node(l, _, v, r, _) -> values_aux (v :: values_aux accu r) l
let values s =
values_aux [] s
let choose = min_binding
(** Added into why stdlib version *)
......
......@@ -240,6 +240,18 @@ module type S =
(** [add_new x v e m] binds [x] to [v] in [m] if [x] is not bound,
and raises [exn] otherwise. *)
val keys: 'a t -> key list
(** Return the list of all keys of the given map.
The returned list is sorted in increasing order with respect
to the ordering [Ord.compare], where [Ord] is the argument
given to {!Map.Make}. *)
val values: 'a t -> 'a list
(** Return the list of all values of the given map.
The returned list is sorted in increasing order with respect
to the ordering [Ord.compare] of the keys, where [Ord] is the argument
given to {!Map.Make}. *)
module type Set =
sig
type elt = key
......
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