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 mqi_handle = function
 185     [] -> raise NoOtherChoices
 186   | (proof, [])::tl -> (proof, [])::tl
 187   | (proof, (goal,0)::gtl)::tl -> auto_new mqi_handle tl
 188   | (proof, (goal,depth)::gtl)::tl ->
 189       let _,metasenv,_,_ = 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               let local_choices =
 200                 new_search_theorems
 201                   search_theorems_in_context proof goal (depth-1) gtl in
 202               let global_choices =
 203                 new_search_theorems
 204                   (TacticChaser.searchTheorems mqi_handle)
 205                   proof goal (depth-1) gtl in
 206               let all_choices =
 207                 local_choices@global_choices@tl in
 208               let sorting_list (_,g1) (_,g2) =
 209                 let l1 = List.length g1 in
 210                 let l2 = List.length g2 in
 211                 if (l1 = l2 && not(l1 = 0)) then
 212                 (snd(List.nth g2 0)) - (snd(List.nth g1 0))
 213                 else l1 - l2 in
 214               let reorder =
 215                 List.stable_sort sorting_list all_choices
 216               in
 217                 auto_new mqi_handle reorder
 218           | None -> auto_new mqi_handle ((proof,gtl)::tl)
 219 ;;
 220
 221
 222 let auto_tac mqi_handle =
 223  let auto_tac mqi_handle (proof,goal) =
 224   prerr_endline "Entro in Auto";
 225   try
 226     let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
 227 prerr_endline "AUTO_TAC HA FINITO";
 228     (proof,[])
 229   with
 230   | NoOtherChoices ->
 231       prerr_endline("Auto failed");
 232       raise (ProofEngineTypes.Fail "No Applicable theorem")
 233  in
 234   ProofEngineTypes.mk_tactic (auto_tac mqi_handle)
 235 ;;
 236
 237 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
 238 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
 239 funzione di callback che restituisce la (sola) hyp da applicare *)
 240
 241 let assumption_tac =
 242  let module PET = ProofEngineTypes in
 243  let assumption_tac status =
 244   let (proof, goal) = status in
 245   let module C = Cic in
 246   let module R = CicReduction in
 247   let module S = CicSubstitution in
 248   let module PT = PrimitiveTactics in
 249    let _,metasenv,_,_ = proof in
 250     let _,context,ty = CicUtil.lookup_meta goal metasenv in
 251      let rec find n = function
 252         hd::tl ->
 253          (match hd with
 254              (Some (_, C.Decl t)) when
 255                (R.are_convertible context (S.lift n t) ty) -> n
 256            | (Some (_, C.Def (_,Some ty'))) when
 257                (R.are_convertible context ty' ty) -> n
 258            | (Some (_, C.Def (t,None))) when
 259                (R.are_convertible context
 260                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
 261            | _ -> find (n+1) tl
 262          )
 263       | [] -> raise (PET.Fail "Assumption: No such assumption")
 264      in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
 265  in
 266   PET.mk_tactic assumption_tac
 267 ;;
 268
 269 (* ANCORA DA DEBUGGARE *)
 270
 271 exception AllSelectedTermsMustBeConvertible;;
 272
 273 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
 274 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 275 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 276
 277 let generalize_tac
 278  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
 279  =
 280   let module PET = ProofEngineTypes in
 281   let generalize_tac mk_fresh_name_callback terms status =
 282    let (proof, goal) = status in
 283    let module C = Cic in
 284    let module P = PrimitiveTactics in
 285    let module T = Tacticals in
 286     let _,metasenv,_,_ = proof in
 287     let _,context,ty = CicUtil.lookup_meta goal metasenv in
 288      let typ =
 289       match terms with
 290          [] -> assert false
 291        | he::tl ->
 292           (* We need to check that all the convertibility of all the terms *)
 293           List.iter
 294            (function t ->
 295              if not (CicReduction.are_convertible context he t) then
 296               raise AllSelectedTermsMustBeConvertible
 297            ) tl ;
 298           (CicTypeChecker.type_of_aux' metasenv context he)
 299      in
 300       PET.apply_tactic
 301       (T.thens
 302        ~start:
 303          (P.cut_tac
 304           (C.Prod(
 305             (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ),
 306             typ,
 307             (ProofEngineReduction.replace_lifting_csc 1
 308               ~equality:(==)
 309               ~what:terms
 310               ~with_what:(List.map (function _ -> C.Rel 1) terms)
 311               ~where:ty)
 312           )))
 313        ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac])
 314        status
 315  in
 316   PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 317 ;;
 318
 319