]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/eliminationTactics.ml
transcript: now we can generate procedural output
[helm.git] / helm / software / components / tactics / eliminationTactics.ml
1 (* Copyright (C) 2002, HELM Team.
2  *
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  *
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  *
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  *
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 module C    = Cic
29 module I    = CicInspect
30 module S    = CicSubstitution
31 module TC   = CicTypeChecker 
32 module P    = PrimitiveTactics
33 module T    = Tacticals
34 module PESR = ProofEngineStructuralRules
35 module F    = FreshNamesGenerator
36 module PET  = ProofEngineTypes
37 module RT   = ReductionTactics
38 module E    = CicEnvironment
39 module R    = CicReduction
40 module Un   = CicUniv
41 module PEH  = ProofEngineHelpers
42
43 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
44
45 let get_inductive_def uri =
46    match E.get_obj Un.oblivion_ugraph uri with
47       | C.InductiveDefinition (tys, _, lpsno, _), _ -> 
48          lpsno, tys
49       | _                                           -> assert false
50
51 let is_not_recursive uri tyno tys = 
52    let map mutinds (_, ty) = 
53 (* FG: we can do much better here *)      
54       let map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
55 (**********************************)      
56       let premises, _ = PEH.split_with_whd ([], ty) in
57       List.fold_left map mutinds (List.tl premises)
58    in
59    let msg = "recursiveness check non implemented for mutually inductive types" in
60    if List.length tys > 1 then raise (PET.Fail (lazy msg)) else
61    let _, _, _, constructors = List.nth tys tyno in
62    let mutinds = List.fold_left map I.S.empty constructors in
63    I.S.is_empty mutinds
64
65 let rec check_type sorts metasenv context t = 
66    match R.whd ~delta:true context t with
67       | C.MutInd (uri, tyno, _) as t -> 
68          let lpsno, tys = get_inductive_def uri in
69          let _, inductive, arity, _ = List.nth tys tyno in
70          let _, psno = PEH.split_with_whd ([], arity) in
71          let not_relation = (lpsno = psno) in
72          let not_recursive = is_not_recursive uri tyno tys in
73          let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
74          let sort = match PEH.split_with_whd (context, ty_ty) with
75             | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
76             | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
77             | _                        -> assert false
78          in
79          let right_sort = List.mem sort sorts in
80          if not_relation && inductive && not_recursive && right_sort then
81          begin
82             HLog.warn (Printf.sprintf "Decomposing %s %u" (UriManager.string_of_uri uri) (succ tyno));
83             true 
84          end
85          else false 
86       | C.Appl (hd :: tl)         -> check_type sorts metasenv context hd
87       | _                         -> false
88
89 (* unexported tactics *******************************************************)
90
91 let rec scan_tac ~old_context_length ~index ~tactic =
92    let scan_tac status =
93       let (proof, goal) = status in
94       let _, metasenv, _subst, _, _, _ = proof in
95       let _, context, _ = CicUtil.lookup_meta goal metasenv in
96       let context_length = List.length context in
97       let rec aux index =
98          match PEH.get_name context index with 
99             | _ when index <= 0 -> (proof, [goal])
100             | None              -> aux (pred index)
101             | Some what         -> 
102                let tac = T.then_ ~start:(tactic ~what)
103                                  ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic)
104                in
105                try PET.apply_tactic tac status 
106                with PET.Fail _ -> aux (pred index)
107       in aux (index + context_length - old_context_length)
108    in
109    PET.mk_tactic scan_tac
110
111 let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
112    let elim_clear_unfold_tac status =
113       let (proof, goal) = status in
114       let _, metasenv, _subst, _, _, _ = proof in
115       let _, context, _ = CicUtil.lookup_meta goal metasenv in
116       let index, ty = PEH.lookup_type metasenv context what in
117       let tac = 
118          if check_type sorts metasenv context (S.lift index ty) then 
119             T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
120                     ~continuation:(PESR.clear [what])
121          else 
122             let msg = "unexported elim_clear: not an decomposable type" in
123             raise (PET.Fail (lazy msg))
124       in
125       PET.apply_tactic tac status
126    in
127    PET.mk_tactic elim_clear_unfold_tac
128
129 (* elim type ****************************************************************)
130
131 let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
132   ?using what
133 =
134   let elim =
135     P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
136   in
137   let elim_type_tac status =
138     let tac =
139       T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
140     in
141     PET.apply_tactic tac status
142   in
143   PET.mk_tactic elim_type_tac
144
145 (* decompose ****************************************************************)
146
147 (* robaglia --------------------------------------------------------------- *)
148
149   (** perform debugging output? *)
150 let debug = false
151 let debug_print = fun _ -> ()
152
153   (** debugging print *)
154 let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
155
156 (* roba seria ------------------------------------------------------------- *)
157
158 let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))]) 
159                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
160    let decompose_tac status =
161       let (proof, goal) = status in
162       let _, metasenv, _subst, _,_, _ = proof in
163       let _, context, _ = CicUtil.lookup_meta goal metasenv in
164       let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
165       let old_context_length = List.length context in      
166       let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
167       in
168       PET.apply_tactic tac status
169    in
170    PET.mk_tactic decompose_tac