let set =
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
in
- (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
+ (* we have the invariant that the list and the set have the same
+ * cardinality *)
+ EqualitySet.elements set, set
;;
+
let make_empty_active () = [], Indexing.empty ;;
let make_active eq_list =
eq_list, List.fold_left Indexing.index Indexing.empty eq_list
let size_of_passive (passive_list, _) = List.length passive_list;;
let size_of_active (active_list, _) = List.length active_list;;
+
let passive_is_empty = function
| [], s when EqualitySet.is_empty s -> true
| [], s -> assert false (* the set and the list should be in sync *)
(Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
(List.map Equality.string_of_equality equalities))));
- Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
+Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
match equalities with
| [] -> []
| hd::tl ->
Equality.mk_equality bag
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
in
-(* match Indexing.subsumption env table goal_equation with*)
- match Indexing.unification env table goal_equation with
+ match Indexing.subsumption env table goal_equation with
+ (* match Indexing.unification env table goal_equation with *)
| Some (subst, equality, swapped ) ->
(*
prerr_endline
else
p
in (goalproof, p, id, subst, cicmenv))
- (Indexing.unification_all env table goal_equation)
+ (Indexing.subsumption_all env table goal_equation)
+ (* (Indexing.unification_all env table goal_equation) *)
| _ -> assert false
;;
let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
let m = Subst.apply_subst_metasenv s m in
Some (goalproof, reflproof, 0, s,m)
- with _ -> None)
+ with CicUnification.UnificationFailure _ -> None)
| _ -> None
;;
| [] -> active_goals, []
| hd::tl ->
let changed,selected = simplify_goal bag env hd active in
-(*
- if changed then
- prerr_endline ("--------------- goal semplificato");
-*)
let (_,_,t1) = selected in
+ (*
+ if changed && Utils.debug then
+ prerr_endline ("goal semplificato: " ^ CicPp.ppterm t1); *)
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
active_goals
in
if already_in then
- aux tl
+ aux tl
else
let passive_goals = tl in
let new_passive_goals =
(* replacing fake mets with real ones *)
(* prerr_endline "replacing metas..."; *)
let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
- if proof_menv = [] then prerr_endline "VUOTA";
CicMetaSubst.ppmetasenv [] proof_menv;
let what, with_what =
List.fold_left
~where:type_of_goal
in
let goal_proof,goal_ty,real_menv,_ =
- prerr_endline "parte la refine";
try
CicRefine.type_of_aux' metasenv context goal_proof
CicUniv.empty_ugraph
let cleaned_goal = Utils.remove_local_context type_of_goal in
let canonical_menv,other_menv =
List.partition (fun (_,c,_) -> c = context) metasenv in
- prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));
+ (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
debug_print (lazy (string_of_int (List.length (fst active))));
match (check_if_goal_is_identity env goal) with
None -> subsumed
| Some id -> id::subsumed in
+ debug_print (lazy "dopo subsumed");
let res =
List.map
(fun
status goalproof newproof subsumption_id subsumption_subst proof_menv
in
let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
- let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+ let newmetasenv =
+ other_menv @
+ List.filter
+ (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+ in
+ let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
(subst, proof,gl)) subsumed_or_id
- in res, !maxmeta
+ in
+ res, !maxmeta
let given_clause
let cleaned_goal = Utils.remove_local_context type_of_goal in
let canonical_menv,other_menv =
List.partition (fun (_,c,_) -> c = context) metasenv in
- prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));
+ (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
- let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
+ let canonical_menv =
+ List.map
+ (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
+ in
let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in