Commit 81badfbc authored by Simon Cruanes's avatar Simon Cruanes

added basic compilation support with ocamlgraph autoconf for hypothesis selection transformation

parent 2aa1e6dc
......@@ -70,6 +70,7 @@ else
DYNLINK =
endif
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA = $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
......@@ -107,6 +108,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
eliminate_inductive eliminate_let eliminate_if \
explicit_polymorphism
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
LIBMODULES = src/config \
......@@ -120,6 +122,14 @@ LIBMODULES = src/config \
LIBDIRS = util core parser driver transform printer
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
ifeq (@enable_hypothesis_selection@,yes)
LIB_TRANSFORM += hypothesis_selection
LIBINCLUDES += -I +ocamlgraph
INCLUDES += -I +ocamlgraph
EXTLIBS += ocamlgraph/graph
endif
LIBML = $(addsuffix .ml, $(LIBMODULES))
LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
......
......@@ -269,7 +269,15 @@ else
enable_tptp2why_support=yes
fi
# hypothesis_selection
AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes)
if test "$enable_hypothesis_selection" = no; then
enable_hypothesis_selection=no
else
enable_hypothesis_selection=yes
fi
#Viewer for ps and pdf
dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
......@@ -319,6 +327,8 @@ AC_SUBST(COQVERSION)
AC_SUBST(MENHIR)
AC_SUBST(enable_tptp2why_support)
AC_SUBST(enable_hypothesis_selection)
dnl AC_SUBST(PSVIEWER)
dnl AC_SUBST(PDFVIEWER)
......@@ -345,3 +355,4 @@ if test "$enable_coq_support" = "yes" ; then
echo " Lib : $COQLIB"
fi
echo "tptp2why support : $enable_tptp2why_support"
echo "hypothesis selection : $enable_hypothesis_selection"
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(**s Transformation which removes most hypothesis, only keeping the one
a graph-based heuristic finds close enough to the goal *)
open Util
open Ident
open Ty
open Term
open Decl
open Task
(* requires ocamlgraph. TODO : recode this inside *)
open Graph.Pack.Digraph
open Graph.Pack.Graph
(** module used to reduce formulae to Conjonctive Normal Form *)
module CNF = struct
end
(** module used to compute the graph of constants *)
module GraphConstant = struct
end
(** module used to compute the directed graph of predicates *)
module GraphPredicate = struct
end
(** module that makes the final selection *)
module Select = struct
end
(* TODO : think of a correct way to insert this kind of transformation *)
(** the transformation to be registered *)
let hypothesis_selection =
Register.store (fun () ->
Trans.identity)
let _ = Register.register_transform
"hypothesis_selection" hypothesis_selection
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