helm/software/components/ng_tactics/nAuto.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 open Printf
  15
  16 let debug = false
  17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = CicNotationPt
  22
  23 (* =================================== paramod =========================== *)
  24 let auto_paramod ~params:(l,_) status goal =
  25   let gty = get_goalty status goal in
  26   let n,h,metasenv,subst,o = status#obj in
  27   let status,t = term_of_cic_term status gty (ctx_of gty) in
  28   let status, l =
  29     List.fold_left
  30       (fun (status, l) t ->
  31         let status, t = disambiguate status t None (ctx_of gty) in
  32         let status, ty = typeof status (ctx_of t) t in
  33         let status, t =  term_of_cic_term status t (ctx_of gty) in
  34         let status, ty = term_of_cic_term status ty (ctx_of ty) in
  35         (status, (t,ty) :: l))
  36       (status,[]) l
  37   in
  38   match
  39     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
  40   with
  41   | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
  42   | (pt, metasenv, subst)::_ ->
  43       let status = status#set_obj (n,h,metasenv,subst,o) in
  44       instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
  45 ;;
  46
  47 let auto_paramod_tac ~params status =
  48   NTactics.distribute_tac (auto_paramod ~params) status
  49 ;;
  50
  51 (* =================================== auto =========================== *)
  52 let auto_tac ~params status =
  53   prerr_endline "I teoremi noti sono";
  54   NDiscriminationTree.DiscriminationTree.iter status#auto_cache
  55     (fun _ t ->
  56       List.iter (fun t ->
  57        prerr_endline
  58         (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
  59        (NDiscriminationTree.TermSet.elements t));
  60   status
  61 ;;
  62
  63 (* ========================= dispatching of auto/auto_paramod ============ *)
  64 let auto_tac ~params:(_,flags as params) =
  65   if List.mem_assoc "paramodulation" flags then
  66     auto_paramod_tac ~params
  67   else
  68     auto_tac ~params
  69 ;;
  70
  71 (* EOF *)