]> matita.cs.unibo.it Git - helm.git/commitdiff
procedural : some improvements.
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 21 Feb 2007 14:15:55 +0000 (14:15 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 21 Feb 2007 14:15:55 +0000 (14:15 +0000)
decompose tactic: user provided premise and types removed.
                  The decomposable types are now the non-recursive inductive
  types without right parameters and are auto-detected

12 files changed:
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralConversion.ml
helm/software/components/acic_procedural/proceduralConversion.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/eliminationTactics.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/help/C/sec_tactics.xml

index b1cbc74abdacec4633ff828efcb1a71999355da7..22936c1a4531a6338dcb2ca3e7916cf062f41490 100644 (file)
@@ -228,7 +228,7 @@ and mk_fwd_rewrite st dtext name tl direction =
          [T.Branch (qs, ""); p2; p1] 
 
 and mk_fwd_proof st dtext name = function
-   | C.AAppl (_, hd :: tl) as v -> 
+   | C.AAppl (_, hd :: tl) as v                         -> 
       if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else  
       if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
       let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
@@ -241,11 +241,16 @@ and mk_fwd_proof st dtext name = function
             let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
             [T.LetIn (name, v, dtext ^ text)]
       end
-   | v                          -> 
-      [T.LetIn (name, v, dtext)] 
+   | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
+      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
+         | None   -> [T.LetIn (name, v, dtext)] 
+         | Some v -> mk_fwd_proof st dtext name v
+      end
+   | v                                                  ->
+      [T.LetIn (name, v, dtext)]
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t) as what -> 
+   | C.ALambda (_, name, v, t) as what             ->
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
       let ety = match get_inner_types st what with
@@ -253,7 +258,7 @@ and mk_proof st = function
         | None          -> None
       in
       mk_proof (add st entry intro ety) t
-   | C.ALetIn (_, name, v, t) as what  ->
+   | C.ALetIn (_, name, v, t) as what              ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
@@ -264,16 +269,16 @@ and mk_proof st = function
         [T.Apply (what, dtext)]
       in
       mk_intros st script
-   | C.ARel _ as what                  ->
+   | C.ARel _ as what                              ->
       let _, dtext = test_depth st in
       let text = "assumption" in
       let script = [T.Apply (what, dtext ^ text)] in 
       mk_intros st script
-   | C.AMutConstruct _ as what         ->
+   | C.AMutConstruct _ as what                     ->
       let _, dtext = test_depth st in
       let script = [T.Apply (what, dtext)] in 
       mk_intros st script   
-   | C.AAppl (_, hd :: tl) as t        ->
+   | C.AAppl (_, hd :: tl) as t                    ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
          let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
@@ -308,7 +313,15 @@ and mk_proof st = function
          [T.Apply (t, dtext)]
       in
       mk_intros st script
-   | t                                 ->
+   | C.AMutCase (id, uri, tyno, outty, arg, cases) ->
+      begin match Cn.mk_ind st.context id uri tyno outty arg cases with 
+         | None   -> 
+            let text = Printf.sprintf "%s" "UNEXPANDED: mutcase" in
+            let script = [T.Note text] in
+            mk_intros st script
+         | Some t -> mk_proof st t
+      end
+   | t                                             ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in
       mk_intros st script
index abd6fd62a8f897f7df4e2b884258706db50804bf..555523a621f2929f46d926f396bb66458f45c43b 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module C = Cic
+module C    = Cic
+module E    = CicEnvironment
+module Un   = CicUniv
+module TC   = CicTypeChecker 
+module D    = Deannotate
+module UM   = UriManager
+
+module T    = ProceduralTypes
+
+(* helpers ******************************************************************)
+
+let cic = D.deannotate_term
+
+let get_ind_type uri tyno =
+   match E.get_obj Un.empty_ugraph uri with
+      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
+      | _                                           -> assert false
+
+let get_default_eliminator context uri tyno ty =
+   let _, (name, _, _, _) = get_ind_type uri tyno in
+   let sort, _ = TC.type_of_aux' [] context ty Un.empty_ugraph in
+   let ext = match sort with
+      | C.Sort C.Prop     -> "_ind"
+      | C.Sort C.Set      -> "_rec"
+      | C.Sort C.CProp    -> "_rec"
+      | C.Sort (C.Type _) -> "_rect" 
+      | C.Meta (_,_)      -> assert false
+      | _                 -> assert false
+    in
+    let buri = UM.buri_of_uri uri in
+    let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
+    C.Const (uri, [])
+
+(* proof construction *******************************************************)
 
 let rec need_whd i = function
    | C.ACast (_, t, _)               -> need_whd i t
