X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=3ef39d0c512dbb52c6b35398b78d1199ca02dc83;hb=8465f33f9ad62040f41a2a2604745cda11725d98;hp=1398424353462320e130403a5bbc0a325d4d8e6b;hpb=9897efac755aac85095075b7e0a967fe340092c1;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 139842435..3ef39d0c5 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/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
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_) = proof in
+  let (_,metasenv,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = CicMkImplicit.new_meta metasenv subst in
+  let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -321,25 +321,25 @@ let apply_with_subst ~term ~subst (proof, goal) =
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
      newmetasenv''
    in
-   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
-    (newproof, 
-     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   subst,
+   (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+   max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 
 
 (* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_with_subst ~term ~subst status
+    apply_with_subst ~term ~subst ~maxmeta status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
-  | CicTypeChecker.TypeCheckerFailure msg ->
-      raise (Fail msg)
+  | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_with_subst ~term status in
+  let subst, status, _ = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
@@ -365,7 +365,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
  =
   let module C = Cic in
   let module R = CicReduction in
-   let (_,metasenv,_,_) = proof in
+   let (_,metasenv,_,_, _) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
@@ -385,7 +385,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty = proof in
+   let curi,metasenv,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
@@ -420,7 +420,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty = proof in
+   let curi,metasenv,pbo,pty, attrs = proof in
    (* occur check *)
    let occur i t =
      let m = CicUtil.metas_of_term t in 
@@ -456,7 +456,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
 let exact_tac ~term =
  let exact_tac ~term (proof, goal) =
   (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_,_) = proof in
+  let (_,metasenv,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
@@ -480,12 +480,12 @@ let elim_tac ~term =
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,proofbo,proofty) = proof in
+   let (curi,metasenv,proofbo,proofty, attrs) = 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) =
-     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 =
@@ -544,13 +544,13 @@ let elim_tac ~term =
             ProofEngineHelpers.compare_metasenvs
              ~oldmetasenv:metasenv ~newmetasenv:metasenv''
            in
-           let proof' = curi,metasenv'',proofbo,proofty 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
+              let (_,metasenv''',_,_, _) = proof'' in
                List.filter
                 (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
                 ) new_goals @ new_goals'
@@ -560,6 +560,99 @@ 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, attrs) = 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
+        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)
+;;
+
+
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                     ?depth ?using what =
  Tacticals.then_ ~start:(elim_tac ~term:what)
@@ -586,7 +679,7 @@ let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =
-      let curi, metasenv, pbo, pty = proof in
+      let curi, metasenv, pbo, pty, attrs = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
       let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in