From: Wilmer Ricciotti Date: Fri, 27 Nov 2009 15:04:40 +0000 (+0000) Subject: ndestruct now clears off identity equations whenever it's possible. X-Git-Tag: make_still_working~3194 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00da35cbf619e0d1f3d7fde7e6a0e6e4dc6c0915;p=helm.git ndestruct now clears off identity equations whenever it's possible. --- diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml index 776d5dace..4f87707eb 100644 --- a/helm/software/components/ng_tactics/nDestructTac.ml +++ b/helm/software/components/ng_tactics/nDestructTac.ml @@ -26,8 +26,9 @@ (* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *) open NTacStatus +open Continuationals.Stack -let debug = true +let debug = false let pp = if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) @@ -328,15 +329,14 @@ let discriminate_tac ~context cur_eq status = NTactics.intro_tac "Deq"; NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] - @ dbranches it leftno @ + @ dbranches it leftno @ [NTactics.shift_tac; - NTactics.intro_tac "discriminate"; - NTactics.apply_tac ("",0,mk_appl [mk_id "discriminate"; + NTactics.intro_tac "#discriminate"; + NTactics.apply_tac ("",0,mk_appl [mk_id "#discriminate"; CicNotationPt.Implicit `JustOne; CicNotationPt.Implicit `JustOne; mk_id eq_name ]); - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern; - NTactics.clear_tac ["discriminate"]; + NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; + NTactics.clear_tac ["#discriminate"]; NTactics.merge_tac] ) status ;; @@ -357,10 +357,8 @@ let subst_tac ~context ~dir cur_eq = let var = match var with | NCic.Rel i -> i | _ -> assert false in - let names_to_gen, indices_to_gen = + let names_to_gen, _ = cascade_select_in_ctx ~subst:(get_subst status) context (var+cur_eq) in - let moved_indices = List.fold_left - (fun acc x -> if x > cur_eq then acc+1 else acc) 0 indices_to_gen in let gen_tac x = NTactics.generalize_tac ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in @@ -369,97 +367,108 @@ let subst_tac ~context ~dir cur_eq = NTactics.rewrite_tac ~dir ~what:("",0,mk_id eq_name) ~where:default_pattern; NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern]@ - (List.map NTactics.intro_tac (List.rev names_to_gen))) status, - (List.length context - cur_eq + 1 - moved_indices) + ~where:default_pattern; + NTactics.clear_tac [eq_name]]@ + (List.map NTactics.intro_tac (List.rev names_to_gen))) status ;; -let get_ctx status = - let ref_ctx = ref [] in - let status = NTactics.distribute_tac - (fun st goal -> - let ctx = ctx_of (get_goalty st goal) in - ref_ctx := ctx; st) status in - !ref_ctx +let get_ctx st goal = + ctx_of (get_goalty st goal) ;; -let rec select_eq ctx i status acc = - try - match (List.nth ctx (List.length ctx - i - 1)) with - | n, (NCic.Decl s | NCic.Def (s,_)) -> - (let _,ctx_s = HExtlib.split_nth (List.length ctx - i) ctx in - let status, s = NTacStatus.whd status ctx_s (mk_cic_term ctx_s s) in - let status, s = term_of_cic_term status s ctx_s in - pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_s ~subst:[] ~metasenv:[] s))); - if (List.for_all (fun x -> x <> n) acc) then - match s with - | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;_;_] -> - if NUri.name_of_uri u = "eq" then status, Some (List.length ctx - i) - else select_eq ctx (i+1) status acc - | _ -> select_eq ctx (i+1) status acc - else select_eq ctx (i+1) status acc) - with Failure _ | Invalid_argument _ -> status, None +(* = select + classify *) +let select_eq ctx acc status goal = + let classify ~subst ctx' l r = + (* FIXME: metasenv *) + if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r + then status, `Identity + else status, (match hd_of_term l, hd_of_term r with + | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref), + NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) -> + if ki != kj then `Discriminate (0,true) + else + let rit = NReference.mk_indty true kref in + let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in + let it = List.nth its itno in + let newprods = (nargs it nleft (ki-1)) + 1 in + `Discriminate (newprods, false) + | NCic.Rel j, _ + when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r -> + `Subst `LeftToRight + | _, NCic.Rel j + when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l -> + `Subst `RightToLeft + | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle + | _ -> `Blob) in + let rec aux i = + try + let index = List.length ctx - i in + match (List.nth ctx (index - 1)) with + | n, (NCic.Decl ty | NCic.Def (ty,_)) -> + (let _,ctx_ty = HExtlib.split_nth index ctx in + let status, ty = NTacStatus.whd status ctx_ty (mk_cic_term ctx_ty ty) in + let status, ty = term_of_cic_term status ty ctx_ty in + pp (lazy (Printf.sprintf "select_eq tries %s" (NCicPp.ppterm ~context:ctx_ty ~subst:[] ~metasenv:[] ty))); + match ty with + | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r] when NUri.name_of_uri u = "eq" -> + (let status, kind = classify ~subst:(get_subst status) ctx_ty l r in + match kind with + | `Identity -> + let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in + if NCicTypeChecker.does_not_occur ~subst:(get_subst status) ctx (index - 1) index goalty + then status, Some (List.length ctx - i), kind + else aux (i+1) + | `Cycle | `Blob -> aux (i+1) (* XXX: skip cyclic/blob equations for now *) + | _ -> + if (List.for_all (fun x -> x <> n) acc) then + status, Some (List.length ctx - i), kind + else aux (i+1)) + | _ -> aux (i+1)) + with Failure _ | Invalid_argument _ -> status, None, `Blob + in aux 0 ;; -let classify ~subst ctx i status = - let _, (NCic.Decl s | NCic.Def (s,_)) = List.nth ctx (i-1) in - let _,ctx' = HExtlib.split_nth i ctx in - let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in - let status, s = term_of_cic_term status s ctx' in - match s with - | NCic.Appl [_;_;l;r] -> - (* FIXME: metasenv *) - if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r - then status, `Identity - else status, (match hd_of_term l, hd_of_term r with - | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref), - NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) -> - if ki != kj then `Discriminate (0,true) - else - let rit = NReference.mk_indty true kref in - let _,_,its,_,itno = NCicEnvironment.get_checked_indtys rit in - let it = List.nth its itno in - let newprods = (nargs it nleft (ki-1)) + 1 in - `Discriminate (newprods, false) - | NCic.Rel j, _ - when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j r -> - `Subst `LeftToRight - | _, NCic.Rel j - when NCicTypeChecker.does_not_occur ~subst ctx' (j-1) j l -> - `Subst `RightToLeft - | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle - | _ -> `Blob) - | _ -> raise (Failure "classify") -;; - -let rec destruct_tac0 nprods i status acc = - let ctx = get_ctx status in +let rec destruct_tac0 nprods acc status goal = + let ctx = get_ctx status goal in let subst = get_subst status in - let status, selection = select_eq ctx i status acc in - match selection with - | None -> - pp (lazy (Printf.sprintf "destruct: nprods is %d, i is %d, no selection, context is %s" nprods i (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + let get_newgoal os ns ogoal = + let go, gc = NTactics.compare_statuses ~past:os ~present:ns in + let go' = ([ogoal] @- gc) @+ go in + match go' with [] -> assert false | g::_ -> g + in + let status, selection, kind = select_eq ctx acc status goal in + pp (lazy ("destruct: acc is " ^ String.concat "," acc )); + match selection, kind with + | None, _ -> + pp (lazy (Printf.sprintf "destruct: nprods is %d, no selection, context is %s" nprods (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); if nprods > 0 then - let status' = NTactics.intro_tac (mk_fresh_name ctx 'e' 0) status in - destruct_tac0 (nprods-1) (List.length ctx) status' acc + let status' = NTactics.exec (NTactics.intro_tac (mk_fresh_name ctx 'e' 0)) status goal in + destruct_tac0 (nprods-1) acc status' (get_newgoal status status' goal) else status - | Some cur_eq -> pp (lazy (Printf.sprintf - "destruct: nprods is %d, i is %d, selection is %s, context is %s" - nprods i (name_of_rel ~context:ctx cur_eq) (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); - match classify ~subst ctx cur_eq status with - | status,`Discriminate (newprods,conflict) -> - let status' = discriminate_tac ~context:ctx cur_eq status in - if conflict then status' - else destruct_tac0 (nprods+newprods) (List.length ctx - cur_eq + 1) - status' (name_of_rel ~context:ctx cur_eq::acc) - | status, `Subst dir -> - let status', next_i = subst_tac ~context:ctx ~dir cur_eq status in - destruct_tac0 nprods next_i status' acc - | status, `Identity - | status, `Cycle (* TODO *) - | status, `Blob -> - destruct_tac0 nprods (cur_eq+1) status acc + | Some cur_eq, `Discriminate (newprods,conflict) -> + pp (lazy (Printf.sprintf "destruct: discriminate - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + let status' = NTactics.exec (discriminate_tac ~context:ctx cur_eq) status goal in + if conflict then status' + else destruct_tac0 (nprods+newprods) + (name_of_rel ~context:ctx cur_eq::acc) status' (get_newgoal status status' goal) + | Some cur_eq, `Subst dir -> + pp (lazy (Printf.sprintf "destruct: subst - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + let status' = NTactics.exec (subst_tac ~context:ctx ~dir cur_eq) status goal in + pp (lazy (Printf.sprintf " ctx after subst = %s" (NCicPp.ppcontext ~metasenv:[] ~subst (get_ctx status' (get_newgoal status status' goal))))); + let eq_name,_ = List.nth ctx (cur_eq-1) in + destruct_tac0 nprods (List.filter (fun x -> x <> eq_name) acc) status' (get_newgoal status status' goal) + | Some cur_eq, `Identity -> + pp (lazy (Printf.sprintf "destruct: identity - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + let eq_name,_ = List.nth ctx (cur_eq-1) in + let status' = NTactics.exec (NTactics.clear_tac [eq_name]) status goal in + destruct_tac0 nprods (List.filter (fun x -> x <> eq_name) acc) status' (get_newgoal status status' goal) + | Some cur_eq, `Cycle -> (* TODO, should never happen *) + pp (lazy (Printf.sprintf "destruct: cycle - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + assert false + | Some cur_eq, `Blob -> + pp (lazy (Printf.sprintf "destruct: blob - nprods is %d, selection is %d, context is %s" nprods cur_eq (NCicPp.ppcontext ~metasenv:[] ~subst ctx))); + assert false ;; -let destruct_tac status = destruct_tac0 0 0 status [];; +let destruct_tac s = NTactics.distribute_tac (destruct_tac0 0 []) s;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 25baae97a..4af0c3fb7 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -24,8 +24,14 @@ val skip_tac: 's NTacStatus.tactic val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic +val compare_statuses : past:#NTacStatus.lowtac_status -> present:#NTacStatus.lowtac_status -> int list * int list + val distribute_tac: NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic +val exec : ((int * Continuationals.Stack.switch) list * 'a list * 'b list * + [> `NoTag ]) + list NTacStatus.status NTacStatus.tactic -> + (#NTacStatus.lowtac_status as 's) -> Continuationals.goal -> 's val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic