(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) let debug_print = fun _ -> () (* Da rimuovere, solo per debug*) let print_context ctx = let print_name = function Cic.Name n -> n | Cic.Anonymous -> "_" in List.fold_right (fun i (output,context) -> let (newoutput,context') = match i with Some (n,Cic.Decl t) -> print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context | Some (n,Cic.Def (t,None)) -> print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context | None -> "_ ?= _\n", None::context | Some (_,Cic.Def (_,Some _)) -> assert false in output^newoutput,context' ) ctx ("",[]) ;; 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 = try Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status ) 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 depth = 5;; let width = 3;; let new_search_theorems f proof goal depth gtl sign = let choices = f (proof,goal) in List.map (function (proof, goallist) -> (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign)) choices ;; exception NoOtherChoices;; let rec auto dbd = function [] -> [] | (proof, [], sign)::tl -> (proof, [], sign)::tl | (proof, (goal,0)::_, _)::tl -> auto dbd tl | (proof, (((goal,depth)::gtl) as allg), sign)::tl -> (* first we check if the metavariable has not been already closed as a side effect by some other application *) let facts = (depth = 1) in let name,metasenv,p,statement = proof in let meta_inf = (try let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in Some (ey, ty) with _ -> None) in match meta_inf with Some (ey, ty) -> (* the goal is still there *) (* debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p)); debug_print ("CURRENT HYP = " ^ (fst (print_context ey))); *) (* if the goal contains metavariables we use the input signature for at_most constraints *) let is_meta_closed = CicUtil.is_meta_closed ty in 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 proof goal (depth-1) [] new_sign in let global_choices = new_search_theorems (fun status -> List.map snd (MetadataQuery.hint ~dbd ~facts:facts ?signature:sign status)) proof goal (depth-1) [] new_sign in (* we proceed depth-first on the current goal. This is a MAJOR optimization, since in case of success, and if the goal is meta_closed, we may just drop the alternatives tl1, avoiding useless backtracking. *) let all_choices = local_choices@global_choices in (match (auto dbd all_choices) with [] -> auto dbd tl | (proof,[],_)::tl1 -> let all_choices = let gtl' = List.map fst gtl in if (gtl = [] || is_meta_closed) then (proof,gtl,sign)::tl else let tl2 = (List.map (function (p,l,s) -> (p,l@gtl,s)) tl1) in (proof,gtl,sign)::tl2@tl in auto dbd all_choices | _ -> assert false) | None -> auto dbd ((proof,gtl,sign)::tl) ;; let auto_tac ?num dbd = let auto_tac dbh (proof,goal) = debug_print "Entro in Auto"; match (auto dbd [(proof, [(goal,depth)],None)]) with [] -> debug_print("Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (proof,[],_)::_ -> debug_print "AUTO_TAC HA FINITO"; (proof,[]) | _ -> assert false in ProofEngineTypes.mk_tactic (auto_tac dbd) ;; (************************** EXPERIMENTAL VERSION ****************************) (* 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 = 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 -> [] ;; (** splits a list of goals in three groups: closed propositional goals, open propositional goals and non proposotional goals *) let split proof l = let _,metasenv,_,_ = proof in List.fold_left (fun (c,o,z,n) g -> try let (_, ey, ty) = CicUtil.lookup_meta g metasenv in let ty_sort,u = CicTypeChecker.type_of_aux' metasenv ey ty CicUniv.empty_ugraph in let b,_ = CicReduction.are_convertible ey (Cic.Sort Cic.Prop) ty_sort u in if b then (if CicUtil.is_meta_closed ty then (g::c,o,z,n) else (c,g::o,z,n)) else (c,o,z,g::n) with CicUtil.Meta_not_found _ -> (c,o,g::z,n) ) ([],[],[],[]) l ;; let my_weight dbd sign proof g = let res = search_theorems_in_context (proof,g) in (* @ (List.map snd (MetadataQuery.experimental_hint ~dbd ~facts:false ?signature:sign (proof,g))) in *) List.fold_left (fun n (_,(_,l)) -> n+(List.length l)+1) 0 res ;; let add_weight dbd sign proof = List.map (function g -> (g,my_weight dbd sign proof g)) ;; (* let reorder_goals dbd sign proof goals = List.rev goals *) (* let reorder_goals dbd sign proof goals = let (c,o,z,n) = split proof goals in c@o@n@z *) let reorder_goals dbd sign proof goals = let (c,o,z,n) = split proof goals in match o with [] -> c@n@z | [g] ->c@[g]@n@z | l -> let l' = add_weight dbd sign proof l in c@(List.map fst (List.sort (fun (_,x) (_,y) -> x - y) l'))@n@z 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 is_in_metasenv goal metasenv = try let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in true with _ -> false let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals = 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 (is_in_metasenv 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 "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; debug_print (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 "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *) [] (* the empty list means no choices, i.e. failure *) | No _ | NotYetInspected -> (* debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p)); debug_print ("CURRENT HYP = " ^ (fst (print_context 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 = [] in (* new_search_theorems (fun status -> List.map snd (MetadataQuery.experimental_hint ~dbd ~facts:facts ?signature:sign 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 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 ("ty = "^CicPp.ppterm ty); debug_print ("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 = function [] -> [] | (subst,(proof, goals, sign))::tl -> let _,metasenv,_,_ = proof in let is_in_metasenv (goal, _) = try let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in true with _ -> false in let goals'= List.filter is_in_metasenv goals in auto_new_aux dbd width already_seen_goals ((subst,(proof, goals', sign))::tl) and auto_new_aux dbd width already_seen_goals = function [] -> [] | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd width already_seen_goals tl | (subst,(proof, goals, _))::tl when (List.length goals) > width+1 -> auto_new dbd width already_seen_goals tl | (subst,(proof, (goal,depth)::gtl, sign))::tl -> let maxdepthgoals,othergoals = let rec aux acc = function (g,d)::l when d=depth -> aux (g::acc) l |l -> (acc,l) in aux [goal] gtl in let _,metasenv,p,_ = proof in let len1 = List.length maxdepthgoals in let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in let len2 = List.length maxdepthgoals in match maxdepthgoals with [] -> debug_print ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth); auto_new dbd width already_seen_goals((subst,(proof, othergoals, sign))::tl) | goal::tgs -> let gtl = (List.map (fun x->(x,depth)) tgs)@othergoals in begin let meta_inf = try let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in Some (ey,ty) with _ -> None in match meta_inf with | Some (ey,ty) -> begin match (auto_single dbd proof goal ey ty depth (width - (List.length gtl) - (len1-len2)) sign already_seen_goals) with [] -> auto_new dbd width already_seen_goals 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 all_choices | _ -> assert false end | None -> debug_print "caso none"; auto_new dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl) end ;; let auto_tac_new ~(dbd:Mysql.dbd) = let auto_tac dbd (proof,goal) = Hashtbl.clear inspected_goals; debug_print "Entro in Auto"; let id t = t in match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with [] -> debug_print("Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> debug_print "AUTO_TAC HA FINITO"; let _,_,p,_ = proof in debug_print (CicPp.ppterm p); (proof,[]) | _ -> assert false in ProofEngineTypes.mk_tactic (auto_tac dbd) ;;