]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/compose.ml
Trick: the refiner always subst-expands the outtype, so that the beta-redex
[helm.git] / helm / software / components / tactics / compose.ml
1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
24  *)
25
26 let debug = false;;
27 let debug_print = 
28   if not debug then (fun _ -> ()) else (fun s -> prerr_endline (Lazy.force s))
29 ;;
30
31 let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
32
33 let compose_core t2 t1 (proof, goal) =
34   let _,metasenv,_subst,_,_,_ = proof in
35   let _,context,_ = CicUtil.lookup_meta goal metasenv in
36   let ty1,_ = 
37     CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph 
38   in
39   let ty2,_ = 
40     CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph 
41   in
42   let saturated_ty2, menv_for_saturated_ty2, args_t2 = 
43     let maxm = CicMkImplicit.new_meta metasenv [] in
44     let ty2, menv, args, _ = 
45       TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in
46     ty2, menv, args
47   in
48   let saturations_t2 = 
49     let rec aux n = function 
50       | Cic.Meta (i,_)::tl -> 
51           let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in
52           if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop)
53             CicUniv.oblivion_ugraph) 
54           then n else aux (n+1) tl
55       | _::tl -> aux (n+1) tl
56       | [] -> n+1
57     in
58       List.length args_t2 - aux 0 args_t2 +1
59   in
60   debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context
61     [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^
62     " saturations_t2:" ^ string_of_int saturations_t2));
63   (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
64   let unif menv t = 
65     let m, menv2 =
66       let n = CicMkImplicit.new_meta menv [] in
67       let irl = 
68         CicMkImplicit.identity_relocation_list_for_metavariable context
69       in
70       Cic.Meta (n,irl), ((n,context,t)::menv)
71     in
72     try 
73       let _ = 
74         CicUnification.fo_unif menv context t saturated_ty2
75           CicUniv.oblivion_ugraph
76       in 
77         true, menv2, m
78     with
79     | CicUnification.UnificationFailure _
80     | CicUnification.Uncertain _ -> false, menv2, m
81   in
82   (* check which "positions" in the input arrow unifies with saturated_ty2 *)
83   let rec positions menv cur saturations = function 
84     | Cic.Prod (n,s,t) -> 
85         let b, newmenv, sb = unif menv s in
86         if b then
87           (saturations - cur - 1) :: 
88             (positions newmenv (cur + 1) saturations 
89              (CicSubstitution.subst sb t))
90         else
91           positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
92     | _ -> []
93   in
94   (* position is a list of arities, that is if t1 : a -> b -> c and saturations
95    * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations
96    * is 1 then (t1 t2 ?) of type b -> c *)
97   let rec generate positions menv acc =
98     match positions with
99     | [] -> acc, menv
100     | saturations_t1::tl ->
101       try
102         let t, menv1, _ =
103           CloseCoercionGraph.generate_composite t2 t1 context menv
104             CicUniv.oblivion_ugraph saturations_t2 saturations_t1
105         in
106         assert (List.length menv1 = List.length menv);
107         generate tl menv (t::acc)
108       with 
109       | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
110   in
111   let terms, metasenv =
112     generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
113   in
114   (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
115   let proof = 
116     let uri, _, _subst, bo, ty, attrs = proof in
117     uri, metasenv, _subst, bo, ty, attrs
118   in
119   (* now we have the terms, we generalize them and intros them *)
120   let proof, goal =
121     List.fold_left 
122       (fun (proof,goal) t ->
123         let lazy_of t =
124           ProofEngineTypes.const_lazy_term t
125         in
126         let proof, gl = 
127           ProofEngineTypes.apply_tactic
128             (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None))
129             (proof,goal)
130         in
131         assert(List.length gl = 1);
132         proof,List.hd gl)
133       (proof,goal) terms
134   in
135   (proof, goal), List.length terms
136 ;;
137
138 let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
139   let ((proof, goal), k), n = 
140     match t2 with
141     | Some t2 -> compose_core t1 t2 proofstatus, n-1
142     | None -> 
143         let k = 
144           let proof, goal = proofstatus in
145           let _,metasenv,subst,_,_,_ = proof in
146           let _,_,ty = CicUtil.lookup_meta goal metasenv in
147           count_pi (CicMetaSubst.apply_subst subst ty)
148         in
149         (proofstatus, k), n
150   in
151   let (proof, goal), k = 
152     (* fix iterates n times the composition *)
153     let rec fix proofstatus k t = function
154       | 0 -> proofstatus, k
155       | n ->
156           let t = CicSubstitution.lift k t in
157           let proof, gl =  
158             ProofEngineTypes.apply_tactic 
159               (PrimitiveTactics.intros_tac 
160                 ~howmany:k ?mk_fresh_name_callback ()) proofstatus
161           in
162           assert (List.length gl = 1);
163           let goal = List.hd gl in
164           let k, proofstatus =
165             (* aux compose t with every previous result *)
166             let rec aux k proofstatus = function
167               | 0 -> k, proofstatus
168               | n -> 
169                  let (proof, goal), k1 = 
170                    compose_core t (Cic.Rel n) proofstatus 
171                  in
172                  aux (k+k1) (proof, goal) (n-1)
173             in
174               aux 0 (proof, goal) k
175           in
176           fix proofstatus k t (n-1)
177     in
178       fix (proof, goal) k t1 n
179   in
180   let howmany = 
181     match howmany with
182     | None -> None
183     | Some i ->
184         if i - k < 0 then (* we should generalize back and clear *) Some 0
185         else Some (i - k)
186   in
187      ProofEngineTypes.apply_tactic 
188       (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
189       (proof,goal)
190 ;;
191
192 let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
193   ProofEngineTypes.mk_tactic 
194     (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)
195 ;;