From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 13 Sep 2006 17:22:21 +0000 (+0000)
Subject: Bug fixed in injection: injection can now work on inductive types that have
X-Git-Tag: make_still_working~6896
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6034f308db1dbe8d99d20a083e95b6b09c0a6613;hp=5412a7f12ed2034b4dfb6104440a2308d6a6e8e1;p=helm.git

Bug fixed in injection: injection can now work on inductive types that have
right parameters. It is still bugged on inductive types with left parameters.
---

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 9c9998907..97e9597c6 100644
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -115,35 +115,72 @@ and injection1_tac ~term ~i =
                 let tty',_ = 
 		  CicTypeChecker.type_of_aux' metasenv context t1' 
 		    CicUniv.empty_ugraph  in
-                let pattern =
-                      match fst(CicEnvironment.get_obj 
-				  CicUniv.empty_ugraph turi ) with
-                         C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx,_)  ->
-                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
-                           let i_constr_id,_ = List.nth constructor_list (consno - 1) in
-                            List.map
-                             (function (id,cty) ->
-                               let reduced_cty = CicReduction.whd context cty in
-                                let rec aux t k =
-                                 match t with
-                                    C.Prod (_,_,target) when (k <= nr_ind_params_dx) ->
-                                     aux target (k+1)
-                                  | C.Prod (binder,source,target) when (k > nr_ind_params_dx) ->
- 				    let binder' =
-                                      match binder with
-                                         C.Name b -> C.Name b
-                                       | C.Anonymous -> C.Name "y"
-                                     in
-                                      C.Lambda (binder',source,(aux target (k+1)))
-                                  | _ ->
-                                     let nr_param_constr = k - 1 - nr_ind_params_dx in
-                                      if (id = i_constr_id)
-                                       then C.Rel (nr_param_constr - i + 1)
-                                       else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *)
-                                in aux reduced_cty 1
-                             )
-                             constructor_list
-                       | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible"))
+                let patterns,outtype =
+                 match
+                  fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi)
+                 with
+                    C.InductiveDefinition (ind_type_list,_,paramsno,_)->
+                     let _,_,_,constructor_list =
+                      List.nth ind_type_list typeno in
+                     let i_constr_id,_ =
+                      List.nth constructor_list (consno - 1) in
+                     let patterns =
+                      List.map
+                       (function (id,cty) ->
+                         let reduced_cty = CicReduction.whd context cty in
+                          let rec aux t k =
+                           match t with
+                              C.Prod (_,_,target) when k <= paramsno ->
+                               aux target (k+1)
+                            | C.Prod (binder,source,target) when k > paramsno ->
+ 		               let binder' =
+                                match binder with
+                                   C.Name b -> C.Name b
+                                 | C.Anonymous -> C.Name "y"
+                               in
+                                C.Lambda (binder',source,(aux target (k+1)))
+                            | _ ->
+                               let nr_param_constr = k - 1 - paramsno in
+                                if id = i_constr_id
+                                 then C.Rel (nr_param_constr - i + 1)
+                                 else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *)
+                          in aux reduced_cty 1
+                       ) constructor_list in
+                     let outtype =
+                      let rec to_lambdas te head =
+                       match CicReduction.whd context te with
+                        | C.Prod (name,so,ta) ->
+                           C.Lambda (name,so,to_lambdas ta head)
+                        | _ -> head in
+                      let rec skip_prods n te =
+                       match n, CicReduction.whd context te with
+                          0, _ -> te
+                        | n, C.Prod (_,_,ta) -> skip_prods (n - 1) ta
+                        | _, _ -> assert false
+                      in
+                       let abstracted_tty =
+                        match CicSubstitution.lift (paramsno + 1) tty with
+                           C.MutInd _ as tty' -> tty'
+                         | C.Appl l ->
+                             let keep,abstract =
+                              HExtlib.split_nth (paramsno +1) l in
+                             let rec mk_rels =
+                              function
+                                 0 -> []
+                               | n -> C.Rel n :: (mk_rels (n - 1))
+                             in
+                              C.Appl (keep@mk_rels (List.length abstract))
+                         | _ -> assert false
+                       in
+                        match ind_type_list with
+                           [] -> assert false
+                         | (_,_,ty,_)::_ ->
+                            to_lambdas (skip_prods paramsno ty)
+                             (C.Lambda (C.Name "x", abstracted_tty,
+                               S.lift (2+paramsno) tty'))
+                      in
+                       patterns,outtype
+                  | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible"))
                 in
                 ProofEngineTypes.apply_tactic   
                  (T.thens 
@@ -170,15 +207,18 @@ and injection1_tac ~term ~i =
                                ~pattern:(ProofEngineTypes.conclusion_pattern
                                 (Some new_t1'))
                                (fun _ m u ->
-                                 C.Appl [ C.Lambda (C.Name "x", tty,
-                                  C.MutCase (turi, typeno,
-                                   (C.Lambda ((C.Name "x"),
-                                    (S.lift 1 tty),
-                                    (S.lift 2 tty'))),
-                                   (C.Rel 1), pattern
-                                  )
-                                 );
-                                 t1], m, u))
+let xxx =
+                                 C.Appl [
+                                  C.Lambda
+                                   (C.Name "x",
+                                     tty,
+                                     C.MutCase
+                                      (turi,typeno,outtype,C.Rel 1,patterns)) ;
+                                  t1]
+in
+(*prerr_endline ("XXX: " ^ CicPp.ppterm xxx);*)
+xxx,
+                                 m, u))
                         status
                        ))
                      ~continuation: