From 6dd2a996e8443d57fa3e3d0988829d01485d838a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Oct 2009 09:37:05 +0000 Subject: [PATCH] auto snapshot --- .../components/ng_tactics/andOrTree.ml | 8 + .../components/ng_tactics/andOrTree.mli | 3 +- helm/software/components/ng_tactics/nAuto.ml | 311 ++++++++++++++---- .../software/components/ng_tactics/zipTree.ml | 14 +- .../components/ng_tactics/zipTree.mli | 1 + 5 files changed, 269 insertions(+), 68 deletions(-) diff --git a/helm/software/components/ng_tactics/andOrTree.ml b/helm/software/components/ng_tactics/andOrTree.ml index 22d36844f..57be10271 100644 --- a/helm/software/components/ng_tactics/andOrTree.ml +++ b/helm/software/components/ng_tactics/andOrTree.ml @@ -61,6 +61,14 @@ let downO p = | Node(`And s,[]) -> Solution s | _ -> assert false +let downOr p = + match downr p with + | Some x -> Todo x + | None -> + match eject p with + | Node(`And s,[]) -> Solution s + | _ -> assert false + let left = left let right = right diff --git a/helm/software/components/ng_tactics/andOrTree.mli b/helm/software/components/ng_tactics/andOrTree.mli index 9570c62d9..2a8eea24d 100644 --- a/helm/software/components/ng_tactics/andOrTree.mli +++ b/helm/software/components/ng_tactics/andOrTree.mli @@ -29,7 +29,8 @@ val start : ('s,'g) tree -> (andT,'s,'g) position val upA : (andT,'s,'g) position -> (orT,'s,'g) position option val upO : (orT,'s,'g) position -> (andT,'s,'g) position val downA : (andT,'s,'g) position -> ('s,'g) subtreeO -val downO : (orT,'s,'g) position -> ('s,'g) subtreeA +val downO : (orT,'s,'g) position -> ('s,'g) subtreeA +val downOr : (orT,'s,'g) position -> ('s,'g) subtreeA val left : ('a,'s,'g) position -> ('a,'s,'g) position option val right : ('a,'s,'g) position -> ('a,'s,'g) position option diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index b2620735d..f5d29784a 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1028,11 +1028,13 @@ type 'a op = * step *) | S of goal * (#tac_status as 'a) (* * cic_term * candidate (* int was minsize *) *) + | L of goal * (#tac_status as 'a) let pp_goal (g,_) = string_of_int g let pp_item = function | D g -> "D" ^ pp_goal g | S (g,_) -> "S" ^ pp_goal g + | L (g,_) -> "L" ^ pp_goal g type flags = { do_types : bool; (* solve goals in Type *) @@ -1068,7 +1070,7 @@ let only _ _ _ = true;; let candidate_no = ref 0;; let sort_new_elems l = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l + List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l ;; let try_candidate flags depth status t g = @@ -1125,6 +1127,10 @@ let applicative_case depth signature status flags g gty cache = in elems ;; +let calculate_goal_ty (goalno,_) status = + try Some (get_goalty status goalno) + with Error _ -> None +;; let equational_and_applicative_case signature flags status g depth gty cache @@ -1153,21 +1159,28 @@ let equational_and_applicative_case elems in let elems = - (* XXX calculate the sort *) - List.map (fun c,s,gl -> c,1,s,List.map (fun i -> i,P) gl) elems + List.map (fun c,s,gl -> + c,1,1,s,List.map (fun i -> + let sort = + match calculate_goal_ty (i,()) s with + | None -> assert false + | Some gty -> + let _, sort = typeof s (ctx_of gty) gty in + match term_of_cic_term s sort (ctx_of sort) with + | _, NCic.Sort NCic.Prop -> P + | _ -> T + in + i,sort) gl) elems in let elems = sort_new_elems elems in elems, cache ;; -let calculate_goal_ty (goalno,_) status = - try Some (get_goalty status goalno) - with Error _ -> None -;; + let d_goals l = let rec aux acc = function | (D g)::tl -> aux (acc@[g]) tl - | (S _)::tl -> aux acc tl + | (S _|L _)::tl -> aux acc tl | [] -> acc in aux [] l @@ -1196,7 +1209,7 @@ let intro_case status gno gty depth cache name = debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); incr candidate_no; (* XXX calculate the sort *) - [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]], + [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]], cache ;; @@ -1211,68 +1224,152 @@ let do_something signature flags s gno depth gty cache = module T = ZipTree module Z = AndOrTree +let img_counter = ref 0 ;; let show pos = - debug_print (lazy("generating a.dot")); + incr img_counter; + let file = ("/tmp/a"^string_of_int !img_counter^".dot") in + debug_print (lazy("generating " ^ file)); debug_do (fun () -> - let oc = open_out "/tmp/a.dot" in + let oc = open_out file in let fmt = Format.formatter_of_out_channel oc in GraphvizPp.Dot.header fmt; Z.dump pp_item pos fmt; GraphvizPp.Dot.trailer fmt; Format.fprintf fmt "@?"; close_out oc; - ignore(Sys.command ("dot -Tpng /tmp/a.dot > /tmp/a.png")); - ignore(Sys.command ("eog /tmp/a.png"))) + ignore(Sys.command ("dot -Tpng "^file^" > "^file^".png")); + (*ignore(Sys.command ("eog "^file^".png"))*)) ;; -let rightmost_bro pred = - let rec fst pos = +let rightmost_bro pred pos = + let rec last acc pos = + let acc = if pred pos then Some pos else acc in match Z.right pos with - | None -> None - | Some pos -> - if pred pos then Some pos else fst pos + | None -> acc + | Some pos -> last acc pos in - fst + last None pos ;; -let is_not_S pos = +let leftmost_bro pred pos = + let rec fst pos = + if pred pos then Some pos else + match Z.right pos with + | None -> None + | Some pos -> fst pos + in + fst pos +;; + +let rec first_left_mark_L_as_D pred pos = + if pred pos then + Some pos + else + let pos = + match Z.getA pos with + | s,L (g,_) -> + Z.inject T.Nil (Z.setA s (D g) pos) + | _ -> pos + in + match Z.left pos with + | None -> None + | Some pos -> + first_left_mark_L_as_D pred pos +;; + +let is_oS pos = match Z.getO pos with - | S _ -> false - | D _ -> true + | S _ -> true + | D _ | L _ -> false ;; -let rec next_choice_point (pos : 'a and_pos) : 'a or_pos option = - let rec giveup_right_giveup_up_backtrack_left (pos : 'a and_pos) = - match Z.upA pos with - | None -> None - | Some alts -> - match rightmost_bro is_not_S alts with - | None -> - let upalts = Z.upO alts in - let upalts = Z.inject T.Nil upalts in - backtrack_left_giveup_right_giveup_up upalts - | Some _ as x -> x - and backtrack_left_giveup_right_giveup_up (pos : 'a and_pos) = - let pos = Z.inject T.Nil pos in - let pos = match Z.getA pos with s,D g | s, S (g,_) -> Z.setA s (D g) pos in - match Z.left pos with - | None -> giveup_right_giveup_up_backtrack_left pos - | Some (pos as left_bro) -> - match Z.downA pos with - | Z.Unexplored -> assert false (* we explore left2right *) - | Z.Alternatives alts -> - match rightmost_bro is_not_S alts with - | None -> backtrack_left_giveup_right_giveup_up left_bro - | Some _ as x -> x - in - backtrack_left_giveup_right_giveup_up pos + +let is_aS pos = + match Z.getA pos with + | _,S _ -> true + | _,D _ | _,L _ -> false +;; + +let is_not_oS x = not (is_oS x);; +let is_not_aS x = not (is_aS x);; + +let is_oL pos = match Z.getO pos with L _ -> true | _ -> false ;; +let is_aL pos = match Z.getA pos with _,L _ -> true | _ -> false ;; + +let is_not_oL x = not (is_oL x) ;; +let is_not_aL x = not (is_aL x) ;; + +let rec forall_left pred pos = + match Z.left pos with + | None -> true + | Some pos -> if pred pos then forall_left pred pos else false +;; + + +let rec product = function + | [] -> [] + | ((g,s) :: tl) as l -> (s,List.map fst l) :: product tl +;; + +let has_no_alternatives (pos : 'a and_pos) = + match Z.getA pos with + | _, L _ -> true + | _ -> false +;; + +let rec collect_left_up (pos : 'a and_pos) = + match Z.left pos with + | Some pos -> + (match Z.getA pos with + | _, L (g,s) -> (g,s) :: collect_left_up pos + | _ -> []) + | None -> + match Z.upA pos with + | None -> [] (* root *) + | Some pos -> collect_left_up (Z.upO pos) +;; + +let compute_failed_goals (pos : 'a and_pos) = + let curr = match Z.getA pos with (s,_,_),D g -> (g,s) | _ -> assert false in + product (List.rev (curr :: collect_left_up pos) ) +;; + +let pp_failures l = + debug_print (lazy("CACHE FAILURES/UNDERINSPECTION")); + List.iter (fun (s,gl) -> + debug_print (lazy("FAIL: " ^ + String.concat " , " (List.map (fun g -> + match calculate_goal_ty g s with + | None -> + (try + let (i,_) = g in + let _,_,_,subst,_ = s#obj in + let _,cc,_,ty = NCicUtils.lookup_subst i subst in + let ty = mk_cic_term cc ty in + string_of_int i^":"^ppterm s ty + with NCicUtils.Subst_not_found _ -> "XXXX") + | Some gty -> + let s, gty = apply_subst s (ctx_of gty) gty in + string_of_int (fst g)^":"^ppterm s gty) gl)))) + l +;; + +let is_closed pos = + match Z.getA pos with + | (s,_,_),S (g,_) + | (s,_,_),D g -> + (match calculate_goal_ty g s with + | None -> true + | Some gty -> metas_of_term s gty = []) + | _, L _ -> assert false ;; let auto_main flags signature (pos : 'a and_pos) cache = - let solved g depth size s pos = + let solved g depth size s (pos : 'a and_pos) = Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos in - let failed pos = + let failed (pos : 'a and_pos) = + pp_failures (compute_failed_goals pos); Z.inject (T.Node(`Or,[])) pos in @@ -1284,32 +1381,111 @@ let auto_main flags signature (pos : 'a and_pos) cache = and nextO ~unfocus (pos : 'a or_pos) cache = match Z.getO pos with - | S _ -> assert false (* XXX set to Nil when backtrack *) + | S _ | L _ -> assert false (* XXX set to Nil when backtrack *) | D g -> match Z.downO pos with - | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache + | Z.Solution (s,_,_) -> move_solution_up ~unfocus true s pos cache | Z.Todo pos -> next ~unfocus:true pos cache + and next_choice_point (pos : 'a and_pos) cache = + + let rec global_choice_point (pos : 'a and_pos) : 'a auto_result = +(* prerr_endline "global"; show pos; *) + match Z.upA pos with + | None -> Gaveup + | Some alts -> + let alts = Z.inject T.Nil alts in + let alts = + match Z.getO alts with + | S (s,g) -> Z.setO (L (s,g)) alts + | D (g) -> Z.setO (L (g,Obj.magic g)) alts + (* L (and other marks) for OR should have no arguments *) + | L _ -> assert false + in + match Z.right alts with + | None -> + let upalts = Z.upO alts in + let upalts = Z.inject T.Nil upalts in + let upalts = + match Z.getA upalts with + | s,S (a,b) -> Z.setA s (L (a,b)) upalts + | _,L _ -> assert false + | s,D (a) -> Z.setA s (L (a,Obj.magic a)) upalts + in + backtrack upalts + | Some pos -> + match Z.downO pos with + | Z.Solution (s,_,_) -> + move_solution_up ~unfocus:false true s pos cache + | Z.Todo pos -> next ~unfocus:true pos cache + + and backtrack (pos : 'a and_pos) : 'a auto_result = +(* prerr_endline "backtrack"; show pos; *) + let pos = Z.inject T.Nil pos in + let pos = + match Z.getA pos with + | s,D g | s, S (g,_) | s,L(g,_) -> Z.setA s (D g) pos + in + match first_left_mark_L_as_D is_aS pos with + | None -> global_choice_point pos + | Some pos -> + let rec local_choice_point pos = +(* prerr_endline "local"; show pos; *) + match Z.downA pos with + | Z.Unexplored -> attack pos cache (Z.getA pos) + | Z.Alternatives alts -> + match leftmost_bro is_not_oL alts with + | None -> assert false (* is not L, thus has alternatives *) + | Some pos -> + let is_D = is_not_oS pos in + match if is_D then Z.downO pos else Z.downOr pos with + | Z.Solution (s,_,_) -> assert(is_D); + move_solution_up ~unfocus:false true s pos cache + | Z.Todo pos when is_D -> attack pos cache (Z.getA pos) + | Z.Todo pos -> + match first_left_mark_L_as_D is_aS pos with + | Some pos -> local_choice_point pos + | None -> assert false + in + local_choice_point pos + in + backtrack pos + and next_choice (pos : 'a and_pos) cache = - match next_choice_point pos with - | None -> Gaveup - | Some pos -> nextO ~unfocus:true pos cache + next_choice_point pos cache and move_solution_up - ~unfocus (status : #tac_status as 'a) (pos : 'a or_pos) cache + ~unfocus are_sons_L + (status : #tac_status as 'a) (pos : 'a or_pos) cache = let pos = (* mark as solved *) match Z.getO pos with - | S _ -> assert false (* XXX *) - | D g -> Z.setO (S (g,status)) pos + | L _ -> assert false (* XXX *) + | S (g,_) + | D g -> + if are_sons_L then + Z.inject T.Nil (Z.setO (L (g,status)) pos) + else + Z.setO (S (g,status)) pos in + let has_alternative_or = match Z.right pos with None -> false | _ -> true in let pos = Z.upO pos in + let are_all_lbro_L = forall_left is_aL pos in + let has_no_alternative = + ((not has_alternative_or) && are_sons_L) || + is_closed pos + in match Z.getA pos with + | _, L _ -> assert false | (_, size, depth), S (g,_) (* S if already solved and then solved again because of a backtrack *) | (_, size, depth), D g -> - let newg = S (g,status) in (* TODO: cache success g *) - let status = if unfocus then NTactics.unfocus_tac status else status in + let newg = + if has_no_alternative then (L (g,status)) else (S (g,status))in + (* TODO: cache success g *) + let pos = if has_no_alternative then Z.inject T.Nil pos else pos in +(* let status = if unfocus then NTactics.unfocus_tac status else status + * in *) let news = status,size,depth in let pos = Z.setA news newg pos in match Z.right pos with @@ -1317,18 +1493,22 @@ let auto_main flags signature (pos : 'a and_pos) cache = | None -> match Z.upA pos with | None -> Proved (status, Some (pos,cache)) - | Some pos -> move_solution_up ~unfocus:true status pos cache + | Some pos -> + move_solution_up + ~unfocus:true (has_no_alternative && are_all_lbro_L) + status pos cache and attack pos cache and_item = - (* show pos; *) (* uncomment to show the tree *) + show pos; (* uncomment to show the tree *) match and_item with | _, S _ -> assert false (* next would close the proof or give a D *) + | _, L _ -> assert false (* L is a final solution *) | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout -> debug_print ~depth (lazy ("fail timeout")); Gaveup | (s, depth, width), D (_, T as g) when not flags.do_types -> debug_print ~depth (lazy "skip goal in Type"); - next ~unfocus:true (solved g depth width s pos) cache + next ~unfocus:false (solved g depth width s pos) cache | (_,depth,_), D _ when depth > flags.maxdepth -> debug_print ~depth (lazy "fail depth"); next_choice (failed pos) cache @@ -1374,9 +1554,10 @@ let auto_main flags signature (pos : 'a and_pos) cache = let size_gl l = List.length (prop_only l) in let subtrees = List.map - (fun (_cand,depth_incr,s,gl) -> + (fun (_cand,depth_incr,size_mult,s,gl) -> D(gno,P), - T.Node (`And (s,depth+depth_incr,size+size_gl gl), + T.Node (`And + (s,depth+depth_incr,size+size_mult*(size_gl gl)), List.map (fun g -> D g,T.Nil) gl)) subgoals in @@ -1434,7 +1615,7 @@ let auto_tac ~params:(_univ,flags) status = in s#set_stack stack in - up_to 2 depth + up_to depth depth ;; let group_by_tac ~eq_predicate ~action:tactic status = diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml index 45c7f02b9..30f09940e 100644 --- a/helm/software/components/ng_tactics/zipTree.ml +++ b/helm/software/components/ng_tactics/zipTree.ml @@ -29,6 +29,15 @@ let down = function | Loc (ctx, Node (s,(x,t)::tl)) -> Some (Loc (Ctx (ctx,s,[],x,tl),t)) ;; +let downr = function + | Loc (_,(Nil|Node (_,[]))) -> None + | Loc (ctx, Node (s,(_::_ as l))) -> + match List.rev l with + | [] -> assert false + | (x,t) :: tl -> + Some (Loc (Ctx (ctx,s,tl,x,[]),t)) +;; + let up = function | Loc (Top,_) -> None | Loc (Ctx(ctx,s,l,x,r),t) -> Some (Loc (ctx,Node (s,(List.rev l)@[x,t]@r))) @@ -95,7 +104,7 @@ let dump ppg pps pos fmt = match pos with | Top -> () | Ctx(ctx,s,l,x,r) -> - let t = Node(s,l@[x,skip]@r) in + let t = Node(s,(List.rev l)@[x,skip]@r) in let cur = !c in aux_t t; incr c; @@ -107,10 +116,11 @@ let dump ppg pps pos fmt = aux ctx in let Loc (ctx, t) = pos in - let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->l in + let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->List.rev l in let cur = !c in Pp.node ("node"^string_of_int !c) ~attrs:["style","filled";"fillcolor","red";"color","red"] fmt; + Pp.edge ("node"^string_of_int !c) ("node"^string_of_int !c) fmt; aux_t t; incr c; Pp.edge diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli index bed576157..751d3720d 100644 --- a/helm/software/components/ng_tactics/zipTree.mli +++ b/helm/software/components/ng_tactics/zipTree.mli @@ -18,6 +18,7 @@ val start : ('s,'g) tree -> ('a,'s,'g) position val up : ('a,'s,'g) position -> ('b,'s,'g) position option val down : ('a,'s,'g) position -> ('b,'s,'g) position option +val downr : ('a,'s,'g) position -> ('b,'s,'g) position option val left : ('a,'s,'g) position -> ('b,'s,'g) position option val right : ('a,'s,'g) position -> ('b,'s,'g) position option -- 2.39.2