| [] -> min
| hd::tl -> my_min_elt (my_min hd min) tl
in
- (* let current = EqualitySet.min_elt pos_set in *)
- let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in
+(* let current = EqualitySet.min_elt pos_set in *)
+ let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in
let passive_table =
Indexing.remove_index passive_table current
in
(* adds to passive a list of equalities new_pos *)
-let add_to_passive passive new_pos =
+let add_to_passive passive new_pos preferred =
let (pos_list, pos_set), table = passive in
let ok set equality = not (EqualitySet.mem equality set) in
let pos = List.filter (ok pos_set) new_pos in
let add set equalities =
List.fold_left (fun s e -> EqualitySet.add e s) set equalities
in
- (pos_list @ pos, add pos_set pos),
+ let pos_head, pos_tail =
+ List.partition
+ (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)
+ pos
+ in
+ (pos_head @ pos_list @ pos_tail, add pos_set pos),
table
;;
let find (_,_,g) where =
List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
in
- let simplified =
List.fold_left
- (fun acc goal ->
+ (fun (acc_a,acc_p) goal ->
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)
- (* active_goals active_goals *)
- [] active_goals
- in
- if List.length active_goals <> List.length simplified then
- prerr_endline "SEMPLIFICANDO HO SCARTATO...";
- (simplified,passive_goals)
- (*
- HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
- (List.sort (fun (_,_,t1) (_,_,t2) -> compare t1 t1)
- ((*goals @*) simplified))
- *)
+ if changed then
+ if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
+ else
+ if find g acc_a then acc_a,acc_p else g::acc_a,acc_p)
+ ([],passive_goals) active_goals
;;
let check_if_goals_set_is_solved env active goals =
*)
let infer_goal_set_with_current env current goals active =
- let active_goals, passive_goals = goals in
- let active_goals, _ =
+ let active_goals, passive_goals =
simplify_goal_set env goals active
in
let l,table,_ = build_table [current] in
let size_of_goal_set_a (l,_) = List.length l;;
let size_of_goal_set_p (_,l) = List.length l;;
+
+let pp_goals label goals context =
+ let names = Utils.names_of_context context in
+ List.iter
+ (fun _,_,g ->
+ prerr_endline
+ (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names)))
+ (fst goals);
+ List.iter
+ (fun _,_,g ->
+ prerr_endline
+ (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names)))
+ (snd goals);
+;;
(** given-clause algorithm with full reduction strategy: NEW implementation *)
(* here goals is a set of goals in OR *)
let given_clause
eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
=
- let names = Utils.names_of_context context in
let initial_time = Unix.gettimeofday () in
let iterations_left iterno =
let now = Unix.gettimeofday () in
Equality.collect active passive goal
end;
let current, passive = select env goals passive in
- let _ =
- List.iter
- (fun _,_,g ->
- 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
(* SIMPLIFICATION OF CURRENT *)
+ prerr_endline
+ ("Selected : " ^
+ Equality.string_of_equality ~env current);
let res =
forward_simplify eq_uri env (Utils.Positive, current) active
in
match res with
| None -> step goals theorems passive active (iterno+1)
| Some current ->
+(*
+ prerr_endline
+ ("Selected simpl: " ^
+ Equality.string_of_equality ~env current);
+*)
(* GENERATION OF NEW EQUATIONS *)
prerr_endline "infer";
let new' = infer eq_uri env current active in
in
(* FORWARD AND BACKWARD SIMPLIFICATION *)
prerr_endline "fwd/back simpl";
- let rec simplify new' active passive =
+ let rec simplify new' active passive head =
let new' =
forward_simplify_new eq_uri env new' ~passive active
in
List.fold_left filter_dependent passive pruned
in
match newa, retained with
- | None, None -> active, passive, new'
+ | None, None -> active, passive, new', head
| Some p, None
- | None, Some p -> simplify (new' @ p) active passive
- | Some p, Some rp -> simplify (new' @ p @ rp) active passive
+ | None, Some p -> simplify (new' @ p) active passive head
+ | Some p, Some rp ->
+ simplify (new' @ p @ rp) active passive (head @ p)
+ in
+ let active, passive, new', head =
+ simplify new' active passive []
in
- let active, passive, new' = simplify new' active passive in
prerr_endline "simpl goal with new";
let goals =
let a,b,_ = build_table new' in
let _ = <:stop<simplify_goal_set new>> in
rc
in
- let passive = add_to_passive passive new' in
+ let passive = add_to_passive passive new' head in
step goals theorems passive active (iterno+1)
end
in
(Equality.string_of_equality ~env e)) new'))))
in
let new' = List.filter accept_fun new' in
- let passive = add_to_passive passive new' in
+ let passive = add_to_passive passive new' [] in
saturate_equations eq_uri env goal accept_fun passive active
;;
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
+ let cleaned_goal = Utils.remove_local_context type_of_goal in
+ Utils.set_goal_symbols cleaned_goal;
let names = Utils.names_of_context context in
let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
- let cleaned_goal = Utils.remove_local_context type_of_goal in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
let res, time =
let t1 = Unix.gettimeofday () in
*)
let goals = make_goal_set goal in
let max_iterations = 10000 in
- let max_time = Unix.gettimeofday () +. 300. (* minutes *) in
+ let max_time = Unix.gettimeofday () +. 600. (* minutes *) in
given_clause
eq_uri env goals theorems passive active max_iterations max_time
in
CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
if demod_table <> "" then
begin
+ let eql =
+ if eql = [] then [eq_what] else eql
+ in
let demod =
let demod = Str.split (Str.regexp "_") demod_table in
List.map (fun other -> find_in_ctx 1 other context) demod
projects / helm.git / commitdiff