helm/gTopLevel/proofEngine.ml

   1 (* Copyright (C) 2000, 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 open ProofEngineHelpers
  27 open ProofEngineTypes
  28
  29   (* proof assistant status *)
  30
  31 let proof = ref (None : proof option)
  32 let goal = ref (None : goal option)
  33
  34 let apply_tactic ~tactic:tactic =
  35  match !proof,!goal with
  36     None,_
  37   | _,None -> assert false
  38   | Some proof', Some goal' ->
  39      let (newproof, newgoals) = tactic ~status:(proof', goal') in
  40      proof := Some newproof;
  41      goal :=
  42       (match newgoals, newproof with
  43           goal::_, _ -> Some goal
  44         | [], (_,(goal,_,_)::_,_,_) ->
  45            (* the tactic left no open goal ; let's choose the first open goal *)
  46 (*CSC: here we could implement and use a proof-tree like notion... *)
  47            Some goal
  48         | _, _ -> None)
  49
  50 (* metas_in_term term                                                *)
  51 (* Returns the ordered list of the metas that occur in [term].       *)
  52 (* Duplicates are removed. The implementation is not very efficient. *)
  53 let metas_in_term term =
  54  let module C = Cic in
  55   let rec aux =
  56    function
  57       C.Rel _
  58     | C.Var _ -> []
  59     | C.Meta (n,_) -> [n]
  60     | C.Sort _
  61     | C.Implicit -> []
  62     | C.Cast (te,ty) -> (aux te) @ (aux ty)
  63     | C.Prod (_,s,t) -> (aux s) @ (aux t)
  64     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
  65     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
  66     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
  67     | C.Const _
  68     | C.MutInd _
  69     | C.MutConstruct _ -> []
  70     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  71        (aux outt) @ (aux t) @
  72         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
  73     | C.Fix (i,fl) ->
  74         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
  75     | C.CoFix (i,fl) ->
  76         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
  77   in
  78    let metas = aux term in
  79     let rec elim_duplicates =
  80      function
  81         [] -> []
  82       | he::tl ->
  83          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
  84     in
  85      elim_duplicates metas
  86
  87 (* perforate context term ty                                                 *)
  88 (* replaces the term [term] in the proof with a new metavariable whose type  *)
  89 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
  90 (* could be easily computed; so the only reasons to have it as an argument   *)
  91 (* are efficiency reasons.                                                   *)
  92 let perforate context term ty =
  93  let module C = Cic in
  94   match !proof with
  95      None -> assert false
  96    | Some (uri,metasenv,bo,gty as proof') ->
  97       let newmeta = new_meta proof' in
  98        (* We push the new meta at the end of the list for pretty-printing *)
  99        (* purposes: in this way metas are ordered.                        *)
 100        let metasenv' = metasenv@[newmeta,context,ty] in
 101         let irl = identity_relocation_list_for_metavariable context in
 102 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
 103         let bo' =
 104          ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
 105         in
 106         (* It may be possible that some metavariables occurred only in *)
 107         (* the term we are perforating and they now occurs no more. We *)
 108         (* get rid of them, collecting the really useful metavariables *)
 109         (* in metasenv''.                                              *)
 110 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
 111 (*CSC: di una metavariabile che compare in bo'!!!!!!!                     *)
 112          let newmetas = metas_in_term bo' in
 113           let metasenv'' =
 114            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
 115           in
 116            proof := Some (uri,metasenv'',bo',gty) ;
 117            goal := Some newmeta
 118
 119
 120 (************************************************************)
 121 (*                  Some easy tactics.                      *)
 122 (************************************************************)
 123
 124 (*CSC: generatore di nomi? Chiedere il nome? *)
 125 let fresh_name =
 126  let next_fresh_index = ref 0
 127 in
 128  function () ->
 129   incr next_fresh_index ;
 130   "fresh_name" ^ string_of_int !next_fresh_index
 131
 132 let reduction_tactic reduction_function term =
 133  let curi,metasenv,pbo,pty =
 134   match !proof with
 135      None -> assert false
 136    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 137  in
 138  let metano,context,ty =
 139   match !goal with
 140      None -> assert false
 141    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 142  in
 143   (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 144   (* the type of one metavariable. So we replace it everywhere.   *)
 145   (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
 146   (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma,  *)
 147   (*CSC: e' meglio prima cercare il termine e scoprirne il        *)
 148   (*CSC: contesto, poi ridurre e infine rimpiazzare.              *)
 149    let replace context where=
 150 (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
 151 (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!!      *)
 152 (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
 153    try
 154     let term' = reduction_function context term in
 155      ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
 156       ~where:where
 157    with
 158     _ -> where
 159    in
 160     let ty' = replace context ty in
 161     let context' =
 162      List.fold_right
 163       (fun entry context ->
 164         match entry with
 165            Some (name,Cic.Def  t) ->
 166             (Some (name,Cic.Def  (replace context t)))::context
 167          | Some (name,Cic.Decl t) ->
 168             (Some (name,Cic.Decl (replace context t)))::context
 169          | None -> None::context
 170       ) context []
 171     in
 172      let metasenv' =
 173       List.map
 174        (function
 175            (n,_,_) when n = metano -> (metano,context',ty')
 176          | _ as t -> t
 177        ) metasenv
 178      in
 179       proof := Some (curi,metasenv',pbo,pty) ;
 180       goal := Some metano
 181
 182 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 183 let reduction_tactic_in_scratch reduction_function term ty =
 184  let metasenv =
 185   match !proof with
 186      None -> []
 187    | Some (_,metasenv,_,_) -> metasenv
 188  in
 189  let metano,context,_ =
 190   match !goal with
 191      None -> assert false
 192    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 193  in
 194   let term' = reduction_function context term in
 195    ProofEngineReduction.replace
 196     ~equality:(==) ~what:term ~with_what:term' ~where:ty
 197
 198 let whd    = reduction_tactic CicReduction.whd
 199 let reduce = reduction_tactic ProofEngineReduction.reduce
 200 let simpl  = reduction_tactic ProofEngineReduction.simpl
 201
 202 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd
 203 let reduce_in_scratch =
 204  reduction_tactic_in_scratch ProofEngineReduction.reduce
 205 let simpl_in_scratch  =
 206  reduction_tactic_in_scratch ProofEngineReduction.simpl
 207
 208 (* It is just the opposite of whd. The code should probably be merged. *)
 209 let fold term =
 210  let curi,metasenv,pbo,pty =
 211   match !proof with
 212      None -> assert false
 213    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 214  in
 215  let metano,context,ty =
 216   match !goal with
 217      None -> assert false
 218    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 219  in
 220   let term' = CicReduction.whd context term in
 221    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 222    (* the type of one metavariable. So we replace it everywhere.   *)
 223    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 224    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 225    let replace =
 226     ProofEngineReduction.replace
 227      ~equality:
 228       (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
 229      ~what:term' ~with_what:term
 230    in
 231     let ty' = replace ty in
 232     let context' =
 233      List.map
 234       (function
 235           Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
 236         | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
 237         | None -> None
 238       ) context
 239     in
 240      let metasenv' =
 241       List.map
 242        (function
 243            (n,_,_) when n = metano -> (metano,context',ty')
 244          | _ as t -> t
 245        ) metasenv
 246      in
 247       proof := Some (curi,metasenv',pbo,pty) ;
 248       goal := Some metano
 249
 250 (************************************************************)
 251 (*              Tactics defined elsewhere                   *)
 252 (************************************************************)
 253
 254   (* primitive tactics *)
 255
 256 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 257 let intros () =
 258   apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
 259 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 260 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 261 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 262 let elim_intros_simpl term =
 263   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
 264 let change ~goal_input:what ~input:with_what =
 265   apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
 266
 267   (* structural tactics *)
 268
 269 let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
 270 let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 271
 272   (* other tactics *)
 273
 274 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 275 let ring () = apply_tactic Ring.ring_tac
 276 let fourier () = apply_tactic FourierR.fourier_tac
 277 let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)