X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FprimitiveTactics.ml;h=50626aff0ed3f7d41b012a4483b106436d4569fe;hb=609a4bb85c88a5e5090f7db0a6bcf547ba9d0593;hp=6646157240d93ab648ed54386908b03b51da1a28;hpb=2a39b3fe15889f379932c642f4775a5f8e756022;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 664615724..50626aff0 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/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), _ 
@@ -647,89 +652,129 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,proofbo,proofty, attrs) = proof in
-   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-    let termty = CicReduction.whd context termty in
-    let (termty,metasenv',arguments,fresh_meta) =
-     TermUtil.saturate_term
-      (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
-    let term = if arguments = [] then term else Cic.Appl (term::arguments) in
-    let uri,exp_named_subst,typeno,args =
-     match termty with
-        C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
-      | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
-          (uri,exp_named_subst,typeno,args)
-      | _ -> raise NotAnInductiveTypeToEliminate
-    in
-     let paramsno,itty,patterns =
-      match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
-         C.InductiveDefinition (tys,_,paramsno,_),_ ->
-          let _,_,itty,cl = List.nth tys typeno in
-          let rec aux n context t =
-           match n,CicReduction.whd context t with
-              0,C.Prod (name,source,target) ->
-               let fresh_name =
-                mk_fresh_name_callback metasenv' context name
-                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
-                 ~typ:source
-               in
-                C.Lambda (fresh_name,C.Implicit None,
-                 aux 0 (Some (fresh_name,C.Decl source)::context) target)
-            | n,C.Prod (name,source,target) ->
-               let fresh_name =
-                mk_fresh_name_callback metasenv' context name
-                 (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
-                 ~typ:source
-               in
-                aux (n-1) (Some (fresh_name,C.Decl source)::context) target
-            | 0,_ -> C.Implicit None
-            | _,_ -> assert false
-          in
-           paramsno,itty,
-           List.map (function (_,cty) -> aux paramsno context cty) cl 
-       | _ -> assert false
-     in
-      let outtype =
-       let target =
-        C.Lambda (C.Name "fixme",C.Implicit None,
-         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))
+  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let termty = CicReduction.whd context termty in
+  let (termty,metasenv',arguments,fresh_meta) =
+   TermUtil.saturate_term
+    (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+  let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+  let uri,exp_named_subst,typeno,args =
+    match termty with
+    | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+    | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+        (uri,exp_named_subst,typeno,args)
+    | _ -> raise NotAnInductiveTypeToEliminate
+  in
+  let paramsno,itty,patterns,right_args =
+    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    | C.InductiveDefinition (tys,_,paramsno,_),_ ->
+       let _,left_parameters,right_args = 
+         List.fold_right 
+           (fun x (n,acc1,acc2) -> 
+             if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2)) 
+           args (List.length args - paramsno, [],[])
        in
-        let rec add_lambdas =
-         function
-            0 -> target
-          | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
-        in
-         add_lambdas (count_prods context itty - paramsno)
-      in
-       let term_to_refine =
-        C.MutCase (uri,typeno,outtype,term,patterns)
+       let _,_,itty,cl = List.nth tys typeno in
+       let rec aux left_parameters context t =
+         match left_parameters,CicReduction.whd context t with
+         | [],C.Prod (name,source,target) ->
+            let fresh_name =
+              mk_fresh_name_callback metasenv' context name ~typ:source
+            in
+             C.Lambda (fresh_name,C.Implicit None,
+             aux [] (Some (fresh_name,C.Decl source)::context) target)
+         | hd::tl,C.Prod (name,source,target) ->
+             (* left parameters instantiation *)
+             aux tl context (CicSubstitution.subst hd target)
+         | [],_ -> C.Implicit None
+         | _ -> assert false
        in
-        let refined_term,_,metasenv'',_ = 
-         CicRefine.type_of_aux' metasenv' context term_to_refine
-           CicUniv.empty_ugraph
+        paramsno,itty,
+        List.map (function (_,cty) -> aux left_parameters context cty) cl,
+        right_args
+    | _ -> assert false
+  in
+  let outtype =
+    let n_right_args = List.length right_args in
+    let n_lambdas = n_right_args + 1 in
+    let lifted_ty = CicSubstitution.lift n_lambdas ty in
+    let captured_ty = 
+      let what = 
+        List.map (CicSubstitution.lift n_lambdas) (right_args)
+      in
+      let with_what meta = 
+        let rec mkargs = function 
+          | 0 -> assert false
+          | 1 -> []
+          | n -> 
+              (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1)) 
         in
-         let new_goals =
-          ProofEngineHelpers.compare_metasenvs
-           ~oldmetasenv:metasenv ~newmetasenv:metasenv''
-         in
-         let proof' = curi,metasenv'',proofbo,proofty, attrs in
-          let proof'', new_goals' =
-           apply_tactic (apply_tac ~term:refined_term) (proof',goal)
-          in
-           (* The apply_tactic can have closed some of the new_goals *)
-           let patched_new_goals =
-            let (_,metasenv''',_,_,_) = proof'' in
-             List.filter
-              (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
-              ) new_goals @ new_goals'
-           in
-            proof'', patched_new_goals
- in
+        mkargs n_lambdas 
+      in
+      let replaced = ref false in
+      let replace = ProofEngineReduction.replace_lifting
+       ~equality:(fun a b -> let rc = CicUtil.alpha_equivalence a b in 
+                  if rc then replaced := true; rc)
+      in
+      let captured = 
+        replace ~what:[CicSubstitution.lift n_lambdas term] 
+          ~with_what:[Cic.Rel 1] ~where:lifted_ty
+      in
+      if not !replaced then
+        (* this means the matched term is not there, 
+         * but maybe right params are: we user rels (to right args lambdas) *)
+        replace ~what ~with_what:(with_what false) ~where:captured
+      else
+        (* since the matched is there, rights should be inferrable *)
+        replace ~what ~with_what:(with_what true) ~where:captured
+    in
+    let captured_term_ty = 
+      let term_ty = CicSubstitution.lift n_right_args 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_right_args)
+      | _ -> 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 n_lambdas
+  in
+  let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+  let refined_term,_,metasenv'',_ = 
+    CicRefine.type_of_aux' metasenv' context term_to_refine
+      CicUniv.empty_ugraph
+  in
+  let new_goals =
+    ProofEngineHelpers.compare_metasenvs
+      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+  in
+  let proof' = curi,metasenv'',proofbo,proofty, attrs in
+  let proof'', new_goals' =
+    apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+  in
+  (* The apply_tactic can have closed some of the new_goals *)
+  let patched_new_goals =
+    let (_,metasenv''',_,_,_) = proof'' in
+      List.filter
+        (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+        new_goals @ new_goals'
+    in
+    proof'', patched_new_goals
+  in
   mk_tactic (cases_tac ~term)
 ;;