Commit 7d7bc1a4 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

elimination of indictive predicates

parent d813b7f2
......@@ -129,7 +129,7 @@ PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
split_conjunction.cmo encoding_decorate.cmo\
remove_logic_definition.cmo
remove_logic_definition.cmo eliminate_inductive.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\
......
(**************************************************************************)
(* *)
(* 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 Ident
open Term
open Decl
open Task
let log acc (ps,_) = create_logic_decl [ps, None] :: acc
let axm acc (pr,f) = create_prop_decl Paxiom pr f :: acc
let imp acc (_,al) = List.fold_left axm acc al
let exi vl (_,f) =
let rec descend f = match f.f_node with
| Fquant (Fforall,f) ->
let vl,tl,f = f_open_quant f in
f_exists vl tl (descend f)
| Fbinop (Fimplies,g,f) ->
f_and g (descend f)
| Fapp (_,tl) ->
let marry acc v t = f_and_simp acc (f_app ps_equ [v;t]) in
List.fold_left2 marry f_true vl tl
| _ -> assert false
in
descend f
let inv acc (ps,al) =
let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
let tl = List.map t_var vl in
let hd = f_app ps tl in
let dj = Util.map_join_left (exi tl) f_or al in
let ax = f_forall vl [[Fmla hd]] (f_implies hd dj) in
let nm = id_derive (ps.ls_name.id_long ^ "_inversion") ps.ls_name in
create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
let elim d = match d.d_node with
| Dind il ->
let dl = List.fold_left log [] il in
let dl = List.fold_left imp dl il in
let dl = List.fold_left inv dl il in
List.rev dl
| _ -> [d]
let elim = Register.store (fun () -> Trans.decl elim None)
let () = Driver.register_transform "eliminate_inductive" elim
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