Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
;;
+let pp_goal_set msg goals names =
+ let active_goals, passive_goals = goals in
+ prerr_endline ("////" ^ msg);
+ prerr_endline ("ACTIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ active_goals)));
+ prerr_endline ("PASSIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ passive_goals)))
+;;
+
let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
let names = names_of_context ctx in
+(*
Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
*)
match ty with
match Indexing.unification env table goal_equation with
| Some (subst, equality, swapped ) ->
prerr_endline
- ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
- prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+ ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+ prerr_endline
+ ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+ prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
| (Some p) as ok -> ok
;;
-let simplify_goal_set env goals passive active =
+let simplify_goal_set env goals ?passive active =
let active_goals, passive_goals = goals in
let find (_,_,g) where =
List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
let simplified =
List.fold_left
(fun acc goal ->
- match simplify_goal env goal ~passive active with
+ match simplify_goal env goal ?passive active with
| changed, g ->
if changed then prerr_endline "???????????????cambiato ancora";
if find g acc then acc else g::acc)
let infer_goal_set env active goals =
let active_goals, passive_goals = goals in
let rec aux = function
- | [] -> goals
+ | [] -> active_goals, []
| hd::tl ->
let changed,selected = simplify_goal env hd active in
if changed then
prerr_endline ("--------------- goal semplificato");
let (_,_,t1) = selected in
- if (List.exists
- (fun (_,_,t) ->
- Equality.meta_convertibility t t1)
- active_goals) then aux tl
- else
- let passive_goals = tl in
- let new_passive_goals =
- if Utils.metas_of_term t1 = [] then passive_goals
- else
- let new' =
- Indexing.superposition_left env (snd active) selected in
- passive_goals @ new'
+ let already_in =
+ List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ active_goals
in
- selected::active_goals, new_passive_goals
+ if already_in then
+ aux tl
+ else
+ let passive_goals = tl in
+ let new_passive_goals =
+ if Utils.metas_of_term t1 = [] then passive_goals
+ else
+ let newmaxmeta,new' =
+ Indexing.superposition_left env (snd active) selected
+ !maxmeta
+ in
+ maxmeta := newmaxmeta;
+ passive_goals @ new'
+ in
+ selected::active_goals, new_passive_goals
in
aux passive_goals
;;
let infer_goal_set_with_current env current goals =
let active_goals, passive_goals = goals in
- let _,table,_ = build_table [current] in
- active_goals,
+ let l,table,_ = build_table [current] in
+ let active_goals, _ =
+ simplify_goal_set env goals (l,table)
+ in
+ active_goals,
List.fold_left
(fun acc g ->
- let new' = Indexing.superposition_left env table g in
+ let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+ maxmeta := newmaxmeta;
acc @ new')
passive_goals active_goals
;;
prerr_endline (Printf.sprintf "Current goal = %s\n"
(CicPp.pp g names)))
(fst goals);
+ List.iter
+ (fun _,_,g ->
+ prerr_endline (Printf.sprintf "Passive goal = %s\n"
+ (CicPp.pp g names)))
+ (snd goals);
prerr_endline (Printf.sprintf "Selected = %s\n"
(Equality.string_of_equality ~env current))
in
let new' = infer eq_uri env current active in
prerr_endline "infer goal";
let goals = infer_goal_set_with_current env current goals in
+(*
+ match check_if_goals_set_is_solved env active goals with
+ | Some p ->
+ prerr_endline
+ (Printf.sprintf "Found a proof in: %f\n"
+ (Unix.gettimeofday() -. initial_time));
+ ParamodulationSuccess p
+ | None ->
+*)
let active =
let al, tbl = active in
al @ [current], Indexing.index tbl current
let goals =
let a,b,_ = build_table new' in
let _ = <:start<simplify_goal_set new>> in
- let rc = simplify_goal_set env goals passive (a,b) in
+ let rc = simplify_goal_set env goals ~passive (a,b) in
let _ = <:stop<simplify_goal_set new>> in
rc
in
let al, tbl = active in
al @ [current], Indexing.index tbl current
in
+ (* alla fine new' contiene anche le attive semplificate!
+ * quindi le aggiungo alle passive insieme alle new *)
let rec simplify new' active passive =
let new' = forward_simplify_new eq_uri env new' ~passive active in
let active, passive, newa, retained, pruned =
| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
+let eq_and_ty_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri,t
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
let saturate
+ caso_strano
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
reset_refs ();
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goalno) (maxm+2)
+ find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
in
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
*)
let goals = make_goal_set goal in
let max_iterations = 10000 in
- let max_time = Unix.gettimeofday () +. 600. (* minutes *) in
+ let max_time = Unix.gettimeofday () +. 300. (* minutes *) in
given_clause
eq_uri env goals theorems passive active max_iterations max_time
in
prerr_endline
(Equality.pp_proof names goalproof newproof subsumption_subst
subsumption_id type_of_goal);
- prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
prerr_endline "ENDOFPROOFS";
(* generation of the CIC proof *)
let side_effects =
Equality.build_goal_proof
eq_uri goalproof initial type_of_goal side_effects
in
+ prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
(*prerr_endline (CicPp.pp goal_proof names);*)
let env = (metasenv, context, ugraph) 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 false dbd context (proof, goal') (maxm+2) in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
let equalities = (* equalities @ *) library_equalities in
let eq_uri = eq_of_goal goal in
let eq_indexes, equalities, maxm = find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2)
+ find_library_equalities false dbd context (proof, goal') (maxm+2)
in
let library_equalities = List.map snd library_equalities in
maxmeta := maxm+2; (* TODO ugly!! *)
;;
let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
- let module I = Inference in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let eq_uri = eq_of_goal ty in
Inference.find_equalities context proof
in
let lib_eq_uris, library_equalities, maxm =
- I.find_library_equalities dbd context (proof, goal) (maxm+2) in
+ Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in
if library_equalities = [] then prerr_endline "VUOTA!!!";
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
;;
+let rec find_in_ctx i name = function
+ | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
+ | Some (Cic.Name name', _)::tl when name = name' -> i
+ | _::tl -> find_in_ctx (i+1) name tl
+;;
+
+let rec position_of i x = function
+ | [] -> assert false
+ | j::tl when j <> x -> position_of (i+1) x tl
+ | _ -> i
+;;
+
+(* Syntax:
+ * auto superposition target = NAME
+ * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
+ *
+ * - if table is omitted no superposition will be performed
+ * - if demod_table is omitted no demodulation will be prformed
+ * - subterms_only is passed to Indexing.superposition_right
+ *
+ * lists are coded using _ (example: H_H1_H2)
+ *)
+let superposition_tac ~target ~table ~subterms_only ~demod_table status =
+ reset_refs();
+ Indexing.init_index ();
+ let proof,goalno = status in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri,tty = eq_and_ty_of_goal ty in
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let names = names_of_context context in
+ let eq_index, equalities, maxm = find_equalities context proof in
+ let eq_what =
+ let what = find_in_ctx 1 target context in
+ List.nth equalities (position_of 0 what eq_index)
+ in
+ let eq_other =
+ if table <> "" then
+ let other =
+ let others = Str.split (Str.regexp "_") table in
+ List.map (fun other -> find_in_ctx 1 other context) others
+ in
+ List.map
+ (fun other -> List.nth equalities (position_of 0 other eq_index))
+ other
+ else
+ []
+ in
+ let index = List.fold_left Indexing.index Indexing.empty eq_other in
+ let maxm, eql =
+ if table = "" then maxm,[eq_what] else
+ Indexing.superposition_right
+ ~subterms_only eq_uri maxm env index eq_what
+ in
+ prerr_endline ("Superposition right:");
+ prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
+ prerr_endline ("\n table: ");
+ List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other;
+ prerr_endline ("\n result: ");
+ List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+ prerr_endline ("\n result (cut&paste): ");
+ List.iter
+ (fun e ->
+ let t = Equality.term_of_equality eq_uri e in
+ prerr_endline (CicPp.pp t names))
+ eql;
+ prerr_endline ("\n result proofs: ");
+ List.iter (fun e ->
+ prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+ let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+ Subst.ppsubst s ^ "\n" ^
+ CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
+ if demod_table <> "" then
+ begin
+ let demod =
+ let demod = Str.split (Str.regexp "_") demod_table in
+ List.map (fun other -> find_in_ctx 1 other context) demod
+ in
+ let eq_demod =
+ List.map
+ (fun demod -> List.nth equalities (position_of 0 demod eq_index))
+ demod
+ in
+ let table = List.fold_left Indexing.index Indexing.empty eq_demod in
+ let maxm,eql =
+ List.fold_left
+ (fun (maxm,acc) e ->
+ let maxm,eq =
+ Indexing.demodulation_equality
+ eq_uri maxm env table Utils.Positive e
+ in
+ maxm,eq::acc)
+ (maxm,[]) eql
+ in
+ let eql = List.rev eql in
+ prerr_endline ("\n result [demod]: ");
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+ prerr_endline ("\n result [demod] (cut&paste): ");
+ List.iter
+ (fun e ->
+ let t = Equality.term_of_equality eq_uri e in
+ prerr_endline (CicPp.pp t names))
+ eql;
+ end;
+ proof,[goalno]
+;;
+
let get_stats () =
<:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
- Equality.get_stats ();;
+ Equality.get_stats ()
+;;
projects / helm.git / blobdiff