now destruct takes an optional list of term rather than a sigle optional term

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 3e87ffba5a3b56573bcc5bfb4812c74dd8d354b7..2b0f4db5f1ad329091df4241cbf1247e466e67cf 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -71,7 +71,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Cut of loc * 'ident option * 'term
   | Decompose of loc * 'ident option list
   | Demodulate of loc
-  | Destruct of loc * 'term option
+  | Destruct of loc * 'term list option
   | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
            'ident intros_spec
   | ElimType of loc * 'term * 'term option * 'ident intros_spec

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index eb1a18e5ad00d365ba23e3db088b620ece02ceab..cf9106ea374d44527481c5e12297be63ee52f9f2 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -68,13 +68,14 @@ let pp_intros_specs s = function
    | None, idents     -> Printf.sprintf " %s%s" s (pp_idents idents)
    | Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents)
 
-let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms)
 
 let opt_string_pp = function
    | None -> ""
    | Some what -> what ^ " "
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
+ let pp_terms = pp_terms ~term_pp in
  let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
  let pp_reduction_kind = pp_reduction_kind ~term_pp in
  let pp_tactic_pattern =
@@ -127,7 +128,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
       (pp_intros_specs "names " (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, None) -> "destruct" 
-  | Destruct (_, Some term) -> "destruct " ^ term_pp term
+  | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
   | Elim (_, what, using, pattern, specs) ->
       Printf.sprintf "elim %s%s %s%s" 
       (term_pp what)
@@ -159,7 +160,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
         (if linear then " linear " else "")
        (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
-        (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
+        (match terms with [] -> "" | _ -> " to " ^ pp_terms terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> 

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index afcbf7f26709a0ea6ddd875852b07a5e6a157b06..e8e3171a08fa9290bd0d8405c63d0238843d7522 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -112,7 +112,7 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Demodulate _ -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm
+  | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         ~pattern what

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 2fe6b9aaee80949f0130b972cc8bae673ace256f..53142e252bfe90a135405bfe32dd00c008d7b91d 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -216,9 +216,13 @@ let rec disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Destruct (loc, Some term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Destruct(loc, Some term)
+    | GrafiteAst.Destruct (loc, Some terms) ->
+        let map term (metasenv, terms) =
+           let metasenv, term = disambiguate_term context metasenv term in
+           metasenv, term :: terms
+        in
+        let metasenv, terms = List.fold_right map terms (metasenv, []) in 
+       metasenv, GrafiteAst.Destruct(loc, Some terms)
     | GrafiteAst.Destruct (loc, None) ->
         metasenv,GrafiteAst.Destruct(loc,None)
     | GrafiteAst.Exact (loc, term) -> 
@@ -264,12 +268,12 @@ let rec disambiguate_tactic
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
-       let f term to_what =
-          let metasenv,term = disambiguate_term context metasenv term in
-          term :: to_what
+       let f term (metasenv, to_what) =
+          let metasenv, term = disambiguate_term context metasenv term in
+          metasenv, term :: to_what
        in
-       let to_what = List.fold_right f to_what [] in 
-       let metasenv,what = disambiguate_term context metasenv what in
+       let metasenv, to_what = List.fold_right f to_what (metasenv, []) in 
+       let metasenv, what = disambiguate_term context metasenv what in
        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | GrafiteAst.Left loc ->
        metasenv,GrafiteAst.Left loc

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 83e9d10d879904456952cfacf10bb03f60becd69..a0fd3335806f1468e3c637621b4cc4f9faef0c64 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -170,8 +170,8 @@ EXTEND
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] ->
-        GrafiteAst.Destruct (loc, xt)
+    | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+        GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index 8164fc5f68a2165029697fc74b4fbff6e31060c9..a8bfc007d42ac395c2c5995686bc6cbc181daf33 100644 (file)
--- a/components/tactics/destructTactic.ml
+++ b/components/tactics/destructTactic.ml
@@ -247,7 +247,7 @@ let exists context = function
    | C.Rel i -> List.nth context (pred i) <> None
    | _       -> true
 
-let rec recur_on_child_tac ~before =
+let recur_on_child_tac ~before ~after =
    let recur_on_child status = 
       let (proof, goal) = status in
       let _, metasenv, _subst, _, _, _ = proof in
@@ -259,13 +259,12 @@ let rec recur_on_child_tac ~before =
          S.lift distance term, m, ug
       in
       let lterm = mk_lterm (Cic.Rel 1) in
-      let continuation = destruct ~first_time:false lterm in
-      let tactic = T.then_ ~start:before ~continuation in
+      let tactic = T.then_ ~start:before ~continuation:(after lterm) in
       PET.apply_tactic tactic status  
    in
    PET.mk_tactic recur_on_child
    
-and injection_tac ~lterm ~i ~continuation =
+let injection_tac ~lterm ~i ~continuation ~recur =
  let give_name seed = function
    | C.Name _ as name -> name
    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
@@ -429,7 +428,7 @@ and injection_tac ~lterm ~i ~continuation =
        let tactic = 
           T.thens ~start: (P.cut_tac cutted)
                    ~continuations:[
-                     recur_on_child_tac continuation;
+                     recur_on_child_tac continuation recur;
                      fill_cut_tac term
                   ]
         in
@@ -438,7 +437,7 @@ and injection_tac ~lterm ~i ~continuation =
  in
   PET.mk_tactic injection_tac
 
-and subst_tac ~lterm ~direction ~where ~continuation =
+let subst_tac ~lterm ~direction ~where ~continuation ~recur =
    let subst_tac status =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
@@ -455,17 +454,18 @@ and subst_tac ~lterm ~direction ~where ~continuation =
             debug_print (lazy ("nella premessa: " ^ name));
            let pattern = None, [name, PET.hole], None in
             let start = ET.rewrite_tac ~direction ~pattern term [] in
-            let ok_tactic = recur_on_child_tac continuation in
+            let ok_tactic = recur_on_child_tac continuation recur in
            T.if_ ~start ~continuation:ok_tactic ~fail:continuation         
       in 
       PET.apply_tactic tactic status
    in
    PET.mk_tactic subst_tac
 
-and destruct ~first_time lterm =
+let rec destruct ~first_time lterm =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
  in
+ let recur = destruct ~first_time:false in
  let destruct status = 
   let (proof, goal) = status in
   let _,metasenv,_subst, _,_, _ = proof in
@@ -492,10 +492,10 @@ and destruct ~first_time lterm =
                    clear_term false (mk_lterm with_what)
                 ]
              in
-             subst_tac ~direction ~lterm ~where:None ~continuation
+             subst_tac ~direction ~lterm ~where:None ~continuation ~recur
            | Some (C.Name name, _) :: tl when j < index && j <> k ->
              debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
-             subst_tac ~direction ~lterm ~where:(Some name) 
+             subst_tac ~direction ~lterm ~where:(Some name) ~recur 
                        ~continuation:(traverse_context false (succ j) tl)
            | _ :: tl -> traverse_context first_time (succ j) tl
         in
@@ -519,7 +519,7 @@ and destruct ~first_time lterm =
                         if are_convertible hd1 hd2 metasenv context then
                            traverse_list first_time (succ i) tl1 tl2
                         else
-                          injection_tac ~i ~lterm ~continuation:
+                          injection_tac ~i ~lterm ~recur ~continuation:
                              (traverse_list false (succ i) tl1 tl2)
                       | _ -> assert false 
                       (* i 2 termini hanno in testa lo stesso costruttore, 
@@ -563,7 +563,7 @@ and destruct ~first_time lterm =
    PET.mk_tactic destruct
 
 (* destruct performs either injection or discriminate or subst *)
-let destruct_tac xterm =
+let destruct_tac xterms =
    let destruct status =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
@@ -572,9 +572,11 @@ let destruct_tac xterm =
          let distance = List.length c - List.length context in
           S.lift distance term, m, ug
       in
-      let tactics = match xterm with 
-         | Some term -> [destruct ~first_time:true (mk_lterm term)]
-         | None      ->
+      let tactics = match xterms with 
+         | Some terms -> 
+           let map term = destruct ~first_time:false (mk_lterm term) in
+           List.map map terms
+         | None       ->
             let rec mk_tactics first_time i tacs = function
               | []           -> List.rev tacs
               | Some _ :: tl -> 

diff --git a/components/tactics/destructTactic.mli b/components/tactics/destructTactic.mli
index 0ecccdab0a80fdd63eb6fe951016bb5c64e4c2db..cc3f0d5cf7b8b654da2468872691e57e1f05e0b1 100644 (file)
--- a/components/tactics/destructTactic.mli
+++ b/components/tactics/destructTactic.mli
@@ -27,4 +27,4 @@
    looking for constructors. If the two sides differ on two constructors,
    it closes the current goal. If they differ by other two terms it introduces
    an equality. *)
-val destruct_tac: Cic.term option -> ProofEngineTypes.tactic
+val destruct_tac: Cic.term list option -> ProofEngineTypes.tactic

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 45bfa7e3bb4de18551eb4cbd83c67d097325eb08..8c97039fb2eabf789b8031f1746a34a366b91ad8 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Nov  7 13:24:27 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Nov 14 12:07:32 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -32,7 +32,7 @@ val decompose :
   unit -> ProofEngineTypes.tactic
 val demodulate :
   dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
-val destruct : Cic.term option -> ProofEngineTypes.tactic
+val destruct : Cic.term list option -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int ->