DEPOBJS = \
$(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
+ trie.ml \
path_indexing.ml \
discrimination_tree.ml \
test_indexing.ml \
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo,
- C.Implicit None
+ Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
(* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
(* proof; other; proof']) *)
in
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
- newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
+
+ let res =
+ (C.Implicit None, (eq_ty, left, right, ordering), newmetasenv, newargs)
+ in
+ Inference.store_proof res newproof;
+ newmeta, res
in
(* let build_newtarget = *)
(* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo',
- C.Implicit None
+ Inference.ProofBlock (s, eq_URI, t', eq_found, target)
(* (\* M. *\)apply_subst s *)
(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
(* proof; other; proof']) *)
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
- (newproof, (eq_ty, left, right, neworder), [], [])
+
+ let res = (C.Implicit None, (eq_ty, left, right, neworder), [], []) in
+ Inference.store_proof res newproof;
+ res
in
(* let build_new = *)
(* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo',
- C.Implicit None
+ Inference.ProofBlock (s, eq_URI, t', eq_found, target)
(* (\* M. *\)apply_subst s *)
(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
(* eqproof; other; proof']) *)
let neworder = !Utils.compare_terms left right
and newmenv = newmetas @ menv'
and newargs = args @ args' in
- let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs)
+ let eq' =
+ (C.Implicit None, (eq_ty, left, right, neworder), newmenv, newargs)
and env = (metasenv, context, ugraph) in
let newm, eq' = Inference.fix_metas !maxmeta eq' in
newm, eq'
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
+
+ Inference.store_proof newequality newproof;
newequality
in
open Utils;;
+type equality =
+ Cic.term * (* proof *)
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+;;
+
+
+type proof =
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+ equality
+ | NoProof
+;;
+
+
let string_of_equality ?env =
match env with
| None -> (
;;
+let prooftable = Hashtbl.create 2001;;
+
+let store_proof equality proof =
+ if not (Hashtbl.mem prooftable equality) then
+ Hashtbl.add prooftable equality proof
+;;
+
+
+let delete_proof equality =
+(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ Hashtbl.remove prooftable equality
+;;
+
+
+let rec build_term_proof equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof for %s\n"
+ (string_of_equality equality);
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+(* (string_of_equality eq) (string_of_equality eq'); *)
+(* print_newline (); *)
+ let proof' = build_term_proof eq in
+ let eqproof = build_term_proof eq' in
+ let _, (ty, what, other, _), menv', args' = eq in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+;;
+
+
let rec metas_of_term = function
| Cic.Meta (i, c) -> [i]
| Cic.Var (_, ens)
;;
-type equality =
- Cic.term * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term * (* right side *)
- Utils.comparison) * (* ordering *)
- Cic.metasenv * (* environment for metas *)
- Cic.term list (* arguments *)
-;;
-
-
let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
let module C = Cic in
let module S = CicSubstitution in
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
let o = !Utils.compare_terms t1 t2 in
- Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
+ let e = (p, (ty, t1, t2, o), newmetas, args) in
+ store_proof e (BasicProof p);
+ Some e, (newmeta+1)
| _ -> None, newmeta
)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
let t1 = S.lift index t1
and t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
- Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
+ let e = (C.Rel index, (ty, t1, t2, o), [], []) in
+ store_proof e (BasicProof (C.Rel index));
+ Some e, (newmeta+1)
| _ -> None, newmeta
in (
match do_find context term with
let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
let o = !Utils.compare_terms t1 t2 in
- (proof, (ty, t1, t2, o), [], [])
+ let e = (proof, (ty, t1, t2, o), [], []) in
+ store_proof e (BasicProof proof);
+ e
+(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
raise TermIsNotAnEquality
;;
Utils.comparison) * (* ordering *)
Cic.metasenv * (* environment for metas *)
Cic.term list (* arguments *)
-;;
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+type proof =
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+ equality
+ | NoProof
+
+
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
exception MatchingFailure
val extract_differing_subterms:
Cic.term -> Cic.term -> (Cic.term * Cic.term) option
+
+
+val store_proof: equality -> proof -> unit
+
+val delete_proof: equality -> unit
+
+val build_term_proof: equality -> Cic.term
type result =
| Failure
- | Success of Cic.term option * environment
+ | Success of Inference.equality option * environment
;;
let contains_empty env (negative, positive) =
let metasenv, context, ugraph = env in
try
- let (proof, _, _, _) =
+ let found =
List.find
(fun (proof, (ty, left, right, ordering), m, a) ->
fst (CicReduction.are_convertible context left right ugraph))
negative
in
- true, Some proof
+ true, Some found
with Not_found ->
false, None
;;
Indexing.demodulation !maxmeta env table current in
maxmeta := newmeta;
if is_identity env newcurrent then
- if sign = Negative then Some (sign, newcurrent) else None
+ if sign = Negative then Some (sign, newcurrent)
+ else (Inference.delete_proof newcurrent; None)
else
Some (sign, newcurrent)
in
if ok then res else None
| Some (Positive, c) ->
if Indexing.in_index active_table c then
- None
+ (Inference.delete_proof c; None)
else
match passive_table with
| None -> res
| Some passive_table ->
- if Indexing.in_index passive_table c then None else res
+ if Indexing.in_index passive_table c then
+ (Inference.delete_proof c; None)
+ else res
(* | Some (s, c) -> if find_duplicate s c all then None else res *)
let new_pos_set =
List.fold_left
(fun s e ->
- if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+ if not (Inference.is_identity env e) then
+ if EqualitySet.mem e s then
+ (Inference.delete_proof e; s)
+ else
+ EqualitySet.add e s
+ else
+ (Inference.delete_proof e; s))
EqualitySet.empty new_pos
in
let new_pos = EqualitySet.elements new_pos_set in
let is_duplicate =
match passive_table with
- | None -> (fun e -> not (Indexing.in_index active_table e))
+ | None ->
+ (fun e ->
+ let ok = not (Indexing.in_index active_table e) in
+ if not ok then Inference.delete_proof e;
+ ok)
| Some passive_table ->
- (fun e -> not ((Indexing.in_index active_table e) ||
- (Indexing.in_index passive_table e)))
+ (fun e ->
+ let ok = not ((Indexing.in_index active_table e) ||
+ (Indexing.in_index passive_table e)) in
+ if not ok then Inference.delete_proof e;
+ ok)
in
new_neg, List.filter is_duplicate new_pos
let active, newa =
List.fold_right
(fun (s, eq) (res, tbl) ->
- if (is_identity env eq) || (find eq res) then
+ if List.mem (s, eq) res then
res, tbl
+ else if (is_identity env eq) || (find eq res) then (
+ Inference.delete_proof eq;
+ res, tbl
+ ) (* else if (find eq res) then *)
+(* res, tbl *)
else
(s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
active_list ([], Indexing.empty_table ()),
List.fold_right
(fun (s, eq) (n, p) ->
- if (s <> Negative) && (is_identity env eq) then
+ if (s <> Negative) && (is_identity env eq) then (
+ Inference.delete_proof eq;
(n, p)
- else
+ ) else
if s = Negative then eq::n, p
else n, eq::p)
newa ([], [])
Printf.printf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current);
print_newline ();
- let proof, _, _, _ = current in
- Success (Some proof, env)
+ Success (Some current, env)
) else (
print_endline "\n================================================";
Printf.printf "selected: %s %s"
let t2 = Unix.gettimeofday () in
infer_time := !infer_time +. (t2 -. t1);
- let res, proof = contains_empty env new' in
+ let res, goal = contains_empty env new' in
if res then
- Success (proof, env)
+ Success (goal, env)
else
let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' (* ~passive *) active in
(* (EqualitySet.elements ps)))); *)
(* print_newline (); *)
given_clause env passive active
- | true, proof ->
- Success (proof, env)
+ | true, goal ->
+ Success (goal, env)
)
;;
Printf.printf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current);
print_newline ();
- let proof, _, _, _ = current in
- Success (Some proof, env)
+ Success (Some current, env)
) else (
print_endline "\n================================================";
Printf.printf "selected: %s %s"
| false, _ ->
let passive = add_to_passive passive new' in
given_clause_fullred env passive active
- | true, proof ->
- Success (proof, env)
+ | true, goal ->
+ Success (goal, env)
)
;;
match res with
| Failure ->
Printf.printf "NO proof found! :-(\n\n"
- | Success (Some proof, env) ->
- Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
- (PP.pp proof (names_of_context context))
- (finish -. start);
-(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *)
-(* " demodulate: %.9f\n subsumption: %.9f\n") *)
-(* fs_time_info.build_all fs_time_info.demodulate *)
-(* fs_time_info.subsumption; *)
+ | Success (Some goal, env) ->
+ Printf.printf "OK, found a proof!\n";
+ let proof = Inference.build_term_proof goal in
+ print_endline (PP.pp proof (names_of_context context));
+ print_endline (string_of_float (finish -. start));
| Success (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
projects / helm.git / commitdiff