]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/primitiveTactics.ml
matitadep: we now handle the inline of an uri, we removed the -exclude option
[helm.git] / helm / software / components / tactics / primitiveTactics.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 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
29 exception NotAnInductiveTypeToEliminate
30 exception WrongUriToVariable of string
31 exception NotAnEliminator
32
33 module PET = ProofEngineTypes
34
35 (* lambda_abstract newmeta ty *)
36 (* returns a triple [bo],[context],[ty'] where              *)
37 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
38 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
39 (* So, lambda_abstract is the core of the implementation of *)
40 (* the Intros tactic.                                       *)
41 (* howmany = -1 means Intros, howmany > 0 means Intros n    *)
42 let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
43  let module C = Cic in
44   let rec collect_context context howmany do_whd ty =
45    match howmany with
46    | 0 ->  
47         let irl =
48           CicMkImplicit.identity_relocation_list_for_metavariable context
49         in
50          context, ty, (C.Meta (newmeta,irl))
51    | _ -> 
52       match ty with 
53         C.Cast (te,_)   -> collect_context context howmany do_whd te 
54       | C.Prod (n,s,t)  ->
55          let n' = mk_fresh_name metasenv context n ~typ:s in
56           let (context',ty,bo) =
57            let entry = match n' with
58               | C.Name _    -> Some (n',(C.Decl s))
59               | C.Anonymous -> None
60            in
61            let ctx = entry :: context in
62            collect_context ctx (howmany - 1) do_whd t 
63           in
64            (context',ty,C.Lambda(n',s,bo))
65       | C.LetIn (n,s,sty,t) ->
66          let (context',ty,bo) =
67           collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t
68          in
69           (context',ty,C.LetIn(n,s,sty,bo))
70       | _ as t ->
71         if howmany <= 0 then
72          let irl =
73           CicMkImplicit.identity_relocation_list_for_metavariable context
74          in
75           context, t, (C.Meta (newmeta,irl))
76         else if do_whd then
77           let t = CicReduction.whd ~delta:true context t in
78           collect_context context howmany false t
79         else
80          raise (PET.Fail (lazy "intro(s): not enough products or let-ins"))
81   in
82    collect_context context howmany true ty 
83
84 let eta_expand metasenv context t arg =
85  let module T = CicTypeChecker in
86  let module S = CicSubstitution in
87  let module C = Cic in
88   let rec aux n =
89    function
90       t' when t' = S.lift n arg -> C.Rel (1 + n)
91     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
92     | C.Var (uri,exp_named_subst) ->
93        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
94         C.Var (uri,exp_named_subst')
95     | C.Meta (i,l) ->
96        let l' =
97         List.map (function None -> None | Some t -> Some (aux n t)) l
98        in
99         C.Meta (i, l')
100     | C.Sort _
101     | C.Implicit _ as t -> t
102     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
103     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
104     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
105     | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t)
106     | C.Appl l -> C.Appl (List.map (aux n) l)
107     | C.Const (uri,exp_named_subst) ->
108        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
109         C.Const (uri,exp_named_subst')
110     | C.MutInd (uri,i,exp_named_subst) ->
111        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
112         C.MutInd (uri,i,exp_named_subst')
113     | C.MutConstruct (uri,i,j,exp_named_subst) ->
114        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
115         C.MutConstruct (uri,i,j,exp_named_subst')
116     | C.MutCase (sp,i,outt,t,pl) ->
117        C.MutCase (sp,i,aux n outt, aux n t,
118         List.map (aux n) pl)
119     | C.Fix (i,fl) ->
120        let tylen = List.length fl in
121         let substitutedfl =
122          List.map
123           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
124            fl
125         in
126          C.Fix (i, substitutedfl)
127     | C.CoFix (i,fl) ->
128        let tylen = List.length fl in
129         let substitutedfl =
130          List.map
131           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
132            fl
133         in
134          C.CoFix (i, substitutedfl)
135   and aux_exp_named_subst n =
136    List.map (function uri,t -> uri,aux n t)
137   in
138    let argty,_ = 
139     T.type_of_aux' metasenv context arg CicUniv.oblivion_ugraph (* TASSI: FIXME *)
140    in
141     let fresh_name =
142      FreshNamesGenerator.mk_fresh_name ~subst:[]
143       metasenv context (Cic.Name "Heta") ~typ:argty
144     in
145      (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
146
147 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
148 let classify_metas newmeta in_subst_domain subst_in metasenv =
149  List.fold_right
150   (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
151     if in_subst_domain i then
152      old_uninst,new_uninst
153     else
154      let ty' = subst_in canonical_context ty in
155       let canonical_context' =
156        List.fold_right
157         (fun entry canonical_context' ->
158           let entry' =
159            match entry with
160               Some (n,Cic.Decl s) ->
161                Some (n,Cic.Decl (subst_in canonical_context' s))
162             | None -> None
163             | Some (n,Cic.Def (bo,ty)) ->
164                Some
165                 (n,
166                   Cic.Def
167                    (subst_in canonical_context' bo,
168                     subst_in canonical_context' ty))
169           in
170            entry'::canonical_context'
171         ) canonical_context []
172      in
173       if i < newmeta then
174        ((i,canonical_context',ty')::old_uninst),new_uninst
175       else
176        old_uninst,((i,canonical_context',ty')::new_uninst)
177   ) metasenv ([],[])
178
179 (* Useful only inside apply_tac *)
180 let
181  generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst
182 =
183  let module C = Cic in
184   let params =
185     let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
186     CicUtil.params_of_obj o
187   in
188    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
189     let next_fresh_meta = ref newmeta in
190     let newmetasenvfragment = ref [] in
191     let exp_named_subst_diff = ref [] in
192      let rec aux =
193       function
194          [],[] -> []
195        | uri::tl,[] ->
196           let ty =
197             let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
198               match o with
199                   C.Variable (_,_,ty,_,_) ->
200                     CicSubstitution.subst_vars !exp_named_subst_diff ty
201                 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
202           in
203 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
204            (match ty with
205                C.Sort (C.Type _) as s -> (* TASSI: ?? *)
206                  let fresh_meta = !next_fresh_meta in
207                  let fresh_meta' = fresh_meta + 1 in
208                   next_fresh_meta := !next_fresh_meta + 2 ;
209                   let subst_item = uri,C.Meta (fresh_meta',[]) in
210                    newmetasenvfragment :=
211                     (fresh_meta,[],C.Sort (C.Type (CicUniv.fresh()))) ::
212                      (* TASSI: ?? *)
213                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
214                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
215                    subst_item::(aux (tl,[]))
216              | _ ->
217 *)
218               let irl =
219                 CicMkImplicit.identity_relocation_list_for_metavariable context
220               in
221               let subst_item = uri,C.Meta (!next_fresh_meta,irl) in
222                newmetasenvfragment :=
223                 (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
224                exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
225                incr next_fresh_meta ;
226                subst_item::(aux (tl,[]))(*)*)
227        | uri::tl1,((uri',_) as s)::tl2 ->
228           assert (UriManager.eq uri uri') ;
229           s::(aux (tl1,tl2))
230        | [],_ -> assert false
231      in
232       let exp_named_subst' = aux (params,exp_named_subst) in
233        !exp_named_subst_diff,!next_fresh_meta,
234         List.rev !newmetasenvfragment, exp_named_subst'
235    in
236     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
237 ;;
238
239 let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termty goal_arity =
240   let (consthead,newmetasenv,arguments,_) =
241    TermUtil.saturate_term newmeta' metasenv' context termty
242     goal_arity in
243   let subst,newmetasenv',_ = 
244    CicUnification.fo_unif_subst 
245      subst context newmetasenv consthead ty CicUniv.oblivion_ugraph
246   in
247   let t = 
248     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
249   in
250   subst,newmetasenv',t
251
252 let rec count_prods context ty =
253  match CicReduction.whd context ty with
254     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
255   | _ -> 0
256
257 let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
258   (* Assumption: The term "term" must be closed in the current context *)
259  let module T = CicTypeChecker in
260  let module R = CicReduction in
261  let module C = Cic in
262   let (_,metasenv,_subst,_,_, _) = proof in
263   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
264   let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
265    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
266     match term with
267        C.Var (uri,exp_named_subst) ->
268         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
269          generalize_exp_named_subst_with_fresh_metas context newmeta uri
270           exp_named_subst
271         in
272          exp_named_subst_diff,newmeta',newmetasenvfragment,
273           C.Var (uri,exp_named_subst')
274      | C.Const (uri,exp_named_subst) ->
275         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
276          generalize_exp_named_subst_with_fresh_metas context newmeta uri
277           exp_named_subst
278         in
279          exp_named_subst_diff,newmeta',newmetasenvfragment,
280           C.Const (uri,exp_named_subst')
281      | C.MutInd (uri,tyno,exp_named_subst) ->
282         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
283          generalize_exp_named_subst_with_fresh_metas context newmeta uri
284           exp_named_subst
285         in
286          exp_named_subst_diff,newmeta',newmetasenvfragment,
287           C.MutInd (uri,tyno,exp_named_subst')
288      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
289         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
290          generalize_exp_named_subst_with_fresh_metas context newmeta uri
291           exp_named_subst
292         in
293          exp_named_subst_diff,newmeta',newmetasenvfragment,
294           C.MutConstruct (uri,tyno,consno,exp_named_subst')
295      | _ -> [],newmeta,[],term
296    in
297    let metasenv' = metasenv@newmetasenvfragment in
298    let termty,_ = 
299      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
300    in
301    let termty =
302      CicSubstitution.subst_vars exp_named_subst_diff termty in
303    let goal_arity = count_prods context ty in
304    let subst,newmetasenv',t = 
305     let rec add_one_argument n =
306      try
307       new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty
308         termty n
309      with CicUnification.UnificationFailure _ when n > 0 ->
310       add_one_argument (n - 1)
311     in
312      add_one_argument goal_arity
313    in
314    let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
315    let apply_subst = CicMetaSubst.apply_subst subst in
316    let old_uninstantiatedmetas,new_uninstantiatedmetas =
317      (* subst_in doesn't need the context. Hence the underscore. *)
318      let subst_in _ = CicMetaSubst.apply_subst subst in
319      classify_metas newmeta in_subst_domain subst_in newmetasenv'
320    in
321    let bo' = apply_subst t in
322    let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
323    let subst_in =
324      (* if we just apply the subtitution, the type is irrelevant:
325               we may use Implicit, since it will be dropped *)
326       ((metano,(context,bo',Cic.Implicit None))::subst)
327    in
328    let (newproof, newmetasenv''') = 
329     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
330      newmetasenv''
331    in
332    let subst = ((metano,(context,bo',ty))::subst) in
333    subst,
334    (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
335    max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
336
337
338 (* ALB *)
339 let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
340   try
341 (*     apply_tac_verbose ~term status *)
342     apply_with_subst ~term ~subst ~maxmeta status
343       (* TODO cacciare anche altre eccezioni? *)
344   with 
345   | CicUnification.UnificationFailure msg
346   | CicTypeChecker.TypeCheckerFailure msg -> raise (PET.Fail msg)
347
348 (* ALB *)
349 let apply_tac_verbose ~term status =
350   let subst, status, _ = apply_with_subst ~term status in
351   (CicMetaSubst.apply_subst subst), status
352
353 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
354
355   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
356   sollevino _solamente_ Fail *)
357 let apply_tac ~term =
358  let apply_tac ~term status =
359   try
360     apply_tac ~term status
361       (* TODO cacciare anche altre eccezioni? *)
362   with 
363   | CicUnification.UnificationFailure msg
364   | CicTypeChecker.TypeCheckerFailure msg ->
365       raise (PET.Fail msg)
366  in
367   PET.mk_tactic (apply_tac ~term)
368
369 let applyP_tac ~term =
370    let applyP_tac status =
371       let res = PET.apply_tactic (apply_tac ~term) status in res
372    in
373    PET.mk_tactic applyP_tac
374
375 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
376  let intros_tac (proof, goal)
377  =
378   let module C = Cic in
379   let module R = CicReduction in
380    let (_,metasenv,_subst,_,_, _) = proof in
381    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
382     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
383      let (context',ty',bo') =
384       lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback
385      in
386       let (newproof, _) =
387        ProofEngineHelpers.subst_meta_in_proof proof metano bo'
388         [newmeta,context',ty']
389       in
390        (newproof, [newmeta])
391  in
392   PET.mk_tactic intros_tac
393   
394 let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
395  let cut_tac
396   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
397   term (proof, goal)
398  =
399   let module C = Cic in
400    let curi,metasenv,_subst,pbo,pty, attrs = proof in
401    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
402     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
403     let newmeta2 = newmeta1 + 1 in
404     let fresh_name =
405      mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
406     let context_for_newmeta1 =
407      (Some (fresh_name,C.Decl term))::context in
408     let irl1 =
409      CicMkImplicit.identity_relocation_list_for_metavariable
410       context_for_newmeta1
411     in
412     let irl2 =
413       CicMkImplicit.identity_relocation_list_for_metavariable context
414     in
415      let newmeta1ty = CicSubstitution.lift 1 ty in
416       let bo' = 
417         Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1))
418       in
419       let (newproof, _) =
420        ProofEngineHelpers.subst_meta_in_proof proof metano bo'
421         [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
422       in
423        (newproof, [newmeta1 ; newmeta2])
424  in
425   PET.mk_tactic (cut_tac ~mk_fresh_name_callback term)
426
427 let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
428  let letin_tac
429   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
430   term (proof, goal)
431  =
432   let module C = Cic in
433    let curi,metasenv,_subst,pbo,pty, attrs = proof in
434    (* occur check *)
435    let occur i t =
436      let m = CicUtil.metas_of_term t in 
437      List.exists (fun (j,_) -> i=j) m
438    in
439    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
440    if occur metano term then
441      raise 
442        (ProofEngineTypes.Fail (lazy
443          "You can't letin a term containing the current goal"));
444     let tty,_ =
445       CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
446      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
447      let fresh_name =
448       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
449      let context_for_newmeta =
450       (Some (fresh_name,C.Def (term,tty)))::context in
451      let irl =
452       CicMkImplicit.identity_relocation_list_for_metavariable
453        context_for_newmeta
454      in
455       let newmetaty = CicSubstitution.lift 1 ty in
456       let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in
457        let (newproof, _) =
458          ProofEngineHelpers.subst_meta_in_proof
459            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
460        in
461         (newproof, [newmeta])
462  in
463   PET.mk_tactic (letin_tac ~mk_fresh_name_callback term)
464
465   (** functional part of the "exact" tactic *)
466 let exact_tac ~term =
467  let exact_tac ~term (proof, goal) =
468   (* Assumption: the term bo must be closed in the current context *)
469   let (_,metasenv,_subst,_,_, _) = proof in
470   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
471   let module T = CicTypeChecker in
472   let module R = CicReduction in
473   let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
474   let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
475   if b then
476    begin
477     let (newproof, metasenv') =
478       ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
479     (newproof, [])
480    end
481   else
482    raise (PET.Fail (lazy "The type of the provided term is not the one expected."))
483  in
484   PET.mk_tactic (exact_tac ~term)
485
486 (* not really "primitive" tactics .... *)
487   
488 module TC  = CicTypeChecker
489 module UM  = UriManager
490 module R   = CicReduction
491 module C   = Cic
492 module PEH = ProofEngineHelpers
493 module PER = ProofEngineReduction
494 module MS  = CicMetaSubst 
495 module S   = CicSubstitution 
496 module T   = Tacticals
497 module RT  = ReductionTactics
498
499 let rec args_init n f =
500    if n <= 0 then [] else f n :: args_init (pred n) f
501
502 let mk_predicate_for_elim 
503  ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no = 
504    let instantiated_eliminator =
505       let f n = if n = 1 then arg else C.Implicit None in
506       C.Appl (using :: args_init args_no f)
507    in
508    let _actual_arg, iety, _metasenv', _ugraph = 
509       CicRefine.type_of_aux' metasenv context instantiated_eliminator ugraph
510    in
511    let _actual_meta, actual_args = match iety with
512       | C.Meta (i, _)                  -> i, []
513       | C.Appl (C.Meta (i, _) :: args) -> i, args
514       | _                              -> assert false
515    in
516 (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
517    let rec mk_pred metasenv context' pred arg' cpattern' = function
518       | []           -> metasenv, pred, arg'
519       | arg :: tail -> 
520 (* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
521          let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
522          let argty = CicReduction.whd context argty in         
523          let fresh_name = 
524             FreshNamesGenerator.mk_fresh_name 
525             ~subst:[] metasenv context' C.Anonymous ~typ:argty in
526          let hyp = Some (fresh_name, C.Decl argty) in
527          let lazy_term c m u =  
528           let distance  = List.length c - List.length context in
529            S.lift distance arg, m, u in
530          let pattern = Some lazy_term, [], Some cpattern' in
531          let subst, metasenv, _ugraph, _conjecture, selected_terms =
532           ProofEngineHelpers.select ~metasenv ~ugraph
533            ~conjecture:(0, context, pred) ~pattern in
534          let metasenv = MS.apply_subst_metasenv subst metasenv in  
535          let map (_context_of_t, t) l = t :: l in
536          let what = List.fold_right map selected_terms [] in
537          let arg' = MS.apply_subst subst arg' in
538          let argty = MS.apply_subst subst argty in
539          let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
540          let pred = MS.apply_subst subst pred in
541          let pred = C.Lambda (fresh_name, argty, pred) in
542          let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
543          mk_pred metasenv (hyp :: context') pred arg' cpattern' tail 
544    in
545    let metasenv, pred, arg = 
546       mk_pred metasenv context goal arg cpattern (List.rev actual_args)
547    in
548    HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
549    metasenv, pred, arg, actual_args
550
551 let beta_after_elim_tac upto predicate =
552    let beta_after_elim_tac status =
553       let proof, goal = status in
554       let _, metasenv, _subst, _, _, _ = proof in
555       let _, _, ty = CicUtil.lookup_meta goal metasenv in
556       let mk_pattern ~equality ~upto ~predicate ty =
557          (* code adapted from ProceduralConversion.generalize *)
558          let meta = C.Implicit None in
559          let hole = C.Implicit (Some `Hole) in
560          let anon = C.Anonymous in
561          let is_meta =
562             let map b = function
563                | C.Implicit None when b -> b
564                | _                      -> false
565             in
566             List.fold_left map true
567          in
568          let rec gen_fix len k (name, i, ty, bo) =
569             name, i, gen_term k ty, gen_term (k + len) bo
570          and gen_cofix len k (name, ty, bo) =
571             name, gen_term k ty, gen_term (k + len) bo
572          and gen_term k = function
573             | C.Sort _ 
574             | C.Implicit _
575             | C.Const (_, _)
576             | C.Var (_, _)
577             | C.MutInd (_, _, _)
578             | C.MutConstruct (_, _, _, _)
579             | C.Meta (_, _) 
580             | C.Rel _ -> meta
581             | C.Appl (hd :: tl) when equality hd (S.lift k predicate) ->
582                assert (List.length tl = upto);
583                hole
584             | C.Appl ts -> 
585                let ts = List.map (gen_term k) ts in
586                if is_meta ts then meta else C.Appl ts
587             | C.Cast (te, ty) -> 
588                let te, ty = gen_term k te, gen_term k ty in
589                if is_meta [te; ty] then meta else C.Cast (te, ty)
590             | C.MutCase (sp, i, outty, t, pl) ->         
591                let outty, t, pl = gen_term k outty, gen_term k t, List.map (gen_term k) pl in
592                if is_meta (outty :: t :: pl) then meta else hole (* C.MutCase (sp, i, outty, t, pl) *)
593             | C.Prod (_, s, t) -> 
594                let s, t = gen_term k s, gen_term (succ k) t in
595                if is_meta [s; t] then meta else C.Prod (anon, s, t)
596             | C.Lambda (_, s, t) ->
597                let s, t = gen_term k s, gen_term (succ k) t in
598                if is_meta [s; t] then meta else C.Lambda (anon, s, t)
599             | C.LetIn (_, s, ty, t) -> 
600                let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in
601                if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t)
602             | C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl)
603             | C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl)
604          in
605          None, [], Some (gen_term 0 ty)
606       in
607       let equality = CicUtil.alpha_equivalence in
608       let pattern = mk_pattern ~equality ~upto ~predicate ty in
609       let tactic = RT.head_beta_reduce_tac ~delta:false ~upto ~pattern in
610       PET.apply_tactic tactic status
611    in
612    PET.mk_tactic beta_after_elim_tac
613
614 (* ANCORA DA DEBUGGARE *)
615
616 exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
617 exception TheSelectedTermsMustLiveInTheGoalContext
618 exception AllSelectedTermsMustBeConvertible;;
619 exception GeneralizationInHypothesesNotImplementedYet;;
620
621 let generalize_tac 
622  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
623  pattern
624  =
625   let module PET = ProofEngineTypes in
626   let generalize_tac mk_fresh_name_callback
627        ~pattern:(term,hyps_pat,_) status
628   =
629    if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
630    let (proof, goal) = status in
631    let module C = Cic in
632    let module T = Tacticals in
633     let uri,metasenv,_subst,pbo,pty, attrs = proof in
634     let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
635     let subst,metasenv,u,selected_hyps,terms_with_context =
636      ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
637       ~conjecture ~pattern in
638     let context = CicMetaSubst.apply_subst_context subst context in
639     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
640     let pbo = CicMetaSubst.apply_subst subst pbo in
641     let pty = CicMetaSubst.apply_subst subst pty in
642     let term =
643      match term with
644         None -> None
645       | Some term ->
646           Some (fun context metasenv ugraph -> 
647                   let term, metasenv, ugraph = term context metasenv ugraph in
648                    CicMetaSubst.apply_subst subst term,
649                     CicMetaSubst.apply_subst_metasenv subst metasenv,
650                     ugraph)
651     in
652     let u,typ,term, metasenv' =
653      let context_of_t, (t, metasenv, u) =
654       match terms_with_context, term with
655          [], None ->
656           raise
657            UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
658        | [], Some t -> context, t context metasenv u
659        | (context_of_t, _)::_, Some t -> 
660            context_of_t, t context_of_t metasenv u
661        | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)
662      in
663       let t,subst,metasenv' =
664        try
665         CicMetaSubst.delift_rels [] metasenv
666          (List.length context_of_t - List.length context) t
667        with
668         CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
669          raise TheSelectedTermsMustLiveInTheGoalContext
670       in
671        (*CSC: I am not sure about the following two assertions;
672          maybe I need to propagate the new subst and metasenv *)
673        assert (subst = []);
674        assert (metasenv' = metasenv);
675        let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
676         u,typ,t,metasenv
677     in
678     (* We need to check:
679         1. whether they live in the context of the goal;
680            if they do they are also well-typed since they are closed subterms
681            of a well-typed term in the well-typed context of the well-typed
682            term
683         2. whether they are convertible
684     *)
685     ignore (
686      List.fold_left
687       (fun u (context_of_t,t) ->
688         (* 1 *)
689         let t,subst,metasenv'' =
690          try
691           CicMetaSubst.delift_rels [] metasenv'
692            (List.length context_of_t - List.length context) t
693          with
694           CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
695            raise TheSelectedTermsMustLiveInTheGoalContext in
696         (*CSC: I am not sure about the following two assertions;
697           maybe I need to propagate the new subst and metasenv *)
698         assert (subst = []);
699         assert (metasenv'' = metasenv');
700         (* 2 *)
701         let b,u1 = CicReduction.are_convertible ~subst context term t u in 
702          if not b then 
703           raise AllSelectedTermsMustBeConvertible
704          else
705           u1
706       ) u terms_with_context) ;
707     let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
708     let proof,goals =
709      PET.apply_tactic 
710       (T.thens 
711         ~start:
712           (cut_tac 
713            (C.Prod(
714              (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
715              typ,
716              (ProofEngineReduction.replace_lifting_csc 1
717                ~equality:(==) 
718                ~what:(List.map snd terms_with_context)
719                ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
720                ~where:ty)
721            )))
722         ~continuations:
723           [(apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ;
724             T.id_tac])
725         status
726     in
727      let _,metasenv'',_subst,_,_, _ = proof in
728       (* CSC: the following is just a bad approximation since a meta
729          can be closed and then re-opened! *)
730       (proof,
731         goals @
732          (List.filter
733            (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'')
734            (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
735              ~newmetasenv:metasenv')))
736  in
737   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
738 ;;
739
740 let generalize_pattern_tac pattern =
741  let generalize_pattern_tac (proof,goal) =
742    let _,metasenv,_,_,_,_ = proof in
743    let conjecture = CicUtil.lookup_meta goal metasenv in
744    let _,context,_ = conjecture in 
745    let generalize_hyps =
746     let _,hpatterns,_ = ProofEngineHelpers.sort_pattern_hyps context pattern in
747      List.map fst hpatterns in
748    let ids_and_patterns =
749     List.map
750      (fun id ->
751        let rel,_ = ProofEngineHelpers.find_hyp id context in
752         id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole))
753      ) generalize_hyps in
754    let tactics =
755     List.map
756      (function (id,pattern) ->
757        Tacticals.then_ ~start:(generalize_tac pattern)
758         ~continuation:(Tacticals.try_tactic
759           (ProofEngineStructuralRules.clear [id]))
760      ) ids_and_patterns
761    in
762     PET.apply_tactic (Tacticals.seq tactics) (proof,goal)
763  in
764   PET.mk_tactic (generalize_pattern_tac)
765 ;;
766
767 let pattern_after_generalize_pattern_tac (tp, hpatterns, cpattern) =
768  let cpattern =
769   match cpattern with
770      None -> ProofEngineTypes.hole
771    | Some t -> t
772  in
773  let cpattern =
774   List.fold_left
775    (fun t (_,ty) -> Cic.Prod (Cic.Anonymous, ty, t)) cpattern hpatterns
776  in
777   tp, [], Some cpattern
778 ;;
779
780 let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = 
781  let elim_tac pattern (proof, goal) =
782    let ugraph = CicUniv.oblivion_ugraph in
783    let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
784    let conjecture = CicUtil.lookup_meta goal metasenv in
785    let metano, context, ty = conjecture in 
786    let pattern = pattern_after_generalize_pattern_tac pattern in
787    let cpattern =
788     match pattern with 
789       | None, [], Some cpattern -> cpattern
790       | _ -> raise (PET.Fail (lazy "not implemented")) in    
791     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
792     let termty = CicReduction.whd context termty in
793     let termty, metasenv', arguments, _fresh_meta =
794      TermUtil.saturate_term
795       (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
796     let term = if arguments = [] then term else Cic.Appl (term::arguments) in
797     let uri, exp_named_subst, typeno, _args =
798      match termty with
799         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
800       | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
801           (uri,exp_named_subst,typeno,args)
802       | _ -> raise NotAnInductiveTypeToEliminate
803     in
804      let eliminator_uri =
805       let buri = UM.buri_of_uri uri in
806       let name = 
807         let o,_ugraph = CicEnvironment.get_obj ugraph uri in
808        match o with
809           C.InductiveDefinition (tys,_,_,_) ->
810            let (name,_,_,_) = List.nth tys typeno in
811             name
812         | _ -> assert false
813       in
814       let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in
815       let ext =
816        match ty_ty with
817           C.Sort C.Prop -> "_ind"
818         | C.Sort C.Set  -> "_rec"
819         | C.Sort (C.CProp _) -> "_rect"
820         | C.Sort (C.Type _)-> "_rect" 
821         | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
822         | _ -> assert false
823       in
824        UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
825      in
826       let eliminator_ref = match using with
827          | None   -> C.Const (eliminator_uri, exp_named_subst)
828          | Some t -> t 
829        in
830        let ety, _ugraph = 
831          TC.type_of_aux' metasenv' context eliminator_ref ugraph in
832 (* FG: ADDED PART ***********************************************************)
833 (* FG: we can not assume eliminator is the default eliminator ***************)
834    let splits, args_no = PEH.split_with_whd (context, ety) in
835    let pred_pos = match List.hd splits with
836       | _, C.Rel i when i > 1 && i <= args_no -> i
837       | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
838       | _ -> raise NotAnEliminator
839    in
840    let metasenv', pred, term, actual_args = match pattern with 
841       | None, [], Some (C.Implicit (Some `Hole)) ->
842          metasenv', C.Implicit None, term, []
843       | _                                        ->
844          mk_predicate_for_elim 
845             ~args_no ~context ~ugraph ~cpattern
846             ~metasenv:metasenv' ~arg:term ~using:eliminator_ref ~goal:ty
847    in
848 (* FG: END OF ADDED PART ****************************************************)
849       let term_to_refine =
850          let f n =
851             if n = pred_pos then pred else
852             if n = 1 then term else C.Implicit None
853          in
854          C.Appl (eliminator_ref :: args_init args_no f)
855       in
856       let refined_term,_refined_termty,metasenv'',_ugraph = 
857          CicRefine.type_of_aux' metasenv' context term_to_refine ugraph
858       in
859       let new_goals =
860          ProofEngineHelpers.compare_metasenvs
861             ~oldmetasenv:metasenv ~newmetasenv:metasenv''
862       in
863       let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
864       let proof'', new_goals' =
865          PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
866       in
867       (* The apply_tactic can have closed some of the new_goals *)
868       let patched_new_goals =
869          let (_,metasenv''',_subst,_,_, _) = proof'' in
870          List.filter
871             (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
872             new_goals @ new_goals'
873       in
874       let res = proof'', patched_new_goals in
875       let upto = List.length actual_args in
876       if upto = 0 then res else 
877       let continuation = beta_after_elim_tac upto pred in
878       let dummy_status = proof,goal in
879       PET.apply_tactic
880          (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)
881          dummy_status
882    in
883    let reorder_pattern ((proof, goal) as status) =
884      let _,metasenv,_,_,_,_ = proof in
885      let conjecture = CicUtil.lookup_meta goal metasenv in
886      let _,context,_ = conjecture in
887      let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
888       PET.apply_tactic
889        (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
890          ~continuation:(PET.mk_tactic (elim_tac pattern))) status
891    in
892     PET.mk_tactic reorder_pattern
893 ;;
894
895 let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term =
896  let cases_tac pattern (proof, goal) =
897   let module TC = CicTypeChecker in
898   let module U = UriManager in
899   let module R = CicReduction in
900   let module C = Cic in
901   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
902   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
903   let pattern = pattern_after_generalize_pattern_tac pattern in
904   let _cpattern =
905    match pattern with 
906      | None, [], Some cpattern ->
907         let rec is_hole =
908          function
909             Cic.Implicit (Some `Hole) -> true
910           | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt
911           | _ -> false
912         in
913          if not (is_hole cpattern) then
914           raise (PET.Fail (lazy "not implemented"))
915      | _ -> raise (PET.Fail (lazy "not implemented")) in    
916   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
917   let termty = CicReduction.whd context termty in
918   let (termty,metasenv',arguments,fresh_meta) =
919    TermUtil.saturate_term
920     (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
921   let term = if arguments = [] then term else Cic.Appl (term::arguments) in
922   let uri,exp_named_subst,typeno,args =
923     match termty with
924     | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
925     | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
926         (uri,exp_named_subst,typeno,args)
927     | _ -> raise NotAnInductiveTypeToEliminate
928   in
929   let paramsno,itty,patterns,right_args =
930     match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
931     | C.InductiveDefinition (tys,_,paramsno,_),_ ->
932        let _,left_parameters,right_args = 
933          List.fold_right 
934            (fun x (n,acc1,acc2) -> 
935              if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2)) 
936            args (List.length args - paramsno, [],[])
937        in
938        let _,_,itty,cl = List.nth tys typeno in
939        let rec aux left_parameters context t =
940          match left_parameters,CicReduction.whd context t with
941          | [],C.Prod (name,source,target) ->
942             let fresh_name =
943               mk_fresh_name_callback metasenv' context name ~typ:source
944             in
945              C.Lambda (fresh_name,C.Implicit None,
946              aux [] (Some (fresh_name,C.Decl source)::context) target)
947          | hd::tl,C.Prod (name,source,target) ->
948              (* left parameters instantiation *)
949              aux tl context (CicSubstitution.subst hd target)
950          | [],_ -> C.Implicit None
951          | _ -> assert false
952        in
953         paramsno,itty,
954         List.map (function (_,cty) -> aux left_parameters context cty) cl,
955         right_args
956     | _ -> assert false
957   in
958   let outtype =
959     let n_right_args = List.length right_args in
960     let n_lambdas = n_right_args + 1 in
961     let lifted_ty = CicSubstitution.lift n_lambdas ty in
962     let captured_ty = 
963       let what = 
964         List.map (CicSubstitution.lift n_lambdas) (right_args)
965       in
966       let with_what meta = 
967         let rec mkargs = function 
968           | 0 -> assert false
969           | 1 -> []
970           | n -> 
971               (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1)) 
972         in
973         mkargs n_lambdas 
974       in
975       let replaced = ref false in
976       let replace = ProofEngineReduction.replace_lifting
977        ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in 
978                   if rc then replaced := true; rc)
979        ~context:[]
980       in
981       let captured = 
982         replace ~what:[CicSubstitution.lift n_lambdas term] 
983           ~with_what:[Cic.Rel 1] ~where:lifted_ty
984       in
985       if not !replaced then
986         (* this means the matched term is not there, 
987          * but maybe right params are: we user rels (to right args lambdas) *)
988         replace ~what ~with_what:(with_what false) ~where:captured
989       else
990         (* since the matched is there, rights should be inferrable *)
991         replace ~what ~with_what:(with_what true) ~where:captured
992     in
993     let captured_term_ty = 
994       let term_ty = CicSubstitution.lift n_right_args termty in
995       let rec mkrels = function 0 -> []|n -> (Cic.Rel n)::(mkrels (n-1)) in
996       let rec fstn acc l n = 
997         if n = 0 then acc else fstn (acc@[List.hd l]) (List.tl l) (n-1) 
998       in
999       match term_ty with
1000       | C.MutInd _ -> term_ty
1001       | C.Appl ((C.MutInd (a,b,c))::args) -> 
1002            C.Appl ((C.MutInd (a,b,c))::
1003                fstn [] args paramsno @ mkrels n_right_args)
1004       | _ -> raise NotAnInductiveTypeToEliminate
1005     in
1006     let rec add_lambdas = function
1007       | 0 -> captured_ty
1008       | 1 -> 
1009           C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
1010       | n -> 
1011            C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
1012                      C.Implicit None, (add_lambdas (n-1)))
1013     in
1014     add_lambdas n_lambdas
1015   in
1016   let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
1017   let refined_term,_,metasenv'',_ = 
1018     CicRefine.type_of_aux' metasenv' context term_to_refine
1019       CicUniv.oblivion_ugraph
1020   in
1021   let new_goals =
1022     ProofEngineHelpers.compare_metasenvs
1023       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
1024   in
1025   let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
1026   let proof'', new_goals' =
1027     PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
1028   in
1029   (* The apply_tactic can have closed some of the new_goals *)
1030   let patched_new_goals =
1031     let (_,metasenv''',_subst,_,_,_) = proof'' in
1032       List.filter
1033         (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
1034         new_goals @ new_goals'
1035     in
1036     proof'', patched_new_goals
1037   in
1038    let reorder_pattern ((proof, goal) as status) =
1039      let _,metasenv,_,_,_,_ = proof in
1040      let conjecture = CicUtil.lookup_meta goal metasenv in
1041      let _,context,_ = conjecture in
1042      let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
1043       PET.apply_tactic
1044        (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
1045          ~continuation:(PET.mk_tactic (cases_tac pattern))) status
1046    in
1047     PET.mk_tactic reorder_pattern
1048 ;;
1049
1050
1051 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
1052                     ?depth ?using ?pattern what =
1053  Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
1054   ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
1055 ;;
1056
1057 (* The simplification is performed only on the conclusion *)
1058 let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
1059                           ?depth ?using ?pattern what =
1060  Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
1061   ~continuation:
1062    (Tacticals.thens
1063      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
1064      ~continuations:
1065        [ReductionTactics.simpl_tac
1066          ~pattern:(ProofEngineTypes.conclusion_pattern None)])
1067 ;;