(* let debug_print = fun _ -> () *)
-(* Profiling code
-let new_experimental_hint =
- let profile = CicUtil.profile "new_experimental_hint" in
- fun ~dbd ~facts ?signature ~universe status ->
- profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
-*) let new_experimental_hint = MetadataQuery.new_experimental_hint
-
-(* In this versions of auto_tac we maintain an hash table of all inspected
- goals. We assume that the context is invariant for application.
- To this aim, it is essential to sall hint_verbose, that in turns calls
- apply_verbose. *)
-
-type exitus =
- No of int
- | Yes of Cic.term * int
- | NotYetInspected
-
-let inspected_goals = Hashtbl.create 503;;
-
-let search_theorems_in_context status =
- let (proof, goal) = status in
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let module PET = ProofEngineTypes in
- let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let rec find n = function
- | [] -> []
- | hd::tl ->
- let res =
- (* we should check that the hypothesys has not been cleared *)
- if List.nth context (n-1) = None then
- None
- else
- try
- let (subst,(proof, goal_list)) =
- PT.apply_tac_verbose ~term:(C.Rel n) status
- in
- (*
- let goal_list =
- List.stable_sort (compare_goal_list proof) goal_list in
- *)
- Some (subst,(proof, goal_list))
- with
- PET.Fail _ -> None
- in
- (match res with
- | Some res -> res::(find (n+1) tl)
- | None -> find (n+1) tl)
- in
- try
- find 1 context
- with Failure s -> []
-;;
-
-
-let compare_goals proof goal1 goal2 =
- let _,metasenv,_,_ = proof in
- let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
- let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
- let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
- CicUniv.empty_ugraph in
- let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
- CicUniv.empty_ugraph in
- let prop1 =
- let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
- CicUniv.empty_ugraph in
- if b then 0 else 1
- in
- let prop2 =
- let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
- CicUniv.empty_ugraph in
- if b then 0 else 1
- in
- prop1 - prop2
-
-
-let new_search_theorems f dbd proof goal depth sign =
- let choices = f (proof,goal)
- in
- List.map
- (function (subst,(proof, goallist)) ->
- (* let goallist = reorder_goals dbd sign proof goallist in *)
- let goallist = List.sort (compare_goals proof) goallist in
- (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
- choices
-;;
-
-exception NoOtherChoices;;
-
-let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
- universe
- =
- if depth = 0 then [] else
- if List.mem ty already_seen_goals then [] else
- let already_seen_goals = ty::already_seen_goals in
- let facts = (depth = 1) in
- let _,metasenv,p,_ = proof in
- (* first of all we check if the goal has been already
- inspected *)
- assert (CicUtil.exists_meta goal metasenv);
- let exitus =
- try Hashtbl.find inspected_goals ty
- with Not_found -> NotYetInspected in
- let is_meta_closed = CicUtil.is_meta_closed ty in
- begin
- match exitus with
- Yes (bo,_) ->
- (*
- debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
- debug_print (lazy (CicPp.ppterm ty));
- *)
- let subst_in =
- (* if we just apply the subtitution, the type
- is irrelevant: we may use Implicit, since it will
- be dropped *)
- CicMetaSubst.apply_subst
- [(goal,(ey, bo, Cic.Implicit None))] in
- let (proof,_) =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal subst_in metasenv in
- [(subst_in,(proof,[],sign))]
- | No d when (d >= depth) ->
- (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
- [] (* the empty list means no choices, i.e. failure *)
- | No _
- | NotYetInspected ->
- debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty));
- debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p));
- debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey));
- let sign, new_sign =
- if is_meta_closed then
- None, Some (MetadataConstraints.signature_of ty)
- else sign,sign in (* maybe the union ? *)
- let local_choices =
- new_search_theorems
- search_theorems_in_context dbd
- proof goal (depth-1) new_sign in
- let global_choices =
- new_search_theorems
- (fun status ->
- List.map snd
- (new_experimental_hint
- ~dbd ~facts:facts ?signature:sign ~universe status))
- dbd proof goal (depth-1) new_sign in
- let all_choices =
- local_choices@global_choices in
- let sorted_choices =
- List.stable_sort
- (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
- Pervasives.compare
- (List.length goals1) (List.length goals2))
- all_choices in
- (match (auto_new dbd width already_seen_goals universe sorted_choices)
- with
- [] ->
- (* no proof has been found; we update the
- hastable *)
- (* if is_meta_closed then *)
- Hashtbl.add inspected_goals ty (No depth);
- []
- | (subst,(proof,[],sign))::tl1 ->
- (* a proof for goal has been found:
- in order to get the proof we apply subst to
- Meta[goal] *)
- if is_meta_closed then
- begin
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable ey in
- let meta_proof =
- subst (Cic.Meta(goal,irl)) in
- Hashtbl.add inspected_goals
- ty (Yes (meta_proof,depth));
-(*
- begin
- let cty,_ =
- CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
- in
- if not (cty = ty) then
- begin
- debug_print (lazy ("ty = "^CicPp.ppterm ty));
- debug_print (lazy ("cty = "^CicPp.ppterm cty));
- assert false
- end
- Hashtbl.add inspected_goals
- ty (Yes (meta_proof,depth));
- end;
-*)
- end;
- (subst,(proof,[],sign))::tl1
- | _ -> assert false)
- end
-
-and auto_new dbd width already_seen_goals universe = function
- | [] -> []
- | (subst,(proof, goals, sign))::tl ->
- let _,metasenv,_,_ = proof in
- let goals'=
- List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
- in
- auto_new_aux dbd
- width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
-
-and auto_new_aux dbd width already_seen_goals universe = function
- | [] -> []
- | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
- | (subst,(proof, (goal,0)::_, _))::tl ->
- auto_new dbd width already_seen_goals universe tl
- | (subst,(proof, goals, _))::tl when
- (List.length goals) > width ->
- auto_new dbd width already_seen_goals universe tl
- | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
- let _,metasenv,p,_ = proof in
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- match (auto_single dbd proof goal ey ty depth
- (width - (List.length gtl)) sign already_seen_goals) universe
- with
- [] -> auto_new dbd width already_seen_goals universe tl
- | (local_subst,(proof,[],sign))::tl1 ->
- let new_subst f t = f (subst t) in
- let is_meta_closed = CicUtil.is_meta_closed ty in
- let all_choices =
- if is_meta_closed then
- (new_subst local_subst,(proof,gtl,sign))::tl
- else
- let tl2 =
- (List.map
- (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
- in
- (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
- auto_new dbd width already_seen_goals universe all_choices
- | _ -> assert false
- ;;
-
-let default_depth = 5
-let default_width = 3
-
-(*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
- ()
-=
- let auto_tac dbd (proof,goal) =
- let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
- Hashtbl.clear inspected_goals;
- debug_print (lazy "Entro in Auto");
- let id t = t in
- let t1 = Unix.gettimeofday () in
- match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
- [] -> debug_print (lazy "Auto failed");
- raise (ProofEngineTypes.Fail "No Applicable theorem")
- | (_,(proof,[],_))::_ ->
- let t2 = Unix.gettimeofday () in
- debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_ = proof in
- debug_print (lazy (CicPp.ppterm p));
- Printf.printf "tempo: %.9f\n" (t2 -. t1);
- (proof,[])
- | _ -> assert false
- in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
-*)
-
-(*
-let paramodulation_tactic = ref
- (fun dbd ?full ?depth ?width status ->
- raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
-
-let term_is_equality = ref
- (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-*)
-
-let bool name params =
- try let _ = List.assoc name params in true with
- | Not_found -> false
+let bool params name default =
+ try
+ let s = List.assoc name params in
+ if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+ else if s = "0" || s = "false" || s = "no" || s= "off" then false
+ else
+ let msg = "Unrecognized value for parameter "^name^"\n" in
+ let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ with Not_found -> default
;;
-let string name params =
+let string params name default =
try List.assoc name params with
- | Not_found -> ""
+ | Not_found -> default
;;
-let int name params =
+let int params name default =
try int_of_string (List.assoc name params) with
- | Not_found -> default_depth
+ | Not_found -> default
| Failure _ ->
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-let auto_tac ~params ~(dbd:HMysql.dbd) =
+let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
(* argument parsing *)
- let depth = int "depth" params in
- let width = int "width" params in
- let paramodulation = bool "paramodulation" params in
- let full = bool "full" params in
- let superposition = bool "superposition" params in
- let target = string "target" params in
- let table = string "table" params in
- let subterms_only = bool "subterms_only" params in
- let caso_strano = bool "caso_strano" params in
- let demod_table = string "demod_table" params in
- (* the real tactic *)
- let auto_tac dbd (proof, goal) =
- let normal_auto () =
- let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
- Hashtbl.clear inspected_goals;
- debug_print (lazy "Entro in Auto");
- let id t = t in
- let t1 = Unix.gettimeofday () in
- match
- auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
- with
- [] -> debug_print(lazy "Auto failed");
- raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
- | (_,(proof,[],_))::_ ->
- let t2 = Unix.gettimeofday () in
- debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_ = proof in
- debug_print (lazy (CicPp.ppterm p));
- debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
- (proof,[])
- | _ -> assert false
- in
- let paramodulation_ok =
- let _, metasenv, _, _ = proof in
- let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- paramodulation && (full || (Equality.term_is_equality meta_goal))
- in
- if paramodulation_ok then (
- debug_print (lazy "USO PARAMODULATION...");
-(* try *)
- try
- let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in
- prerr_endline (Saturation.get_stats ());
- rc
- with exn ->
- prerr_endline (Saturation.get_stats ());
- raise exn
-
-(* with ProofEngineTypes.Fail _ -> *)
-(* normal_auto () *)
- ) else
- normal_auto ()
- in
+ let int = int params
+ and string = string params
+ and bool = bool params in
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let timeout = int "timeout" 0 in
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod = bool "paramodulation" false in
+ (* hacks to debug paramod *)
+ let superposition = bool "superposition" false in
+ let target = string "target" "" in
+ let table = string "table" "" in
+ let subterms_only = bool "subterms_only" false in
+ let demod_table = string "demod_table" "" in
match superposition with
| true ->
- ProofEngineTypes.mk_tactic
- (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table)
- | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
-
-(********************** applyS *******************)
-
-let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity =
- let (consthead,newmetasenv,arguments,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
- let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
- let proof',metasenv =
- let (puri,metasenv,pbo,pty) = proof in
- (puri,newmetasenv,pbo,pty),metasenv
- in
- let proof'',goals =
- match LibraryObjects.eq_URI () with
- | Some uri ->
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
- ~continuation:
- (PrimitiveTactics.cut_tac
- (CicSubstitution.lift 1
- (Cic.Appl
- [Cic.MutInd (uri,0,[]);
- Cic.Sort Cic.Prop;
- consthead;
- ty])))) (proof',goal)
- | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
- in
- match goals with
- [g1;g2] ->
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let cache =
+ let cache =
+ AutoCache.cache_add_context context metasenv AutoCache.cache_empty
+ in
+ if use_only_paramod then (* only paramod *)
+ cache
+ else
+ AutoCache.cache_add_library dbd proof [goal] cache
+ in
+ let oldmetasenv = metasenv in
+ let flags = {
+ AutoTypes.maxdepth =
+ if use_only_paramod then 2 else depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.timeout =
+ if timeout = 0 then float_of_int timeout
+ else Unix.gettimeofday() +. (float_of_int timeout);
+ AutoTypes.use_paramod = use_paramod;
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.dont_cache_failures = false
+ }
+ in
+ match Auto.auto dbd cache context metasenv [goal] flags with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
in
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
- ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
- ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
- ) (proof'',g1)
- in
- proof'',
- (*CSC: Brrrr.... *)
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
- ~newmetasenv:(let _,m,_,_ = proof'' in m)
- | _ -> assert false
-
-let rec count_prods context ty =
- match CicReduction.whd context ty with
- Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
- | _ -> 0
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
+;;
-let applyS_tac ~dbd ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
- match term with
- C.Var (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Var (uri,exp_named_subst')
- | C.Const (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutInd (uri,tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
- | _ -> [],newmeta,[],term
- in
- let metasenv' = metasenv@newmetasenvfragment in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
- in
- let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
- let res =
- new_metasenv_and_unify_and_t dbd proof goal
- newmeta' metasenv' context term' ty termty goal_arity
- in
- res
+let auto_tac ~params ~dbd =
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+;;
-let applyS_tac ~dbd ~term =
- ProofEngineTypes.mk_tactic
- (fun status ->
- try applyS_tac ~dbd ~term status
- with
- | CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (ProofEngineTypes.Fail msg))
+let pp_proofterm = Equality.pp_proofterm;;
projects / helm.git / blobdiff