--- /dev/null
+<matitaprover.{byte,native}>: use_str, use_unix
--- /dev/null
+../../tptp_grafite/ast.ml
\ No newline at end of file
--- /dev/null
+../../extlib/discrimination_tree.ml
\ No newline at end of file
--- /dev/null
+../../extlib/discrimination_tree.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foSubst.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foSubst.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foUnif.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foUnif.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foUtils.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/foUtils.mli
\ No newline at end of file
--- /dev/null
+../../extlib/hExtlib.ml
\ No newline at end of file
--- /dev/null
+../../extlib/hExtlib.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/index.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/index.mli
\ No newline at end of file
--- /dev/null
+../../tptp_grafite/lexer.mll
\ No newline at end of file
--- /dev/null
+let main () =
+ let problem_file = ref "" in
+ Arg.parse [
+ ] (fun x -> problem_file := x) "matitaprover [problemfile]";
+ let hypotheses, goal = Tptp_cnf.parse !problem_file in
+ let module B : Terms.Blob = struct
+ type t = Ast.atom
+ let eq a b = a = b
+ let compare = Pervasives.compare
+ let eqP = Ast.True
+ let pp x = ""
+ let embed x = Terms.Var 0
+ let saturate x y = Terms.Var 0,Terms.Var 0
+ end
+ in
+ let module P = Paramod.Paramod(B) in
+ let bag = Terms.M.empty, 0 in
+ let g_passives = assert false in
+ let passives = assert false in
+ ignore(P.paramod bag ~g_passives ~passives);
+ ()
+;;
+
+main ()
--- /dev/null
+../../ng_paramodulation/orderings.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/orderings.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/paramod.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/paramod.mli
\ No newline at end of file
--- /dev/null
+../../tptp_grafite/parser.mly
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/pp.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/pp.mli
\ No newline at end of file
--- /dev/null
+type location = unit
+let first_pos () = 0
+let last_pos () = 0
+let make_loc _ = ()
--- /dev/null
+../../ng_paramodulation/superposition.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/superposition.mli
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/terms.ml
\ No newline at end of file
--- /dev/null
+../../ng_paramodulation/terms.mli
\ No newline at end of file
--- /dev/null
+module A = Ast;;
+(*
+
+type sort = Prop | Univ;;
+
+let floc = HExtlib.dummy_floc;;
+
+
+let paramod_timeout = ref 600;;
+let depth = ref 10;;
+
+let universe = "Univ" ;;
+let prop = "Prop";;
+
+let kw = [
+ "and","myand"
+];;
+
+let mk_ident s =
+ PT.Ident ((try List.assoc s kw with Not_found -> s),None)
+;;
+
+let rec collect_arities_from_term = function
+ | A.Constant name -> [name,(0,Univ)]
+ | A.Variable name -> [name,(0,Univ)]
+ | A.Function (name,l) ->
+ (name,(List.length l,Univ))::
+ List.flatten (List.map collect_arities_from_term l)
+;;
+
+let rec collect_fv_from_term = function
+ | A.Constant name -> []
+ | A.Variable name -> [name]
+ | A.Function (_,l) ->
+ List.flatten (List.map collect_fv_from_term l)
+;;
+
+let collect_arities_from_atom a =
+ let aux = function
+ | A.Proposition name -> [name,(0,Prop)]
+ | A.Predicate (name,args) ->
+ (name,(List.length args,Prop)) ::
+ (List.flatten (List.map collect_arities_from_term args))
+ | A.True -> []
+ | A.False -> []
+ | A.Eq (t1,t2) ->
+ collect_arities_from_term t1 @ collect_arities_from_term t2
+ | A.NotEq (t1,t2) ->
+ collect_arities_from_term t1 @ collect_arities_from_term t2
+ in
+ HExtlib.list_uniq (List.sort compare (List.flatten (List.map aux a)))
+;;
+
+let collect_fv_from_atom a =
+ let aux = function
+ | A.Proposition name -> [name]
+ | A.Predicate (name,args) ->
+ name :: List.flatten (List.map collect_fv_from_term args)
+ | A.True -> []
+ | A.False -> []
+ | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
+ | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
+ in
+ let rec aux2 = function
+ | [] -> []
+ | hd::tl -> aux hd @ aux2 tl
+ in
+ HExtlib.list_uniq (List.sort compare (aux2 a))
+;;
+
+let rec collect_fv_from_formulae = function
+ | A.Disjunction (a,b) ->
+ collect_fv_from_formulae a @ collect_fv_from_formulae b
+ | A.NegAtom a
+ | A.Atom a -> collect_fv_from_atom [a]
+;;
+
+let rec convert_term = function
+ | A.Variable x -> mk_ident x
+ | A.Constant x -> mk_ident x
+ | A.Function (name, args) ->
+ PT.Appl (mk_ident name :: List.map convert_term args)
+;;
+
+let rec atom_of_formula neg pos = function
+ | A.Disjunction (a,b) ->
+ let neg, pos = atom_of_formula neg pos a in
+ atom_of_formula neg pos b
+ | A.NegAtom a -> a::neg, pos
+ | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
+ | A.Atom a -> neg, a::pos
+;;
+
+let atom_of_formula f =
+ let neg, pos = atom_of_formula [] [] f in
+ neg @ pos
+;;
+
+let rec mk_arrow component tail = function
+ | 0 -> begin
+ match tail with
+ | Prop -> mk_ident prop
+ | Univ -> mk_ident universe
+ end
+ | n ->
+ PT.Binder
+ (`Forall,
+ ((mk_ident "_"),Some (mk_ident component)),
+ mk_arrow component tail (n-1))
+;;
+
+let build_ctx_for_arities univesally arities t =
+ let binder = if univesally then `Forall else `Exists in
+ let rec aux = function
+ | [] -> t
+ | (name,(nargs,sort))::tl ->
+ PT.Binder
+ (binder,
+ (mk_ident name,Some (mk_arrow universe sort nargs)),
+ aux tl)
+ in
+ aux arities
+;;
+
+let convert_atom universally a =
+ let aux = function
+ | A.Proposition p -> mk_ident p
+ | A.Predicate (name,params) ->
+ PT.Appl ((mk_ident name) :: (List.map convert_term params))
+ | A.True -> mk_ident "True"
+ | A.False -> mk_ident "False"
+ | A.Eq (l,r)
+ | A.NotEq (l,r) -> (* removes the negation *)
+ PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r]
+ in
+ let rec aux2 = function
+ | [] -> assert false
+ | [x] -> aux x
+ | he::tl ->
+ if universally then
+ PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl)
+ else
+ PT.Appl [mk_ident "And";aux he;aux2 tl]
+ in
+ let arities = collect_arities_from_atom a in
+ let fv = collect_fv_from_atom a in
+ build_ctx_for_arities universally
+ (List.filter
+ (function (x,(0,Univ)) -> List.mem x fv | _-> false)
+ arities)
+ (aux2 a)
+;;
+
+let collect_arities atom ctx =
+ let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in
+ collect_arities_from_atom atoms
+;;
+
+let collect_arities_from_formulae f =
+ let rec collect_arities_from_formulae = function
+ | A.Disjunction (a,b) ->
+ collect_arities_from_formulae a @ collect_arities_from_formulae b
+ | A.NegAtom a
+ | A.Atom a -> collect_arities_from_atom [a]
+ in
+ HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
+;;
+
+let is_formulae_1eq_negated f =
+ let atom = atom_of_formula f in
+ match atom with
+ | [A.NotEq (l,r)] -> true
+ | _ -> false
+;;
+
+let collect_fv_1stord_from_formulae f =
+ let arities = collect_arities_from_formulae f in
+ let fv = collect_fv_from_formulae f in
+ List.map fst
+ (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
+;;
+
+let rec convert_formula fv no_arities context f =
+ let atom = atom_of_formula f in
+ let t = convert_atom (fv = []) atom in
+ let rec build_ctx n = function
+ | [] -> t
+ | hp::tl ->
+ PT.Binder
+ (`Forall,
+ (mk_ident ("H" ^ string_of_int n),
+ Some (convert_formula [] true [] hp)),
+ build_ctx (n+1) tl)
+ in
+ let arities = if no_arities then [] else collect_arities atom context in
+ build_ctx_for_arities true arities (build_ctx 0 context)
+;;
+
+let check_if_atom_is_negative = function
+ | A.True -> false
+ | A.False -> true
+ | A.Proposition _ -> false
+ | A.Predicate _ -> false
+ | A.Eq _ -> false
+ | A.NotEq _ -> true
+;;
+
+let rec check_if_formula_is_negative = function
+ | A.Disjunction (a,b) ->
+ check_if_formula_is_negative a && check_if_formula_is_negative b
+ | A.NegAtom a -> not (check_if_atom_is_negative a)
+ | A.Atom a -> check_if_atom_is_negative a
+;;
+
+let ng_generate_tactics fv ueq_case context arities =
+ [ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
+ @
+ (HExtlib.list_mapi
+ (fun (name,_) _->
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+ GA.NDot(floc)])))
+ arities)
+ @
+ (HExtlib.list_mapi
+ (fun _ i->
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
+ context)
+ @
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.NTactic(floc,
+ [GA.NApply (floc,
+ PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
+ PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+ GA.Executable(floc,GA.NTactic(floc,
+ [GA.NPos (floc,[2])]))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.NTactic(floc, [
+ if (*ueq_case*) true then
+ GA.NAuto (floc,(
+ HExtlib.list_mapi
+ (fun _ i ->
+ mk_ident ("H" ^ string_of_int i))
+ context
+ ,[]))
+ else
+ GA.NAuto (floc,([],[
+ "depth",string_of_int 5;
+ "width",string_of_int 5;
+ "size",string_of_int 20;
+ "timeout",string_of_int 10;
+ ]))
+ ;
+ GA.NSemicolon(floc)]));
+(*
+ GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))
+*)
+ ]@
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
+ GA.NSkip floc; GA.NMerge floc]))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+ GA.NSemicolon(floc)]))]@
+ [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
+;;
+
+let generate_tactics fv ueq_case =
+ [GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Exists floc),GA.Branch floc));
+ GA.Executable(floc,GA.Tactic(floc, None,
+ (GA.Pos (floc,[2]))))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.Tactic(floc, Some (
+ if true (*ueq_case*) then
+ GA.AutoBatch (floc,([],["paramodulation","";
+ "timeout",string_of_int !paramod_timeout]))
+ else
+ GA.AutoBatch (floc,([],[
+ "depth",string_of_int 5;
+ "width",string_of_int 5;
+ "size",string_of_int 20;
+ "timeout",string_of_int 10;
+ ]))
+ ),
+ GA.Semicolon(floc)));
+ GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))
+ ]@
+(if fv <> [] then
+ (List.flatten
+ (List.map
+ (fun _ ->
+ [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
+ GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
+ (GA.Merge floc)))])
+ fv))
+ else [])@
+ [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
+ GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
+;;
+
+let convert_ast ng statements context = function
+ | A.Comment s ->
+ let s = String.sub s 1 (String.length s - 1) in
+ let s =
+ if s.[String.length s - 1] = '\n' then
+ String.sub s 0 (String.length s - 1)
+ else
+ s
+ in
+ statements @ [GA.Comment (floc,GA.Note (floc,s))],
+ context
+ | A.Inclusion (s,_) ->
+ statements @ [
+ GA.Comment (
+ floc, GA.Note (
+ floc,"Inclusion of: " ^ s))], context
+ | A.AnnotatedFormula (name,kind,f,_,_) ->
+ match kind with
+ | A.Axiom
+ | A.Hypothesis ->
+ statements, f::context
+ | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
+ statements, f::context
+ | A.Negated_conjecture ->
+ let ueq_case = is_formulae_1eq_negated f in
+ let fv = collect_fv_1stord_from_formulae f in
+ let old_f = f in
+ let f =
+ PT.Binder
+ (`Forall,
+ (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))),
+ convert_formula fv false context f)
+ in
+ let o = PT.Theorem (`Theorem,name,f,None) in
+ (statements @
+ [ GA.Executable(floc,GA.Command(floc,
+ (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
+ if ng then
+ ng_generate_tactics fv ueq_case context
+ (let atom = atom_of_formula old_f in collect_arities atom context)
+ else generate_tactics fv ueq_case),
+ context
+ | A.Definition
+ | A.Lemma
+ | A.Theorem
+ | A.Conjecture
+ | A.Lemma_conjecture
+ | A.Plain
+ | A.Unknown -> assert false
+;;
+
+(* HELPERS *)
+let resolve ~tptppath s =
+ let resolved_name =
+ if Filename.check_suffix s ".p" then
+ (assert (String.length s > 5);
+ let prefix = String.sub s 0 3 in
+ tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+ else
+ tptppath ^ "/" ^ s
+ in
+ if HExtlib.is_regular resolved_name then
+ resolved_name
+ else
+ begin
+ prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
+ exit 1
+ end
+;;
+
+(* MAIN *)
+let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
+ paramod_timeout := timeout;
+ depth := def_depth;
+ let rec aux = function
+ | [] -> []
+ | ((A.Inclusion (file,_)) as hd) :: tl ->
+ let file = resolve ~tptppath file in
+ let lexbuf = Lexing.from_channel (open_in file) in
+ let statements = Parser.main Lexer.yylex lexbuf in
+ hd :: aux (statements @ tl)
+ | hd::tl -> hd :: aux tl
+ in
+ let statements = aux [A.Inclusion (filename,[])] in
+ let grafite_ast_statements,_ =
+ List.fold_left
+ (fun (st, ctx) f ->
+ let newst, ctx = convert_ast ng st ctx f in
+ newst, ctx)
+ ([],[]) statements
+ in
+ let pp t =
+ (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
+ * which will show up using the following command line:
+ * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
+ let width = max_int in
+ let term_pp prec content_term =
+ let pres_term = TermContentPres.pp_ast content_term in
+ let lookup_uri = fun _ -> None in
+ let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
+ let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
+ Pcre.substitute
+ ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
+ s
+ in
+ CicNotationPp.set_pp_term (term_pp 90);
+ let lazy_term_pp = fun x -> assert false in
+ let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
+ Pcre.replace ~pat:"theorem" ~templ:"ntheorem"
+ (GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex:false ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t)
+ in
+ let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
+ let extra_statements_start = [
+ (*GA.Executable(floc,GA.Command(floc,
+ GA.Set(floc,"baseuri",buri)))*)]
+ in
+ let preamble =
+ match raw_preamble with
+ | None ->
+ pp (GA.Executable(floc,
+ GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
+ | Some s -> s buri
+ in
+ let extra_statements_end = [] in
+ let aliases = []
+ (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
+ ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
+ ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
+ ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
+ ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
+ ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
+ in
+ let s1 = List.map pp extra_statements_start in
+ let s2 =
+ List.map
+ (fun (n,s) ->
+ LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
+ aliases
+ in
+ let s3 = List.map pp grafite_ast_statements in
+ let s4 = List.map pp extra_statements_end in
+ String.concat "\n" (s1@[preamble]@s2@s3@s4)
+;;
+*)
+
+let parse _ = assert false;;
--- /dev/null
+val parse: string -> unit list * unit list
--- /dev/null
+../../extlib/trie.ml
\ No newline at end of file
--- /dev/null
+../../extlib/trie.mli
\ No newline at end of file
+cicUniv.cmi:
unshare.cmi: cic.cmo
deannotate.cmi: cic.cmo
cicParser.cmi: cic.cmo
cicUtil.cmi: cic.cmo
helmLibraryObjects.cmi: cic.cmo
-discrimination_tree.cmi: cic.cmo
+libraryObjects.cmi:
+cic_indexable.cmi: cic.cmo
path_indexing.cmi: cic.cmo
cicInspect.cmi: cic.cmo
cic.cmo: cicUniv.cmi
helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi
libraryObjects.cmo: libraryObjects.cmi
libraryObjects.cmx: libraryObjects.cmi
-discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi
-discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
+cic_indexable.cmo: cicUtil.cmi cic.cmo cic_indexable.cmi
+cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi
path_indexing.cmo: cic.cmo path_indexing.cmi
path_indexing.cmx: cic.cmx path_indexing.cmi
cicInspect.cmo: cic.cmo cicInspect.cmi
cicUtil.cmi: cic.cmx
helmLibraryObjects.cmi: cic.cmx
libraryObjects.cmi:
-discrimination_tree.cmi: cic.cmx
+cic_indexable.cmi: cic.cmx
path_indexing.cmi: cic.cmx
cicInspect.cmi: cic.cmx
cic.cmo: cicUniv.cmi
helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi
libraryObjects.cmo: libraryObjects.cmi
libraryObjects.cmx: libraryObjects.cmi
-discrimination_tree.cmo: cicUtil.cmi cic.cmx discrimination_tree.cmi
-discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
+cic_indexable.cmo: cicUtil.cmi cic.cmx cic_indexable.cmi
+cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi
path_indexing.cmo: cic.cmx path_indexing.cmi
path_indexing.cmx: cic.cmx path_indexing.cmi
cicInspect.cmo: cic.cmx cicInspect.cmi
cicUtil.mli \
helmLibraryObjects.mli \
libraryObjects.mli \
- discrimination_tree.mli \
+ cic_indexable.mli \
path_indexing.mli \
cicInspect.mli
IMPLEMENTATION_FILES = \
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM 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. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: discrimination_tree.ml 8991 2008-09-19 12:47:23Z tassi $ *)
+
+module CicIndexable : Discrimination_tree.Indexable
+with type input = Cic.term and type constant_name = UriManager.uri
+= struct
+
+ type input = Cic.term
+ type constant_name = UriManager.uri
+ open Discrimination_tree
+
+ let ppelem = function
+ | Constant (uri,arity) ->
+ "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")"
+ | Bound (i,arity) ->
+ "("^string_of_int i ^ "," ^ string_of_int arity^")"
+ | Variable -> "?"
+ | Proposition -> "Prop"
+ | Datatype -> "Type"
+ | Dead -> "Dead"
+ ;;
+
+ let path_string_of =
+ let rec aux arity = function
+ | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable]
+ | Cic.Appl (Cic.Lambda _ :: _) ->
+ [Variable] (* maybe we should b-reduce *)
+ | Cic.Appl [] -> assert false
+ | Cic.Appl (hd::tl) ->
+ aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
+ | Cic.Cast (t,_) -> aux arity t
+ | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable]
+ (* I think we should CicSubstitution.subst Implicit t *)
+ | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *)
+ | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable]
+ | Cic.Rel i -> [Bound (i, arity)]
+ | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition]
+ | Cic.Sort _ -> assert (arity=0); [Datatype]
+ | Cic.Const _ | Cic.Var _
+ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
+ [Constant (CicUtil.uri_of_term t, arity)]
+ | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead]
+ in
+ aux 0
+ ;;
+
+ let compare e1 e2 =
+ match e1,e2 with
+ | Constant (u1,a1),Constant (u2,a2) ->
+ let x = UriManager.compare u1 u2 in
+ if x = 0 then Pervasives.compare a1 a2 else x
+ | e1,e2 -> Pervasives.compare e1 e2
+ ;;
+
+ let string_of_path l = String.concat "." (List.map ppelem l) ;;
+end
+
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM 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. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+module CicIndexable : Discrimination_tree.Indexable
+with type input = Cic.term and type constant_name = UriManager.uri
+
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM 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. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-type 'a path_string_elem =
- | Constant of 'a * int (* name, arity *)
- | Bound of int * int (* rel, arity *)
- | Variable (* arity is 0 *)
- | Proposition (* arity is 0 *)
- | Datatype (* arity is 0 *)
- | Dead (* arity is 0 *)
-;;
-
-type 'a path = ('a path_string_elem) list;;
-
-module type Indexable = sig
- type input
- type constant_name
- val compare:
- constant_name path_string_elem ->
- constant_name path_string_elem -> int
- val string_of_path : constant_name path -> string
- val path_string_of : input -> constant_name path
-end
-
-module CicIndexable : Indexable
-with type input = Cic.term and type constant_name = UriManager.uri
-= struct
-
- type input = Cic.term
- type constant_name = UriManager.uri
-
- let ppelem = function
- | Constant (uri,arity) ->
- "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")"
- | Bound (i,arity) ->
- "("^string_of_int i ^ "," ^ string_of_int arity^")"
- | Variable -> "?"
- | Proposition -> "Prop"
- | Datatype -> "Type"
- | Dead -> "Dead"
- ;;
-
- let path_string_of =
- let rec aux arity = function
- | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable]
- | Cic.Appl (Cic.Lambda _ :: _) ->
- [Variable] (* maybe we should b-reduce *)
- | Cic.Appl [] -> assert false
- | Cic.Appl (hd::tl) ->
- aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
- | Cic.Cast (t,_) -> aux arity t
- | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable]
- (* I think we should CicSubstitution.subst Implicit t *)
- | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *)
- | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable]
- | Cic.Rel i -> [Bound (i, arity)]
- | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition]
- | Cic.Sort _ -> assert (arity=0); [Datatype]
- | Cic.Const _ | Cic.Var _
- | Cic.MutInd _ | Cic.MutConstruct _ as t ->
- [Constant (CicUtil.uri_of_term t, arity)]
- | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead]
- in
- aux 0
- ;;
-
- let compare e1 e2 =
- match e1,e2 with
- | Constant (u1,a1),Constant (u2,a2) ->
- let x = UriManager.compare u1 u2 in
- if x = 0 then Pervasives.compare a1 a2 else x
- | e1,e2 -> Pervasives.compare e1 e2
- ;;
-
- let string_of_path l = String.concat "." (List.map ppelem l) ;;
-end
-
-let arity_of = function
- | Constant (_,a)
- | Bound (_,a) -> a
- | _ -> 0
-;;
-
-module type DiscriminationTree =
- sig
-
- type input
- type data
- type dataset
- type constant_name
- type t
-
- val iter : t -> (constant_name path -> dataset -> unit) -> unit
-
- val empty : t
- val index : t -> input -> data -> t
- val remove_index : t -> input -> data -> t
- val in_index : t -> input -> (data -> bool) -> bool
- val retrieve_generalizations : t -> input -> dataset
- val retrieve_unifiables : t -> input -> dataset
- end
-
-module Make (I:Indexable) (A:Set.S) : DiscriminationTree
-with type constant_name = I.constant_name and type input = I.input
-and type data = A.elt and type dataset = A.t =
-
- struct
-
- module OrderedPathStringElement = struct
- type t = I.constant_name path_string_elem
- let compare = I.compare
- end
-
- type constant_name = I.constant_name
- type data = A.elt
- type dataset = A.t
- type input = I.input
-
- module PSMap = Map.Make(OrderedPathStringElement);;
-
- type key = PSMap.key
-
- module DiscriminationTree = Trie.Make(PSMap);;
-
- type t = A.t DiscriminationTree.t
-
- let empty = DiscriminationTree.empty;;
-
- let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
-
- let index tree term info =
- let ps = I.path_string_of term in
- let ps_set =
- try DiscriminationTree.find ps tree with Not_found -> A.empty
- in
- DiscriminationTree.add ps (A.add info ps_set) tree
- ;;
-
- let remove_index tree term info =
- let ps = I.path_string_of term in
- try
- let ps_set = A.remove info (DiscriminationTree.find ps tree) in
- if A.is_empty ps_set then DiscriminationTree.remove ps tree
- else DiscriminationTree.add ps ps_set tree
- with Not_found -> tree
- ;;
-
- let in_index tree term test =
- let ps = I.path_string_of term in
- try
- let ps_set = DiscriminationTree.find ps tree in
- A.exists test ps_set
- with Not_found -> false
- ;;
-
- (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
- (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
- skip all its progeny, thus you want to reach t.
-
- You need to skip as many elements as the sum of all arieties contained
- in the progeny of f.
-
- The input ariety is the one of f while the path is x.g....t
- Should be the equivalent of after_t in the literature (handbook A.R.)
- *)
- let rec skip arity path =
- if arity = 0 then path else match path with
- | [] -> assert false
- | m::tl -> skip (arity-1+arity_of m) tl
- ;;
-
- (* the equivalent of skip, but on the index, thus the list of trees
- that are rooted just after the term represented by the tree root
- are returned (we are skipping the root) *)
- let skip_root = function DiscriminationTree.Node (value, map) ->
- let rec get n = function DiscriminationTree.Node (v, m) as tree ->
- if n = 0 then [tree] else
- PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
- in
- PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
- ;;
-
- let retrieve unif tree term =
- let path = I.path_string_of term in
- let rec retrieve path tree =
- match tree, path with
- | DiscriminationTree.Node (Some s, _), [] -> s
- | DiscriminationTree.Node (None, _), [] -> A.empty
- | DiscriminationTree.Node (_, map), Variable::path when unif ->
- List.fold_left A.union A.empty
- (List.map (retrieve path) (skip_root tree))
- | DiscriminationTree.Node (_, map), node::path ->
- A.union
- (if not unif && node = Variable then A.empty else
- try retrieve path (PSMap.find node map)
- with Not_found -> A.empty)
- (try
- match PSMap.find Variable map,skip (arity_of node) path with
- | DiscriminationTree.Node (Some s, _), [] -> s
- | n, path -> retrieve path n
- with Not_found -> A.empty)
- in
- retrieve path tree
- ;;
-
- let retrieve_generalizations tree term = retrieve false tree term;;
- let retrieve_unifiables tree term = retrieve true tree term;;
- end
-;;
-
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM 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. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-
-type 'a path_string_elem =
- | Constant of 'a * int (* name, arity *)
- | Bound of int * int (* rel, arity *)
- | Variable (* arity is 0 *)
- | Proposition (* arity is 0 *)
- | Datatype (* arity is 0 *)
- | Dead (* arity is 0 *)
-;;
-
-type 'a path = ('a path_string_elem) list;;
-
-module type Indexable = sig
- type input
- type constant_name
- val compare:
- constant_name path_string_elem ->
- constant_name path_string_elem -> int
- val string_of_path : constant_name path -> string
- val path_string_of : input -> constant_name path
-end
-
-module CicIndexable : Indexable
-with type input = Cic.term and type constant_name = UriManager.uri
-
-module type DiscriminationTree =
- sig
-
- type input
- type data
- type dataset
- type constant_name
- type t
-
- val iter : t -> (constant_name path -> dataset -> unit) -> unit
-
- val empty : t
- val index : t -> input -> data -> t
- val remove_index : t -> input -> data -> t
- val in_index : t -> input -> (data -> bool) -> bool
- val retrieve_generalizations : t -> input -> dataset
- val retrieve_unifiables : t -> input -> dataset
- end
-
-
-module Make (I : Indexable) (A : Set.S) : DiscriminationTree
-with type constant_name = I.constant_name and type input = I.input
-and type data = A.elt and type dataset = A.t
-
+componentsConf.cmi:
+hExtlib.cmi:
+hMarshal.cmi:
+patternMatcher.cmi:
+hLog.cmi:
+trie.cmi:
+discrimination_tree.cmi:
+hTopoSort.cmi:
+refCounter.cmi:
+graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
hExtlib.cmo: hExtlib.cmi
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
+discrimination_tree.cmo: trie.cmi discrimination_tree.cmi
+discrimination_tree.cmx: trie.cmx discrimination_tree.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
refCounter.cmo: refCounter.cmi
+componentsConf.cmi:
+hExtlib.cmi:
+hMarshal.cmi:
+patternMatcher.cmi:
+hLog.cmi:
+trie.cmi:
+discrimination_tree.cmi:
+hTopoSort.cmi:
+refCounter.cmi:
+graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
hExtlib.cmo: hExtlib.cmi
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
+discrimination_tree.cmo: trie.cmi discrimination_tree.cmi
+discrimination_tree.cmx: trie.cmx discrimination_tree.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
refCounter.cmo: refCounter.cmi
patternMatcher.mli \
hLog.mli \
trie.mli \
+ discrimination_tree.mli \
hTopoSort.mli \
refCounter.mli \
graphvizPp.mli \
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM 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. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id$ *)
+
+type 'a path_string_elem =
+ | Constant of 'a * int (* name, arity *)
+ | Bound of int * int (* rel, arity *)
+ | Variable (* arity is 0 *)
+ | Proposition (* arity is 0 *)
+ | Datatype (* arity is 0 *)
+ | Dead (* arity is 0 *)
+;;
+
+type 'a path = ('a path_string_elem) list;;
+
+module type Indexable = sig
+ type input
+ type constant_name
+ val compare:
+ constant_name path_string_elem ->
+ constant_name path_string_elem -> int
+ val string_of_path : constant_name path -> string
+ val path_string_of : input -> constant_name path
+end
+
+let arity_of = function
+ | Constant (_,a)
+ | Bound (_,a) -> a
+ | _ -> 0
+;;
+
+module type DiscriminationTree =
+ sig
+
+ type input
+ type data
+ type dataset
+ type constant_name
+ type t
+
+ val iter : t -> (constant_name path -> dataset -> unit) -> unit
+
+ val empty : t
+ val index : t -> input -> data -> t
+ val remove_index : t -> input -> data -> t
+ val in_index : t -> input -> (data -> bool) -> bool
+ val retrieve_generalizations : t -> input -> dataset
+ val retrieve_unifiables : t -> input -> dataset
+ end
+
+module Make (I:Indexable) (A:Set.S) : DiscriminationTree
+with type constant_name = I.constant_name and type input = I.input
+and type data = A.elt and type dataset = A.t =
+
+ struct
+
+ module OrderedPathStringElement = struct
+ type t = I.constant_name path_string_elem
+ let compare = I.compare
+ end
+
+ type constant_name = I.constant_name
+ type data = A.elt
+ type dataset = A.t
+ type input = I.input
+
+ module PSMap = Map.Make(OrderedPathStringElement);;
+
+ type key = PSMap.key
+
+ module DiscriminationTree = Trie.Make(PSMap);;
+
+ type t = A.t DiscriminationTree.t
+
+ let empty = DiscriminationTree.empty;;
+
+ let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
+
+ let index tree term info =
+ let ps = I.path_string_of term in
+ let ps_set =
+ try DiscriminationTree.find ps tree with Not_found -> A.empty
+ in
+ DiscriminationTree.add ps (A.add info ps_set) tree
+ ;;
+
+ let remove_index tree term info =
+ let ps = I.path_string_of term in
+ try
+ let ps_set = A.remove info (DiscriminationTree.find ps tree) in
+ if A.is_empty ps_set then DiscriminationTree.remove ps tree
+ else DiscriminationTree.add ps ps_set tree
+ with Not_found -> tree
+ ;;
+
+ let in_index tree term test =
+ let ps = I.path_string_of term in
+ try
+ let ps_set = DiscriminationTree.find ps tree in
+ A.exists test ps_set
+ with Not_found -> false
+ ;;
+
+ (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
+ (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
+ skip all its progeny, thus you want to reach t.
+
+ You need to skip as many elements as the sum of all arieties contained
+ in the progeny of f.
+
+ The input ariety is the one of f while the path is x.g....t
+ Should be the equivalent of after_t in the literature (handbook A.R.)
+ *)
+ let rec skip arity path =
+ if arity = 0 then path else match path with
+ | [] -> assert false
+ | m::tl -> skip (arity-1+arity_of m) tl
+ ;;
+
+ (* the equivalent of skip, but on the index, thus the list of trees
+ that are rooted just after the term represented by the tree root
+ are returned (we are skipping the root) *)
+ let skip_root = function DiscriminationTree.Node (value, map) ->
+ let rec get n = function DiscriminationTree.Node (v, m) as tree ->
+ if n = 0 then [tree] else
+ PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
+ in
+ PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
+ ;;
+
+ let retrieve unif tree term =
+ let path = I.path_string_of term in
+ let rec retrieve path tree =
+ match tree, path with
+ | DiscriminationTree.Node (Some s, _), [] -> s
+ | DiscriminationTree.Node (None, _), [] -> A.empty
+ | DiscriminationTree.Node (_, map), Variable::path when unif ->
+ List.fold_left A.union A.empty
+ (List.map (retrieve path) (skip_root tree))
+ | DiscriminationTree.Node (_, map), node::path ->
+ A.union
+ (if not unif && node = Variable then A.empty else
+ try retrieve path (PSMap.find node map)
+ with Not_found -> A.empty)
+ (try
+ match PSMap.find Variable map,skip (arity_of node) path with
+ | DiscriminationTree.Node (Some s, _), [] -> s
+ | n, path -> retrieve path n
+ with Not_found -> A.empty)
+ in
+ retrieve path tree
+ ;;
+
+ let retrieve_generalizations tree term = retrieve false tree term;;
+ let retrieve_unifiables tree term = retrieve true tree term;;
+ end
+;;
+
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM 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. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+type 'a path_string_elem =
+ | Constant of 'a * int (* name, arity *)
+ | Bound of int * int (* rel, arity *)
+ | Variable (* arity is 0 *)
+ | Proposition (* arity is 0 *)
+ | Datatype (* arity is 0 *)
+ | Dead (* arity is 0 *)
+;;
+
+type 'a path = ('a path_string_elem) list;;
+
+module type Indexable = sig
+ type input
+ type constant_name
+ val compare:
+ constant_name path_string_elem ->
+ constant_name path_string_elem -> int
+ val string_of_path : constant_name path -> string
+ val path_string_of : input -> constant_name path
+end
+
+module type DiscriminationTree =
+ sig
+
+ type input
+ type data
+ type dataset
+ type constant_name
+ type t
+
+ val iter : t -> (constant_name path -> dataset -> unit) -> unit
+
+ val empty : t
+ val index : t -> input -> data -> t
+ val remove_index : t -> input -> data -> t
+ val in_index : t -> input -> (data -> bool) -> bool
+ val retrieve_generalizations : t -> input -> dataset
+ val retrieve_unifiables : t -> input -> dataset
+ end
+
+
+module Make (I : Indexable) (A : Set.S) : DiscriminationTree
+with type constant_name = I.constant_name and type input = I.input
+and type data = A.elt and type dataset = A.t
+
module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
- type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
+ type t = Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t
val empty : t
val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
val retrieve_unifiables : t -> Cic.term -> PosEqSet.t
val remove_index : t -> Equality.equality -> t
val index : t -> Equality.equality -> t
val in_index : t -> Equality.equality -> bool
- val iter : t -> (Discrimination_tree.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
+ val iter : t -> (Cic_indexable.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
end
module DT =
module PosEqSet = Set.Make(OrderedPosEquality);;
- include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet)
+ include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet)
(* DISCRIMINATION TREES *)
module PosEqSet = Set.Make(OrderedPosEquality);;
- include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet)
+ include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet)
(* DISCRIMINATION TREES *)
module type EqualityIndex =
sig
module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
- type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
+ type t = Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t
val empty : t
val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
val retrieve_unifiables : t -> Cic.term -> PosEqSet.t
val remove_index : t -> Equality.equality -> t
val index : t -> Equality.equality -> t
val in_index : t -> Equality.equality -> bool
- val iter : t -> (Discrimination_tree.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
+ val iter : t -> (Cic_indexable.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
end
module DT : EqualityIndex
with type elt = Utils.pos * Equality.equality
and type t = Equality_indexing.DT.PosEqSet.t
type t =
- Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
+ Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t
end
val check_for_duplicates : Cic.metasenv -> string -> unit
let compare = Pervasives.compare
end
module S = Set.Make(Codomain)
-module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S)
+module TI = Discrimination_tree.Make(Cic_indexable.CicIndexable)(S)
type universe = TI.t
let empty = TI.empty ;;
projects / helm.git / commitdiff