helm/ocaml/tactics/variousTactics.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
  27 (* Da rimuovere, solo per debug*)
  28 let print_context ctx =
  29     let print_name =
  30      function
  31         Cic.Name n -> n
  32       | Cic.Anonymous -> "_"
  33     in
  34      List.fold_right
  35       (fun i (output,context) ->
  36         let (newoutput,context') =
  37          match i with
  38             Some (n,Cic.Decl t) ->
  39               print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
  40           | Some (n,Cic.Def (t,None)) ->
  41               print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
  42           | None ->
  43               "_ ?= _\n", None::context
  44           | Some (_,Cic.Def (_,Some _)) -> assert false
  45         in
  46          output^newoutput,context'
  47       ) ctx ("",[])
  48   ;;
  49
  50
  51
  52
  53
  54 let search_theorems_in_context status =
  55   let (proof, goal) = status in
  56   let module C = Cic in
  57   let module R = CicReduction in
  58   let module S = CicSubstitution in
  59   let module PET = ProofEngineTypes in
  60   let module PT = PrimitiveTactics in
  61   prerr_endline "Entro in search_context";
  62   let _,metasenv,_,_ = proof in
  63   let _,context,ty = CicUtil.lookup_meta goal metasenv in
  64   let rec find n = function
  65       [] -> []
  66     | hd::tl ->
  67         let res =
  68           try
  69             Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status )
  70           with
  71             PET.Fail _ -> None in
  72         (match res with
  73           Some res -> res::(find (n+1) tl)
  74         | None -> find (n+1) tl)
  75   in
  76   try
  77     let res = find 1 context in
  78     prerr_endline "Ho finito context";
  79     res
  80   with Failure s ->
  81     prerr_endline ("SIAM QUI = " ^ s); []
  82 ;;
  83
  84 exception NotAProposition;;
  85 exception NotApplicableTheorem;;
  86 exception MaxDepth;;
  87
  88 let depth = 3;;
  89
  90 (*
  91 let rec auto_tac_aux mqi_handle level proof goal =
  92 prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level));
  93 if level = 0 then
  94   (* (proof, [goal]) *)
  95   (prerr_endline ("MaxDepth");
  96    raise MaxDepth)
  97 else
  98   (* let us verify that the metavariable is still an open goal --
  99      it could have been closed by closing other goals -- and that
 100      it is of sort Prop *)
 101   let _,metasenv,_,_ = proof in
 102   let meta_inf =
 103     (try
 104        let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
 105          Some (ey, ty)
 106      with _ -> None) in
 107   match meta_inf with
 108       Some (ey, ty) ->
 109         prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
 110         prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
 111         (* if the goal does not have a sort Prop we return the
 112            current proof and a list containing the goal *)
 113         let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in
 114           if CicReduction.are_convertible
 115             ey (Cic.Sort Cic.Prop) ty_sort then
 116             (* sort Prop *)
 117             (* choices is a list of pairs proof and goallist *)
 118             let choices  =
 119               (search_theorems_in_context (proof,goal))@
 120               (TacticChaser.searchTheorems mqi_handle (proof,goal))
 121             in
 122             let rec try_choices = function
 123                 [] -> raise NotApplicableTheorem
 124               | (proof,goallist)::tl ->
 125 prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
 126                   (try
 127                      List.fold_left
 128                        (fun proof goal ->
 129                             auto_tac_aux mqi_handle (level-1) proof goal)
 130                        proof goallist
 131                    with
 132                      | MaxDepth
 133                      | NotApplicableTheorem
 134                      | NotAProposition ->
 135                          try_choices tl) in
 136               try_choices choices
 137           else
 138             (* CUT AND PASTE DI PROVA !! *)
 139             let choices  =
 140               (search_theorems_in_context (proof,goal))@
 141               (TacticChaser.searchTheorems mqi_handle (proof,goal))
 142             in
 143             let rec try_choices = function
 144                 [] -> raise NotApplicableTheorem
 145               | (proof,[])::tl -> proof
 146               | _::tl -> try_choices tl in
 147             try_choices choices
 148             (* raise NotAProposition *)
 149     | None -> proof
 150 ;;
 151
 152 let auto_tac mqi_handle =
 153  let module PET = ProofEngineTypes in
 154  let auto_tac mqi_handle (proof,goal) =
 155   prerr_endline "Entro in Auto";
 156   try
 157     let proof = auto_tac_aux mqi_handle depth proof goal in
 158     prerr_endline "AUTO_TAC HA FINITO";
 159      (proof,[])
 160   with
 161   | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
 162   | NotApplicableTheorem ->
 163       prerr_endline("No applicable theorem");
 164       raise (ProofEngineTypes.Fail "No Applicable theorem")
 165  in
 166   PET.mk_tactic (auto_tac mqi_handle)
 167 ;;
 168
 169 *)
 170
 171 (**** ESPERIMENTO ************************)
 172
 173 let new_search_theorems f proof goal depth gtl =
 174   let local_choices = f (proof,goal)
 175   in
 176   List.map
 177     (function (proof, goallist) ->
 178        (proof, (List.map (function g -> (g,depth)) goallist)@gtl))
 179     local_choices
 180 ;;
 181
 182 exception NoOtherChoices;;
 183
 184 let rec auto_new dbh = function
 185     [] -> raise NoOtherChoices
 186   | (proof, [])::tl -> (proof, [])::tl
 187   | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
 188   | (proof, (goal,depth)::gtl)::tl ->
 189       let _,metasenv,proof_obj,_ = proof in
 190       let meta_inf =
 191         (try
 192            let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
 193              Some (ey, ty)
 194          with _ -> None) in
 195         match meta_inf with
 196             Some (ey, ty) ->
 197                prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
 198                prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
 199                prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj));
 200               let local_choices =
 201                 new_search_theorems
 202                   search_theorems_in_context proof goal (depth-1) gtl in
 203               let global_choices =
 204                 new_search_theorems
 205                   (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
 206 (*                (TacticChaser.searchTheorems mqi_handle)  *)
 207                   proof goal (depth-1) gtl in
 208               let all_choices =
 209                 local_choices@global_choices@tl in
 210               let sorting_list (_,g1) (_,g2) =
 211                 let l1 = List.length g1 in
 212                 let l2 = List.length g2 in
 213                 if (l1 = l2 && not(l1 = 0)) then
 214                 (snd(List.nth g2 0)) - (snd(List.nth g1 0))
 215                 else l1 - l2 in
 216               let reorder =
 217                 List.stable_sort sorting_list all_choices
 218               in
 219                 auto_new dbh reorder
 220           | None -> auto_new dbh ((proof,gtl)::tl)
 221 ;;
 222
 223
 224 let auto_tac ~(dbh:Dbi.connection) =
 225 (*   CicMetaSubst.reset_counters (); *)
 226  let auto_tac dbh (proof,goal) =
 227   prerr_endline "Entro in Auto";
 228   try
 229     (match auto_new dbh [(proof, [(goal,depth)])] with
 230     | (proof,_)::_  ->
 231       prerr_endline "AUTO_TAC HA FINITO";
 232   (*     CicMetaSubst.print_counters (); *)
 233       (proof,[])
 234     | _ -> assert false)
 235   with
 236   | NoOtherChoices ->
 237       prerr_endline("Auto failed");
 238       raise (ProofEngineTypes.Fail "No Applicable theorem")
 239  in
 240   ProofEngineTypes.mk_tactic (auto_tac dbh)
 241 ;;
 242
 243 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
 244 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
 245 funzione di callback che restituisce la (sola) hyp da applicare *)
 246
 247 let assumption_tac =
 248  let module PET = ProofEngineTypes in
 249  let assumption_tac status =
 250   let (proof, goal) = status in
 251   let module C = Cic in
 252   let module R = CicReduction in
 253   let module S = CicSubstitution in
 254   let module PT = PrimitiveTactics in
 255    let _,metasenv,_,_ = proof in
 256     let _,context,ty = CicUtil.lookup_meta goal metasenv in
 257      let rec find n = function
 258         hd::tl ->
 259          (match hd with
 260              (Some (_, C.Decl t)) when
 261                (R.are_convertible context (S.lift n t) ty) -> n
 262            | (Some (_, C.Def (_,Some ty'))) when
 263                (R.are_convertible context ty' ty) -> n
 264            | (Some (_, C.Def (t,None))) when
 265                (R.are_convertible context
 266                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
 267            | _ -> find (n+1) tl
 268          )
 269       | [] -> raise (PET.Fail "Assumption: No such assumption")
 270      in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
 271  in
 272   PET.mk_tactic assumption_tac
 273 ;;
 274
 275 (* ANCORA DA DEBUGGARE *)
 276
 277 exception AllSelectedTermsMustBeConvertible;;
 278
 279 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
 280 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 281 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 282
 283 let generalize_tac
 284  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
 285  =
 286   let module PET = ProofEngineTypes in
 287   let generalize_tac mk_fresh_name_callback terms status =
 288    let (proof, goal) = status in
 289    let module C = Cic in
 290    let module P = PrimitiveTactics in
 291    let module T = Tacticals in
 292     let _,metasenv,_,_ = proof in
 293     let _,context,ty = CicUtil.lookup_meta goal metasenv in
 294      let typ =
 295       match terms with
 296          [] -> assert false
 297        | he::tl ->
 298           (* We need to check that all the convertibility of all the terms *)
 299           List.iter
 300            (function t ->
 301              if not (CicReduction.are_convertible context he t) then
 302               raise AllSelectedTermsMustBeConvertible
 303            ) tl ;
 304           (CicTypeChecker.type_of_aux' metasenv context he)
 305      in
 306       PET.apply_tactic
 307       (T.thens
 308        ~start:
 309          (P.cut_tac
 310           (C.Prod(
 311             (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ),
 312             typ,
 313             (ProofEngineReduction.replace_lifting_csc 1
 314               ~equality:(==)
 315               ~what:terms
 316               ~with_what:(List.map (function _ -> C.Rel 1) terms)
 317               ~where:ty)
 318           )))
 319        ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac])
 320        status
 321  in
 322   PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 323 ;;
 324
 325