let other' = U.guarded_simpl context (apply_subst s other) in *)
let other' = apply_subst s other in
let order = cmp c' other' in
- let names = U.names_of_context context in
if order = U.Gt then
res
else
let c' = apply_subst s c
and other' = apply_subst s other in
let order = cmp c' other' in
- let names = U.names_of_context context in
if order <> U.Lt && order <> U.Le then
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
let rec demodulation_aux ?(typecheck=false)
metasenv context ugraph table lift_amount term =
+ (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
+
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let newgoal, newproof =
(* qua *)
let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
- let t' =
- let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
- incr sup_r_counter;
- let l, r =
- if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- (name, ty, S.lift 1 eq_ty, l, r)
- in
let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
incr sup_r_counter;
let bo'' =
and newargs = args @ args' in
let eq' =
let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
- and env = (metasenv, context, ugraph) in
+ (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
let newm, eq' = Inference.fix_metas !maxmeta eq' in
newm, eq'
in
let maxmeta = ref newmeta in
let proof, metas, term = goal in
let metasenv' = metasenv @ metas in
+ Printf.eprintf "siam qua\n";
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
| Inference.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
Inference.ProofGoalBlock (pb, parent_proof)
- | (Inference.SubProof (term, meta_index, p) as subproof) ->
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "replacing %s" *)
-(* (Inference.string_of_proof subproof))); *)
+ | Inference.SubProof (term, meta_index, p) ->
Inference.SubProof (term, meta_index, repl p)
| _ -> assert false
in repl proof
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
!maxmeta, (newproof, newmetasenv, newterm)
in
+ Printf.eprintf "bum0\n";
let res =
demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
in
+ Printf.eprintf "bum\n";
match res with
| Some t ->
let newmeta, newgoal = build_newgoal t in
if Inference.meta_convertibility term newg then
newmeta, newgoal
else
- demodulation_goal newmeta env table newgoal
+ begin
+ Printf.eprintf "reducing %s to %s \n"
+ (CicPp.ppterm term) (CicPp.ppterm newg);
+ demodulation_goal newmeta env table newgoal
+ end
| None ->
newmeta, goal
;;
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let proof, metas, term = theorem in
let term, termty, metas = theorem in
let metasenv' = metasenv @ metas in
-
+
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
Inference.BasicProof term)
in
(Inference.build_proof_term newproof, bo)
- in
+ in
+
let m = Inference.metas_of_term newterm in
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
!maxmeta, (newterm, newty, newmetasenv)
let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
let module I = Inference in
let curi,metasenv,pbo,pty = proof in
- let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let eq_indexes, equalities, maxm = I.find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
I.find_library_equalities dbd context (proof, goal) (maxm+2) in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof goalterm, [], goalterm in
+ let initgoal = Inference.BasicProof goalterm, [], ty in
let equalities = equalities @ library_equalities in
let table =
List.fold_left
(fun tbl eq -> index tbl eq)
empty equalities
in
- let _,(newproof, newty, newmetasenv) = demodulation_goal
+ let newmeta,(newproof,newmetasenv, newty) = demodulation_goal
maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
in
- let proofterm = Inference.build_proof_term newproof in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- initialstatus
+ if newmeta != maxm then
+ begin
+ let opengoal = Cic.Meta(maxm,irl) in
+ let proofterm =
+ Inference.build_proof_term ~noproof:opengoal newproof in
+ prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context));
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv));
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
+ end
+ else raise (ProofEngineTypes.Fail (lazy "no progress"))
let demodulate_tac ~dbd ~pattern =
ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
Cic.term list (* arguments *)
and proof =
- | NoProof
+ | NoProof (* term is the goal missing a proof *)
| BasicProof of Cic.term
| ProofBlock of
Cic.substitution * UriManager.uri *
let rec string_of_proof = function
- | NoProof -> "NoProof"
+ | NoProof -> "NoProof "
| BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
| SubProof (t, i, p) ->
Printf.sprintf "SubProof(%s, %s, %s)"
;;
-let build_proof_term proof =
+let build_proof_term ?(noproof=Cic.Implicit None) proof =
let rec do_build_proof proof =
match proof with
| NoProof ->
Printf.fprintf stderr "WARNING: no proof!\n";
- Cic.Implicit None
+ noproof
| BasicProof term -> term
| ProofGoalBlock (proofbit, proof) ->
print_endline "found ProofGoalBlock, going up...";
let meta_convertibility_aux table t1 t2 =
let module C = Cic in
- let print_table t =
- String.concat ", "
- (List.map
- (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
- in
let rec aux ((table_l, table_r) as table) t1 t2 =
match t1, t2 with
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
let meta_convertibility t1 t2 =
- let f t =
- String.concat ", "
- (List.map
- (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
- in
if t1 = t2 then
true
else
try
- let l, r = meta_convertibility_aux ([], []) t1 t2 in
+ ignore(meta_convertibility_aux ([], []) t1 t2);
true
with NotMetaConvertible ->
false
let candidates =
List.fold_left
(fun l uri ->
- let suri = UriManager.string_of_uri uri in
if UriManager.UriSet.mem uri blacklist then
l
else
;;
-let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
let table = Hashtbl.create (List.length args) in
let newargs, newmeta =
List.fold_right
(Hashtbl.copy table)
in
let rec fix_proof = function
- | NoProof -> NoProof
+ | NoProof -> NoProof
| BasicProof term -> BasicProof (repl term)
| ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
let subst' =
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-let is_identity ((metasenv, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), menv, _) as equality) ->
+let is_identity (metasenv, context, ugraph) = function
+ | (_, _, (ty, left, right, _), menv, _) ->
(left = right ||
(* (meta_convertibility left right) || *)
(fst (CicReduction.are_convertible
Cic.term list (* arguments *)
and proof =
- | NoProof
+ | NoProof (* no proof *)
| BasicProof of Cic.term (* already a proof of a goal *)
| ProofBlock of (* proof of a rewrite step *)
Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
(** builds the Cic.term encoded by proof *)
-val build_proof_term: proof -> Cic.term
+val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
val string_of_proof: proof -> string
let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-Utils.compare_terms := Utils.rpo;;
+(* Utils.compare_terms := Utils.rpo;; *)
(* Utils.compare_terms := Utils.nonrec_kbo;; *)
(* Utils.compare_terms := Utils.ao;; *)
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-
-let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality (_, _, (_, left, right, _), _, _) =
let m1 = symbols_of_term left in
let m =
TermMap.fold
m
;;
-
module OrderedEquality = struct
type t = Inference.equality
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = active_list @ pl in
let t2 = Unix.gettimeofday () in
fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
let demodulate table goal =
let newmeta, newgoal =
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
let a_theorems, p_theorems = theorems in
let demodulate table theorem =
let newmeta, newthm =
let aux (goal, r) tl =
let propagate_subst subst (proof, metas, term) =
let rec repl = function
- | NoProof -> NoProof
+ | NoProof -> NoProof
| BasicProof t ->
BasicProof (CicMetaSubst.apply_subst subst t)
| ProofGoalBlock (p, pb) ->
al @ [(sign, current)], Indexing.index tbl current
in
let passive = add_to_passive passive new' in
- let (_, ns), (_, ps), _ = passive in
given_clause dbd env goals theorems passive active
| true, goal ->
let proof =
let init () = ();;
-(* UGLY SIDE EFFECT...
-if connect_to_auto then (
- AutoTactic.paramodulation_tactic := saturate;
- AutoTactic.term_is_equality := Inference.term_is_equality;
-);;
-*)
-
let retrieve_and_print dbd term metasenv ugraph =
let module C = Cic in
let module T = CicTypeChecker in
in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
- let goal = Inference.BasicProof new_meta_goal, [], goal in
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2)
- in
+ find_library_equalities dbd context (proof, goal') (maxm+2) in
let t2 = Unix.gettimeofday () in
- maxmeta := maxm+2;
- let equalities =
- let equalities = (* equalities @ *) library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "\n\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
-(* Printf.sprintf "%s: %s" *)
- (UriManager.string_of_uri u)
-(* (string_of_equality e) *)
- )
- equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let (u, e) = e in
- let active = List.map (fun (u, e) -> (Positive, e))
- (others @ others_simpl) in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env (Positive, e) (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> (u, (snd e))::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
- let res =
- List.rev (simpl (*(Positive,*) hd others [])
- in
- debug_print
- (lazy
- (Printf.sprintf "\nequalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
- Printf.sprintf "%s: %s"
- (UriManager.string_of_uri u)
- (string_of_equality e)
- )
- res))));
- res
+ maxmeta := maxm+2;
+ let equalities = (* equalities @ *) library_equalities in
+ debug_print
+ (lazy
+ (Printf.sprintf "\n\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let (u, e) = e in
+ let active = List.map (fun (u, e) -> (Positive, e))
+ (others @ others_simpl) in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
in
- debug_print
- (lazy
- (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+ let res = forward_simplify env (Positive, e) (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, (snd e))::others_simpl
+ )
+ in
+ let equalities =
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (string_of_equality e)
+ )
+ res))));
+ res in
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
;;
ty
in
let env = (metasenv, context, ugraph) in
- let t1 = Unix.gettimeofday () in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
let equalities =
(List.map
(string_of_equality ~env) equalities));
print_endline "--------------------------------------------------";
- let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
if !time_limit < 1. then time_limit := 60.;
let ra, rp =
saturate_equations env goal (fun e -> true) passive active
in
- let finish = Unix.gettimeofday () in
let initial =
List.fold_left (fun s e -> EqualitySet.add e s)
EqualitySet.empty equalities
in
- let addfun s e = EqualitySet.add e s
- (*
+ let addfun s e =
if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
- *)
in
let passive =
else
begin
prerr_endline ("t1 = "^(CicPp.ppterm t1));
- prerr_endline ("t2 = "^(CicPp.ppterm t2)); flush;
+ prerr_endline ("t2 = "^(CicPp.ppterm t2));
assert false
end
with
(* settable by the user... *)
-(* let compare_terms = ref nonrec_kbo;; *)
+let compare_terms = ref nonrec_kbo;;
(* let compare_terms = ref ao;; *)
-let compare_terms = ref rpo;;
+(* let compare_terms = ref rpo;; *)
let guarded_simpl context t = t
(*
projects / helm.git / commitdiff