From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Apr 2007 11:20:22 +0000 (+0000)
Subject: hopefully fixed cases implementation
X-Git-Tag: make_still_working~6415
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=631ef9768bce3958ca275cb7e5f0ff2de8e5e2a1;p=helm.git

hopefully fixed cases implementation
---

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 664615724..de68ca053 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -54,7 +54,8 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
       | C.Prod (n,s,t)  ->
          let n' = mk_fresh_name metasenv context n ~typ:s in
           let (context',ty,bo) =
-           collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) do_whd t 
+           let ctx = (Some (n',(C.Decl s)))::context in
+           collect_context ctx (howmany - 1) do_whd t 
           in
            (context',ty,C.Lambda(n',s,bo))
       | C.LetIn (n,s,t) ->
@@ -545,6 +546,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
          TC.type_of_aux' metasenv' context eliminator_ref ugraph in
 (* FG: ADDED PART ***********************************************************)
 (* FG: we can not assume eliminator is the default eliminator ***************)
+(*
    let add_lambdas n t =
       let rec aux n t =
          if n <= 0 then t 
@@ -552,6 +554,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       in
       aux n (S.lift n t)
    in
+*)
    let rec args_init n f =
       if n <= 0 then [] else f n :: args_init (pred n) f
    in
@@ -561,11 +564,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
       | _ -> raise NotAnEliminator
    in
+(*
    let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
    let termty_ty =
       let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
       CicReduction.whd context termty_ty
    in
+*)
 (*   
    let metasenv', term, pred, upto = match cpatt, termty_ty with
       | C.Implicit (Some `Hole), _ 
@@ -689,22 +694,54 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
            paramsno,itty,
            List.map (function (_,cty) -> aux paramsno context cty) cl 
        | _ -> assert false
+     in
+     let _,right_args = 
+       List.fold_right 
+         (fun x (n,acc) -> if n > 0 then (n-1,x::acc) else (n,acc)) 
+         args (List.length args - paramsno, [])
      in
       let outtype =
-       let target =
-        C.Lambda (C.Name "fixme",C.Implicit None,
-         ProofEngineReduction.replace_lifting
+       let n_lambdas = List.length right_args + 1 in
+       let lifted_ty = CicSubstitution.lift n_lambdas ty in
+       let replace = ProofEngineReduction.replace_lifting
           ~equality:(ProofEngineReduction.alpha_equivalence)
-          ~what:[CicSubstitution.lift (paramsno+1) term]
-          ~with_what:[C.Rel (paramsno+1)]
-          ~where:(CicSubstitution.lift (paramsno+1) ty))
        in
-        let rec add_lambdas =
-         function
-            0 -> target
-          | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
+       let captured_ty = 
+         let what = 
+           List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
+         in
+         let with_what = 
+           let rec mkargs = function 
+             | 0 -> []
+             | 1 -> [Cic.Rel 1]
+             | n -> (Cic.Implicit None)::(mkargs (n-1)) 
+           in
+           mkargs n_lambdas 
+         in
+         replace ~what ~with_what ~where:lifted_ty
+       in
+       let captured_term_ty = 
+         let term_ty = CicSubstitution.lift (n_lambdas-1) termty in
+         let rec mkrels = function 0 -> []|n -> (Cic.Rel n)::(mkrels (n-1)) in
+         let rec fstn acc l n = 
+           if n = 0 then acc else fstn (acc@[List.hd l]) (List.tl l) (n-1) 
+         in
+         match term_ty with
+         | C.MutInd _ -> term_ty
+         | C.Appl ((C.MutInd (a,b,c))::args) -> 
+              C.Appl ((C.MutInd (a,b,c))::
+                  fstn [] args paramsno @ mkrels (n_lambdas -1))
+         | _ -> raise NotAnInductiveTypeToEliminate
+       in
+        let rec add_lambdas = function
+          | 0 -> captured_ty
+          | 1 -> 
+              C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+          | n -> 
+              C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
+                        C.Implicit None, (add_lambdas (n-1)))
         in
-         add_lambdas (count_prods context itty - paramsno)
+         add_lambdas n_lambdas
       in
        let term_to_refine =
         C.MutCase (uri,typeno,outtype,term,patterns)