let connect_to_auto = true;;
+let debug_print = Utils.debug_print;;
(* profiling statistics... *)
let infer_time = ref 0.;;
;;
-
+(*
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
let pp_goal_set msg goals names =
let active_goals, passive_goals = goals in
- prerr_endline ("////" ^ msg);
- prerr_endline ("ACTIVE G: " ^
+ debug_print (lazy ("////" ^ msg));
+ debug_print (lazy ("ACTIVE G: " ^
(String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
- active_goals)));
- prerr_endline ("PASSIVE G: " ^
+ active_goals))));
+ debug_print (lazy ("PASSIVE G: " ^
(String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
- passive_goals)))
+ passive_goals))))
;;
let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
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)))
+ debug_print (lazy
+ (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)))
+ debug_print (lazy
+ (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
(snd goals);
;;
let print_status iterno goals active passive =
- prerr_endline
+ debug_print (lazy
(Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
iterno (size_of_active active) (size_of_passive passive)
- (size_of_goal_set_a goals) (size_of_goal_set_p goals))
+ (size_of_goal_set_a goals) (size_of_goal_set_p goals)))
;;
(** given-clause algorithm with full reduction strategy: NEW implementation *)
in
match check_if_goals_set_is_solved bag env active goals with
| Some p ->
- prerr_endline
+ debug_print (lazy
(Printf.sprintf "\nFound a proof in: %f\n"
- (Unix.gettimeofday() -. initial_time));
+ (Unix.gettimeofday() -. initial_time)));
ParamodulationSuccess (p,active,passive)
| None ->
(* SELECTION *)
if s_iterno < saturation_steps then
let current, passive = select env goals passive in
(* SIMPLIFICATION OF CURRENT *)
- prerr_endline
+ debug_print (lazy
("Selected : " ^
- Equality.string_of_equality ~env current);
+ Equality.string_of_equality ~env current));
forward_simplify bag eq_uri env current active, passive
else
None, passive
try
let _ = CicUtil.lookup_meta i metasenv in metasenv
with CicUtil.Meta_not_found _ ->
- prerr_endline ("not found: "^(string_of_int i));
+ debug_print (lazy ("not found: "^(string_of_int i)));
let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
(i,context,Cic.Meta(j,irl))::metasenv
in
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
bag status
goalproof newproof subsumption_id subsumption_subst proof_menv
=
- if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
- else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
+ if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
+ else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let names = Utils.names_of_context context in
- prerr_endline "Proof:";
- prerr_endline
+ debug_print (lazy "Proof:");
+ debug_print (lazy
(Equality.pp_proof bag names goalproof newproof subsumption_subst
- subsumption_id type_of_goal);
+ subsumption_id type_of_goal));
(*
prerr_endline ("max weight: " ^
(string_of_int (Equality.max_weight goalproof newproof)));
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
- prerr_endline (CicPp.ppterm goal_proof);
- CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+ debug_print (lazy (CicPp.ppterm goal_proof));
+ 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
| CicUnification.AssertFailure s -> assert false
(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
in
- prerr_endline "+++++++++++++ FINE UNIF";
+ Utils.debug_print (lazy "+++++++++++++ FINE UNIF");
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno (CicMetaSubst.apply_subst final_subst)
+ proof goalno final_subst
(List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
let open_goals =
let all_subsumed bag maxm status active passive =
maxmeta := maxm;
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
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 goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
- prerr_endline (string_of_int (List.length (fst active)));
+ debug_print (lazy (string_of_int (List.length (fst active))));
(* we simplify using both actives passives *)
let table =
List.fold_left
active (list_of_passive passive) in
let _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
- prerr_endline (CicPp.ppterm ty);
+ debug_print (lazy (CicPp.ppterm ty));
let subsumed = find_all_subsumed bag env (snd table) goal in
let subsumed_or_id =
match (check_if_goal_is_identity env goal) with
let mp = max_l passive_l in
*)
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = 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
let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
- prerr_endline ">>>>>> ACTIVES >>>>>>>>";
- List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
active_l;
- prerr_endline ">>>>>>>>>>>>>>";
+ debug_print (lazy ">>>>>>>>>>>>>>");
let goals = make_goal_set goal in
match
(* given_caluse non prende in input maxm ????? *)
projects / helm.git / blobdiff