Commit 0b18ac43 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

small improvement in hypothesis_selection

no more warnings for tptp2why.ml
small changes for explicit_polymorphism
parent 1b305533
......@@ -75,7 +75,7 @@ end = struct
let all_decls = List.concat
(List.map (getAllDecls include_dir) to_include) in
all_decls @ real_decl
(** parses a single file *)
and myparse chan =
let lb = Lexing.from_channel chan in
......@@ -83,9 +83,10 @@ end = struct
let read_channel
?(debug=false) ?(parse_only=false) ?(type_only=false) env file c =
?(debug=false) ?(parse_only=false) ?(type_only=false) _env file c =
if debug then Format.eprintf "tptp2why : starts parsing %s@." file;
let decls = getDeclsFromChan c in
if parse_only then Theory.Mnm.empty else
if parse_only || type_only then Theory.Mnm.empty else
let my_theory = theory_of_decls file decls in
Theory.Mnm.add "Tptp" my_theory Theory.Mnm.empty
......@@ -147,3 +148,10 @@ open Init *)
(** register as a .p/.ax file parser *)
let () =
Env.register_format "tptp" ["p"] Process.read_channel Process.report
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
......@@ -17,10 +17,9 @@
(* *)
(**************************************************************************)
(*s transformation from polymorphic logic to untyped logic. The polymorphic
(**s transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)
(* TODO : preserve builtin types *)
open Util
open Ident
......@@ -36,7 +35,7 @@ module Debug = struct
Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
Pretty.print_tv key vprinter value) m
let print_mty vprinter fmter m =
let print_mty vprinter fmter m =
Mty.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
Pretty.print_ty key vprinter value) m
......@@ -92,8 +91,8 @@ module Utils = struct
(** [drop n l] is [l], without its [n] first elements *)
let rec drop n l = match (n,l) with
| (0, _) -> l
| (n, []) -> failwith "dropping items from empty list"
| (_, x::xs) -> drop (n-1) xs
| (_, []) -> failwith "dropping items from empty list"
| (_, _::xs) -> drop (n-1) xs
(** explore a type to seek all type vars *)
let rec find_tyvars tyvars ty = match ty.ty_node with
......@@ -128,14 +127,6 @@ module Utils = struct
List.fold_left find_tyvars acc l.ls_args
(** kind of composition of filter and map *)
let rec mapSome f = function
| e::es -> (match f e with
| Some x -> x :: mapSome f es
| None -> mapSome f es)
| [] -> []
(** [find_matching_vars tv_to_ty left right] matches [left]
against [right] to deduce a mapping from type vars in [left]
to types in [right]. [tv_to_ty] is a mapping given in argument.
......@@ -222,7 +213,7 @@ module Transform = struct
(** transforms a type into a term (new args of polymorphic symbols) *)
let rec ty_to_term tblT varM tv_to_ty ty =
match ty.ty_node with
| Tyvar x ->
| Tyvar _ ->
let new_ty = ty_to_ty tv_to_ty ty in
begin match new_ty.ty_node with
| Tyvar _ -> (* var -> var, stop there *)
......@@ -266,7 +257,7 @@ module Transform = struct
| _ -> (* default case : traverse *)
t_map (term_transform tblT tblL varM)
(fmla_transform tblT tblL varM) t
(** (trivial) translation of formulae *)
(** translation of formulae *)
and fmla_transform tblT tblL varM f = match f.f_node with
| Fapp(p,terms) when (not (ls_equal p ps_equ)) && not(ls_equal p ps_neq) ->
let new_p = findL tblL p in
......
......@@ -28,11 +28,24 @@ open Decl
open Task
(* requires ocamlgraph. TODO : recode this inside *)
open Graph.Pack.Digraph
open Graph.Pack.Graph
open Graph.Persistent
module Int_Dft = struct
type t = int
let compare = Pervasives.compare
let default = max_int
end
module GP = Digraph.AbstractLabeled(struct type t = Term.lsymbol end)(Int_Dft)
module GC = Graph.AbstractLabeled(struct type t = int end)(Int_Dft)
module Util = struct
end
(** module used to reduce formulae to Conjonctive Normal Form *)
module CNF = struct
(** module used to reduce formulae to Normal Form *)
module NF = struct (* add memoization ? *)
end
......@@ -41,28 +54,64 @@ end
(** module used to compute the graph of constants *)
module GraphConstant = struct
let update gc task_head = assert false
end
(** module used to compute the directed graph of predicates *)
module GraphPredicate = struct
module GraphPredicate : sig
val update : GP.t -> Task.task_hd -> GP.t
end = struct
let analyse_prop gp prop = assert false
let add_symbol gp lsymbol = GP.add_vertex gp
(GP.V.create lsymbol)
(** takes a constant graph and a task_head, and add any interesting
element to the graph it returns. *)
let update gp task_head =
match task_head.task_decl with
| Decl {d_node = Dprop (_,_,prop_decl) } ->
(* a proposition to analyse *)
analyse_prop gp prop_decl
| Decl {d_node = Dlogic logic_decls } ->
(* a symbol to add *)
List.fold_left (fun gp logic_decl -> add_symbol gp (fst logic_decl))
gp logic_decls
| _ -> gp
end
(** module that makes the final selection *)
module Select = struct
let filter (gc,gp) decl = assert false
end
(* TODO : think of a correct way to insert this kind of transformation *)
(** collects data on predicates and constants in task *)
let collect_info =
Trans.fold (fun t (gc, gp) ->
GraphConstant.update gc t, GraphPredicate.update gp t)
(GC.empty, GP.empty)
(** the transformation, made from applying collect_info and
then mapping Select.filter *)
let transformation task =
let (gc,gp) = Trans.apply collect_info task in
Trans.apply (Trans.decl (Select.filter (gc,gp)) None) task
(** the transformation to be registered *)
let hypothesis_selection =
Register.store (fun () ->
Trans.identity)
Register.store
(fun () -> Trans.store transformation)
let _ = Register.register_transform
"hypothesis_selection" hypothesis_selection
(*
Local Variables:
compile-command: "unset LANG; make -k -C ../.."
End:
*)
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