]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/discriminationTactics.ml
More warnings.
[helm.git] / helm / software / components / tactics / discriminationTactics.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 let debug = false
29 let debug_print = 
30   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
31 ;;
32
33 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
34 diversi *)
35
36 let discriminate_tac ~term =
37  let module C = Cic in
38  let module U = UriManager in
39  let module P = PrimitiveTactics in
40  let module T = Tacticals in
41  let true_URI =
42   match LibraryObjects.true_URI () with
43      Some uri -> uri
44    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
45  let false_URI =
46   match LibraryObjects.false_URI () with
47      Some uri -> uri
48    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
49  let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
50  let find_discriminating_consno t1 t2 =
51    let rec aux t1 t2 =
52      match t1, t2 with
53      | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
54      | C.Appl ((C.MutConstruct _ as constr1) :: args1),
55        C.Appl ((C.MutConstruct _ as constr2) :: args2)
56        when constr1 = constr2 ->
57          let rec aux_list l1 l2 =
58            match l1, l2 with
59            | [], [] -> None
60            | hd1 :: tl1, hd2 :: tl2 ->
61                (match aux hd1 hd2 with
62                | None -> aux_list tl1 tl2
63                | Some _ as res -> res)
64            | _ -> (* same constructor applied to a different number of args *)
65                assert false
66          in
67          aux_list args1 args2
68      | ((C.MutConstruct (_,_,consno1,subst1)),
69        (C.MutConstruct (_,_,consno2,subst2)))
70      | ((C.MutConstruct (_,_,consno1,subst1)),
71        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
72      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
73        (C.MutConstruct (_,_,consno2,subst2)))
74      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
75        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
76        when (consno1 <> consno2) || (subst1 <> subst2) ->
77          Some consno2
78      | _ -> fail "not a discriminable equality"
79    in
80    aux t1 t2
81  in
82  let mk_branches_and_outtype turi typeno consno context args =
83     (* a list of "True" except for the element in position consno which
84      * is "False" *)
85     match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
86     | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
87         let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
88         let false_constr_id,_ = List.nth constructor_list (consno - 1) in
89         let branches =
90          List.map 
91            (fun (id,cty) ->
92              (* dubbio: e' corretto ridurre in questo context ??? *)
93              let red_ty = CicReduction.whd context cty in
94              let rec aux t k =
95                match t with
96                | C.Prod (_,_,target) when (k <= paramsno) ->
97                    CicSubstitution.subst (List.nth args (k-1))
98                      (aux target (k+1))
99                | C.Prod (binder,source,target) when (k > paramsno) ->
100                    C.Lambda (binder, source, (aux target (k+1)))
101                | _ -> 
102                    if (id = false_constr_id)
103                    then (C.MutInd(false_URI,0,[]))
104                    else (C.MutInd(true_URI,0,[]))
105              in
106              (CicSubstitution.lift 1 (aux red_ty 1)))
107            constructor_list in
108         let outtype =
109          let seed = ref 0 in
110          let rec mk_lambdas rev_left_args =
111           function
112              0, args, C.Prod (_,so,ta) ->
113               C.Lambda
114                (C.Name (incr seed; "x" ^ string_of_int !seed),
115                so,
116                mk_lambdas rev_left_args (0,args,ta))
117            | 0, args, C.Sort _ ->
118               let rec mk_rels =
119                function
120                   0 -> []
121                 | n -> C.Rel n :: mk_rels (n - 1) in
122               let argsno = List.length args in
123                C.Lambda
124                 (C.Name "x",
125                  (if argsno + List.length rev_left_args > 0 then
126                    C.Appl
127                     (C.MutInd (turi, typeno, []) ::
128                      (List.map
129                       (CicSubstitution.lift (argsno + 1))
130                       (List.rev rev_left_args)) @
131                      mk_rels argsno)
132                   else
133                    C.MutInd (turi,typeno,[])),
134                  C.Sort C.Prop)
135            | 0, _, _ -> assert false (* seriously screwed up *)
136            | n, he::tl, C.Prod (_,_,ta) ->
137               mk_lambdas (he::rev_left_args)(n-1,tl,CicSubstitution.subst he ta)
138            | n,_,_ ->
139               assert false (* we should probably reduce in some context *)
140          in
141           mk_lambdas [] (paramsno, args, rty)
142         in
143          branches, outtype 
144     | _ -> assert false
145  in
146  let discriminate'_tac ~term status = 
147   let (proof, goal) = status in
148   let _,metasenv,_subst,_,_, _ = proof in
149   let _,context,_ = CicUtil.lookup_meta goal metasenv in
150   let termty,_ = 
151     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
152   in
153   match termty with
154    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
155      when LibraryObjects.is_eq_URI equri ->
156       let turi,typeno,exp_named_subst,args = 
157         match tty with
158         | (C.MutInd (turi,typeno,exp_named_subst)) ->
159             turi,typeno,exp_named_subst,[]
160         | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
161             turi,typeno,exp_named_subst,args
162         | _ -> fail "not a discriminable equality"
163       in
164       let consno =
165         match find_discriminating_consno t1 t2 with
166         | Some consno -> consno
167         | None -> fail "discriminating terms are structurally equal"
168       in
169       let branches,outtype =
170        mk_branches_and_outtype turi typeno consno context args
171       in
172       ProofEngineTypes.apply_tactic
173        (T.then_
174          ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
175          ~continuation:
176            (T.then_
177              ~start:
178                (ReductionTactics.change_tac 
179                  ~pattern:(ProofEngineTypes.conclusion_pattern None)
180                  (fun _ m u ->
181                    C.Appl [
182                      C.Lambda ( C.Name "x", tty,
183                        C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
184                      t2 ],
185                    m, u))
186              ~continuation:
187                (T.then_
188                  ~start:
189                    (EqualityTactics.rewrite_simpl_tac
190                      ~direction:`RightToLeft
191                      ~pattern:(ProofEngineTypes.conclusion_pattern None)
192                      term [])
193                  ~continuation:
194                    (IntroductionTactics.constructor_tac ~n:1)))) status
195     | _ -> fail "not an equality"
196   in
197   ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
198 ;;
199
200 let exn_nonproj = 
201   ProofEngineTypes.Fail (lazy "Injection: not a projectable equality");;
202 let exn_noneq = 
203   ProofEngineTypes.Fail (lazy "Injection: not an equality");;
204 let exn_nothingtodo = 
205   ProofEngineTypes.Fail (lazy "Nothing to do");;
206 let exn_discrnonind =
207   ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible");;
208 let exn_injwronggoal = 
209   ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct");;
210 let exn_noneqind =
211   ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");;
212
213 let pp ctx t = 
214   let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
215   CicPp.pp t names
216 ;;
217
218 let rec injection_tac ~first_time ~term ~liftno ~continuation =
219  let module C = Cic in
220  let module CR = CicReduction in
221  let module U = UriManager in
222  let module P = PrimitiveTactics in
223  let module T = Tacticals in
224  let module PST = ProofEngineStructuralRules in
225  let module PET = ProofEngineTypes in
226  let are_convertible hd1 hd2 metasenv context = 
227    fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
228  in
229  let injection_tac ~term status = 
230   let (proof, goal) = status in
231   let _,metasenv,_subst, _,_, _ = proof in
232   let _,context,_ = CicUtil.lookup_meta goal metasenv in
233   let term = CicSubstitution.lift liftno term in
234   let termty,_ = 
235     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
236   in
237   debug_print (lazy ("\ninjection su: " ^ pp context termty)); 
238   let tac =
239     match termty with
240     | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] 
241       when LibraryObjects.is_eq_URI equri -> begin
242         match (CicReduction.whd ~delta:true context tty) with
243         | C.MutInd (turi,typeno,ens)
244         | C.Appl (C.MutInd (turi,typeno,ens)::_) -> begin
245             match t1,t2 with
246             | C.MutConstruct (uri1,typeno1,consno1,ens1),
247               C.MutConstruct (uri2,typeno2,consno2,ens2)
248               when (uri1 = uri2) && (typeno1 = typeno2) && 
249                     (consno1 = consno2) && (ens1 = ens2) ->
250                 if first_time then raise exn_nothingtodo
251                 else continuation ~liftno
252             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
253               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
254               when (uri1 = uri2) && (typeno1 = typeno2) &&
255               (consno1 = consno2) && (ens1 = ens2) ->
256                 let rec traverse_list i l1 l2 =
257                   match l1,l2 with
258                   | [],[] when first_time -> continuation
259                   | [],[] -> begin
260                      match term with
261                      | C.Rel n -> begin
262                         match List.nth context (n-1) with
263                         | Some (C.Name id,_) ->
264                            fun ~liftno ->
265                              T.then_ ~start:(PST.clear ~hyps:[id])
266                                ~continuation:(continuation ~liftno)
267                         | _ -> assert false
268                         end
269                      | _ -> assert false
270                      end
271                   | hd1::tl1,hd2::tl2 -> 
272                      if are_convertible hd1 hd2 metasenv context then
273                        traverse_list (i+1) tl1 tl2
274                      else
275                        injection1_tac ~i ~term
276                          ~continuation:(traverse_list (i+1) tl1 tl2)
277                   | _ -> assert false 
278                       (* i 2 termini hanno in testa lo stesso costruttore, 
279                        * ma applicato a un numero diverso di termini *)
280                 in
281                   traverse_list 1 applist1 applist2 ~liftno
282             | C.MutConstruct (uri1,typeno1,consno1,ens1),
283               C.MutConstruct (uri2,typeno2,consno2,ens2)
284             | C.MutConstruct (uri1,typeno1,consno1,ens1),
285               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
286             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
287               C.MutConstruct (uri2,typeno2,consno2,ens2)
288             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
289               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
290               when (consno1 <> consno2) || (ens1 <> ens2) -> 
291                 discriminate_tac ~term
292             | _ when not first_time -> continuation ~liftno
293             | _ (* when first_time *) -> 
294                 match term with
295                 | Cic.Rel i ->
296                   let name = 
297                     match List.nth context (i-1) with
298                     | Some (Cic.Name s, Cic.Def _) -> s
299                     | Some (Cic.Name s, Cic.Decl _) -> s
300                     | _ -> assert false
301                   in
302                   Tacticals.then_
303                     ~start:(ReductionTactics.simpl_tac 
304                       ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None))
305                     ~continuation:(injection_tac ~first_time:false ~term ~liftno
306                       ~continuation)
307                 | _ -> raise exn_nonproj
308             end
309         | _ when not first_time -> continuation ~liftno
310         | _ (* when first_time *) -> raise exn_nonproj
311         end 
312     | _ -> raise exn_nonproj
313   in  
314     PET.apply_tactic tac status
315  in 
316    PET.mk_tactic (injection_tac ~term)
317
318 and injection1_tac ~term ~i ~liftno ~continuation =
319  let module C = Cic in
320  let module CTC = CicTypeChecker in
321  let module CU = CicUniv in
322  let module S = CicSubstitution in
323  let module U = UriManager in
324  let module P = PrimitiveTactics in
325  let module PET = ProofEngineTypes in
326  let module T = Tacticals in
327  let give_name seed = function
328    | C.Name _ as name -> name
329    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
330  in
331  let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in
332  let injection1_tac ~term ~i status =
333   let (proof, goal) = status in
334   (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma 
335    * differiscono (o potrebbero differire?) nell'i-esimo parametro 
336    * del costruttore *)
337   let term = CicSubstitution.lift liftno term in
338   let _,metasenv,_subst,_,_, _ = proof in
339   let _,context,_ = CicUtil.lookup_meta goal metasenv in
340   let termty,_ = 
341     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
342   in
343   debug_print (lazy ("\ninjection1 su : " ^ pp context termty)); 
344   match termty with (* an equality *)
345   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
346     when LibraryObjects.is_eq_URI equri -> 
347       let turi,typeno,ens,params =
348         match tty with (* some inductive type *)
349         | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[]
350         | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params
351         | _ -> raise exn_noneqind
352       in
353       let t1',t2',consno = (* sono i due sottotermini che differiscono *)
354         match t1,t2 with
355         | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
356           C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
357           when (uri1 = uri2) && (typeno1 = typeno2) && 
358                (consno1 = consno2) && (ens1 = ens2) -> 
359                (* controllo ridondante *)
360             List.nth applist1 (i-1),List.nth applist2 (i-1),consno2
361         | _ -> assert false
362       in
363       let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
364       let patterns,outtype =
365         match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
366         | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
367            let left_params, right_params = HExtlib.split_nth paramsno params in
368            let _,_,_,constructor_list = List.nth ind_type_list typeno in
369            let i_constr_id,_ = List.nth constructor_list (consno - 1) in
370            let patterns =
371              let seed = ref 0 in
372              List.map
373                (function (id,cty) ->
374                  let reduced_cty = CicReduction.whd context cty in
375                  let rec aux k = function
376                    | C.Prod (_,_,tgt) when k <= paramsno -> 
377                        let left = List.nth left_params (k-1) in
378                        aux (k+1) (CicSubstitution.subst left tgt)
379                    | C.Prod (binder,source,target) when k > paramsno ->
380                       let binder' = give_name seed binder in
381                       C.Lambda (binder',source,(aux (k+1) target))
382                    | _ ->
383                      let nr_param_constr = k - paramsno - 1 in
384                      if id = i_constr_id then C.Rel (k - i)
385                      else S.lift nr_param_constr t1' 
386                      (* + 1 per liftare anche il lambda aggiunto
387                       * esternamente al case *)
388                  in CicSubstitution.lift 1 (aux 1 reduced_cty))
389                constructor_list 
390            in
391            (* this code should be taken from cases_tac *)
392            let outtype =
393              let seed = ref 0 in
394              let rec to_lambdas te head =
395                match CicReduction.whd context te with
396                | C.Prod (binder,so,ta) ->
397                    let binder' = give_name seed binder in
398                    C.Lambda (binder',so,to_lambdas ta head)
399                | _ -> head 
400              in
401              let rec skip_prods params te =
402                match params, CicReduction.whd context te with
403                | [], _ -> te
404                | left::tl, C.Prod (_,_,ta) -> 
405                    skip_prods tl (CicSubstitution.subst left ta)
406                | _, _ -> assert false
407              in
408              let abstracted_tty =
409                let tty =
410                  List.fold_left (fun x y -> CicSubstitution.subst y x) tty left_params
411                in
412                (* non lift, ma subst coi left! *)
413                match S.lift 1 tty with
414                | C.MutInd _ as tty' -> tty'
415                | C.Appl l ->
416                    let keep,abstract = HExtlib.split_nth (paramsno +1) l in
417                    let keep = List.map (S.lift paramsno) keep in
418                    C.Appl (keep@mk_rels (List.length abstract))
419                | _ -> assert false
420              in
421              match ind_type_list with
422              | [] -> assert false
423              | (_,_,ty,_)::_ ->
424                (* this is in general wrong, do as in cases_tac *)
425                to_lambdas (skip_prods left_params ty)
426                  (C.Lambda 
427                    (C.Name "cased", abstracted_tty,
428                      (* here we should capture right parameters *)
429                      (* 1 for his Lambda, one for the Lambda outside the match
430                       * and then one for each to_lambda *)
431                      S.lift (2+List.length right_params) tty'))
432           in
433             patterns,outtype
434         | _ -> raise exn_discrnonind
435       in
436       let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
437       let changed = 
438         C.Appl [ C.Lambda (C.Name "x", tty, 
439                   C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
440       in
441       (* check if cutted and changed are well typed and if t1' ~ changed *)
442       let go_on =
443         try
444           let _,g = CicTypeChecker.type_of_aux' metasenv context  cutted
445             CicUniv.empty_ugraph
446           in
447           let _,g = CicTypeChecker.type_of_aux' metasenv context changed g in
448           fst (CicReduction.are_convertible ~metasenv context  t1' changed g)
449         with
450         | CicTypeChecker.TypeCheckerFailure _ -> false
451       in
452       if not go_on then
453         PET.apply_tactic Tacticals.id_tac status
454       else
455         (debug_print (lazy ("CUT: " ^ pp context cutted)); 
456         PET.apply_tactic   
457           (T.thens ~start: (P.cut_tac cutted)
458              ~continuations:
459                [injection_tac ~first_time:false ~liftno:0 ~term:(C.Rel 1)
460                   ~continuation:
461                    (fun ~liftno:x -> continuation ~liftno:(liftno+1+x))
462                     (* here I need to lift all the continuations by 1;
463                        since I am setting back liftno to 0, I actually
464                        need to lift all the continuations by liftno + 1 *)
465                ;T.then_ 
466                   ~start:(PET.mk_tactic 
467                     (fun status ->    
468                       debug_print (lazy "riempo il cut"); 
469                       let (proof, goal) = status in
470                       let _,metasenv,_subst,_,_, _ = proof in
471                       let _,context,gty =CicUtil.lookup_meta goal metasenv in
472                       let gty = Unshare.unshare gty in
473                       let new_t1' = 
474                         match gty with 
475                         | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
476                         | _ -> raise exn_injwronggoal
477                       in
478                       debug_print 
479                         (lazy ("metto questo: " ^ pp context changed));
480                       debug_print 
481                         (lazy ("al posto di questo: " ^ pp context new_t1'));
482                       debug_print 
483                         (lazy ("nel goal: " ^ pp context gty));
484                       debug_print 
485                         (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
486                       debug_print 
487                         (lazy ("e poi rewrite con: "^pp context term));
488                       let rc = 
489                         PET.apply_tactic 
490                           (ReductionTactics.change_tac
491                             ~pattern:(None, [], 
492                               Some (ProofEngineHelpers.pattern_of 
493                               ~term:gty [new_t1']))
494                             (fun _ m u -> changed,m,u))
495                           status
496                         in rc
497                       ))
498                   ~continuation:
499                     (T.then_
500                       ~start:
501                         (EqualityTactics.rewrite_simpl_tac
502                           ~direction:`LeftToRight
503                           ~pattern:(PET.conclusion_pattern None)
504                           term [])
505                       ~continuation:EqualityTactics.reflexivity_tac)
506                ])     
507           status)
508    | _ -> raise exn_noneq
509  in
510   PET.mk_tactic (injection1_tac ~term ~i)
511 ;;
512
513 (* destruct performs either injection or discriminate *)
514 (* equivalent to Coq's "analyze equality"             *)
515 let destruct_tac =
516  injection_tac
517   ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
518 ;;