]> matita.cs.unibo.it Git - helm.git/commitdiff
ndestruct now clears off identity equations whenever it's possible.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 27 Nov 2009 15:04:40 +0000 (15:04 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 27 Nov 2009 15:04:40 +0000 (15:04 +0000)
helm/software/components/ng_tactics/nDestructTac.ml
helm/software/components/ng_tactics/nTactics.mli

index 776d5dace0be53f410266bcf2fb776da1515d6c7..4f87707ebdc2f20c2ab33d0dd101788192daffd6 100644 (file)
@@ -26,8 +26,9 @@
 (* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *)
 
 open NTacStatus
+open Continuationals.Stack
 
-let debug = tru
+let debug = fals
 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;;
index 25baae97a61815fcc4e7a58754dd82d3c329881a..4af0c3fb7a0d14f01672ad7d6a20c91e3fe7f124 100644 (file)
@@ -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