helm/gTopLevel/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 (* identity_relocation_list_for_metavariable i canonical_context         *)
  27 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
  28 (* where n = List.length [canonical_context]                             *)
  29 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
  30 let identity_relocation_list_for_metavariable canonical_context =
  31  let canonical_context_length = List.length canonical_context in
  32   let rec aux =
  33    function
  34       (_,[]) -> []
  35     | (n,None::tl) -> None::(aux ((n+1),tl))
  36     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
  37   in
  38    aux (1,canonical_context)
  39
  40 (* Returns the first meta whose number is above the *)
  41 (* number of the higher meta.                       *)
  42 let new_meta ~proof =
  43  let metasenv =
  44   match proof with
  45      None -> assert false
  46    | Some (_,metasenv,_,_) -> metasenv
  47  in
  48   let rec aux =
  49    function
  50       None,[] -> 1
  51     | Some n,[] -> n
  52     | None,(n,_,_)::tl -> aux (Some n,tl)
  53     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  54   in
  55    1 + aux (None,metasenv)
  56
  57 let subst_meta_in_proof proof meta term newmetasenv =
  58  let (uri,metasenv,bo,ty) =
  59   match proof with
  60      None -> assert false
  61    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
  62  in
  63   let subst_in = CicUnification.apply_subst [meta,term] in
  64    let metasenv' =
  65     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
  66    in
  67     let metasenv'' =
  68      List.map
  69       (function i,canonical_context,ty ->
  70         let canonical_context' =
  71          List.map
  72           (function
  73               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
  74             | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
  75             | None -> None
  76           ) canonical_context
  77         in
  78          i,canonical_context',(subst_in ty)
  79       ) metasenv'
  80     in
  81      let bo' = subst_in bo in
  82       let newproof = Some (uri,metasenv'',bo',ty) in
  83        (newproof, metasenv'')
  84
  85 (*CSC: commento vecchio *)
  86 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
  87 (* This (heavy) function must be called when a tactic can instantiate old *)
  88 (* metavariables (i.e. existential variables). It substitues the metasenv *)
  89 (* of the proof with the result of removing [meta] from the domain of     *)
  90 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
  91 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
  92 (*  current proof.                                                        *)
  93 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
  94 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
  95 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
  96 (*CSC: [newmetasenv].                                             *)
  97 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
  98  let (uri,bo,ty) =
  99   match proof with
 100      None -> assert false
 101    | Some (uri,_,bo,ty) -> uri,bo,ty
 102  in
 103   let bo' = subst_in bo in
 104   let metasenv' =
 105    List.fold_right
 106     (fun metasenv_entry i ->
 107       match metasenv_entry with
 108          (m,canonical_context,ty) when m <> meta ->
 109            let canonical_context' =
 110             List.map
 111              (function
 112                  None -> None
 113                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
 114                | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
 115              ) canonical_context
 116            in
 117             (m,canonical_context',subst_in ty)::i
 118        | _ -> i
 119     ) newmetasenv []
 120   in
 121    let newproof = Some (uri,metasenv',bo',ty) in
 122     (newproof, metasenv')
 123