debian version 0.6.3-2

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 16be77edb443c84c3c7845182564dacfb1601cce..03257dfa1bf46cdbd0563208d2170237e176fa1b 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,73 +23,13 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* mk_fresh_name context name typ                      *)
-(* returns an identifier which is fresh in the context *)
-(* and that resembles [name] as much as possible.      *)
-(* [typ] will be the type of the variable              *)
-let mk_fresh_name context name ~typ =
- let module C = Cic in
-  let basename =
-   match name with
-      C.Anonymous ->
-       (*CSC: great space for improvements here *)
-       (try
-         (match CicTypeChecker.type_of_aux' [] context typ with
-             C.Sort C.Prop -> "H"
-           | C.Sort C.Set -> "x"
-           | _ -> "H"
-         )
-        with CicTypeChecker.TypeCheckerFailure _ -> "H"
-       )
-    | C.Name name ->
-       Str.global_replace (Str.regexp "[0-9]*$") "" name
-  in
-   let already_used name =
-    List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
-   in
-    if not (already_used basename) then
-     C.Name basename
-    else
-     let rec try_next n =
-      let name' = basename ^ string_of_int n in
-       if already_used name' then
-        try_next (n+1)
-       else
-        C.Name name'
-     in
-      try_next 1
-;;
-
-(* identity_relocation_list_for_metavariable i canonical_context         *)
-(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
-(* where n = List.length [canonical_context]                             *)
-(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
- let canonical_context_length = List.length canonical_context in
-  let rec aux =
-   function
-      (_,[]) -> []
-    | (n,None::tl) -> None::(aux ((n+1),tl))
-    | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
-  in
-   aux (1,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta.                       *)
-let new_meta ~proof =
- let (_,metasenv,_,_) = proof in
-  let rec aux =
-   function
-      None,[] -> 1
-    | Some n,[] -> n
-    | None,(n,_,_)::tl -> aux (Some n,tl)
-    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
-  in
-   1 + aux (None,metasenv)
+let new_meta_of_proof ~proof:(_, metasenv, _, _) =
+  CicMkImplicit.new_meta metasenv []
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,bo,ty = proof in
-  let subst_in = CicUnification.apply_subst [meta,term] in
+    (* empty context is ok for term since it wont be used by apply_subst *)
+  let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
    in
@@ -100,15 +40,20 @@ let subst_meta_in_proof proof meta term newmetasenv =
          List.map
           (function
               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
             | None -> None
+            | Some (_,Cic.Def (_,Some _)) -> assert false
           ) canonical_context
         in
          i,canonical_context',(subst_in ty)
       ) metasenv'
     in
      let bo' = subst_in bo in
-      let newproof = uri,metasenv'',bo',ty in
+     (* Metavariables can appear also in the *statement* of the theorem
+      * since the parser does not reject as statements terms with
+      * metavariable therein *)
+     let ty' = subst_in ty in
+      let newproof = uri,metasenv'',bo',ty' in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -126,6 +71,10 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
  let (uri,_,bo,ty) = proof in
   let bo' = subst_in bo in
+  (* Metavariables can appear also in the *statement* of the theorem
+   * since the parser does not reject as statements terms with
+   * metavariable therein *)
+  let ty' = subst_in ty in
   let metasenv' =
    List.fold_right
     (fun metasenv_entry i ->
@@ -136,13 +85,21 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
              (function
                  None -> None
                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
-               | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
+               | Some (i,Cic.Def (t,None))  ->
+                  Some (i,Cic.Def ((subst_in t),None))
+               | Some (_,Cic.Def (_,Some _))  -> assert false
              ) canonical_context
            in
             (m,canonical_context',subst_in ty)::i
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = uri,metasenv',bo',ty in
+   let newproof = uri,metasenv',bo',ty' in
     (newproof, metasenv')
 
+let compare_metasenvs ~oldmetasenv ~newmetasenv =
+ List.map (function (i,_,_) -> i)
+  (List.filter
+   (function (i,_,_) ->
+     not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
+;;