Bug fixed in cases (it did not produced the right number of lambdas for the

[helm.git] / helm / software / components / tactics / primitiveTactics.ml

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index c9d68d9deccfe96770cf888097cfcc1797ec6a20..2e9a3db33f9204afa1ab3ccccb19a96f43f06af0 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -231,7 +231,7 @@ let
 
 let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty
+   TermUtil.saturate_term newmeta' metasenv' context termty
     goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
@@ -485,7 +485,7 @@ let elim_tac ~term =
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
     let (termty,metasenv',arguments,fresh_meta) =
-     ProofEngineHelpers.saturate_term
+     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 =
@@ -560,6 +560,100 @@ let elim_tac ~term =
   mk_tactic (elim_tac ~term)
 ;;
 
+let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+ let cases_tac ~term (proof, goal) =
+  let module T = CicTypeChecker in
+  let module U = UriManager in
+  let module R = CicReduction in
+  let module C = Cic in
+   let (curi,metasenv,proofbo,proofty) = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let termty,_ = T.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))
+       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)
+       in
+prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
+        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 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)
+;;
+
+
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                     ?depth ?using what =
  Tacticals.then_ ~start:(elim_tac ~term:what)