Commit beaf1bbe authored by Andrei Paskevich's avatar Andrei Paskevich

add Libencoding to factorize some common code

parent 3cab5a04
...@@ -108,7 +108,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \ ...@@ -108,7 +108,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf whyconf
LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction \ split_conjunction libencoding \
eliminate_definition eliminate_algebraic \ eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \ eliminate_inductive eliminate_let eliminate_if \
encoding_enumeration encoding encoding_decorate_mono \ encoding_enumeration encoding encoding_decorate_mono \
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
open Util
open Ident
open Ty
open Term
open Decl
(* sort symbol of (polymorphic) types *)
let ts_type = create_tysymbol (id_fresh "ty") [] None
(* sort of (polymorphic) types *)
let ty_type = ty_app ts_type []
(* ts_type declaration *)
let d_ts_type = create_ty_decl [ts_type, Tabstract]
(* function symbol mapping ty_type^n to ty_type *)
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)
(* test whether a function symbol has ty_type as ls_value *)
let is_ls_of_ts ls = match ls.ls_value with
| Some { ty_node = Tyapp (ts,_) } when ts_equal ts ts_type -> true
| _ -> false
(* 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)
| Tyapp (ts,tl) ->
t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl tdl =
let add td acc = 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
in
List.fold_right add tdl []
(* sort symbol by default (= undeco) *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
(* sort by default (= undeco) *)
let ty_base = ty_app ts_base []
(* ts_base declaration *)
let d_ts_base = create_ty_decl [ts_base, Tabstract]
(* convert a constant to a functional symbol of type ty_base *)
let ls_of_const =
let ht = Hterm.create 63 in
let ls_of_t t = match t.t_node with
| Tconst _ ->
begin try Hterm.find ht t with Not_found ->
let s = Pp.string_of Pretty.print_term t in
create_fsymbol (id_fresh ("const_" ^ s)) [] ty_base
end
| _ -> assert false
in
fun c -> ls_of_t (t_const c)
(* convert a constant to a term of type ty_base *)
let term_of_const c = t_app (ls_of_const c) [] ty_base
(* convert a set of preserved tysymbols to a set of types *)
let tyset_of_tsset kept =
let add ts acc = match ts.ts_def with
| Some ty -> Sty.add ty acc
| None -> Sty.add (ty_app ts []) acc
in
Sts.fold add kept Sty.empty
(* monomorphise modulo the set of kept types * and an lsymbol map *)
let vs_monomorph kept vs =
if ty_equal vs.vs_ty ty_type || Sty.mem vs.vs_ty kept
then vs else create_vsymbol (id_clone vs.vs_name) ty_base
let rec t_monomorph kept lsmap consts vmap t =
let t_mono = t_monomorph kept lsmap consts in
let f_mono = f_monomorph kept lsmap consts in
t_label_copy t (match t.t_node with
| Tbvar _ ->
assert false
| Tvar v ->
Mvs.find v vmap
| Tconst c ->
let ls = ls_of_const c in
consts := Sls.add ls !consts;
t_app ls [] ty_base
| 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
t_app fs (List.map (t_mono vmap) tl) ty
| Tif (f,t1,t2) ->
t_if (f_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
| Tlet (t1,b) ->
let u,t2,close = t_open_bound_cb b in
let v = vs_monomorph kept u in
let t2 = t_mono (Mvs.add u (t_var v) vmap) t2 in
t_let (t_mono vmap t1) (close v t2)
| Tcase _ ->
Printer.unsupportedTerm t "no match expressions at this point"
| Teps b ->
let u,f,close = f_open_bound_cb b in
let v = vs_monomorph kept u in
let f = f_mono (Mvs.add u (t_var v) vmap) f in
t_eps (close v f))
and f_monomorph kept lsmap consts vmap f =
let t_mono = t_monomorph kept lsmap consts in
let f_mono = f_monomorph kept lsmap consts in
f_label_copy f (match f.f_node with
| Fapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
f_equ (t_mono vmap t1) (t_mono vmap t2)
| Fapp (ps,tl) ->
f_app (lsmap ps) (List.map (t_mono vmap) tl)
| Fquant (q,b) ->
let ul,tl,f1,close = f_open_quant_cb b in
let vl = List.map (vs_monomorph kept) ul in
let add acc u v = Mvs.add u (t_var v) acc in
let vmap = List.fold_left2 add vmap ul vl in
let tl = tr_map (t_mono vmap) (f_mono vmap) tl in
f_quant q (close vl tl (f_mono vmap f1))
| Fbinop (op,f1,f2) ->
f_binary op (f_mono vmap f1) (f_mono vmap f2)
| Fnot f1 ->
f_not (f_mono vmap f1)
| Ftrue | Ffalse ->
f
| Fif (f1,f2,f3) ->
f_if (f_mono vmap f1) (f_mono vmap f2) (f_mono vmap f3)
| Flet (t,b) ->
let u,f1,close = f_open_bound_cb b in
let v = vs_monomorph kept u in
let f1 = f_mono (Mvs.add u (t_var v) vmap) f1 in
f_let (t_mono vmap t) (close v f1)
| Fcase _ ->
Printer.unsupportedFmla f "no match expressions at this point")
let d_monomorph kept lsmap d =
let consts = ref Sls.empty in
let dl = match d.d_node with
| Dtype tdl ->
let add td acc = match td with
| _, Talgebraic _ ->
Printer.unsupportedDecl d "no algebraic types at this point"
| { ts_def = Some _ }, _ -> acc
| ts, _ when Sty.exists (ty_s_any (ts_equal ts)) kept -> acc
| _ -> create_ty_decl [td] :: acc
in
List.fold_right add tdl []
| Dlogic ldl ->
let conv (ls,ld) =
let ls =
if ls_equal ls ps_equ || is_ls_of_ts ls then ls else lsmap ls
in
match ld with
| Some ld ->
let ul,e = open_ls_defn ld in
let vl = List.map (vs_monomorph kept) ul in
let add acc u v = Mvs.add u (t_var v) acc in
let vmap = List.fold_left2 add Mvs.empty ul vl in
let e = match e with
| Term t -> Term (t_monomorph kept lsmap consts vmap t)
| Fmla f -> Fmla (f_monomorph kept lsmap consts vmap f)
in
make_ls_defn ls vl e
| None ->
ls, None
in
[create_logic_decl (List.map conv ldl)]
| Dind idl ->
let iconv (pr,f) = pr, f_monomorph kept lsmap consts Mvs.empty f in
let conv (ls,il) = lsmap ls, List.map iconv il in
[create_ind_decl (List.map conv idl)]
| Dprop (k,pr,f) ->
[create_prop_decl k pr (f_monomorph kept lsmap consts Mvs.empty f)]
in
let add ls acc = create_logic_decl [ls,None] :: acc in
Sls.fold add !consts dl
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
open Ty
open Term
open Decl
(* sort symbol of (polymorphic) types *)
val ts_type : tysymbol
(* sort of (polymorphic) types *)
val ty_type : ty
(* ts_type declaration *)
val d_ts_type : decl
(* function symbol mapping ty_type^n to ty_type *)
val ls_of_ts : tysymbol -> lsymbol
(* test whether a function symbol has ty_type as ls_value *)
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
(* convert a type declaration to a list of lsymbol declarations *)
val lsdecl_of_tydecl : ty_decl list -> decl list
(* sort symbol by default (= undeco) *)
val ts_base : tysymbol
(* sort by default (= undeco) *)
val ty_base : ty
(* ts_base declaration *)
val d_ts_base : decl
(* convert a constant to a functional symbol of type ty_base *)
val ls_of_const : constant -> lsymbol
(* convert a constant to a term of type ty_base *)
val term_of_const : constant -> term
(* convert a set of preserved tysymbols to a set of types *)
val tyset_of_tsset : Sts.t -> Sty.t
(* monomorphise modulo the set of kept types * and an lsymbol map *)
val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
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