| ParamodulationSuccess of Inference.proof option * environment
;;
+type goal = proof * Cic.metasenv * Cic.term;;
+
+type theorem = Cic.term * Cic.term * Cic.metasenv;;
+
(*
let symbols_of_equality (_, (_, left, right), _, _) =
((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
;;
+
+let make_goals goal =
+ let active = []
+ and passive = [0, [goal]] in
+ active, passive
+;;
+
+
+let make_theorems theorems =
+ theorems, []
+(* let active = [] *)
+(* and passive = theorems in *)
+(* active, passive *)
+;;
+
+
+let activate_goal (active, passive) =
+ match passive with
+ | goal_conj::tl -> true, (goal_conj::active, tl)
+ | [] -> false, (active, passive)
+;;
+
+
+let activate_theorem (active, passive) =
+ match passive with
+ | theorem::tl -> true, (theorem::active, tl)
+ | [] -> false, (active, passive)
+;;
+
let simplify_goal env goal ?passive (active_list, active_table) =
let pl, passive_table =
let newmeta, newgoal =
Indexing.demodulation_goal !maxmeta env table goal in
maxmeta := newmeta;
- newgoal
+ goal != newgoal, newgoal
in
- let goal =
+ let changed, goal =
match passive_table with
| None -> demodulate active_table goal
| Some passive_table ->
- let goal = demodulate active_table goal in
- demodulate passive_table goal
+ let changed, goal = demodulate active_table goal in
+ let changed', goal = demodulate passive_table goal in
+ (changed || changed'), goal
in
- let _ =
- let p, _, t = goal in
- debug_print
- (lazy
- (Printf.sprintf "Goal after demodulation: %s, %s"
- (string_of_proof p) (CicPp.ppterm t)))
- in
- goal
+(* let _ = *)
+(* let p, _, t = goal in *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "Goal after demodulation: %s, %s" *)
+(* (string_of_proof p) (CicPp.ppterm t))) *)
+(* in *)
+ changed, goal
;;
let simplify_goals env goals ?passive active =
- List.map
- (fun (d, gl) ->
- let gl = List.map (fun g -> simplify_goal env g ?passive active) gl in
- d, gl)
- goals
+ let a_goals, p_goals = goals in
+ let p_goals =
+ List.map
+ (fun (d, gl) ->
+ let gl =
+ List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
+ d, gl)
+ p_goals
+ in
+ let goals =
+ List.fold_left
+ (fun (a, p) (d, gl) ->
+ let changed = ref false in
+ let gl =
+ List.map
+ (fun g ->
+ let c, g = simplify_goal env g ?passive active in
+ changed := !changed || c; g) gl in
+ if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
+ ([], p_goals) a_goals
+ in
+ goals
;;
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 =
Indexing.demodulation_theorem !maxmeta env table theorem in
maxmeta := newmeta;
- newthm
+ theorem != newthm, newthm
in
+ let foldfun table (a, p) theorem =
+ let changed, theorem = demodulate table theorem in
+ if changed then (a, theorem::p) else (theorem::a, p)
+ in
+ let mapfun table theorem = snd (demodulate table theorem) in
match passive_table with
- | None -> List.map (demodulate active_table) theorems
+ | None ->
+ let p_theorems = List.map (mapfun active_table) p_theorems in
+ List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
+(* List.map (demodulate active_table) theorems *)
| Some passive_table ->
- let theorems = List.map (demodulate active_table) theorems in
- List.map (demodulate passive_table) theorems
+ let p_theorems = List.map (mapfun active_table) p_theorems in
+ let p_theorems, a_theorems =
+ List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
+ let p_theorems = List.map (mapfun passive_table) p_theorems in
+ List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
+(* let theorems = List.map (demodulate active_table) theorems in *)
+(* List.map (demodulate passive_table) theorems *)
;;
let proof, metas, term = goal in
debug_print
(lazy
- (Printf.sprintf "apply_to_goal with goal: %s, %s"
- (string_of_proof proof) (CicPp.ppterm term)));
+ (Printf.sprintf "apply_to_goal with goal: %s"
+ (* (string_of_proof proof) *)(CicPp.ppterm term)));
let status =
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
in
debug_print
(lazy
- (Printf.sprintf "new sub goal: %s, %s"
- (string_of_proof p') (CicPp.ppterm ty)));
+ (Printf.sprintf "new sub goal: %s"
+ (* (string_of_proof p') *)(CicPp.ppterm ty)));
(p', menv, ty))
newgoals
in
+ let goals =
+ let weight t =
+ let w, m = weight_of_term t in
+ w + 2 * (List.length m)
+ in
+ List.sort
+ (fun (_, _, t1) (_, _, t2) ->
+ Pervasives.compare (weight t1) (weight t2))
+ goals
+ in
(* debug_print *)
(* (lazy *)
(* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *)
let rec aux = function
| goal::tl ->
let propagate_subst subst (proof, metas, term) =
- debug_print
- (lazy
- (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n"
- (print_subst subst) (string_of_proof proof)
- (CicPp.ppterm term)));
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" *)
+(* (print_subst subst) (string_of_proof proof) *)
+(* (CicPp.ppterm term))); *)
let rec repl = function
| NoProof -> NoProof
| BasicProof t ->
BasicProof (CicMetaSubst.apply_subst subst t)
| ProofGoalBlock (p, pb) ->
- debug_print (lazy "HERE");
+(* debug_print (lazy "HERE"); *)
let pb' = repl pb in
ProofGoalBlock (p, pb')
| SubProof (t, i, p) ->
let t' = CicMetaSubst.apply_subst subst t in
- debug_print
- (lazy
- (Printf.sprintf
- "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n"
- i (CicPp.ppterm t) (print_subst subst)
- (CicPp.ppterm t')));
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf *)
+(* "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" *)
+(* i (CicPp.ppterm t) (print_subst subst) *)
+(* (CicPp.ppterm t'))); *)
let p = repl p in
SubProof (t', i, p)
| ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
| `No -> `No (depth, goals)
| `GoOn sl (* (subst, gl) *) ->
(* let tl = List.map (propagate_subst subst) tl in *)
- debug_print (lazy "GO ON!!!");
+(* debug_print (lazy "GO ON!!!"); *)
let l =
List.map
(fun (s, gl) ->
(depth+1, gl @ (List.map (propagate_subst s) tl))) sl
in
- debug_print
- (lazy
- (Printf.sprintf "%s\n"
- (String.concat "; "
- (List.map
- (fun (s, gl) ->
- (Printf.sprintf "[%s]"
- (String.concat "; "
- (List.map
- (fun (p, _, g) ->
- (Printf.sprintf "<%s, %s>"
- (string_of_proof p)
- (CicPp.ppterm g))) gl)))) l))));
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "%s\n" *)
+(* (String.concat "; " *)
+(* (List.map *)
+(* (fun (s, gl) -> *)
+(* (Printf.sprintf "[%s]" *)
+(* (String.concat "; " *)
+(* (List.map *)
+(* (fun (p, _, g) -> *)
+(* (Printf.sprintf "<%s, %s>" *)
+(* (string_of_proof p) *)
+(* (CicPp.ppterm g))) gl)))) l)))); *)
`GoOn l (* (depth+1, gl @ tl) *)
| `Ok (subst, gl) ->
if tl = [] then
in
true, GoalsSet.singleton newgoals
| `GoOn newgoals ->
- let print_set set msg =
- debug_print
- (lazy
- (Printf.sprintf "%s:\n%s" msg
- (String.concat "\n"
- (GoalsSet.fold
- (fun (d, gl) l ->
- let gl' =
- List.map (fun (_, _, t) -> CicPp.ppterm t) gl
- in
- let s =
- Printf.sprintf "%d, [%s]" d
- (String.concat "; " gl')
- in
- s::l) set []))))
- in
- let set = add_to set (goals::tl) in
+(* let print_set set msg = *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "%s:\n%s" msg *)
+(* (String.concat "\n" *)
+(* (GoalsSet.fold *)
+(* (fun (d, gl) l -> *)
+(* let gl' = *)
+(* List.map (fun (_, _, t) -> CicPp.ppterm t) gl *)
+(* in *)
+(* let s = *)
+(* Printf.sprintf "%d, [%s]" d *)
+(* (String.concat "; " gl') *)
+(* in *)
+(* s::l) set [])))) *)
+(* in *)
+
+(* let r, s = *)
+(* try aux set tl with SearchSpaceOver -> false, GoalsSet.empty *)
+(* in *)
+(* if r then *)
+(* r, s *)
+(* else *)
+
+ let set' = add_to set (goals::tl) in
(* print_set set "SET BEFORE"; *)
- let n = GoalsSet.cardinal set in
- let set = add_to set newgoals in
+(* let n = GoalsSet.cardinal set in *)
+ let set' = add_to set' newgoals in
(* print_set set "SET AFTER"; *)
- let m = GoalsSet.cardinal set in
+(* let m = GoalsSet.cardinal set in *)
(* if n < m then *)
- false, set
+ false, set'
(* else *)
(* let _ = print_set set "SET didn't change" in *)
(* aux set tl *)
;;
-let rec given_clause env goals theorems passive active =
+let apply_goal_to_theorems dbd env theorems active goals =
+(* let theorems, _ = theorems in *)
+ let context_hyp, library_thms = theorems in
+ let thm_uris =
+ List.fold_left
+ (fun s (u, _, _, _) -> UriManager.UriSet.add u s)
+ UriManager.UriSet.empty library_thms
+ in
+ let a_goals, p_goals = goals in
+ let goal = List.hd a_goals in
+ let rec aux = function
+ | [] -> false, (a_goals, p_goals)
+ | theorem::tl ->
+ let res = apply_to_goal_conj env [theorem] active goal in
+ match res with
+ | `Ok newgoals ->
+ true, ([newgoals], [])
+ | `No _ ->
+ aux tl
+(* false, (a_goals, p_goals) *)
+ | `GoOn newgoals ->
+ let res, (ag, pg) = aux tl in
+ if res then
+ res, (ag, pg)
+ else
+ let newgoals =
+ List.filter
+ (fun (d, gl) ->
+ (d <= !maxdepth) && (List.length gl) <= !maxwidth)
+ newgoals in
+ let p_goals = newgoals @ pg in
+ let p_goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2))
+ p_goals
+ in
+ res, (ag, p_goals)
+ in
+ let theorems =
+(* let ty = *)
+(* match goal with *)
+(* | (_, (_, _, t)::_) -> t *)
+(* | _ -> assert false *)
+(* in *)
+(* if CicUtil.is_meta_closed ty then *)
+(* let _ = *)
+(* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *)
+(* in *)
+(* let metasenv, context, ugraph = env in *)
+(* let uris = *)
+(* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *)
+(* in *)
+(* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *)
+(* let uris = *)
+(* List.filter *)
+(* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *)
+(* in *)
+(* List.map *)
+(* (fun u -> *)
+(* let t = CicUtil.term_of_uri u in *)
+(* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *)
+(* (t, ty, [])) *)
+(* uris *)
+(* else *)
+ List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms
+ in
+ aux (context_hyp @ theorems)
+;;
+
+
+let apply_theorem_to_goals env theorems active goals =
+ let a_goals, p_goals = goals in
+ let theorem = List.hd (fst theorems) in
+ let theorems = [theorem] in
+ let rec aux p = function
+ | [] -> false, ([], p)
+ | goal::tl ->
+ let res = apply_to_goal_conj env theorems active goal in
+ match res with
+ | `Ok newgoals -> true, ([newgoals], [])
+ | `No _ -> aux p tl
+ | `GoOn newgoals -> aux (newgoals @ p) tl
+ in
+ let ok, (a, p) = aux p_goals a_goals in
+ if ok then
+ ok, (a, p)
+ else
+ let p_goals =
+ List.stable_sort
+ (fun (d1, l1) (d2, l2) ->
+ let r = d2 - d1 in
+ if r <> 0 then r
+ else let r = (List.length l1) - (List.length l2) in
+ if r <> 0 then r
+ else
+ let res = ref 0 in
+ let _ =
+ List.exists2
+ (fun (_, _, t1) (_, _, t2) ->
+ let r = Pervasives.compare t1 t2 in
+ if r <> 0 then (res := r; true) else false) l1 l2
+ in !res)
+ p
+ in
+ ok, (a_goals, p_goals)
+;;
+
+
+let rec given_clause dbd env goals theorems passive active =
+ let goals = simplify_goals env goals active in
+ let ok, goals = activate_goal goals in
+(* let theorems = simplify_theorems env theorems active in *)
+ if ok then
+ let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+(* let ok', theorems = activate_theorem theorems in *)
+ let ok', theorems = false, theorems in
+ if ok' then
+ let ok, goals = apply_theorem_to_goals env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_aux dbd env goals theorems passive active
+ else
+ if (passive_is_empty passive) then ParamodulationFailure
+ else given_clause_aux dbd env goals theorems passive active
+
+and given_clause_aux dbd env goals theorems passive active =
let time1 = Unix.gettimeofday () in
let selection_estimate = get_selection_estimate () in
kept_clauses := (size_of_passive passive) + (size_of_active active);
-(* let refl_equal = *)
-(* CicUtil.term_of_uri *)
-(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)
-(* in *)
- let goals = simplify_goals env goals active in
- let theorems = simplify_theorems env theorems active in
- let is_passive_empty = passive_is_empty passive in
- try
- let ok, goals = apply_to_goals env is_passive_empty theorems active goals in
- if ok then
- let proof =
- match goals with
- | (_, [proof, _, _])::_ -> Some proof
- | _ -> assert false
- in
- ParamodulationSuccess (proof, env)
- else
- match is_passive_empty (* passive_is_empty passive *) with
- | true -> (* ParamodulationFailure *)
- given_clause env goals theorems passive active
- | false ->
- let (sign, current), passive = select env goals passive active in
- let time1 = Unix.gettimeofday () in
- let res = forward_simplify env (sign, current) ~passive active in
- let time2 = Unix.gettimeofday () in
- forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
- match res with
- | None ->
- given_clause env goals theorems passive active
- | Some (sign, current) ->
- if (sign = Negative) && (is_identity env current) then (
- debug_print
- (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
- (string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
- ParamodulationSuccess (Some proof (* current *), env)
- ) else (
- debug_print
- (lazy "\n================================================");
- debug_print (lazy (Printf.sprintf "selected: %s %s"
- (string_of_sign sign)
- (string_of_equality ~env current)));
-
- let t1 = Unix.gettimeofday () in
- let new' = infer env sign current active in
- let t2 = Unix.gettimeofday () in
- infer_time := !infer_time +. (t2 -. t1);
-
- let res, goal' = contains_empty env new' in
- if res then
- let proof =
- match goal' with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
- | None -> None
- in
- ParamodulationSuccess (proof (* goal *), env)
- else
- let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' active in
- let t2 = Unix.gettimeofday () in
- let _ =
- forward_simpl_new_time :=
- !forward_simpl_new_time +. (t2 -. t1)
- in
- let active =
- match sign with
- | Negative -> active
- | Positive ->
- let t1 = Unix.gettimeofday () in
- let active, _, newa, _ =
- backward_simplify env ([], [current]) active
+(* (\* let goals = simplify_goals env goals active in *\) *)
+(* (\* let theorems = simplify_theorems env theorems active in *\) *)
+(* let is_passive_empty = passive_is_empty passive in *)
+(* try *)
+(* let ok, goals = false, [] in (\* apply_to_goals env is_passive_empty theorems active goals in *\) *)
+(* if ok then *)
+(* let proof = *)
+(* match goals with *)
+(* | (_, [proof, _, _])::_ -> Some proof *)
+(* | _ -> assert false *)
+(* in *)
+(* ParamodulationSuccess (proof, env) *)
+(* else *)
+ match passive_is_empty passive with
+ | true -> (* ParamodulationFailure *)
+ given_clause dbd env goals theorems passive active
+ | false ->
+ let (sign, current), passive = select env (fst goals) passive active in
+ let time1 = Unix.gettimeofday () in
+ let res = forward_simplify env (sign, current) ~passive active in
+ let time2 = Unix.gettimeofday () in
+ forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+ match res with
+ | None ->
+ given_clause dbd env goals theorems passive active
+ | Some (sign, current) ->
+ if (sign = Negative) && (is_identity env current) then (
+ debug_print
+ (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+ (string_of_equality ~env current)));
+ let _, proof, _, _, _ = current in
+ ParamodulationSuccess (Some proof (* current *), env)
+ ) else (
+ debug_print
+ (lazy "\n================================================");
+ debug_print (lazy (Printf.sprintf "selected: %s %s"
+ (string_of_sign sign)
+ (string_of_equality ~env current)));
+
+ let t1 = Unix.gettimeofday () in
+ let new' = infer env sign current active in
+ let t2 = Unix.gettimeofday () in
+ infer_time := !infer_time +. (t2 -. t1);
+
+ let res, goal' = contains_empty env new' in
+ if res then
+ let proof =
+ match goal' with
+ | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | None -> None
+ in
+ ParamodulationSuccess (proof (* goal *), env)
+ else
+ let t1 = Unix.gettimeofday () in
+ let new' = forward_simplify_new env new' active in
+ let t2 = Unix.gettimeofday () in
+ let _ =
+ forward_simpl_new_time :=
+ !forward_simpl_new_time +. (t2 -. t1)
+ in
+ let active =
+ match sign with
+ | Negative -> active
+ | Positive ->
+ let t1 = Unix.gettimeofday () in
+ let active, _, newa, _ =
+ backward_simplify env ([], [current]) active
+ in
+ let t2 = Unix.gettimeofday () in
+ backward_simpl_time :=
+ !backward_simpl_time +. (t2 -. t1);
+ match newa with
+ | None -> active
+ | Some (n, p) ->
+ let al, tbl = active in
+ let nn = List.map (fun e -> Negative, e) n in
+ let pp, tbl =
+ List.fold_right
+ (fun e (l, t) ->
+ (Positive, e)::l,
+ Indexing.index tbl e)
+ p ([], tbl)
in
- let t2 = Unix.gettimeofday () in
- backward_simpl_time :=
- !backward_simpl_time +. (t2 -. t1);
- match newa with
- | None -> active
- | Some (n, p) ->
- let al, tbl = active in
- let nn = List.map (fun e -> Negative, e) n in
- let pp, tbl =
- List.fold_right
- (fun e (l, t) ->
- (Positive, e)::l,
- Indexing.index tbl e)
- p ([], tbl)
- in
- nn @ al @ pp, tbl
- in
+ nn @ al @ pp, tbl
+ in
(* let _ = *)
(* Printf.printf "active:\n%s\n" *)
(* (String.concat "\n" *)
(* (string_of_equality ~env e)) pos))); *)
(* print_newline (); *)
(* in *)
- match contains_empty env new' with
- | false, _ ->
- let active =
- let al, tbl = active in
- match sign with
- | Negative -> (sign, current)::al, tbl
- | Positive ->
- al @ [(sign, current)], Indexing.index tbl current
- in
- let passive = add_to_passive passive new' in
- let (_, ns), (_, ps), _ = passive in
+ match contains_empty env new' with
+ | false, _ ->
+ let active =
+ let al, tbl = active in
+ match sign with
+ | Negative -> (sign, current)::al, tbl
+ | Positive ->
+ al @ [(sign, current)], Indexing.index tbl current
+ in
+ let passive = add_to_passive passive new' in
+ let (_, ns), (_, ps), _ = passive in
(* Printf.printf "passive:\n%s\n" *)
(* (String.concat "\n" *)
(* ((List.map (fun e -> "Negative " ^ *)
(* (string_of_equality ~env e)) *)
(* (EqualitySet.elements ps)))); *)
(* print_newline (); *)
- given_clause env goals theorems passive active
- | true, goal ->
- let proof =
- match goal with
- | Some goal ->
- let _, proof, _, _, _ = goal in Some proof
- | None -> None
- in
- ParamodulationSuccess (proof (* goal *), env)
- )
- with SearchSpaceOver ->
- ParamodulationFailure
+ given_clause dbd env goals theorems passive active
+ | true, goal ->
+ let proof =
+ match goal with
+ | Some goal ->
+ let _, proof, _, _, _ = goal in Some proof
+ | None -> None
+ in
+ ParamodulationSuccess (proof (* goal *), env)
+ )
+(* with SearchSpaceOver -> *)
+(* ParamodulationFailure *)
;;
-let rec given_clause_fullred env goals theorems passive active =
+let rec given_clause_fullred dbd env goals theorems passive active =
+ let goals = simplify_goals env goals ~passive active in
+ let ok, goals = activate_goal goals in
+(* let theorems = simplify_theorems env theorems ~passive active in *)
+ if ok then
+ let _ =
+ let print_goals goals =
+ (String.concat "\n"
+ (List.map
+ (fun (d, gl) ->
+ let gl' =
+ List.map
+ (fun (p, _, t) ->
+ (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
+ in
+ Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
+ (print_goals (fst goals)) (print_goals (snd goals))))
+ in
+ let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+ if ok then
+ let proof =
+ match (fst goals) with
+ | (_, [proof, _, _])::_ -> Some proof
+ | _ -> assert false
+ in
+ ParamodulationSuccess (proof, env)
+ else
+ given_clause_fullred_aux dbd env goals theorems passive active
+ else
+(* let ok', theorems = activate_theorem theorems in *)
+(* if ok' then *)
+(* let ok, goals = apply_theorem_to_goals env theorems active goals in *)
+(* if ok then *)
+(* let proof = *)
+(* match (fst goals) with *)
+(* | (_, [proof, _, _])::_ -> Some proof *)
+(* | _ -> assert false *)
+(* in *)
+(* ParamodulationSuccess (proof, env) *)
+(* else *)
+(* given_clause_fullred_aux env goals theorems passive active *)
+(* else *)
+ if (passive_is_empty passive) then ParamodulationFailure
+ else given_clause_fullred_aux dbd env goals theorems passive active
+
+and given_clause_fullred_aux dbd env goals theorems passive active =
let time1 = Unix.gettimeofday () in
let selection_estimate = get_selection_estimate () in
kept_clauses := (size_of_passive passive) + (size_of_active active);
-(* let refl_equal = *)
-(* CicUtil.term_of_uri *)
-(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)
-(* in *)
- let goals = simplify_goals env goals ~passive active in
- let theorems = simplify_theorems env theorems ~passive active in
- let is_passive_empty = passive_is_empty passive in
- try
- let ok, goals = apply_to_goals env is_passive_empty theorems active goals in
- if ok then
- let proof =
- match goals with
- | (_, [proof, _, _])::_ -> Some proof
- | _ -> assert false
- in
- ParamodulationSuccess (proof, env)
- else
- let _ =
- debug_print
- (lazy ("new_goals: " ^ (string_of_int (List.length goals))));
- debug_print
- (lazy
- (String.concat "\n"
- (List.map
- (fun (d, gl) ->
- let gl' =
- List.map
- (fun (p, _, t) ->
- (string_of_proof p) ^ ", " ^ (CicPp.ppterm t)) gl
- in
- Printf.sprintf "%d: %s" d (String.concat "; " gl'))
- goals)));
- in
- match is_passive_empty (* passive_is_empty passive *) with
- | true -> (* ParamodulationFailure *)
- given_clause_fullred env goals theorems passive active
- | false ->
- let (sign, current), passive = select env goals passive active in
- let time1 = Unix.gettimeofday () in
- let res = forward_simplify env (sign, current) ~passive active in
- let time2 = Unix.gettimeofday () in
- forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
- match res with
- | None ->
- given_clause_fullred env goals theorems passive active
- | Some (sign, current) ->
- if (sign = Negative) && (is_identity env current) then (
- debug_print
- (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
- (string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
- ParamodulationSuccess (Some proof (* current *), env)
- ) else (
- debug_print
- (lazy "\n================================================");
- debug_print (lazy (Printf.sprintf "selected: %s %s"
- (string_of_sign sign)
- (string_of_equality ~env current)));
-
- let t1 = Unix.gettimeofday () in
- let new' = infer env sign current active in
- let t2 = Unix.gettimeofday () in
- infer_time := !infer_time +. (t2 -. t1);
-
- let active =
- if is_identity env current then active
- else
- let al, tbl = active in
- match sign with
- | Negative -> (sign, current)::al, tbl
- | Positive ->
- al @ [(sign, current)], Indexing.index tbl current
- in
- let rec simplify new' active passive =
- let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' ~passive active in
- let t2 = Unix.gettimeofday () in
- forward_simpl_new_time :=
- !forward_simpl_new_time +. (t2 -. t1);
- let t1 = Unix.gettimeofday () in
- let active, passive, newa, retained =
- backward_simplify env new' ~passive active in
- let t2 = Unix.gettimeofday () in
- backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
- match newa, retained with
- | None, None -> active, passive, new'
- | Some (n, p), None
- | None, Some (n, p) ->
- let nn, np = new' in
- simplify (nn @ n, np @ p) active passive
- | Some (n, p), Some (rn, rp) ->
- let nn, np = new' in
- simplify (nn @ n @ rn, np @ p @ rp) active passive
- in
- let active, passive, new' = simplify new' active passive in
+(* try *)
+(* let ok, goals = apply_to_goals env is_passive_empty theorems active goals in *)
+(* if ok then *)
+(* let proof = *)
+(* match goals with *)
+(* | (_, [proof, _, _])::_ -> Some proof *)
+(* | _ -> assert false *)
+(* in *)
+(* ParamodulationSuccess (proof, env) *)
+(* else *)
+(* let _ = *)
+(* debug_print *)
+(* (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); *)
+(* debug_print *)
+(* (lazy *)
+(* (String.concat "\n" *)
+(* (List.map *)
+(* (fun (d, gl) -> *)
+(* let gl' = *)
+(* List.map *)
+(* (fun (p, _, t) -> *)
+(* (\* (string_of_proof p) ^ ", " ^ *\) (CicPp.ppterm t)) gl *)
+(* in *)
+(* Printf.sprintf "%d: %s" d (String.concat "; " gl')) *)
+(* goals))); *)
+(* in *)
+ match passive_is_empty passive with
+ | true -> (* ParamodulationFailure *)
+ given_clause_fullred dbd env goals theorems passive active
+ | false ->
+ let (sign, current), passive = select env (fst goals) passive active in
+ let time1 = Unix.gettimeofday () in
+ let res = forward_simplify env (sign, current) ~passive active in
+ let time2 = Unix.gettimeofday () in
+ forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+ match res with
+ | None ->
+ given_clause_fullred dbd env goals theorems passive active
+ | Some (sign, current) ->
+ if (sign = Negative) && (is_identity env current) then (
+ debug_print
+ (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+ (string_of_equality ~env current)));
+ let _, proof, _, _, _ = current in
+ ParamodulationSuccess (Some proof (* current *), env)
+ ) else (
+ debug_print
+ (lazy "\n================================================");
+ debug_print (lazy (Printf.sprintf "selected: %s %s"
+ (string_of_sign sign)
+ (string_of_equality ~env current)));
+
+ let t1 = Unix.gettimeofday () in
+ let new' = infer env sign current active in
+ let t2 = Unix.gettimeofday () in
+ infer_time := !infer_time +. (t2 -. t1);
+
+ let active =
+ if is_identity env current then active
+ else
+ let al, tbl = active in
+ match sign with
+ | Negative -> (sign, current)::al, tbl
+ | Positive ->
+ al @ [(sign, current)], Indexing.index tbl current
+ in
+ let rec simplify new' active passive =
+ let t1 = Unix.gettimeofday () in
+ let new' = forward_simplify_new env new' ~passive active in
+ let t2 = Unix.gettimeofday () in
+ forward_simpl_new_time :=
+ !forward_simpl_new_time +. (t2 -. t1);
+ let t1 = Unix.gettimeofday () in
+ let active, passive, newa, retained =
+ backward_simplify env new' ~passive active in
+ let t2 = Unix.gettimeofday () in
+ backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
+ match newa, retained with
+ | None, None -> active, passive, new'
+ | Some (n, p), None
+ | None, Some (n, p) ->
+ let nn, np = new' in
+ simplify (nn @ n, np @ p) active passive
+ | Some (n, p), Some (rn, rp) ->
+ let nn, np = new' in
+ simplify (nn @ n @ rn, np @ p @ rp) active passive
+ in
+ let active, passive, new' = simplify new' active passive in
- let k = size_of_passive passive in
- if k < (kept - 1) then
- processed_clauses := !processed_clauses + (kept - 1 - k);
-
- let _ =
+ let k = size_of_passive passive in
+ if k < (kept - 1) then
+ processed_clauses := !processed_clauses + (kept - 1 - k);
+
+ let _ =
+ debug_print
+ (lazy
+ (Printf.sprintf "active:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active))))))
+ in
+ let _ =
+ match new' with
+ | neg, pos ->
debug_print
(lazy
- (Printf.sprintf "active:\n%s\n"
+ (Printf.sprintf "new':\n%s\n"
(String.concat "\n"
((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e))
- (fst active))))))
- in
- let _ =
- match new' with
- | neg, pos ->
- debug_print
- (lazy
- (Printf.sprintf "new':\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun e -> "Negative " ^
- (string_of_equality ~env e)) neg) @
- (List.map
- (fun e -> "Positive " ^
- (string_of_equality ~env e)) pos)))))
- in
- match contains_empty env new' with
- | false, _ ->
- let passive = add_to_passive passive new' in
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
+ match contains_empty env new' with
+ | false, _ ->
+ let passive = add_to_passive passive new' in
(* let (_, ns), (_, ps), _ = passive in *)
(* Printf.printf "passive:\n%s\n" *)
(* (String.concat "\n" *)
(* (string_of_equality ~env e)) *)
(* (EqualitySet.elements ps)))); *)
(* print_newline (); *)
- given_clause_fullred env goals theorems passive active
- | true, goal ->
- let proof =
- match goal with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
- | None -> None
- in
- ParamodulationSuccess (proof (* goal *), env)
- )
- with SearchSpaceOver ->
- ParamodulationFailure
+ given_clause_fullred dbd env goals theorems passive active
+ | true, goal ->
+ let proof =
+ match goal with
+ | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | None -> None
+ in
+ ParamodulationSuccess (proof (* goal *), env)
+ )
+(* with SearchSpaceOver -> *)
+(* ParamodulationFailure *)
;;
(* let given_clause_ref = ref given_clause;; *)
-let main dbd term metasenv ugraph =
+let main dbd full term metasenv ugraph =
let module C = Cic in
let module T = CicTypeChecker in
let module PET = ProofEngineTypes in
in
(* let new_meta_goal = Cic.Meta (goal', irl) in *)
let env = (metasenv, context, ugraph) in
- let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
- let context_hyp = find_context_hypotheses env eq_indexes in
- let theorems = context_hyp @ theorems in
+ let theorems =
+ if full then
+ let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
+ let context_hyp = find_context_hypotheses env eq_indexes in
+ context_hyp, theorems
+ else
+ let refl_equal =
+ let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
+ in
+ let t = CicUtil.term_of_uri refl_equal in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ [], [(refl_equal, t, ty, [])]
+ in
let _ =
debug_print
(lazy
"Theorems:\n-------------------------------------\n%s\n"
(String.concat "\n"
(List.map
- (fun (t, ty, _) ->
+ (fun (_, t, ty, _) ->
Printf.sprintf
"Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
- theorems))))
+ (snd theorems)))))
in
try
let goal = Inference.BasicProof new_meta_goal, [], goal in
let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
+(* let res = *)
+(* (if !use_fullred then given_clause_fullred else given_clause) *)
+(* env [0, [goal]] theorems passive active *)
+(* in *)
let res =
+ let goals = make_goals goal in
+(* and theorems = make_theorems theorems in *)
(if !use_fullred then given_clause_fullred else given_clause)
- env [0, [goal]] theorems passive active
+ dbd env goals theorems passive active
in
let finish = Unix.gettimeofday () in
let _ =
(fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
in
let _ =
- Printf.printf "OK, found a proof!\n";
- (* REMEMBER: we have to instantiate meta_proof, we should use
- apply the "apply" tactic to proof and status
- *)
- let names = names_of_context context in
- print_endline (PP.pp proof names);
+(* Printf.printf "OK, found a proof!\n"; *)
+(* (\* REMEMBER: we have to instantiate meta_proof, we should use *)
+(* apply the "apply" tactic to proof and status *)
+(* *\) *)
+(* let names = names_of_context context in *)
+(* print_endline (PP.pp proof names); *)
try
let ty, ug =
CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
let default_depth = !maxdepth
and default_width = !maxwidth;;
+let reset_refs () =
+ maxmeta := 0;
+ symbols_counter := 0;
+ weight_age_counter := !weight_age_ratio;
+ processed_clauses := 0;
+ start_time := 0.;
+ elapsed_time := 0.;
+ maximal_retained_equality := None;
+ infer_time := 0.;
+ forward_simpl_time := 0.;
+ forward_simpl_new_time := 0.;
+ backward_simpl_time := 0.;
+ passive_maintainance_time := 0.;
+ derived_clauses := 0;
+ kept_clauses := 0;
+;;
+
let saturate
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
- maxmeta := 0;
+ reset_refs ();
+ Indexing.init_index ();
maxdepth := depth;
maxwidth := width;
let proof, goal = status in
in
let theorems =
if full then
- let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
+(* let refl_eq = *)
+(* let u = eq_XURI () in *)
+(* let t = CicUtil.term_of_uri u in *)
+(* let ty, _ = *)
+(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
+(* (t, ty, []) *)
+(* in *)
+(* let le_S = *)
+(* let u = UriManager.uri_of_string *)
+(* "cic:/matita/nat/orders/le.ind#xpointer(1/1/2)" in *)
+(* let t = CicUtil.term_of_uri u in *)
+(* let ty, _ = *)
+(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *)
+(* (t, ty, []) *)
+(* in *)
+(* let thms = refl_eq::le_S::[] in *)
+ let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
let context_hyp = find_context_hypotheses env eq_indexes in
- context_hyp @ thms
+(* context_hyp @ thms *)
+ (context_hyp, thms)
else
let refl_equal =
let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
in
let t = CicUtil.term_of_uri refl_equal in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- [(t, ty, [])]
+ [], [(refl_equal, t, ty, [])]
in
let _ =
debug_print
"Theorems:\n-------------------------------------\n%s\n"
(String.concat "\n"
(List.map
- (fun (t, ty, _) ->
+ (fun (_, t, ty, _) ->
Printf.sprintf
"Term: %s, type: %s"
(CicPp.ppterm t) (CicPp.ppterm ty))
- theorems))))
+ (snd theorems)))))
in
let active = make_active () in
let passive = make_passive [(* term_equality *)] equalities in
let start = Unix.gettimeofday () in
- let res = given_clause_fullred env [0, [goal]] theorems passive active in
+(* let res = given_clause_fullred env [0, [goal]] theorems passive active in *)
+ let res =
+ let goals = make_goals goal in
+(* and theorems = make_theorems theorems in *)
+ given_clause_fullred dbd env goals theorems passive active
+ in
let finish = Unix.gettimeofday () in
(res, finish -. start)
in
projects / helm.git / commitdiff