- Procedural: generation of "exact" is now complete

[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 0fa4ebaec60a335ee0be727e741e42fac035cf83..0040d7ebfe1a0ff34ba38b5d4b773114f7eb1002 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -462,26 +462,8 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
  in
   PET.mk_tactic (letin_tac ~mk_fresh_name_callback term)
 
-  (** functional part of the "exact" tactic *)
-let exact_tac ~term =
- let exact_tac ~term (proof, goal) =
-  (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_subst,_,_, _) = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let module T = CicTypeChecker in
-  let module R = CicReduction in
-  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
-  let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
-  if b then
-   begin
-    let (newproof, metasenv') =
-      ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
-    (newproof, [])
-   end
-  else
-   raise (PET.Fail (lazy "The type of the provided term is not the one expected."))
- in
-  PET.mk_tactic (exact_tac ~term)
+(* FG: exact_tac := apply_tac as in NTactics *)
+let exact_tac ~term = apply_tac ~term
 
 (* not really "primitive" tactics .... *)
   
@@ -637,7 +619,7 @@ let generalize_tac
       ~conjecture ~pattern in
     let context = CicMetaSubst.apply_subst_context subst context in
     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-    let pbo = CicMetaSubst.apply_subst subst pbo in
+    let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
     let pty = CicMetaSubst.apply_subst subst pty in
     let term =
      match term with
@@ -955,7 +937,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
         right_args
     | _ -> assert false
   in
-  let outtype =
+  let outtypes =
     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
@@ -985,10 +967,11 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
       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
+        [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
+        [replace ~what ~with_what:(with_what false) ~where:captured;
+         replace ~what ~with_what:(with_what true) ~where:captured]
     in
     let captured_term_ty = 
       let term_ty = CicSubstitution.lift n_right_args termty in
@@ -1003,38 +986,46 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
                fstn [] args paramsno @ mkrels n_right_args)
       | _ -> raise NotAnInductiveTypeToEliminate
     in
-    let rec add_lambdas = function
+    let rec add_lambdas captured_ty = function
       | 0 -> captured_ty
       | 1 -> 
-          C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+          C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas captured_ty 0))
       | n -> 
            C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
-                     C.Implicit None, (add_lambdas (n-1)))
+                     C.Implicit None, (add_lambdas captured_ty (n-1)))
     in
-    add_lambdas n_lambdas
+    List.map (fun x -> add_lambdas x n_lambdas) captured_ty
   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.oblivion_ugraph
-  in
-  let new_goals =
-    ProofEngineHelpers.compare_metasenvs
-      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
-  in
-  let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
-  let proof'', new_goals' =
-    PET.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''',_subst,_,_,_) = proof'' in
-      List.filter
-        (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
-        new_goals @ new_goals'
-    in
-    proof'', patched_new_goals
+  let rec first = (* easier than using tacticals *)
+  function 
+  | [] -> raise (PET.Fail (lazy ("unable to generate a working outtype")))
+  | outtype::rest -> 
+     let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+     try
+       let refined_term,_,metasenv'',_ = 
+         CicRefine.type_of_aux' metasenv' context term_to_refine
+           CicUniv.oblivion_ugraph
+       in
+       let new_goals =
+         ProofEngineHelpers.compare_metasenvs
+           ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+       in
+       let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
+         let proof'', new_goals' =
+           PET.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''',_subst,_,_,_) = proof'' in
+             List.filter
+               (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+               new_goals @ new_goals'
+         in
+         proof'', patched_new_goals
+     with PET.Fail _ | CicRefine.RefineFailure _ | CicRefine.Uncertain _ -> first rest
   in
+   first outtypes
+ in
    let reorder_pattern ((proof, goal) as status) =
      let _,metasenv,_,_,_,_ = proof in
      let conjecture = CicUtil.lookup_meta goal metasenv in