Skip to content

GitLab

why3
why3
Commit 4cd5a72c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

join fsymbol and psymbol into the common lsymbol type

parent e68cdad5
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 300 additions and 344 deletions
src/core/term.ml
View file @ 4cd5a72c
This diff is collapsed.
src/core/term.mli
View file @ 4cd5a72c
......@@ -33,38 +33,30 @@ module Hvs : Hashtbl.S with type key = vsymbol
val create_vsymbol : preid -> ty -> vsymbol
(** Function symbols *)
(** Function and predicate symbols *)
type fsymbol = private {
fs_name : ident;
fs_scheme : ty list * ty;
fs_constr : bool;
type lsymbol = private {
ls_name : ident;
ls_args : ty list;
ls_value : ty option;
ls_constr : bool;
}
val create_fsymbol : preid -> ty list * ty -> bool -> fsymbol
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_fconstr : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol
module Sfs : Set.S with type elt = fsymbol
module Mfs : Map.S with type key = fsymbol
module Hfs : Hashtbl.S with type key = fsymbol
(** Predicate symbols *)
type psymbol = private {
ps_name : ident;
ps_scheme : ty list;
}
val create_psymbol : preid -> ty list -> psymbol
module Sps : Set.S with type elt = psymbol
module Mps : Map.S with type key = psymbol
module Hps : Hashtbl.S with type key = psymbol
module Sls : Set.S with type elt = lsymbol
module Mls : Map.S with type key = lsymbol
module Hls : Hashtbl.S with type key = lsymbol
(** Exceptions *)
exception BadArity
exception NonLinear of vsymbol
exception ConstructorExpected of fsymbol
exception ConstructorExpected of lsymbol
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
(** Patterns *)
......@@ -77,14 +69,14 @@ type pattern = private {
and pattern_node = private
| Pwild
| Pvar of vsymbol
| Papp of fsymbol * pattern list
| Papp of lsymbol * pattern list
| Pas of pattern * vsymbol
(* smart constructors for patterns *)
val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : fsymbol -> pattern list -> ty -> pattern
val pat_app : lsymbol -> pattern list -> ty -> pattern
val pat_as : pattern -> vsymbol -> pattern
(* generic traversal functions *)
......@@ -137,13 +129,13 @@ and term_node = private
| Tbvar of int
| Tvar of vsymbol
| Tconst of constant
| Tapp of fsymbol * term list
| Tapp of lsymbol * term list
| Tlet of term * term_bound
| Tcase of term * term_branch list
| Teps of fmla_bound
and fmla_node = private
| Fapp of psymbol * term list
| Fapp of lsymbol * term list
| Fquant of quant * fmla_quant
| Fbinop of binop * fmla * fmla
| Fnot of fmla
......@@ -178,7 +170,7 @@ module Sfmla : Set.S with type elt = fmla
val t_var : vsymbol -> term
val t_const : constant -> ty -> term
val t_app : fsymbol -> term list -> ty -> term
val t_app : lsymbol -> term list -> ty -> term
val t_let : vsymbol -> term -> term -> term
val t_case : term -> (pattern * term) list -> ty -> term
val t_eps : vsymbol -> fmla -> term
......@@ -188,7 +180,7 @@ val t_label_add : label -> term -> term
(* smart constructors for fmla *)
val f_app : psymbol -> term list -> fmla
val f_app : lsymbol -> term list -> fmla
val f_forall : vsymbol list -> trigger list -> fmla -> fmla
val f_exists : vsymbol list -> trigger list -> fmla -> fmla
val f_quant : quant -> vsymbol list -> trigger list -> fmla -> fmla
......@@ -222,11 +214,11 @@ val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> term -> 'a
val t_fold :
('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> fmla -> 'a
val f_fold :
('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_all : (term -> bool) -> (fmla -> bool) -> fmla -> bool
......@@ -235,29 +227,19 @@ val f_any : (term -> bool) -> (fmla -> bool) -> fmla -> bool
(* symbol-wise map/fold *)
val t_s_map : (tysymbol -> tysymbol) -> (fsymbol -> fsymbol)
-> (psymbol -> psymbol) -> term -> term
val f_s_map : (tysymbol -> tysymbol) -> (fsymbol -> fsymbol)
-> (psymbol -> psymbol) -> fmla -> fmla
val t_s_fold : ('a -> tysymbol -> 'a) -> ('a -> fsymbol -> 'a)
-> ('a -> psymbol -> 'a) -> 'a -> term -> 'a
val f_s_fold : ('a -> tysymbol -> 'a) -> ('a -> fsymbol -> 'a)
-> ('a -> psymbol -> 'a) -> 'a -> fmla -> 'a
val t_s_all : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> term -> bool
val t_s_map : (tysymbol -> tysymbol) -> (lsymbol -> lsymbol) -> term -> term
val f_s_map : (tysymbol -> tysymbol) -> (lsymbol -> lsymbol) -> fmla -> fmla
val f_s_all : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> fmla -> bool
val t_s_fold :
('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
val t_s_any : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> term -> bool
val f_s_fold :
('a -> tysymbol -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> fmla -> 'a
val f_s_any : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> fmla -> bool
val t_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
val t_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
(* map/fold over free variables *)
......@@ -329,8 +311,8 @@ val f_match : fmla -> fmla -> term Mvs.t -> term Mvs.t option
(* built-in symbols *)
val ps_equ : psymbol
val ps_neq : psymbol
val ps_equ : lsymbol
val ps_neq : lsymbol
val f_equ : term -> term -> fmla
val f_neq : term -> term -> fmla
......
src/core/theory.ml
View file @ 4cd5a72c
This diff is collapsed.
src/core/theory.mli
View file @ 4cd5a72c
......@@ -27,7 +27,7 @@ open Term
type ty_def =
| Tabstract
| Talgebraic of fsymbol list
| Talgebraic of lsymbol list
type ty_decl = tysymbol * ty_def
......@@ -37,9 +37,9 @@ type fs_defn
type ps_defn
type logic_decl =
| Lfunction of fsymbol * fs_defn option
| Lpredicate of psymbol * ps_defn option
| Linductive of psymbol * (ident * fmla) list
| Lfunction of lsymbol * fs_defn option
| Lpredicate of lsymbol * ps_defn option
| Linductive of lsymbol * (ident * fmla) list
(* proposition declaration *)
......@@ -64,11 +64,11 @@ type decl = private {
(* smart constructors *)
val make_fs_defn : fsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : psymbol -> vsymbol list -> fmla -> ps_defn
val make_fs_defn : lsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ps_defn
val open_fs_defn : fs_defn -> fsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> psymbol * vsymbol list * fmla
val open_fs_defn : fs_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> lsymbol * vsymbol list * fmla
val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla
......@@ -79,11 +79,11 @@ val create_prop : prop_kind -> preid -> fmla -> decl
(* exceptions *)
exception NotAConstructor of fsymbol
exception ConstructorExpected of lsymbol
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception IllegalConstructor of lsymbol
exception UnboundVars of Svs.t
exception BadDecl of ident
......@@ -102,8 +102,7 @@ type theory = private {
and namespace = private {
ns_ts : tysymbol Mnm.t; (* type symbols *)
ns_fs : fsymbol Mnm.t; (* function symbols *)
ns_ps : psymbol Mnm.t; (* predicate symbols *)
ns_ls : lsymbol Mnm.t; (* logic symbols *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
ns_pr : fmla Mnm.t; (* propositions *)
}
......@@ -130,8 +129,7 @@ val use_export : theory_uc -> theory -> theory_uc
type th_inst = {
inst_ts : tysymbol Mts.t;
inst_fs : fsymbol Mfs.t;
inst_ps : psymbol Mps.t;
inst_ls : lsymbol Mls.t;
}
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
......@@ -148,5 +146,5 @@ exception ClashSymbol of string
(** Debugging *)
val print_th : Format.formatter -> theory_uc -> unit
val print_t : Format.formatter -> theory -> unit
val print_uc : Format.formatter -> theory_uc -> unit
val print_th : Format.formatter -> theory -> unit
src/parser/parser.mly
View file @ 4cd5a72c
......@@ -524,23 +524,22 @@ imp_exp:
clone_subst:
| /* epsilon */
{ { ts_subst = []; fs_subst = []; ps_subst = [] } }
{ { ts_subst = []; ls_subst = [] } }
| WITH list1_comma_subst
{ let t, f, p = $2 in
{ ts_subst = t; fs_subst = f; ps_subst = p } }
{ let t,l = $2 in
{ ts_subst = t; ls_subst = l } }
;
list1_comma_subst:
| subst
{ $1 }
| subst COMMA list1_comma_subst
{ let t,f,p = $1 in let tl,fl,pl = $3 in t@tl, f@fl, p@pl }
{ let t,l = $1 in let tl,ll = $3 in t@tl, l@ll }
;
subst:
| TYPE qualid EQUAL qualid { [$2, $4], [], [] }
| FUNCTION qualid EQUAL qualid { [], [$2, $4], [] }
| PREDICATE qualid EQUAL qualid { [], [], [$2, $4] }
| TYPE qualid EQUAL qualid { [$2, $4], [] }
| LOGIC qualid EQUAL qualid { [], [$2, $4] }
;
/******* programs **************************************************
......
src/parser/ptree.mli
View file @ 4cd5a72c
......@@ -77,8 +77,7 @@ type use = {
type clone_subst = {
ts_subst : (qualid * qualid) list;
fs_subst : (qualid * qualid) list;
ps_subst : (qualid * qualid) list;
ls_subst : (qualid * qualid) list;
}
type param = ident option * pty
......
src/parser/typing.ml
View file @ 4cd5a72c
......@@ -288,34 +288,41 @@ let specialize_tysymbol ~loc x env =
let env = Htv.create 17 in
s, List.map (find_type_var ~loc env) s.ts_args
let find_fsymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_fs
let find_lsymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ls
with Not_found -> error ~loc (UnboundSymbol x)
let find_fsymbol_ns p ns =
find find_fsymbol p ns
let find_lsymbol_ns p ns =
find find_lsymbol p ns
let find_fsymbol p th =
find_fsymbol_ns p (get_namespace th)
let find_lsymbol p th =
find_lsymbol_ns p (get_namespace th)
let specialize_fsymbol ~loc s =
let tl, t = s.fs_scheme in
let tl, t = match s.ls_value with
| Some t -> s.ls_args, t
| _ -> assert false (* FIXME: is it right? *)
in
let env = Htv.create 17 in
s, List.map (specialize ~loc env) tl, specialize ?loc env t
let find_psymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ps
let find_lsymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ls
with Not_found -> error ~loc (UnboundSymbol x)
let find_psymbol_ns p ns =
find find_psymbol p ns
let find_lsymbol_ns p ns =
find find_lsymbol p ns
let find_psymbol p th =
find_psymbol_ns p (get_namespace th)
let find_lsymbol p th =
find_lsymbol_ns p (get_namespace th)
let specialize_psymbol ~loc s =
let tl = match s.ls_value with
| None -> s.ls_args
| _ -> assert false (* FIXME: is it right? *)
in
let env = Htv.create 17 in
s, List.map (specialize ~loc env) s.ps_scheme
s, List.map (specialize ~loc env) tl
(** Typing types *)
......@@ -365,14 +372,14 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
| Tvar of string
| Tconst of constant
| Tapp of fsymbol * dterm list
| Tapp of lsymbol * dterm list
| Tlet of dterm * string * dterm
(* | Tcase of dterm * tbranch list *)
| Tnamed of string * dterm
| Teps of string * dfmla
and dfmla =
| Fapp of psymbol * dterm list
| Fapp of lsymbol * dterm list
| Fquant of quant * string list * dty * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
......@@ -409,15 +416,15 @@ and dterm_node loc env = function
Tvar x, ty
| PPvar x ->
(* 0-arity symbol (constant) *)
let s = find_fsymbol x env.th in
let s = find_lsymbol x env.th in
let s, tyl, ty = specialize_fsymbol ~loc s in
let n = List.length tyl in
if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
Tapp (s, []), ty
| PPapp (x, tl) ->
let s = find_fsymbol x env.th in
let s = find_lsymbol x env.th in
let s, tyl, ty = specialize_fsymbol ~loc s in
let tl = dtype_args s.fs_name loc env tyl tl in
let tl = dtype_args s.ls_name loc env tyl tl in
Tapp (s, tl), ty
| PPconst (ConstInt _ as c) ->
Tconst c, Tyapp (Ty.ts_int, [])
......@@ -469,9 +476,9 @@ and dfmla env e = match e.pp_desc with
let env = { env with dvars = M.add x ty env.dvars } in
Fquant (Fexists, [x], ty, [], dfmla env a)
| PPapp (x, tl) ->
let s = find_psymbol x env.th in
let s = find_lsymbol x env.th in
let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
Fapp (s, tl)
| PPlet ({id=x}, e1, e2) ->
let e1 = dterm env e1 in
......@@ -654,7 +661,7 @@ let add_types loc dl th =
let constructor (loc, id, pl) =
let param (_, t) = ty_of_dty (dty th' t) in
let tyl = List.map param pl in
create_fsymbol (id_user id.id id.id_loc) (tyl, ty) true
create_fconstr (id_user id.id id.id_loc) tyl ty
in
Talgebraic (List.map constructor cl)
in
......@@ -674,7 +681,7 @@ let add_logics loc dl th =
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
if Hashtbl.mem denvs id || Mnm.mem id ns.ns_fs then error ~loc (Clash id);
if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls then error ~loc (Clash id);
let v = id_user id loc in
let denv = create_denv th in
Hashtbl.add denvs id denv;
......@@ -687,7 +694,7 @@ let add_logics loc dl th =
add_decl th (create_logic [Lpredicate (ps, None)])
| Some t -> (* function *)
let t = type_ty (None, t) in
let fs = create_fsymbol v (pl, t) false in
let fs = create_fsymbol v pl t in
Hashtbl.add fsymbols id fs;
add_decl th (create_logic [Lfunction (fs, None)])
in
......@@ -717,7 +724,10 @@ let add_logics loc dl th =
| None -> None
| Some f ->
let f = dfmla denv f in
let vl = mk_vlist ps.ps_scheme in
let vl = match ps.ls_value with
| None -> mk_vlist ps.ls_args
| _ -> assert false
in
let env = env_of_vsymbol_list vl in
Some (make_ps_defn ps vl (fmla env f))
in
......@@ -729,7 +739,10 @@ let add_logics loc dl th =
| Some t ->
let loc = t.pp_loc in
let t = dterm denv t in
let vl = mk_vlist (fst fs.fs_scheme) in
let vl = match fs.ls_value with
| Some _ -> mk_vlist fs.ls_args
| _ -> assert false
in
let env = env_of_vsymbol_list vl in
try Some (make_fs_defn fs vl (term env t))
with _ -> error ~loc (TermExpectedType
......@@ -862,16 +875,12 @@ and add_decl env th = function
let add_ts m (p, q) =
Mts.add (find_tysymbol_ns p t.th_export) (find_tysymbol q th) m
in
let add_fs m (p, q) =
Mfs.add (find_fsymbol_ns p t.th_export) (find_fsymbol q th) m
in
let add_ps m (p, q) =
Mps.add (find_psymbol_ns p t.th_export) (find_psymbol q th) m
let add_ls m (p, q) =
Mls.add (find_lsymbol_ns p t.th_export) (find_lsymbol q th) m
in
let s =
{ inst_ts = List.fold_left add_ts Mts.empty s.ts_subst;
inst_fs = List.fold_left add_fs Mfs.empty s.fs_subst;
inst_ps = List.fold_left add_ps Mps.empty s.ps_subst; }
inst_ls = List.fold_left add_ls Mls.empty s.ls_subst; }
in
clone_export th t s
in
......
src/pretty.ml
View file @ 4cd5a72c
......@@ -55,7 +55,7 @@ let rec print_term fmt t = match t.t_node with
fprintf fmt "<real constant>"
| Tapp (s, tl) ->
fprintf fmt "@[<hov>(%a(%a)@ : %a)@]("
print_ident s.fs_name (print_list comma print_term) tl
print_ident s.ls_name (print_list comma print_term) tl
print_ty t.t_ty
| Tlet (t1,tbound) ->
let vs,t2 = t_open_bound tbound in
......@@ -72,7 +72,7 @@ let print_vsymbol fmt vs =
let rec print_fmla fmt f = match f.f_node with
| Fapp (s,tl) ->
fprintf fmt "@[<hov>(%a(%a))@]"
print_ident s.ps_name (print_list comma print_term) tl
print_ident s.ls_name (print_list comma print_term) tl
| Fquant (q,fquant) ->
let vl,tl,f = f_open_quant fquant in
fprintf fmt "(%s %a %a.@ %a)"
......@@ -107,17 +107,15 @@ and print_tr fmt = function
| TrTerm t -> print_term fmt t
| TrFmla f -> print_fmla fmt f
let print_fsymbol fmt {fs_name = fs_name; fs_scheme = tyl,ty} =
fprintf fmt "%a%a :@ %a"
print_ident fs_name
(print_list_paren comma print_ty) tyl
print_ty ty
let print_psymbol fmt {ps_name = ps_name; ps_scheme = tyl} =
fprintf fmt "%a%a"
print_ident ps_name
(print_list_paren comma print_ty) tyl
let print_lsymbol fmt {ls_name = ls_name; ls_args = tyl; ls_value = vty } =
match vty with
| Some ty ->
fprintf fmt "%a%a :@ %a" print_ident ls_name
(print_list_paren comma print_ty) tyl
print_ty ty
| None ->
fprintf fmt "%a%a" print_ident ls_name
(print_list_paren comma print_ty) tyl
let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
| Tabstract,None ->
......@@ -133,7 +131,7 @@ let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
fprintf fmt "@[<hov>type %a %a =@ @[<hov>%a@]@]"
(print_list_paren comma print_typevar) ts.ts_args
print_ident ts.ts_name
(print_list newline print_fsymbol) d
(print_list newline print_lsymbol) d
| Talgebraic _, Some _ ->
assert false
......@@ -142,14 +140,14 @@ let print_vsymbol fmt {vs_name = vs_name; vs_ty = vs_ty} =
let print_logic_decl fmt = function
| Lfunction (fs,None) ->
fprintf fmt "@[<hov 2>logic %a@]" print_fsymbol fs
fprintf fmt "@[<hov 2>logic %a@]" print_lsymbol fs
| Lfunction (fs,Some fd) ->
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident fs.fs_name
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident fs.ls_name
print_fmla (fs_defn_axiom fd)
| Lpredicate (fs,None) ->
fprintf fmt "@[<hov 2>logic %a@]" print_psymbol fs
fprintf fmt "@[<hov 2>logic %a@]" print_lsymbol fs
| Lpredicate (ps,Some fd) ->
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ps_name
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ls_name
print_fmla (ps_defn_axiom fd)
| Linductive _ ->
assert false (*TODO*)
......
src/pretty.mli
View file @ 4cd5a72c
......@@ -27,9 +27,7 @@ val print_ident : formatter -> ident -> unit
val print_vsymbol : formatter -> vsymbol -> unit
val print_fsymbol : formatter -> fsymbol -> unit
val print_psymbol : formatter -> psymbol -> unit
val print_lsymbol : formatter -> lsymbol -> unit
val print_ty : formatter -> ty -> unit
......
src/transform/inlining.ml
View file @ 4cd5a72c
......@@ -5,26 +5,26 @@ open Theory
let ttrue _ = true
let ffalse _ = false
type env = { fs : (vsymbol list * term) Mfs.t;
ps : (vsymbol list * fmla) Mps.t}
type env = { fs : (vsymbol list * term) Mls.t;
ps : (vsymbol list * fmla) Mls.t}
let empty_env = { fs = Mfs.empty;
ps = Mps.empty}
let empty_env = { fs = Mls.empty;
ps = Mls.empty}
open Format
let print_env fmt env =
let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs
(Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in
fprintf fmt "fs:@[<hov>%a@]@\nps:@[<hov>%a@]@\n"
(print_map Mfs.iter Pretty.print_term Pretty.print_fsymbol) env.fs
(print_map Mps.iter Pretty.print_fmla Pretty.print_psymbol) env.ps
(print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs
(print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps
let rec replacet env t =
let t = substt env t in
match t.t_node with
| Tapp (fs,tl) ->
begin try
let (vs,t) = Mfs.find fs env.fs in
let (vs,t) = Mls.find fs env.fs in
let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
Mvs.empty vs tl in
t_subst m t
......@@ -36,7 +36,7 @@ and replacep env f =
match f.f_node with
| Fapp (ps,tl) ->
begin try
let (vs,t) = Mps.find ps env.ps in
let (vs,t) = Mls.find ps env.ps in
let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
Mvs.empty vs tl in
f_subst m f
......@@ -54,16 +54,16 @@ let fold env d =
| Lfunction (fs,Some fmla) ->
let _,vs,t = open_fs_defn fmla in
let t = replacet env t in
if t_s_any ffalse ((==) fs) ffalse t
if t_s_any ffalse ((==) fs) t
then env,[create_logic [Lfunction(fs,Some (make_fs_defn fs vs t))]]
else {env with fs = Mfs.add fs (vs,t) env.fs},[]
else {env with fs = Mls.add fs (vs,t) env.fs},[]
| Lpredicate (ps,None) -> env,[d]
| Lpredicate (ps,Some fmla) ->
let _,vs,f = open_ps_defn fmla in
let f = replacep env f in
if f_s_any ffalse ffalse ((==) ps) f
if f_s_any ffalse ((==) ps) f
then env,[create_logic [Lpredicate(ps,Some (make_ps_defn ps vs f))]]
else {env with ps = Mps.add ps (vs,f) env.ps},[]
else {env with ps = Mls.add ps (vs,f) env.ps},[]
| Linductive (ps,fmlal) ->
let fmlal = List.map (fun (id,fmla) -> id,replacep env fmla) fmlal in
env,[create_logic [Linductive (ps,fmlal)]]
......
src/transform/simplify_recursive_definition.ml
View file @ 4cd5a72c
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Util
open Ident
open Ty
open Term
......@@ -88,14 +89,12 @@ let elt d =
| Dlogic l ->
let mem = Hid.create 16 in
List.iter (function
| Lfunction (fs,_) as a -> Hid.add mem fs.fs_name a
| Lpredicate (ps,_) as a -> Hid.add mem ps.ps_name a
| Linductive (ps,_) as a -> Hid.add mem ps.ps_name a) l;
| Lfunction (fs,_) as a -> Hid.add mem fs.ls_name a
| Lpredicate (ps,_) as a -> Hid.add mem ps.ls_name a
| Linductive (ps,_) as a -> Hid.add mem ps.ls_name a) l;
let tyoccurences acc _ = acc in
let toccurences acc fs =
if Hid.mem mem fs.fs_name then Sid.add fs.fs_name acc else acc in
let foccurences acc ps =
if Hid.mem mem ps.ps_name then Sid.add ps.ps_name acc else acc in
let loccurences acc ls =
if Hid.mem mem ls.ls_name then Sid.add ls.ls_name acc else acc in
let m = List.fold_left
(fun acc a -> match a with
| Lfunction (fs,l) ->
......@@ -103,20 +102,20 @@ let elt d =
| None -> Sid.empty
| Some fd ->
let fd = fs_defn_axiom fd in
f_s_fold tyoccurences toccurences foccurences Sid.empty fd in
Mid.add fs.fs_name s acc
f_s_fold tyoccurences loccurences Sid.empty fd in
Mid.add fs.ls_name s acc
| Lpredicate (ps,l) ->
let s = match l with
| None -> Sid.empty
| Some fd ->
let fd = ps_defn_axiom fd in
f_s_fold tyoccurences toccurences foccurences Sid.empty fd in
Mid.add ps.ps_name s acc
f_s_fold tyoccurences loccurences Sid.empty fd in
Mid.add ps.ls_name s acc