@@ -59,3 +92,63 @@ let lift k n =
       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
    in
    lift_term k
+
+let fake_annotate c =
+   let get_binder c m =
+      try match List.nth c (pred m) with
+        | Some (C.Name s, _) -> s
+        | _                  -> assert false
+      with
+         | Invalid_argument _ -> assert false 
+   in
+   let mk_decl n v = Some (n, C.Decl v) in
+   let mk_def n v = Some (n, C.Def (v, None)) in
+   let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
+   let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
+   let rec ann_xns c (uri, t) = uri, ann_term c t
+   and ann_ms c = function
+      | None   -> None
+      | Some t -> Some (ann_term c t)
+   and ann_fix newc c (name, i, ty, bo) =
+      "", name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
+   and ann_cofix newc c (name, ty, bo) =
+      "", name, ann_term c ty, ann_term (List.rev_append newc c) bo
+   and ann_term c = function
+      | C.Sort sort -> C.ASort ("", sort)
+      | C.Implicit ann -> C.AImplicit ("", ann)
+      | C.Rel m -> C.ARel ("", "", m, get_binder c m)
+      | C.Const (uri, xnss) -> C.AConst ("", uri, List.map (ann_xns c) xnss)
+      | C.Var (uri, xnss) -> C.AVar ("", uri, List.map (ann_xns c) xnss)
+      | C.MutInd (uri, tyno, xnss) -> C.AMutInd ("", uri, tyno, List.map (ann_xns c) xnss)
+      | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct ("", uri,tyno,consno, List.map (ann_xns c) xnss)
+      | C.Meta (i, mss) -> C.AMeta("", i, List.map (ann_ms c) mss)
+      | C.Appl ts -> C.AAppl ("", List.map (ann_term c) ts)
+      | C.Cast (te, ty) -> C.ACast ("", ann_term c te, ann_term c ty)
+      | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase ("", sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)      
+      | C.Prod (n, s, t) -> C.AProd ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
+      | C.Lambda (n, s, t) -> C.ALambda ("", n, ann_term c s, ann_term (mk_decl n s :: c) t)
+      | C.LetIn (n, s, t) -> C.ALetIn ("", n, ann_term c s, ann_term (mk_def n s :: c) t)
+      | C.Fix (i, fl) -> C.AFix ("", i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
+      | C.CoFix (i, fl) -> C.ACoFix ("", i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
+   in
+   ann_term c
+
+let rec add_abst n t =
+   if n <= 0 then t else
+   let t = C.ALambda ("", C.Anonymous, C.AImplicit ("", None), lift 0 1 t) in  
+   add_abst (pred n) t
+
+let mk_ind context id uri tyno outty arg cases =
+   let lpsno, (_, _, arity, constructors) = get_ind_type uri tyno in
+   let inty, _ = TC.type_of_aux' [] context (cic arg) Un.empty_ugraph in
+   let ps = match inty with
+      | C.MutInd _                  -> []
+      | C.Appl (C.MutInd _ :: args) -> List.map (fake_annotate context) args
+      | _                           -> assert false
+   in
+   let lps, rps = T.list_split lpsno ps in      
+   let eliminator = get_default_eliminator context uri tyno inty in
+   let arg_ref = T.mk_arel 0 "" in
+   let body = C.AMutCase (id, uri, tyno, outty, arg_ref, cases) in
+   let predicate = add_abst (succ (List.length rps)) body in   
+   None
index d5ad4fd1c9634e7620bc4f8d9f53195792ceeeb4..fef3ad07b0aba093fb3d4342bf93c098ceac11e8 100644 (file)
@@ -26,3 +26,8 @@
 val need_whd: int -> Cic.annterm -> bool
 
 val lift: int -> int -> Cic.annterm -> Cic.annterm
+
+val mk_ind: 
+   Cic.context -> Cic.id -> UriManager.uri -> int -> 
+   Cic.annterm -> Cic.annterm -> Cic.annterm list ->
+   Cic.annterm option
index 10d7b6bccad33d454a73385686ea9c085e1944fe..24fb99d79d1b88623462c97eabbaba3287850ce2 100644 (file)
@@ -32,10 +32,6 @@ type loc = Token.flocation
 type ('term, 'lazy_term, 'ident) pattern =
   'lazy_term option * ('ident * 'term) list * 'term option
 
-type ('term, 'ident) type_spec =
-   | Ident of 'ident
-   | Type of UriManager.uri * int 
-
 type 'lazy_term reduction =
   [ `Normalize
   | `Reduce
@@ -56,7 +52,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
-  | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
+  | Decompose of loc * 'ident list
   | Demodulate of loc
   | Destruct of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
index d5fbf80343c42a413c718b27fa3bbc93baf1dfaf..423e68d4f93ce30e5d77e82cb761eeab9fbcaffe 100644 (file)
@@ -95,15 +95,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Cut (_, ident, term) ->
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
-  | Decompose (_, [], what, names) ->
-      sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) 
-  | Decompose (_, types, what, names) ->
-      let to_ident = function
-         | Ident id -> id
-        | Type _   -> assert false 
-      in
-      let types = List.rev_map to_ident types in
-      sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Decompose (_, names) ->
+      sprintf "decompose%s" (pp_intros_specs (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
index ab98132210238daf670872dacbb356cf6817c9df..1714bf470ac8c070e97a98e3327eee7a4183bb50 100644 (file)
@@ -80,15 +80,9 @@ let tactic_of_ast status ast =
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
-  | GrafiteAst.Decompose (_, types, what, names) -> 
-      let to_type = function
-         | GrafiteAst.Type (uri, typeno) -> uri, Some typeno
-        | GrafiteAst.Ident _            -> assert false
-      in
-      let user_types = List.rev_map to_type types in
-      let dbd = LibraryDb.instance () in
+  | GrafiteAst.Decompose (_, names) ->
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+      Tactics.decompose ~mk_fresh_name_callback ()
   | GrafiteAst.Demodulate _ -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
index 7d110e2df6a5e4844d894d4ab96f2afb5ee92691..0c64bbb0794ece3e80c68de116ce640dfbfde413 100644 (file)
@@ -148,24 +148,8 @@ let disambiguate_tactic
     | GrafiteAst.Cut (loc, ident, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Cut (loc, ident, cic)
-    | GrafiteAst.Decompose (loc, types, what, names) ->
-        let disambiguate (metasenv,types) = function
-           | GrafiteAst.Type _   -> assert false
-           | GrafiteAst.Ident id ->
-              (match
-                disambiguate_term context metasenv
-                 (CicNotationPt.Ident(id, None))
-               with
-                | metasenv,Cic.MutInd (uri, tyno, _) ->
-                    metasenv,(GrafiteAst.Type (uri, tyno) :: types)
-                | _ ->
-                  raise (GrafiteDisambiguator.DisambiguationError
-                   (0,[[[],[],None,lazy "Decompose works only on inductive types",true]])))
-        in
-        let metasenv,types =
-         List.fold_left disambiguate (metasenv,[]) types
-        in
-         metasenv,GrafiteAst.Decompose (loc, types, what, names)
+    | GrafiteAst.Decompose (loc, names) ->
+         metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
     | GrafiteAst.Destruct (loc,term) ->
index 64c10b9b47e575db35b37981aa79ffc15c95d3b8..fd757d141a9334ead4539e6c5d74bf0ffc552170 100644 (file)
@@ -157,12 +157,9 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
-        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
-        let types = match types with None -> [] | Some types -> types in
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
        let idents = match idents with None -> [] | Some idents -> idents in
-       let to_spec id = GrafiteAst.Ident id in
-       GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+       GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
index d05826ec0a514e962278afa6e69952bd8df919f7..c98f020d7139a522be67d9b0c97f26a71a76f18e 100644 (file)
 
 (* $Id$ *)
 
-module C = Cic
-module P = PrimitiveTactics
-module T = Tacticals
-module S = ProofEngineStructuralRules
-module F = FreshNamesGenerator
-module E = ProofEngineTypes
-module H = ProofEngineHelpers
-module R = ReductionTactics
-
-(*
-(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
-let search_inductive_types ty =
-   let rec aux types = function 
-      | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> 
-         (uri, typeno) :: types
-      | C.Appl applist -> List.fold_left aux types applist
-      | _              -> types
-   in
-   aux [] ty
-(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *)
-*)
+module C    = Cic
+module P    = PrimitiveTactics
+module T    = Tacticals
+module S    = ProofEngineStructuralRules
+module F    = FreshNamesGenerator
+module PET  = ProofEngineTypes
+module H    = ProofEngineHelpers
+module RT   = ReductionTactics
+module E    = CicEnvironment
+module R    = CicReduction
+module Un   = CicUniv
+
+(* from ProceduralClasify ***************************************************)
+
+let split c t =
+   let add s v c = Some (s, C.Decl v) :: c in
+   let rec aux whd a n c = function
+      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
+      | v when whd        -> v :: a, n
+      | v                 -> aux true a n c (R.whd ~delta:true c v)
+    in
+    aux false [] 0 c t
 
-(* unexported tactics *******************************************************)
+(****************************************************************************)
 
 type type_class = Other
                 | Ind
@@ -55,6 +56,25 @@ type type_class = Other
 
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
+let get_inductive_type uri tyno =
+   match E.get_obj Un.empty_ugraph uri with
+      | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
+         let _, inductive, arity, _ = List.nth tys tyno in
+         lpsno, inductive, arity
+      | _                                           -> assert false
+
+let rec check_type = function 
+   | C.MutInd (uri, tyno, _) -> 
+      let lpsno, inductive, arity = get_inductive_type uri tyno in
+      let _, psno = split [] arity in
+      if lpsno <> psno && inductive then Other else Ind 
+(*   | C.Const (uri, _) as t     -> 
+      if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other
+*)   | C.Appl (hd :: tl)         -> check_type hd
+   | _                         -> Other
+
+(* unexported tactics *******************************************************)
+
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
@@ -69,39 +89,29 @@ let rec scan_tac ~old_context_length ~index ~tactic =
               let tac = T.then_ ~start:(tactic ~what)
                                 ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic)
                in
-              try E.apply_tactic tac status 
-              with E.Fail _ -> aux (pred index)
+              try PET.apply_tactic tac status 
+              with PET.Fail _ -> aux (pred index)
       in aux (index + context_length - old_context_length)
    in
-   E.mk_tactic scan_tac
-
-let rec check_types types = function 
-   | C.MutInd (uri, typeno, _) -> 
-      if List.mem (uri, Some typeno) types then Ind else Other
-   | C.Const (uri, _) as t     -> 
-      if List.mem (uri, None) types then Con (E.const_lazy_term t) else Other
-   | C.Appl (hd :: tl)         -> check_types types hd
-   | _                         -> Other
+   PET.mk_tactic scan_tac
 
-let elim_clear_unfold_tac ~mk_fresh_name_callback ~types ~what =
+let elim_clear_unfold_tac ~mk_fresh_name_callback ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
-      match check_types types ty with 
-         | Ind   ->
-           let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
-                             ~continuation:(S.clear [what])
-           in
-           E.apply_tactic tac status
-         | Con t ->
-           let tac = R.unfold_tac (Some t) ~pattern:(premise_pattern what) in
-           E.apply_tactic tac status
+      let tac = match check_type ty with 
+         | Ind   -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+                           ~continuation:(S.clear [what])
+         | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what)
         | Other -> 
-           raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
+           let msg = "unexported elim_clear: not an decomposable type" in
+           raise (PET.Fail (lazy msg))
+      in
+      PET.apply_tactic tac status
    in
-   E.mk_tactic elim_clear_unfold_tac
+   PET.mk_tactic elim_clear_unfold_tac
 
 (* elim type ****************************************************************)
 
@@ -115,9 +125,9 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
     let tac =
       T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
     in
-    E.apply_tactic tac status
+    PET.apply_tactic tac status
   in
-  E.mk_tactic elim_type_tac
+  PET.mk_tactic elim_type_tac
 
 (* decompose ****************************************************************)
 
@@ -132,22 +142,15 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
-                  ?(user_types=[]) ?what ~dbd =
+let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
       let _, metasenv,_,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
-      let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback ~types in
+      let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in
       let old_context_length = List.length context in      
-      let tac = match what with
-        | Some what -> 
-           T.then_ ~start:(tactic ~what)
-                    ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
-        | None      ->
-            scan_tac ~old_context_length ~index:old_context_length ~tactic
+      let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
       in
-      E.apply_tactic tac status
+      PET.apply_tactic tac status
    in
-   E.mk_tactic decompose_tac
+   PET.mk_tactic decompose_tac
index 379166ac03068c4311df69ea643f0854628c6c68..492566042911d1bdc71a7e3eb115f90bc376c90a 100644 (file)
@@ -29,5 +29,4 @@ val elim_type_tac:
 
 val decompose_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?user_types:((UriManager.uri * int option) list) ->
- ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ unit -> ProofEngineTypes.tactic
index d821a3cb21d2af996c614dcc4f3a2965af44e359..f0ac7adc89d9f2a65ca5266bd3073abe51508a9c 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jan 24 20:31:34 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Feb 21 14:36:23 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -25,8 +25,7 @@ val cut :
   Cic.term -> ProofEngineTypes.tactic
 val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?user_types:(UriManager.uri * int option) list ->
-  ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+  unit -> ProofEngineTypes.tactic
 val demodulate :
   dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
 val destruct : term:Cic.term -> ProofEngineTypes.tactic
index aa9610df0aa83e22c517da9782111274710a0d56..cad04a53c400a3ab17ba867ca49fe9429aedc5b0 100644 (file)
     <title>decompose</title>
     <titleabbrev>decompose</titleabbrev>
     <para><userinput>
-     decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) 
-     H as H<subscript>1</subscript> ... H<subscript>m</subscript>
+     decompose as H<subscript>1</subscript> ... H<subscript>m</subscript>
     </userinput></para>
     <para>
       <variablelist>
           <listitem>
             <para>
             <emphasis role="bold">decompose</emphasis>
-            [<emphasis role="bold">(</emphasis>
-            &id;…
-            <emphasis role="bold">)</emphasis>]
-            [&id;] 
             [<emphasis role="bold">as</emphasis> &id;…]
            </para>
           </listitem>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para> 
-            <command>H</command> must inhabit one inductive type among  
-            <command>
-             T<subscript>1</subscript> ... T<subscript>n</subscript>
-            </command>
-            and the types of a predefined list.
-           </para>
+            <para>None.</para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
             <para>
-            Runs <command>
-             elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
-            </command>, clears <command>H</command> and tries to run itself
-            recursively on each new identifier introduced by 
+            For each each premise <command>H</command> 
+            of type <command>T</command> in the current context
+            where <command>T</command> is a non-recursive inductive type
+            withour right parameters, the tactic runs
+            <command> 
+             elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
+            </command>, clears <command>H</command>  and runs itself
+            recursively on each new premise introduced by 
             <command>elim</command> in the opened sequents. 
-            If <command>H</command> is not provided tries this operation on
-            each premise in the current context.
            </para>
           </listitem>
         </varlistentry>