snapshot (first version in which some extensions work, e.g. infix +)

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 92b89a679c987c293e4395f993930707c5ad3d2b..c6dc1bf4a4169b60ed5eb769d2ac4918a82f541c 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -161,8 +161,9 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
 let new_metasenv_for_apply newmeta proof context ty =
  let module C = Cic in
  let module S = CicSubstitution in
-  let rec aux newmeta =
-   function
+  let rec aux newmeta ty =
+   let ty' = (*CicReduction.whd context*) ty in 
+   match ty' with
       C.Cast (he,_) -> aux newmeta he
 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
       (* If the expected type is a Type, then also Set is OK ==>
@@ -205,11 +206,7 @@ let
  let module C = Cic in
   let params =
     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      match o with
-         C.Constant (_,_,_,params)
-       | C.CurrentProof (_,_,_,_,params)
-       | C.Variable (_,_,_,params)
-       | C.InductiveDefinition (_,params,_) -> params
+    CicUtil.params_of_obj o
   in
    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
     let next_fresh_meta = ref newmeta in
@@ -222,7 +219,7 @@ let
           let ty =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-                 C.Variable (_,_,ty,_) ->
+                 C.Variable (_,_,ty,_,_) ->
                    CicSubstitution.subst_vars !exp_named_subst_diff ty
                | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
           in
@@ -262,6 +259,19 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
+let new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty termty =
+  let (consthead,newmetas,arguments,_) =
+    new_metasenv_for_apply newmeta' proof context termty
+  in
+  let newmetasenv = metasenv'@newmetas in
+  let subst,newmetasenv',_ = 
+    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+  in
+  let t = 
+    if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)
+  in
+  subst,newmetasenv',t
+
 let apply_tac_verbose ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
@@ -303,47 +313,39 @@ let apply_tac_verbose ~term (proof, goal) =
      | _ -> [],newmeta,[],term
    in
    let metasenv' = metasenv@newmetasenvfragment in
-   let termty,_ = (* TASSI:FIXME *)
+   let termty,_ = 
      CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty
    in
-    (* newmeta is the lowest index of the new metas introduced *)
-    let (consthead,newmetas,arguments,_) =
-     new_metasenv_for_apply newmeta' proof context termty
-    in
-     let newmetasenv = metasenv'@newmetas in
-      let subst,newmetasenv',_ = (* TASSI:FIXME *)
-        CicUnification.fo_unif newmetasenv context consthead ty 
-         CicUniv.empty_ugraph
-      in
-       let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
-       let apply_subst = CicMetaSubst.apply_subst subst in
-        let old_uninstantiatedmetas,new_uninstantiatedmetas =
-         (* subst_in doesn't need the context. Hence the underscore. *)
-         let subst_in _ = CicMetaSubst.apply_subst subst in
-          classify_metas newmeta in_subst_domain subst_in newmetasenv'
-        in
-         let bo' =
-          apply_subst
-           (if List.length newmetas = 0 then
-             term'
-            else
-             Cic.Appl (term'::arguments)
-           )
-         in
-         let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-         let subst_in =
-           (* if we just apply the subtitution, the type is irrelevant:
+   let subst,newmetasenv',t = 
+     try
+       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
+         termty
+     with CicUnification.UnificationFailure _ -> 
+       new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
+         (CicReduction.whd context termty)
+   in
+   let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
+   let apply_subst = CicMetaSubst.apply_subst subst in
+   let old_uninstantiatedmetas,new_uninstantiatedmetas =
+     (* subst_in doesn't need the context. Hence the underscore. *)
+     let subst_in _ = CicMetaSubst.apply_subst subst in
+     classify_metas newmeta in_subst_domain subst_in newmetasenv'
+   in
+   let bo' = apply_subst t in
+   let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
+   let subst_in =
+     (* if we just apply the subtitution, the type is irrelevant:
              we may use Implicit, since it will be dropped *)
-           CicMetaSubst.apply_subst 
-            ((metano,(context, bo', Cic.Implicit None))::subst)
-         in
-         let (newproof, newmetasenv''') =
-           subst_meta_and_metasenv_in_proof
-             proof metano subst_in newmetasenv''
-         in
-           (subst_in,(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+     CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+   in
+   let (newproof, newmetasenv''') = 
+     subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
+   in
+     (subst_in,
+       (newproof, 
+          List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
 
@@ -386,7 +388,7 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
  let cut_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
@@ -494,7 +496,7 @@ let elim_tac ~term =
       let name = 
        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
-          C.InductiveDefinition (tys,_,_) ->
+          C.InductiveDefinition (tys,_,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in
             name
         | _ -> assert false
@@ -556,6 +558,11 @@ let elim_tac ~term =
   mk_tactic (elim_tac ~term)
 ;;
 
+let elim_intros_tac ~term =
+ Tacticals.then_ ~start:(elim_tac ~term)
+  ~continuation:(intros_tac ())
+;;
+
 (* The simplification is performed only on the conclusion *)
 let elim_intros_simpl_tac ~term =
  Tacticals.then_ ~start:(elim_tac ~term)