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 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
  27   CicMkImplicit.new_meta metasenv []
  28
  29 let subst_meta_in_proof proof meta term newmetasenv =
  30  let uri,metasenv,bo,ty = proof in
  31     (* empty context is ok for term since it wont be used by apply_subst *)
  32   let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
  33    let metasenv' =
  34     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
  35    in
  36     let metasenv'' =
  37      List.map
  38       (function i,canonical_context,ty ->
  39         let canonical_context' =
  40          List.map
  41           (function
  42               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
  43             | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
  44             | None -> None
  45             | Some (_,Cic.Def (_,Some _)) -> assert false
  46           ) canonical_context
  47         in
  48          i,canonical_context',(subst_in ty)
  49       ) metasenv'
  50     in
  51      let bo' = subst_in bo in
  52      (* Metavariables can appear also in the *statement* of the theorem
  53       * since the parser does not reject as statements terms with
  54       * metavariable therein *)
  55      let ty' = subst_in ty in
  56       let newproof = uri,metasenv'',bo',ty' in
  57        (newproof, metasenv'')
  58
  59 (*CSC: commento vecchio *)
  60 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
  61 (* This (heavy) function must be called when a tactic can instantiate old *)
  62 (* metavariables (i.e. existential variables). It substitues the metasenv *)
  63 (* of the proof with the result of removing [meta] from the domain of     *)
  64 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
  65 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
  66 (*  current proof.                                                        *)
  67 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
  68 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
  69 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
  70 (*CSC: [newmetasenv].                                             *)
  71 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
  72  let (uri,_,bo,ty) = proof in
  73   let bo' = subst_in bo in
  74   (* Metavariables can appear also in the *statement* of the theorem
  75    * since the parser does not reject as statements terms with
  76    * metavariable therein *)
  77   let ty' = subst_in ty in
  78   let metasenv' =
  79    List.fold_right
  80     (fun metasenv_entry i ->
  81       match metasenv_entry with
  82          (m,canonical_context,ty) when m <> meta ->
  83            let canonical_context' =
  84             List.map
  85              (function
  86                  None -> None
  87                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
  88                | Some (i,Cic.Def (t,None))  ->
  89                   Some (i,Cic.Def ((subst_in t),None))
  90                | Some (_,Cic.Def (_,Some _))  -> assert false
  91              ) canonical_context
  92            in
  93             (m,canonical_context',subst_in ty)::i
  94        | _ -> i
  95     ) newmetasenv []
  96   in
  97    let newproof = uri,metasenv',bo',ty' in
  98     (newproof, metasenv')
  99
 100 let compare_metasenvs ~oldmetasenv ~newmetasenv =
 101  List.map (function (i,_,_) -> i)
 102   (List.filter
 103    (function (i,_,_) ->
 104      not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
 105 ;;