]> matita.cs.unibo.it Git - helm.git/commitdiff
Experimental enhancements to the ndestruct tactic. By using the syntax
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 28 Jul 2010 15:44:09 +0000 (15:44 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 28 Jul 2010 15:44:09 +0000 (15:44 +0000)
ndestruct (e1 ... em) skip (H1 ... Hn)

the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal

both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.

helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/ng_tactics/nDestructTac.ml
helm/software/components/ng_tactics/nDestructTac.mli

index ae4dc23f76b4e477f2276d268b96670bd5decdc2..9ea33c2de294acd90212ef37c0fb830000f1324e 100644 (file)
@@ -60,7 +60,7 @@ type ntactic =
    | NCut of loc * CicNotationPt.term
 (* | NDiscriminate of loc * CicNotationPt.term
    | NSubst of loc * CicNotationPt.term *)
-   | NDestruct of loc
+   | NDestruct of loc * string list option * string list
    | NElim of loc * CicNotationPt.term * npattern  
    | NGeneralize of loc * npattern
    | NId of loc
@@ -206,7 +206,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 33
+let magic = 34
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
index 0e79c035d7b0dd9487e71dea28d38e0c0789aa68..5f89df9d6ebca083064425ca71598719650905b0 100644 (file)
@@ -116,7 +116,7 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
 (*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
   | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
-  | NDestruct _ -> "ndestruct"
+  | NDestruct (_,dom,skip) -> "ndestruct ..." 
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
index e55df286b87b5a0d6f069bb4f7de9228cc3f00e4..976b25b55a79f8e7c6f3659777481b1ccaa9a4de 100644 (file)
@@ -797,7 +797,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
   | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
-  | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
+  | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -888,6 +888,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
+        prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =
@@ -899,7 +900,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let status =
          if index_obj then
           let status = index_obj_for_auto status obj in
-           index_eq_for_auto status uri
+           (try index_eq_for_auto status uri
+           with _ -> status)
          else
           status in
 (*
index d7aae9ee8c1bc9021686b619ae096943a3d4c4a0..941bb221871192ae6ecaf32f7d9dcc75fd54dbb9 100644 (file)
@@ -155,6 +155,7 @@ EXTEND
     | id = IDENT -> Some id ]
     ];
   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
+  ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
   tactic_term_list1: [
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
@@ -289,7 +290,10 @@ EXTEND
     | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
 (*  | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
     | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
-    | IDENT "ndestruct" -> G.NTactic(loc,[G.NDestruct loc])
+    | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
+      exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
+        -> let exclude' = match exclude with None -> [] | Some l -> l in
+           G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NTactic(loc,[G.NElim (loc, what, where)])
     | IDENT "ngeneralize"; p=pattern_spec ->
index fd745ccf6af77330023e55aa00703b16a0d1b4ab..7814aacfd50cf6f7409733b24640970d7a13d133 100644 (file)
@@ -28,7 +28,7 @@
 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 _ -> ())
 
@@ -73,7 +73,7 @@ let subst_metasenv_and_fix_names status =
 
 (* input: nome della variabile riscritta
  * output: lista dei nomi delle variabili il cui tipo dipende dall'input *)
-let cascade_select_in_ctx ~subst ctx iname =
+let cascade_select_in_ctx ~subst ctx skip iname =
   let lctx, rctx = HExtlib.split_nth (iname - 1) ctx in
   let lctx = List.rev lctx in
   let rec rm_last = function
@@ -85,7 +85,8 @@ let cascade_select_in_ctx ~subst ctx iname =
        (fun (acc,context) item -> 
           match item with
             | n,(NCic.Decl s | NCic.Def (s,_)) 
-                  when not (List.for_all (fun x -> NCicTypeChecker.does_not_occur ~subst context (x-1) x s) acc) ->
+                  when (not (List.for_all (fun x -> NCicTypeChecker.does_not_occur ~subst context (x-1) x s) acc)
+                   && not (List.mem n skip)) ->
                 List.iter (fun m -> pp (lazy ("acc has " ^ (string_of_int m)))) acc;
                 pp (lazy ("acc occurs in the type of " ^ n));
                 (1::List.map ((+) 1) acc, item::context)
@@ -362,13 +363,25 @@ let discriminate_tac ~context cur_eq status =
     NTactics.merge_tac; print_tac (lazy "the end of discriminate")] 
   ) status
 ;;
+
+let saturate_skip status context skip =
+  HExtlib.list_uniq
+    (List.fold_left
+      (fun acc x -> 
+         let ix = HExtlib.list_index ((=) x) (List.map fst context)
+         in match ix with
+         | None -> acc
+        | Some (i,_) -> 
+            fst (cascade_select_in_ctx ~subst:(get_subst status) context [] (i+1)) @ acc) skip skip)
+;;
       
-let subst_tac ~context ~dir cur_eq =
-  fun status ->
+let subst_tac ~context ~dir skip cur_eq =
+  fun status as oldstatus ->
   let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
   let _,ctx' = HExtlib.split_nth cur_eq context 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
+  let skip = saturate_skip status context skip in
   pp (lazy (Printf.sprintf "subst: equation %s" eq_name));
     let l, r = match s with
       | NCic.Appl [_;_;t1;t2] | NCic.Appl [_;_;t1;_;t2] -> t1,t2
@@ -382,9 +395,12 @@ let subst_tac ~context ~dir cur_eq =
     let names_to_gen, _ = 
       match var with 
       | NCic.Rel var ->
-        cascade_select_in_ctx ~subst:(get_subst status) context (var+cur_eq)
-      | _ -> cascade_select_in_ctx ~subst:(get_subst status) context cur_eq in
+        cascade_select_in_ctx ~subst:(get_subst status) context skip (var+cur_eq)
+      | _ -> cascade_select_in_ctx ~subst:(get_subst status) context skip cur_eq in
     let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
+    if (List.exists (fun x -> List.mem x skip) names_to_gen)
+      then oldstatus
+    else 
     let gen_tac x = 
       NTactics.generalize_tac 
       ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
@@ -394,16 +410,18 @@ let subst_tac ~context ~dir cur_eq =
                    ~what:("",0,mk_id eq_name) ~where:default_pattern;
                  NTactics.reduce_tac ~reduction:(`Normalize true)
                    ~where:default_pattern;
-                 NTactics.clear_tac [eq_name]]@
+                 NTactics.try_tac (NTactics.clear_tac [eq_name])]@
                  (List.map NTactics.intro_tac (List.rev names_to_gen))) status
 ;;
 
-let clearid_tac ~context cur_eq =
+let clearid_tac ~context skip cur_eq =
   fun status ->
   let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
   let _,ctx' = HExtlib.split_nth cur_eq context 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
+  let skip = saturate_skip status context skip in
+  (* 
   let streicher_id = 
     match s with
     | NCic.Appl [_;_;_;_] -> mk_id "streicherK"
@@ -431,6 +449,63 @@ let clearid_tac ~context cur_eq =
                     | [] -> []
                     | _::tl -> tl in
                   List.map NTactics.intro_tac names_to_intro)) status
+*)
+
+  pp (lazy (Printf.sprintf "clearid: equation %s" eq_name));
+    match s with
+    | NCic.Appl [_;_;_;_] -> 
+      (* leibniz *)
+  let streicher_id = mk_id "streicherK"
+  in
+    let names_to_gen, _ = 
+      cascade_select_in_ctx ~subst:(get_subst status) context skip cur_eq in
+    let names_to_gen = names_to_gen @ [eq_name] in
+    let gen_tac x = 
+      NTactics.generalize_tac 
+      ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+    NTactics.block_tac ((List.map gen_tac names_to_gen)@
+                [NTactics.clear_tac names_to_gen;
+                 NTactics.apply_tac ("",0, mk_appl [streicher_id;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne]);
+                 NTactics.reduce_tac ~reduction:(`Normalize true)
+                   ~where:default_pattern] @
+                 (let names_to_intro = 
+                   match List.rev names_to_gen with
+                    | [] -> []
+                    | _::tl -> tl in
+                  List.map NTactics.intro_tac names_to_intro)) status
+    | NCic.Appl [_;_;_;_;_] -> 
+      (* JMeq *) 
+  let streicher_id = mk_id "streicherK"
+  in
+    let names_to_gen, _ = 
+      cascade_select_in_ctx ~subst:(get_subst status) context skip cur_eq in
+    let names_to_gen = names_to_gen (* @ [eq_name]*) in
+    let gen_tac x = 
+      NTactics.generalize_tac 
+      ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+    let gen_eq = NTactics.generalize_tac
+     ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
+                                  CicNotationPt.Implicit `JustOne; 
+                                  CicNotationPt.Implicit `JustOne; 
+                                  CicNotationPt.Implicit `JustOne; 
+                                  mk_id eq_name]),[], Some CicNotationPt.UserInput)) in
+    NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq::
+                [NTactics.clear_tac names_to_gen;
+                 NTactics.try_tac (NTactics.clear_tac [eq_name]);
+                 NTactics.apply_tac ("",0, mk_appl [streicher_id;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne;
+                                                   CicNotationPt.Implicit `JustOne]);
+                 NTactics.reduce_tac ~reduction:(`Normalize true)
+                   ~where:default_pattern] @
+                 (let names_to_intro = List.rev names_to_gen in
+                  List.map NTactics.intro_tac names_to_intro)) status
+    | _ -> assert false
 ;;
 
 let get_ctx st goal =
@@ -438,7 +513,7 @@ let get_ctx st goal =
 ;;
 
 (* = select + classify *)
-let select_eq ctx acc status goal =
+let select_eq ctx acc domain status goal =
   let classify ~subst ctx' l r =
     (* FIXME: metasenv *)
     if NCicReduction.are_convertible ~metasenv:[] ~subst ctx' l r 
@@ -487,14 +562,15 @@ let select_eq ctx acc status goal =
                      status, Some (List.length ctx - i), kind
               | `Cycle | `Blob | `NonEq -> 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
+                 if (List.for_all (fun x -> x <> n) acc) && 
+                    (List.exists (fun x -> x = n) domain) 
+                then status, Some (List.length ctx - i), kind
                  else aux (i+1))
     with Failure _ | Invalid_argument _ -> status, None, `Blob
   in aux 0
 ;;
 
-let rec destruct_tac0 nprods acc status goal =
+let rec destruct_tac0 nprods acc domain skip status goal =
   let ctx = get_ctx status goal in
   let subst = get_subst status in
   let get_newgoal os ns ogoal =
@@ -502,33 +578,56 @@ let rec destruct_tac0 nprods acc status goal =
     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
+  let status, selection, kind  = select_eq ctx acc domain 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.exec (NTactics.intro_tac (mk_fresh_name ctx 'e' 0)) status goal in
-        destruct_tac0 (nprods-1) acc status' (get_newgoal status status' goal)
+      if nprods > 0  then
+        let fresh = mk_fresh_name ctx 'e' 0 in 
+        let status' = NTactics.exec (NTactics.intro_tac fresh) status goal in
+        destruct_tac0 (nprods-1) acc (fresh::domain) skip status' (get_newgoal status status' goal)
       else
         status
   | 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)
+      else 
+        destruct_tac0 (nprods+newprods) 
+             (name_of_rel ~context:ctx cur_eq::acc) 
+             (List.filter (fun x -> x <> name_of_rel ~context:ctx cur_eq) domain)
+             skip 
+             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
+    let status' = NTactics.exec (subst_tac ~context:ctx ~dir skip 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 ->
+    let newgoal = get_newgoal status status' goal in
+    let has_cleared = 
+     try 
+       let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
+     with _ -> true in
+    let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
+    let acc = rm_eq has_cleared acc in
+    let skip = rm_eq has_cleared skip in
+    let domain = rm_eq has_cleared domain in
+      destruct_tac0 nprods acc domain skip status' newgoal
+ | 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 (clearid_tac ~context:ctx cur_eq) status goal in
-        destruct_tac0 nprods (List.filter (fun x -> x <> eq_name) acc) status' (get_newgoal status status' goal)
+      let status' = NTactics.exec (clearid_tac ~context:ctx skip cur_eq) status goal in
+      let newgoal = get_newgoal status status' goal in
+      let has_cleared = 
+       try 
+         let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
+       with _ -> true in
+      let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
+      let acc = rm_eq has_cleared acc in
+      let skip = rm_eq has_cleared skip in
+      let domain = rm_eq has_cleared domain in
+        destruct_tac0 nprods acc domain skip status' newgoal
   | 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
@@ -538,4 +637,12 @@ let rec destruct_tac0 nprods acc status goal =
   | _ -> assert false
 ;;
 
-let destruct_tac s = NTactics.distribute_tac (destruct_tac0 0 []) s;;
+let destruct_tac dom skip s = 
+  NTactics.distribute_tac 
+    (fun s' g -> 
+     let ctx = get_ctx s' g in
+     let domain = match dom with
+       | None -> List.map (fun (n,_) -> n) ctx
+       | Some l -> l 
+     in
+     destruct_tac0 0 [] domain skip s' g) s;;
index a51886511e3d19da77437745c2ffda2d838900f7..714638d24f56dcba221c3767f4e88474a289d9fa 100644 (file)
@@ -11,4 +11,5 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val destruct_tac : 's NTacStatus.tactic
+val destruct_tac : string list option -> string list -> 's NTacStatus.tactic
+