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 *)
;;
-
+(*
let simplify_theorems bag env theorems ?passive (active_list, active_table) =
let pl, passive_table =
match passive with
let p_theorems = List.map (mapfun passive_table) p_theorems in
List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
;;
-
+*)
let rec simpl bag eq_uri env e others others_simpl =
let active = others @ others_simpl in
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
| _ -> None
;;
-let find_all_subsumed bag env table (goalproof,menv,ty) =
+let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when LibraryObjects.is_eq_URI uri ->
let goal_equation =
- Equality.mk_equality bag
- (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
+ (Equality.mk_equality bag
+ (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv))
in
- List.map
+ List.map
(fun (subst, equality, swapped ) ->
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+ Indexing.check_for_duplicates cicmenv "from subsumption";
let p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
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 _,context,_ = env in
try
let s,m,_ =
- Founif.unification m m context left right CicUniv.empty_ugraph
+ Founif.unification [] m context left right CicUniv.empty_ugraph
in
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
;;
let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.Prod(name,s,t)
- | Cic.LetIn(name,s,t) ->
+ | Cic.LetIn(name,s,ty,t) ->
let metasenv,s = aux metasenv n s in
+ let metasenv,ty = aux metasenv n ty in
let metasenv,t = aux metasenv (n+1) t in
- metasenv,Cic.LetIn(name,s,t)
+ metasenv,Cic.LetIn(name,s,ty,t)
| Cic.Const(uri,ens) ->
let metasenv,ens =
List.fold_right
aux metasenv 0 p
;;
-let fix_metasenv metasenv =
+let fix_metasenv context metasenv =
List.fold_left
(fun m (i,c,t) ->
- let m,t = fix_proof m c false t in
+ let m,t = fix_proof m context false t in
let m = List.filter (fun (j,_,_) -> j<>i) m in
- (i,c,t)::m)
+ (i,context,t)::m)
metasenv metasenv
;;
+
(* status: input proof status
* goalproof: forward steps on goal
* newproof: backward steps
in
(* Equality.draw_proof bag names goalproof newproof subsumption_id; *)
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
- let real_menv = fix_metasenv (proof_menv@metasenv) in
+ (* assert (metasenv=[]); *)
+ let real_menv = fix_metasenv context (proof_menv@metasenv) in
let real_menv,goal_proof =
fix_proof real_menv context false goal_proof in
(*
prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
raise exn
in
+ let old_insert_coercions = !CicRefine.insert_coercions in
let goal_proof,goal_ty,real_menv,_ =
(* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
try
debug_print (lazy (CicPp.ppterm goal_proof));
- CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+ CicRefine.insert_coercions := false;
+ let res =
+ CicRefine.type_of_aux'
+ real_menv context goal_proof CicUniv.empty_ugraph
+ in
+ CicRefine.insert_coercions := old_insert_coercions;
+ res
with
| CicRefine.RefineFailure s
| CicRefine.Uncertain s
| CicRefine.AssertFailure s as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names (Lazy.force s) exn
| CicUtil.Meta_not_found i as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
| Invalid_argument "list_fold_left2" as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ raise exn
in
let subst_side_effects,real_menv,_ =
try
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
- let real_metasenv = List.filter (fun i,_,_ -> i<>goalno ) real_menv in
- let real_metasenv =
- CicMetaSubst.apply_subst_metasenv final_subst real_metasenv
- in
- let open_goals =
- (ProofEngineHelpers.compare_metasenvs
- ~oldmetasenv:metasenv ~newmetasenv:real_metasenv)
- in
- (* compaction of metas with the same type *)
- let open_goals, final_subst =
- let open_goals_menv_entry =
- List.map
- (fun i -> List.find (fun (j,_,_) -> j = i) real_metasenv)
- open_goals
- in
- let rec compact openg subst = function
- | [] -> openg, subst
- | (i,c,t)::tl ->
- let eq, tl =
- List.partition
- (fun (_,c1,t1) ->
- prerr_endline (CicPp.ppcontext c ^ " /// " ^
- CicPp.ppcontext c1);
- c1 = c && t1 = t) tl
- in
- prerr_endline (string_of_int i ^ " : " ^ CicPp.ppterm t);
- prerr_endline (string_of_int (List.length eq) ^ " .. " ^ string_of_int
- (List.length tl));
- let openg = i::openg in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable c in
- let subst =
- List.fold_left
- (fun subst (j,_,_) -> (j,(c,Cic.Meta(i,irl),t))::subst)
- subst eq
- in
- compact openg subst tl
- in
- compact [] final_subst open_goals_menv_entry
- in
- (* we redoo this to purge collapsed metas *)
- let real_metasenv =
- CicMetaSubst.apply_subst_metasenv final_subst real_metasenv
- in
+(*
+ let metas_of_proof = Utils.metas_of_term goal_proof in
+*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno final_subst real_metasenv
+ proof goalno final_subst
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
+ let open_goals =
+ (ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
+(*
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+*)
final_subst, proof, open_goals
+
+
+(*
+
+ let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
+ (* prerr_endline (CicPp.pp goal_proof names); *)
+ let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
+ let side_effects_t =
+ List.map (Subst.apply_subst subsumption_subst) side_effects_t
+ in
+ (* 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
+ (fun (acc1,acc2) i ->
+ (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
+ ([],[])
+ metas_still_open_in_proof
+(*
+ (List.filter
+ (fun (i,_,_) ->
+ List.mem i metas_still_open_in_proof
+ (*&& not(List.mem i metas_still_open_in_goal)*))
+ proof_menv)
+*)
+ in
+ let goal_proof_menv =
+ List.filter
+ (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
+ proof_menv
+ in
+ let replace where =
+ (* we need this fake equality since the metas of the hypothesis may be
+ * with a real local context *)
+ ProofEngineReduction.replace_lifting
+ ~equality:(fun x y ->
+ match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false)
+ ~what ~with_what ~where
+ in
+ let goal_proof = replace goal_proof in
+ (* ok per le meta libere... ma per quelle che c'erano e sono rimaste?
+ * what mi pare buono, sostituisce solo le meta farlocche *)
+ let side_effects_t = List.map replace side_effects_t in
+ let free_metas =
+ List.filter (fun i -> i <> goalno)
+ (ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
+ in
+ (* prerr_endline
+ * ("freemetas: " ^
+ * String.concat "," (List.map string_of_int free_metas) ); *)
+ (* check/refine/... build the new proof *)
+ let replaced_goal =
+ ProofEngineReduction.replace
+ ~what:side_effects ~with_what:side_effects_t
+ ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
+ ~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
+ with
+ | CicUtil.Meta_not_found _
+ | CicRefine.RefineFailure _
+ | CicRefine.Uncertain _
+ | CicRefine.AssertFailure _
+ | Invalid_argument "list_fold_left2" as exn ->
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ raise exn
+ in
+ prerr_endline "+++++++++++++ METASENV";
+ prerr_endline
+ (CicMetaSubst.ppmetasenv [] real_menv);
+ let subst_side_effects,real_menv,_ =
+(*
+ prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal);
+ prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
+ prerr_endline ("XX metasenv " ^
+ CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
+*)
+ try
+ CicUnification.fo_unif_subst [] context real_menv
+ goal_ty type_of_goal CicUniv.empty_ugraph
+ with
+ | CicUnification.UnificationFailure s
+ | CicUnification.Uncertain s
+ | CicUnification.AssertFailure s -> assert false
+(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
+ in
+ let final_subst =
+ (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
+ in
+(*
+ let metas_of_proof = Utils.metas_of_term goal_proof in
+*)
+ let proof, real_metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goalno (CicMetaSubst.apply_subst final_subst)
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
+ in
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+
+(*
+ HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
+ in *)
+(*
+ match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
+ in
+*)
+(*
+ Printf.eprintf
+ "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"
+ (String.concat ", " (List.map string_of_int open_goals))
+ (CicMetaSubst.ppmetasenv [] metasenv)
+ (CicMetaSubst.ppmetasenv [] real_metasenv);
+*)
+ final_subst, proof, open_goals
;;
+*)
(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let env = metasenv,context,CicUniv.empty_ugraph in
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)); *)
+ 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))));
(* we simplify using both actives passives *)
List.fold_left
(fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq))
active (list_of_passive passive) in
+ let (_,_,ty) = goal in
+ debug_print (lazy ("prima " ^ CicPp.ppterm ty));
let _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
- debug_print (lazy (CicPp.ppterm ty));
- let subsumed = find_all_subsumed bag env (snd table) goal in
+ debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
+ let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in
+ debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
let subsumed_or_id =
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
(goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+ let subst, proof, gl =
build_proof bag
- status goalproof newproof subsumption_id subsumption_subst proof_menv)
- subsumed_or_id in
+ status goalproof newproof subsumption_id subsumption_subst proof_menv
+ in
+ let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof 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
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
+ let canonical_menv,other_menv =
+ List.partition (fun (_,c,_) -> c = context) metasenv in
+ (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
- let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+ let canonical_menv = List.map (fun (i,_,ty)-> (i,[],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
debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
debug_print (lazy ">>>>>>>>>>>>>>");
let goals = make_goal_set goal in
match
-(* given_caluse non prende in input maxm ????? *)
given_clause bag eq_uri env goals passive active
goal_steps saturation_steps max_time
with
build_proof bag
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
Some (subst, proof,gl),a,p, !maxmeta
;;
+
let add_to_passive eql passives =
add_to_passive passives eql eql
;;
projects / helm.git / blobdiff