From: Andrea Asperti Date: Thu, 16 Jun 2005 16:34:24 +0000 (+0000) Subject: A cleaned version of auto_tac_new. X-Git-Tag: INDEXING_NO_PROOFS~129 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=14725b3cbfe52dd040ee403ebb81657c04a78b63;p=helm.git A cleaned version of auto_tac_new. --- diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 7f6be1d9b..3d4fc7126 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,7 +23,9 @@ * http://cs.unibo.it/helm/. *) -let debug_print = fun _ -> () + let debug_print = prerr_endline + +(* let debug_print = fun _ -> () *) (* Da rimuovere, solo per debug*) let print_context ctx = @@ -220,63 +222,6 @@ let search_theorems_in_context status = [] ;; -(** 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 @@ -355,11 +300,9 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals [] (* 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) @@ -368,14 +311,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals new_search_theorems search_theorems_in_context dbd proof goal (depth-1) new_sign in - let global_choices = [] in -(* + let global_choices = 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 *) + dbd proof goal (depth-1) new_sign in let all_choices = local_choices@global_choices in let sorted_choices = @@ -444,61 +386,30 @@ and auto_new_aux dbd width already_seen_goals = function | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd width already_seen_goals tl | (subst,(proof, goals, _))::tl when - (List.length goals) > width+1 -> + (List.length goals) > width -> 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 (_, 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) + 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 + ;; let default_depth = 5 let default_width = 3