helm/ocaml/tactics/proofEngineHelpers.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* mk_fresh_name context name typ                      *)
  27 (* returns an identifier which is fresh in the context *)
  28 (* and that resembles [name] as much as possible.      *)
  29 (* [typ] will be the type of the variable              *)
  30 let mk_fresh_name context name ~typ =
  31  let module C = Cic in
  32   let basename =
  33    match name with
  34       C.Anonymous ->
  35        (*CSC: great space for improvements here *)
  36        (try
  37          (match CicTypeChecker.type_of_aux' [] context typ with
  38              C.Sort C.Prop -> "H"
  39            | C.Sort C.CProp -> "H"
  40            | C.Sort C.Set -> "x"
  41            | _ -> "H"
  42          )
  43         with CicTypeChecker.TypeCheckerFailure _ -> "H"
  44        )
  45     | C.Name name ->
  46        Str.global_replace (Str.regexp "[0-9]*$") "" name
  47   in
  48    let already_used name =
  49     List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
  50    in
  51     if not (already_used basename) then
  52      C.Name basename
  53     else
  54      let rec try_next n =
  55       let name' = basename ^ string_of_int n in
  56        if already_used name' then
  57         try_next (n+1)
  58        else
  59         C.Name name'
  60      in
  61       try_next 1
  62 ;;
  63
  64 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
  65   CicMkImplicit.new_meta metasenv
  66
  67 let subst_meta_in_proof proof meta term newmetasenv =
  68  let uri,metasenv,bo,ty = proof in
  69   let subst_in = CicMetaSubst.apply_subst [meta,term] in
  70    let metasenv' =
  71     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
  72    in
  73     let metasenv'' =
  74      List.map
  75       (function i,canonical_context,ty ->
  76         let canonical_context' =
  77          List.map
  78           (function
  79               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
  80             | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
  81             | None -> None
  82             | Some (_,Cic.Def (_,Some _)) -> assert false
  83           ) canonical_context
  84         in
  85          i,canonical_context',(subst_in ty)
  86       ) metasenv'
  87     in
  88      let bo' = subst_in bo in
  89       let newproof = uri,metasenv'',bo',ty in
  90        (newproof, metasenv'')
  91
  92 (*CSC: commento vecchio *)
  93 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
  94 (* This (heavy) function must be called when a tactic can instantiate old *)
  95 (* metavariables (i.e. existential variables). It substitues the metasenv *)
  96 (* of the proof with the result of removing [meta] from the domain of     *)
  97 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
  98 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
  99 (*  current proof.                                                        *)
 100 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
 101 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
 102 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
 103 (*CSC: [newmetasenv].                                             *)
 104 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
 105  let (uri,_,bo,ty) = proof in
 106   let bo' = subst_in bo in
 107   let metasenv' =
 108    List.fold_right
 109     (fun metasenv_entry i ->
 110       match metasenv_entry with
 111          (m,canonical_context,ty) when m <> meta ->
 112            let canonical_context' =
 113             List.map
 114              (function
 115                  None -> None
 116                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
 117                | Some (i,Cic.Def (t,None))  ->
 118                   Some (i,Cic.Def ((subst_in t),None))
 119                | Some (_,Cic.Def (_,Some _))  -> assert false
 120              ) canonical_context
 121            in
 122             (m,canonical_context',subst_in ty)::i
 123        | _ -> i
 124     ) newmetasenv []
 125   in
 126    let newproof = uri,metasenv',bo',ty in
 127     (newproof, metasenv')
 128