Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit b926f9f0 authored by François Bobot's avatar François Bobot
Browse files

encoding : guard encoding

Currently all the variables that appear in the return value
are used as supplementarry argument.
parent 7f8a73c9
......@@ -128,7 +128,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
eliminate_inductive eliminate_let eliminate_if \
encoding_enumeration encoding encoding_decorate_mono \
libencoding encoding_decorate encoding_bridge \
encoding_explicit encoding_sort \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
encoding_arrays \
introduction abstraction close_epsilon lift_epsilon
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)
open Util
open Ident
open Ty
open Term
open Decl
open Task
open Libencoding
(** module with printing functions *)
module Debug = struct
let print_mtv vprinter fmter m =
Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
Pretty.print_tv key vprinter value) m
(** utility to print a list of items *)
let rec print_list printer fmter = function
| [] -> Format.fprintf fmter ""
| e::es -> if es = []
then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
else Format.fprintf fmter "@[%a@], %a" printer e
(print_list printer) es
let debug x = Format.eprintf "%s@." x
end
(** {2 module to separate utilities from important functions} *)
module Transform = struct
(* really return the map that replace all the variable of ty1,
If the same variable appear in ty1 and ty2 Ty.ty_match doesn't
bind this variable
*)
let rec ty_match2 s ty1 ty2 =
match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ ->
Mtv.change n1 (function
| None -> Some ty2
| Some ty1 as r when ty_equal ty1 ty2 -> r
| _ -> assert false) s
| Tyapp (f1, l1), Tyapp (f2, l2) when ts_equal f1 f2 ->
List.fold_left2 ty_match2 s l1 l2
| _ -> assert false
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
(** creates a new logic symbol, with a different type if the
given symbol was polymorphic *)
let findL = Wls.memoize 63 (fun lsymbol ->
if ls_equal lsymbol ps_equ || lsymbol.ls_value = None then lsymbol else
let new_ty = ty_freevars Stv.empty (of_option lsymbol.ls_value) in
(* as many t as type vars *)
if Stv.is_empty new_ty then lsymbol (* same type *) else
let add _ acc = ty_type :: acc in
let args = Stv.fold add new_ty lsymbol.ls_args in
(* creates a new lsymbol with the same name but a different type *)
Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
(** {1 transformations} *)
(** translation of terms *)
let rec term_transform kept varM t =
match t.t_node with
| Tapp(f, terms) ->
let terms = args_transform kept varM (of_option f.ls_value)
terms t.t_ty in
t_app (findL f) terms t.t_ty
| _ -> (* default case : traverse *)
t_map (term_transform kept varM) (fmla_transform kept varM) t
(** translation of formulae *)
and fmla_transform kept varM f =
match f.f_node with
(* first case : predicate are not translated *)
| Fapp(p,terms) ->
let terms = List.map (term_transform kept varM) terms in
f_app (findL p) terms
| Fquant(q,b) ->
let vsl,trl,fmla,cb = f_open_quant_cb b 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 *)
(* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)
and args_transform kept varM fs_value args ty =
(* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
let tv_to_ty = ty_match2 Mtv.empty fs_value ty in
(* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
let args = List.map (term_transform kept varM) args in
(* fresh args to be added at the beginning of the list of arguments *)
let add _ ty acc = term_of_ty varM ty :: acc in
Mtv.fold add tv_to_ty args
let logic_guard kept acc lsymbol =
match lsymbol.ls_value with
| None -> acc
| Some ty_val when Sty.mem ty_val kept -> acc
| 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 ty_val terms ty_val in
let fmla =
f_equ (app_type (t_app (findL lsymbol) terms ty_val))
(term_of_ty varM ty_val) in
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 fmla = List.fold_left guard fmla varl in
f_forall_close_simp varl [] fmla
in
let fmla = Libencoding.type_close stv trans () in
Decl.create_prop_decl Paxiom
(create_prsymbol (id_clone lsymbol.ls_name)) fmla::acc
(** transforms a list of logic declarations into another.
Declares new lsymbols with explicit polymorphic signatures,
with guards only the type that appear in the return value type.
*)
let logic_transform kept decls =
(* if there is a definition, we must take it into account *)
let helper = function
| (lsymbol, Some ldef) ->
let new_lsymbol = findL lsymbol in (* new lsymbol *)
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
in
let vars,varM =
match lsymbol.ls_value with
| None -> vars,Mtv.empty
| Some ty_value ->
let new_ty = ty_freevars Stv.empty ty_value in
Stv.fold add new_ty (vars,Mtv.empty) in
(match expr with
| Term t ->
let t = term_transform kept varM t in
Decl.make_fs_defn new_lsymbol vars t
| Fmla f ->
let f = fmla_transform kept varM f in
Decl.make_ps_defn new_lsymbol vars f)
| (lsymbol, None) ->
(findL lsymbol, None)
in
let l = List.fold_left
(fun acc (lsymbol,_) -> logic_guard kept acc lsymbol) [] decls in
(Decl.create_logic_decl (List.map helper decls))::l
(** transform an inductive declaration *)
let ind_transform kept idl =
let iconv (pr,f) = pr, Libencoding.f_type_close (fmla_transform 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
[Decl.create_prop_decl prop_kind prop_name quantified_fmla]
end
(** {2 main part} *)
let decl kept d = match d.d_node with
| Dtype tdl -> d :: Libencoding.lsdecl_of_tydecl tdl
| Dlogic ldl -> Transform.logic_transform kept ldl
| Dind idl -> Transform.ind_transform kept idl
| Dprop prop -> Transform.prop_transform kept prop
let empty_th =
let task = use_export None Theory.builtin_theory in
let task = Task.add_decl task d_ts_type in
let task = Task.add_logic_decl task [Transform.fs_type,None] in
task
let guard =
Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
Trans.decl (decl kept) empty_th)
(** {2 monomorphise task } *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
let ty_base = ty_app ts_base []
let lsmap tyb kept = Wls.memoize 63 (fun ls ->
let tymap ty = if Sty.mem ty kept then ty else tyb in
let ty_res = Util.option_map tymap ls.ls_value in
let ty_arg = List.map tymap ls.ls_args in
if Util.option_eq ty_equal ty_res ls.ls_value &&
List.for_all2 ty_equal ty_arg ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)
let d_ts_base = create_ty_decl [ts_base, Tabstract]
let monomorph tyb = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
let kept = Sty.add ty_type kept in
let tyb = match tyb.ty_node with
| Tyapp (_,[]) when not (Sty.mem tyb kept) -> tyb
| _ -> ty_base
in
let decl = Libencoding.d_monomorph tyb kept (lsmap tyb kept) in
Trans.decl decl (Task.add_decl None d_ts_base))
let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
let tyb = match alo with
| Some [Theory.MAts ts] when ts.ts_args = [] ->
begin match ts.ts_def with
| Some ty -> ty
| None -> ty_app ts []
end
| _ -> ty_base
in
monomorph tyb)
let () = Encoding.register_enco_poly "guard"
(fun _ -> Trans.compose guard monomorph)
......@@ -50,13 +50,16 @@ let rec term_of_ty tvmap ty = match ty.ty_node with
t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
(* rewrite a closed formula modulo its free typevars *)
let f_type_close fn f =
let tvs = f_ty_freevars Stv.empty f in
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
f_forall_close_simp vl [] (fn tvm f)
let f_type_close fn f =
let tvs = f_ty_freevars Stv.empty f in
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
......@@ -106,8 +109,8 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
let ls = ls_of_const ty_base t in
consts := Sls.add ls !consts;
t_app ls [] ty_base
| Tapp (fs,_) when is_ls_of_ts fs ->
t
(* | Tapp (fs,_) when is_ls_of_ts fs -> *)
(* t *)
| Tapp (fs,tl) ->
let fs = lsmap fs in
let ty = of_option fs.ls_value in
......@@ -176,7 +179,7 @@ let d_monomorph ty_base kept lsmap d =
| Dlogic ldl ->
let conv (ls,ld) =
let ls =
if ls_equal ls ps_equ || is_ls_of_ts ls then ls else lsmap ls
if ls_equal ls ps_equ (* || is_ls_of_ts ls *) then ls else lsmap ls
in
match ld with
| Some ld ->
......
......@@ -39,6 +39,9 @@ val is_ls_of_ts : lsymbol -> bool
(* convert a type to a term of type ty_type *)
val term_of_ty : vsymbol 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
(* rewrite a closed formula modulo its free typevars *)
val f_type_close : (vsymbol Mtv.t -> fmla -> fmla) -> fmla -> fmla
......
......@@ -47,7 +47,14 @@ theory Test_simplify_array2
type t2 'a
goal G1 : forall y:int. forall x:t2 int. forall m: t int (t2 int).
get (set m y x) y = x
end
theory Test_guard
type t
logic f t : t
logic a : t
logic b : t
goal G : forall x:t. f a = x
end
theory Test_conjunction
......
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