helm/software/components/tactics/auto.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 open AutoTypes;;
  27 open AutoCache;;
  28
  29 let debug = false;;
  30 let debug_print s =
  31   if debug then prerr_endline (Lazy.force s);;
  32
  33 let is_propositional context sort =
  34   match CicReduction.whd context sort with
  35   | Cic.Sort Cic.Prop
  36   | Cic.Sort (Cic.CProp _) -> true
  37   | _-> false
  38 ;;
  39
  40
  41 type auto_params = Cic.term list * (string * string) list
  42
  43 let elems = ref [] ;;
  44
  45 (* closing a term w.r.t. its metavariables
  46    very naif version: it does not take dependencies properly into account *)
  47
  48 let naif_closure ?(prefix_name="xxx_") t metasenv context =
  49   let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
  50   let n = List.length metasenv in
  51   let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
  52   let _,with_what =
  53     List.fold_left
  54       (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
  55       (n,[]) metasenv
  56   in
  57   let t = CicSubstitution.lift n t in
  58   let body =
  59     ProofEngineReduction.replace_lifting
  60       ~equality:(fun c t1 t2 ->
  61          match t1,t2 with
  62          | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
  63          | _ -> false)
  64       ~context ~what ~with_what ~where:t
  65   in
  66   let _, t =
  67     List.fold_left
  68       (fun (n,t) (_,cc,ty) ->
  69         n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
  70                CicSubstitution.lift n ty,t))
  71       (n-1,body) metasenv
  72   in
  73   t
  74 ;;
  75
  76 let lambda_close ?prefix_name t menv ctx =
  77   let t = naif_closure ?prefix_name t menv ctx in
  78     List.fold_left
  79       (fun (t,i) -> function
  80         | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
  81         | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
  82         | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
  83       (t,List.length menv) ctx
  84 ;;
  85
  86 (* functions for retrieving theorems *)
  87
  88 exception FillingFailure of AutoCache.cache * int
  89
  90 let rec unfold context = function
  91   | Cic.Prod(name,s,t) ->
  92       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
  93         Cic.Prod(name,s,t')
  94   | t -> ProofEngineReduction.unfold context t
  95
  96 let find_library_theorems dbd proof goal =
  97   let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
  98   let terms = List.map CicUtil.term_of_uri univ in
  99   List.map
 100     (fun t ->
 101        (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph)))
 102     terms
 103
 104 let find_context_theorems context metasenv =
 105   let l,_ =
 106     List.fold_left
 107       (fun (res,i) ctxentry ->
 108          match ctxentry with
 109            | Some (_,Cic.Decl t) ->
 110                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
 111            | Some (_,Cic.Def (_,t)) ->
 112                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
 113            | None -> res,i+1)
 114       ([],1) context
 115   in l
 116
 117 let rec is_an_equality = function
 118   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
 119     when (LibraryObjects.is_eq_URI uri) -> true
 120   | Cic.Prod (_, _, t) -> is_an_equality t
 121   | _ -> false
 122 ;;
 123
 124 let partition_equalities =
 125   List.partition (fun (_,ty) -> is_an_equality ty)
 126
 127
 128 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
 129
 130 (* giusto per provare che succede
 131 let is_unit_equation context metasenv oldnewmeta term =
 132   let head, metasenv, args, newmeta =
 133     TermUtil.saturate_term oldnewmeta metasenv context term 0
 134   in
 135   let newmetas =
 136     List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
 137   in
 138     Some (args,metasenv,newmetas,head,newmeta) *)
 139
 140 let is_unit_equation context metasenv oldnewmeta term =
 141   let head, metasenv, args, newmeta =
 142     TermUtil.saturate_term oldnewmeta metasenv context term 0
 143   in
 144   let propositional_args =
 145     HExtlib.filter_map
 146       (function
 147       | Cic.Meta(i,_) ->
 148           let _,_,mt = CicUtil.lookup_meta i metasenv in
 149           let sort,u =
 150             CicTypeChecker.type_of_aux' metasenv context mt
 151               CicUniv.oblivion_ugraph
 152           in
 153           if is_propositional context sort then Some i else None
 154       | _ -> assert false)
 155     args
 156   in
 157     if propositional_args = [] then
 158       let newmetas =
 159         List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
 160       in
 161         Some (args,metasenv,newmetas,head,newmeta)
 162     else None
 163 ;;
 164
 165 let get_candidates universe cache t =
 166   let candidates=
 167     (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
 168   in
 169   let debug_msg =
 170     (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
 171              (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
 172   debug_print debug_msg;
 173   candidates
 174 ;;
 175
 176 let only signature context metasenv t =
 177   try
 178     let ty,_ =
 179       CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
 180     in
 181     let consts = MetadataConstraints.constants_of ty in
 182     let b = MetadataConstraints.UriManagerSet.subset consts signature in
 183     if b then b
 184     else
 185       let ty' = unfold context ty in
 186       let consts' = MetadataConstraints.constants_of ty' in
 187       MetadataConstraints.UriManagerSet.subset consts' signature
 188   with
 189   | CicTypeChecker.TypeCheckerFailure _ -> assert false
 190   | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
 191 ;;
 192
 193 let not_default_eq_term t =
 194   try
 195     let uri = CicUtil.uri_of_term t in
 196       not (LibraryObjects.in_eq_URIs uri)
 197   with Invalid_argument _ -> true
 198
 199 let retrieve_equations dont_filter signature universe cache context metasenv =
 200   match LibraryObjects.eq_URI() with
 201     | None -> []
 202     | Some eq_uri ->
 203         let eq_uri = UriManager.strip_xpointer eq_uri in
 204         let fake= Cic.Meta(-1,[]) in
 205         let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
 206         let candidates = get_candidates universe cache fake_eq in
 207         if dont_filter then candidates
 208         else
 209           let candidates = List.filter not_default_eq_term candidates in
 210           List.filter (only signature context metasenv) candidates
 211
 212 let build_equality bag head args proof newmetas maxmeta =
 213   match head with
 214   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
 215       let p =
 216         if args = [] then proof else Cic.Appl (proof::args)
 217       in
 218       let o = !Utils.compare_terms t1 t2 in
 219       let stat = (ty,t1,t2,o) in
 220       (* let w = compute_equality_weight stat in *)
 221       let w = 0 in
 222       let proof = Equality.Exact p in
 223       let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
 224       (* to clean the local context of metas *)
 225       Equality.fix_metas bag maxmeta e
 226   | _ -> assert false
 227 ;;
 228
 229 let partition_unit_equalities context metasenv newmeta bag equations =
 230   List.fold_left
 231     (fun (units,other,maxmeta)(t,ty) ->
 232        if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
 233          let _ =
 234            HLog.warn
 235            ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
 236              ^ " since it is not meta closed")
 237          in
 238          units,(t,ty)::other,maxmeta
 239        else
 240        match is_unit_equation context metasenv maxmeta ty with
 241          | Some (args,metasenv,newmetas,head,newmeta') ->
 242              let maxmeta,equality =
 243                build_equality bag head args t newmetas newmeta' in
 244              equality::units,other,maxmeta
 245          | None ->
 246              units,(t,ty)::other,maxmeta)
 247     ([],[],newmeta) equations
 248
 249 let empty_tables =
 250   (Saturation.make_active [],
 251    Saturation.make_passive [],
 252    Equality.mk_equality_bag)
 253
 254
 255 let init_cache_and_tables
 256   ?dbd use_library paramod use_context dont_filter universe (proof, goal)
 257 =
 258   (* the local cache in initially empty  *)
 259   let cache = AutoCache.cache_empty in
 260   let _, metasenv, _subst,_, _, _ = proof in
 261   let signature = MetadataQuery.signature_of metasenv goal in
 262   let newmeta = CicMkImplicit.new_meta metasenv [] in
 263   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 264   let ct = if use_context then find_context_theorems context metasenv else [] in
 265   debug_print
 266     (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
 267   let lt =
 268     match use_library, dbd with
 269     | true, Some dbd -> find_library_theorems dbd metasenv goal
 270     | _ -> []
 271   in
 272   debug_print
 273     (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
 274   let cache = cache_add_list cache context (ct@lt) in
 275   let equations =
 276     retrieve_equations dont_filter signature universe cache context metasenv
 277   in
 278   debug_print
 279     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
 280   let eqs_and_types =
 281     HExtlib.filter_map
 282       (fun t ->
 283          let ty,_ =
 284            CicTypeChecker.type_of_aux'
 285              metasenv context t CicUniv.oblivion_ugraph
 286          in
 287          (* retrieve_equations could also return flexible terms *)
 288          if is_an_equality ty then Some(t,ty)
 289          else
 290            try
 291              let ty' = unfold context ty in
 292              if is_an_equality ty' then Some(t,ty') else None
 293            with ProofEngineTypes.Fail _ -> None)
 294       equations
 295   in
 296   let bag = Equality.mk_equality_bag () in
 297   let units, other_equalities, newmeta =
 298     partition_unit_equalities context metasenv newmeta bag eqs_and_types
 299   in
 300   (* SIMPLIFICATION STEP
 301   let equalities =
 302     let env = (metasenv, context, CicUniv.oblivion_ugraph) in
 303     let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
 304     Saturation.simplify_equalities bag eq_uri env units
 305   in
 306   *)
 307   let passive = Saturation.make_passive units in
 308   let no = List.length units in
 309   let active = Saturation.make_active [] in
 310   let active,passive,newmeta =
 311     if paramod then active,passive,newmeta
 312     else
 313       Saturation.pump_actives
 314         context bag newmeta active passive (no+1) infinity
 315   in
 316     (active,passive,bag),cache,newmeta
 317
 318 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
 319   let head, metasenv, args, newmeta =
 320     TermUtil.saturate_term oldnewmeta metasenv context term 0
 321   in
 322   let propositional_args =
 323     HExtlib.filter_map
 324       (function
 325       | Cic.Meta(i,_) ->
 326           let _,_,mt = CicUtil.lookup_meta i metasenv in
 327           let sort,u =
 328             CicTypeChecker.type_of_aux' metasenv context mt
 329               CicUniv.oblivion_ugraph
 330           in
 331           if is_propositional context sort then Some i else None
 332       | _ -> assert false)
 333     args
 334   in
 335   let results,cache,newmeta =
 336     if propositional_args = [] then
 337       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
 338       [args,metasenv,newmetas,head,newmeta],cache,newmeta
 339     else
 340       (*
 341       let proof =
 342         None,metasenv,term,term (* term non e' significativo *)
 343       in *)
 344       let flags =
 345         if fast then
 346           {AutoTypes.default_flags() with
 347            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 348            maxwidth = 2;maxdepth = 2;
 349            use_paramod=true;use_only_paramod=false}
 350         else
 351           {AutoTypes.default_flags() with
 352            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 353            maxwidth = 2;maxdepth = 4;
 354            use_paramod=true;use_only_paramod=false}
 355       in
 356       match auto newmeta tables universe cache context metasenv propositional_args flags with
 357       | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
 358       | substs,cache,newmeta ->
 359           List.map
 360             (fun subst ->
 361               let metasenv =
 362                 CicMetaSubst.apply_subst_metasenv subst metasenv
 363               in
 364               let head = CicMetaSubst.apply_subst subst head in
 365               let newmetas =
 366                 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
 367               in
 368               let args = List.map (CicMetaSubst.apply_subst subst) args in
 369               let newm = CicMkImplicit.new_meta metasenv subst in
 370                 args,metasenv,newmetas,head,max newm newmeta)
 371             substs, cache, newmeta
 372   in
 373   results,cache,newmeta
 374
 375 let build_equalities auto context metasenv tables universe cache newmeta equations =
 376   List.fold_left
 377     (fun (facts,cache,newmeta) (t,ty) ->
 378        (* in any case we add the equation to the cache *)
 379        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
 380        try
 381          let saturated,cache,newmeta =
 382            fill_hypothesis context metasenv newmeta ty tables universe cache auto true
 383          in
 384          let (active,passive,bag) = tables in
 385          let eqs,bag,newmeta =
 386            List.fold_left
 387              (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 388                 let maxmeta,equality =
 389                   build_equality bag head args t newmetas newmeta'
 390                 in
 391                   equality::acc,bag,maxmeta)
 392              ([],bag,newmeta) saturated
 393          in
 394            (eqs@facts, cache, newmeta)
 395        with FillingFailure (cache,newmeta) ->
 396          (* if filling hypothesis fails we add the equation to
 397             the cache *)
 398          (facts,cache,newmeta)
 399       )
 400     ([],cache,newmeta) equations
 401
 402 let close_more tables maxmeta context status auto universe cache =
 403   let (active,passive,bag) = tables in
 404   let proof, goalno = status in
 405   let _, metasenv,_subst,_,_, _ = proof in
 406   let signature = MetadataQuery.signature_of metasenv goalno in
 407   let equations =
 408     retrieve_equations false signature universe cache context metasenv
 409   in
 410   let eqs_and_types =
 411     HExtlib.filter_map
 412       (fun t ->
 413          let ty,_ =
 414            CicTypeChecker.type_of_aux' metasenv context t
 415            CicUniv.oblivion_ugraph in
 416            (* retrieve_equations could also return flexible terms *)
 417            if is_an_equality ty then Some(t,ty) else None)
 418       equations in
 419   let units, cache, maxm =
 420       build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
 421   debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
 422     string_of_int maxm));
 423   List.iter
 424     (fun e -> debug_print (lazy (Equality.string_of_equality e)))
 425     units;
 426   debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
 427   let passive = Saturation.add_to_passive units passive in
 428   let no = List.length units in
 429   debug_print (lazy ("No = " ^ (string_of_int no)));
 430   let active,passive,newmeta =
 431     Saturation.pump_actives context bag maxm active passive (no+1) infinity
 432   in
 433     (active,passive,bag),cache,newmeta
 434
 435 let find_context_equalities
 436   maxmeta bag context proof (universe:Universe.universe) cache
 437 =
 438   let module C = Cic in
 439   let module S = CicSubstitution in
 440   let module T = CicTypeChecker in
 441   let _,metasenv,_subst,_,_, _ = proof in
 442   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
 443   (* if use_auto is true, we try to close the hypothesis of equational
 444     statements using auto; a naif, and probably wrong approach *)
 445   let rec aux cache index newmeta = function
 446     | [] -> [], newmeta,cache
 447     | (Some (_, C.Decl (term)))::tl ->
 448         debug_print
 449           (lazy
 450              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
 451         let do_find context term =
 452           match term with
 453           | C.Prod (name, s, t) when is_an_equality t ->
 454               (try
 455
 456                 let term = S.lift index term in
 457                 let saturated,cache,newmeta =
 458                   fill_hypothesis context metasenv newmeta term
 459                     empty_tables universe cache default_auto false
 460                 in
 461                 let eqs,newmeta =
 462                   List.fold_left
 463                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 464                      let newmeta, equality =
 465                        build_equality
 466                          bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
 467                      in
 468                      equality::acc, newmeta + 1)
 469                    ([],newmeta) saturated
 470                 in
 471                  eqs, newmeta, cache
 472               with FillingFailure (cache,newmeta) ->
 473                 [],newmeta,cache)
 474           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 475               when LibraryObjects.is_eq_URI uri ->
 476               let term = S.lift index term in
 477               let newmeta, e =
 478                 build_equality bag term [] (Cic.Rel index) [] newmeta
 479               in
 480               [e], (newmeta+1),cache
 481           | _ -> [], newmeta, cache
 482         in
 483         let eqs, newmeta, cache = do_find context term in
 484         let rest, newmeta,cache = aux cache (index+1) newmeta tl in
 485         List.map (fun x -> index,x) eqs @ rest, newmeta, cache
 486     | _::tl ->
 487         aux cache (index+1) newmeta tl
 488   in
 489   let il, maxm, cache =
 490     aux cache 1 newmeta context
 491   in
 492   let indexes, equalities = List.split il in
 493   indexes, equalities, maxm, cache
 494 ;;
 495
 496 (********** PARAMETERS PASSING ***************)
 497
 498 let bool params name default =
 499     try
 500       let s = List.assoc name params in
 501       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
 502       else if s = "0" || s = "false" || s = "no" || s= "off" then false
 503       else
 504         let msg = "Unrecognized value for parameter "^name^"\n" in
 505         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
 506         raise (ProofEngineTypes.Fail (lazy msg))
 507     with Not_found -> default
 508 ;;
 509
 510 let string params name default =
 511     try List.assoc name params with
 512     | Not_found -> default
 513 ;;
 514
 515 let int params name default =
 516     try int_of_string (List.assoc name params) with
 517     | Not_found -> default
 518     | Failure _ ->
 519         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 520 ;;
 521
 522 let flags_of_params params ?(for_applyS=false) () =
 523  let int = int params in
 524  let bool = bool params in
 525  let close_more = bool "close_more" false in
 526  let use_paramod = bool "use_paramod" true in
 527  let use_only_paramod =
 528   if for_applyS then true else bool "paramodulation" false in
 529  let use_library = bool "library"
 530    ((AutoTypes.default_flags()).AutoTypes.use_library) in
 531  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
 532  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
 533  let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
 534  let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
 535  let do_type = bool "type" false in
 536  let timeout = int "timeout" 0 in
 537   { AutoTypes.maxdepth =
 538       if use_only_paramod then 2 else depth;
 539     AutoTypes.maxwidth = width;
 540     AutoTypes.maxsize = size;
 541     AutoTypes.timeout =
 542       if timeout = 0 then
 543        if for_applyS then Unix.gettimeofday () +. 30.0
 544        else
 545          infinity
 546       else
 547        Unix.gettimeofday() +. (float_of_int timeout);
 548     AutoTypes.use_library = use_library;
 549     AutoTypes.use_paramod = use_paramod;
 550     AutoTypes.use_only_paramod = use_only_paramod;
 551     AutoTypes.close_more = close_more;
 552     AutoTypes.dont_cache_failures = false;
 553     AutoTypes.maxgoalsizefactor = gsize;
 554     AutoTypes.do_types = do_type;
 555   }
 556
 557 let universe_of_params metasenv context universe tl =
 558   if tl = [] then universe else
 559    let tys =
 560      List.map
 561        (fun term ->
 562          fst (CicTypeChecker.type_of_aux' metasenv context term
 563                 CicUniv.oblivion_ugraph))
 564        tl
 565    in
 566      Universe.index_list Universe.empty context (List.combine tl tys)
 567 ;;
 568
 569
 570 (***************** applyS *******************)
 571
 572 let new_metasenv_and_unify_and_t
 573  dbd flags universe proof goal ?tables newmeta' metasenv'
 574  context term' ty termty goal_arity
 575 =
 576  let (consthead,newmetasenv,arguments,_) =
 577    TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
 578  let term'' =
 579    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
 580  in
 581  let proof',oldmetasenv =
 582   let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
 583    (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
 584  in
 585  let goal_for_paramod =
 586   match LibraryObjects.eq_URI () with
 587   | Some uri ->
 588       Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
 589   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
 590  in
 591  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
 592  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
 593  let proof'' =
 594    let uri,_,_subst,p,ty, attrs = proof' in
 595    uri,metasenv_for_paramod,_subst,p,ty, attrs
 596  in
 597  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 598  let proof''',goals =
 599   ProofEngineTypes.apply_tactic
 600     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 601       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 602         (Cic.Meta(newmeta,irl)) [])
 603    (proof'',goal)
 604  in
 605  let goal = match goals with [g] -> g | _ -> assert false in
 606  let  proof'''', _  =
 607    ProofEngineTypes.apply_tactic
 608      (PrimitiveTactics.apply_tac term'')
 609      (proof''',goal)
 610  in
 611  match
 612    let (active, passive,bag), cache, maxmeta =
 613      init_cache_and_tables ~dbd flags.use_library true true false universe
 614      (proof'''',newmeta)
 615    in
 616      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
 617        max_int max_int flags.timeout
 618  with
 619  | None, _,_,_ ->
 620      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 621  | Some (_,proof''''',_), active,passive,_  ->
 622      proof''''',
 623      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 624        ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
 625 ;;
 626
 627 let rec count_prods context ty =
 628  match CicReduction.whd context ty with
 629     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 630   | _ -> 0
 631
 632 let apply_smart
 633   ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal)
 634 =
 635  let module T = CicTypeChecker in
 636  let module R = CicReduction in
 637  let module C = Cic in
 638   let (_,metasenv,_subst,_,_, _) = proof in
 639   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 640   let flags = flags_of_params params ~for_applyS:true () in
 641   let universe = universe_of_params metasenv context universe univ in
 642   let newmeta = CicMkImplicit.new_meta metasenv subst in
 643    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 644     match term with
 645        C.Var (uri,exp_named_subst) ->
 646         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 647          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 648           exp_named_subst
 649         in
 650          exp_named_subst_diff,newmeta',newmetasenvfragment,
 651           C.Var (uri,exp_named_subst')
 652      | C.Const (uri,exp_named_subst) ->
 653         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 654          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 655           exp_named_subst
 656         in
 657          exp_named_subst_diff,newmeta',newmetasenvfragment,
 658           C.Const (uri,exp_named_subst')
 659      | C.MutInd (uri,tyno,exp_named_subst) ->
 660         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 661          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 662           exp_named_subst
 663         in
 664          exp_named_subst_diff,newmeta',newmetasenvfragment,
 665           C.MutInd (uri,tyno,exp_named_subst')
 666      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 667         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 668          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 669           exp_named_subst
 670         in
 671          exp_named_subst_diff,newmeta',newmetasenvfragment,
 672           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 673      | _ -> [],newmeta,[],term
 674    in
 675    let metasenv' = metasenv@newmetasenvfragment in
 676    let termty,_ =
 677      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
 678    in
 679    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 680    let goal_arity = count_prods context ty in
 681    let proof, gl, active, passive =
 682     new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
 683      newmeta' metasenv' context term' ty termty goal_arity
 684    in
 685     proof, gl, active, passive
 686 ;;
 687
 688 (****************** AUTO ********************)
 689
 690 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 691 let ugraph = CicUniv.oblivion_ugraph;;
 692 let typeof = CicTypeChecker.type_of_aux';;
 693 let ppterm ctx t =
 694   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 695   CicPp.pp t names
 696 ;;
 697 let is_in_prop context subst metasenv ty =
 698   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
 699   is_propositional context sort
 700 ;;
 701
 702 exception NotConvertible;;
 703
 704 let check_proof_is_valid proof metasenv context goalty =
 705   if debug then
 706     begin
 707       try
 708         let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
 709         let b,_ = CicReduction.are_convertible context ty goalty u in
 710         if not b then raise NotConvertible else b
 711       with _ ->
 712         let names =
 713           List.map (function None -> None | Some (x,_) -> Some x) context
 714         in
 715           debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
 716           (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *)
 717           debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
 718           debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
 719         false
 720     end
 721   else true
 722 ;;
 723
 724 let assert_proof_is_valid proof metasenv context goalty =
 725   assert (check_proof_is_valid proof metasenv context goalty)
 726 ;;
 727
 728 let assert_subst_are_disjoint subst subst' =
 729   if debug then
 730     assert(List.for_all
 731              (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 732              subst)
 733   else ()
 734 ;;
 735
 736 let split_goals_in_prop metasenv subst gl =
 737   List.partition
 738     (fun g ->
 739       let _,context,ty = CicUtil.lookup_meta g metasenv in
 740       try
 741         let sort,u = typeof ~subst metasenv context ty ugraph in
 742         is_propositional context sort
 743       with
 744       | CicTypeChecker.AssertFailure s
 745       | CicTypeChecker.TypeCheckerFailure s ->
 746           debug_print
 747             (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
 748           debug_print s;
 749           false)
 750     (* FIXME... they should type! *)
 751     gl
 752 ;;
 753
 754 let split_goals_with_metas metasenv subst gl =
 755   List.partition
 756     (fun g ->
 757       let _,context,ty = CicUtil.lookup_meta g metasenv in
 758       let ty = CicMetaSubst.apply_subst subst ty in
 759       CicUtil.is_meta_closed ty)
 760     gl
 761 ;;
 762
 763 let order_new_goals metasenv subst open_goals ppterm =
 764   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 765   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
 766   let closed_type, open_type = split_goals_with_metas metasenv subst rest in
 767   let open_goals =
 768     (List.map (fun x -> x,P) (open_prop @ closed_prop))
 769     @
 770     (List.map (fun x -> x,T) (open_type @ closed_type))
 771   in
 772   let tys =
 773     List.map
 774       (fun (i,sort) ->
 775         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
 776   in
 777   debug_print (lazy ("   OPEN: "^
 778     String.concat "\n"
 779       (List.map
 780          (function
 781             | (i,t,P) -> string_of_int i   ^ ":"^ppterm t^ "Prop"
 782             | (i,t,T) -> string_of_int i  ^ ":"^ppterm t^ "Type")
 783          tys)));
 784   open_goals
 785 ;;
 786
 787 let is_an_equational_goal = function
 788   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 789   | _ -> false
 790 ;;
 791
 792 (*
 793 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
 794 *)
 795
 796 let calculate_timeout flags =
 797     if flags.timeout = 0. then
 798       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 799        {flags with timeout = infinity})
 800     else
 801       flags
 802 ;;
 803 let is_equational_case goalty flags =
 804   let ensure_equational t =
 805     if is_an_equational_goal t then true
 806     else false
 807     (*
 808       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 809       raise (ProofEngineTypes.Fail (lazy msg))
 810     *)
 811   in
 812   (flags.use_paramod && is_an_equational_goal goalty) ||
 813   (flags.use_only_paramod && ensure_equational goalty)
 814 ;;
 815 (*
 816 let cache_add_success sort cache k v =
 817   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 818   cache k
 819 ;;
 820 *)
 821
 822 type menv = Cic.metasenv
 823 type subst = Cic.substitution
 824 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 825 let candidate_no = ref 0;;
 826 type candidate = int * Cic.term Lazy.t
 827 type cache = AutoCache.cache
 828 type tables =
 829   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
 830
 831 type fail =
 832   (* the goal (mainly for depth) and key of the goal *)
 833   goal * AutoCache.cache_key
 834 type op =
 835   (* goal has to be proved *)
 836   | D of goal
 837   (* goal has to be cached as a success obtained using candidate as the first
 838    * step *)
 839   | S of goal * AutoCache.cache_key * candidate * int
 840 type elem =
 841   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
 842   menv * subst * int * op list * op list * fail list
 843 type status =
 844   (* list of computations that may lead to the solution: all op list will
 845    * end with the same (S(g,_)) *)
 846   elem list
 847 type auto_result =
 848   (* menv, subst, alternatives, tables, cache, maxmeta *)
 849   | Proved of menv * subst * elem list * tables * cache * int
 850   | Gaveup of tables * cache * int
 851
 852
 853 (* the status exported to the external observer *)
 854 type auto_status =
 855   (* context, (goal,candidate) list, and_list, history *)
 856   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 857   (int * Cic.term * int) list * Cic.term Lazy.t list
 858
 859 let d_prefix l =
 860   let rec aux acc = function
 861     | (D g)::tl -> aux (acc@[g]) tl
 862     | _ -> acc
 863   in
 864     aux [] l
 865 ;;
 866 let prop_only l =
 867   List.filter (function (_,_,P) -> true | _ -> false) l
 868 ;;
 869
 870 let d_goals l =
 871   let rec aux acc = function
 872     | (D g)::tl -> aux (acc@[g]) tl
 873     | (S _)::tl -> aux acc tl
 874     | [] -> acc
 875   in
 876     aux [] l
 877 ;;
 878
 879 let calculate_goal_ty (goalno,_,_) s m =
 880   try
 881     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 882     (* XXX applicare la subst al contesto? *)
 883     Some (cc, CicMetaSubst.apply_subst s goalty)
 884   with CicUtil.Meta_not_found i when i = goalno -> None
 885 ;;
 886
 887 let calculate_closed_goal_ty (goalno,_,_) s =
 888   try
 889     let cc,_,goalty = List.assoc goalno s in
 890     (* XXX applicare la subst al contesto? *)
 891     Some (cc, CicMetaSubst.apply_subst s goalty)
 892   with Not_found -> None
 893 ;;
 894
 895 let pp_status ctx status =
 896   if debug then
 897   let names = Utils.names_of_context ctx in
 898   let pp x =
 899     let x =
 900       ProofEngineReduction.replace
 901         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 902           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 903     in
 904     CicPp.pp x names
 905   in
 906   let string_of_do m s (gi,_,_ as g) d =
 907     match calculate_goal_ty g s m with
 908     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 909     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 910   in
 911   let string_of_s m su k (ci,ct) gi =
 912     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 913   in
 914   let string_of_ol m su l =
 915     String.concat " | "
 916       (List.map
 917         (function
 918           | D (g,d,s) -> string_of_do m su (g,d,s) d
 919           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 920         l)
 921   in
 922   let string_of_fl m s fl =
 923     String.concat " | "
 924       (List.map (fun ((i,_,_),ty) ->
 925          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 926   in
 927   let rec aux = function
 928     | [] -> ()
 929     | (m,s,_,_,ol,fl)::tl ->
 930         Printf.eprintf "< [%s] ;;; [%s]>\n"
 931           (string_of_ol m s ol) (string_of_fl m s fl);
 932         aux tl
 933   in
 934     Printf.eprintf "-------------------------- status -------------------\n";
 935     aux status;
 936     Printf.eprintf "-----------------------------------------------------\n";
 937 ;;
 938
 939 let auto_status = ref [] ;;
 940 let auto_context = ref [];;
 941 let in_pause = ref false;;
 942 let pause b = in_pause := b;;
 943 let cond = Condition.create ();;
 944 let mutex = Mutex.create ();;
 945 let hint = ref None;;
 946 let prune_hint = ref [];;
 947
 948 let step _ = Condition.signal cond;;
 949 let give_hint n = hint := Some n;;
 950 let give_prune_hint hint =
 951   prune_hint := hint :: !prune_hint
 952 ;;
 953
 954 let check_pause _ =
 955   if !in_pause then
 956     begin
 957       Mutex.lock mutex;
 958       Condition.wait cond mutex;
 959       Mutex.unlock mutex
 960     end
 961 ;;
 962
 963 let get_auto_status _ =
 964   let status = !auto_status in
 965   let and_list,elems,last =
 966     match status with
 967     | [] -> [],[],[]
 968     | (m,s,_,don,gl,fail)::tl ->
 969         let and_list =
 970           HExtlib.filter_map
 971             (fun (id,d,_ as g) ->
 972               match calculate_goal_ty g s m with
 973               | Some (_,x) -> Some (id,x,d) | None -> None)
 974             (d_goals gl)
 975         in
 976         let rows =
 977           (* these are the S goalsin the or list *)
 978           let orlist =
 979             List.map
 980               (fun (m,s,_,don,gl,fail) ->
 981                 HExtlib.filter_map
 982                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 983                   (List.rev don @ gl))
 984               status
 985           in
 986           (* this function eats id from a list l::[id,x] returning x, l *)
 987           let eat_tail_if_eq id l =
 988             let rec aux (s, l) = function
 989               | [] -> s, l
 990               | ((id1,_,_),k1,c)::tl when id = id1 ->
 991                   (match s with
 992                   | None -> aux (Some c,l) tl
 993                   | Some _ -> assert false)
 994               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 995             in
 996             let c, l = aux (None, []) l in
 997             c, List.rev l
 998           in
 999           let eat_in_parallel id l =
1000             let rec aux (b,eaten, new_l as acc) l =
1001               match l with
1002               | [] -> acc
1003               | l::tl ->
1004                   match eat_tail_if_eq id l with
1005                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
1006                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
1007             in
1008             aux ([],[],[]) l
1009           in
1010           let rec eat_all rows l =
1011             match l with
1012             | [] -> rows
1013             | elem::or_list ->
1014                 match List.rev elem with
1015                 | ((to_eat,depth,_),k,_)::next_lunch ->
1016                     let b, eaten, l = eat_in_parallel to_eat l in
1017                     let eaten = HExtlib.list_uniq eaten in
1018                     let eaten = List.rev eaten in
1019                     let b = true (* List.hd (List.rev b) *) in
1020                     let rows = rows @ [to_eat,k,b,depth,eaten] in
1021                     eat_all rows l
1022                 | [] -> eat_all rows or_list
1023           in
1024           eat_all [] (List.rev orlist)
1025         in
1026         let history =
1027           HExtlib.filter_map
1028             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
1029             gl
1030         in
1031 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
1032         and_list, rows, history
1033   in
1034   !auto_context, elems, and_list, last
1035 ;;
1036
1037 (* Works if there is no dependency over proofs *)
1038 let is_a_green_cut goalty =
1039   CicUtil.is_meta_closed goalty
1040 ;;
1041 let rec first_s = function
1042   | (D _)::tl -> first_s tl
1043   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
1044   | [] -> None
1045 ;;
1046 let list_union l1 l2 =
1047   (* TODO ottimizzare compare *)
1048   HExtlib.list_uniq (List.sort compare (l1 @ l1))
1049 ;;
1050 let rec eq_todo l1 l2 =
1051   match l1,l2 with
1052   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
1053   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
1054     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
1055       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
1056   | [],[] -> true
1057   | _ -> false
1058 ;;
1059 let eat_head todo id fl orlist =
1060   let rec aux acc = function
1061   | [] -> [], acc
1062   | (m, s, _, _, todo1, fl1)::tl as orlist ->
1063       let rec aux1 todo1 =
1064         match first_s todo1 with
1065         | None -> orlist, acc
1066         | Some (((gno,_,_),_,_,_), todo11) ->
1067             (* TODO confronto tra todo da ottimizzare *)
1068             if gno = id && eq_todo todo11 todo then
1069               aux (list_union fl1 acc) tl
1070             else
1071               aux1 todo11
1072       in
1073        aux1 todo1
1074   in
1075     aux fl orlist
1076 ;;
1077 let close_proof p ty menv context =
1078   let metas =
1079     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
1080   in
1081   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
1082   naif_closure p menv context
1083 ;;
1084 (* XXX capire bene quando aggiungere alla cache *)
1085 let add_to_cache_and_del_from_orlist_if_green_cut
1086   g s m cache key todo orlist fl ctx size minsize
1087 =
1088   let cache = cache_remove_underinspection cache key in
1089   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
1090    * canonico! XXX *)
1091   match calculate_closed_goal_ty g s with
1092   | None -> assert false
1093   | Some (canonical_ctx , gty) ->
1094       let goalno,depth,sort = g in
1095       let irl = mk_irl canonical_ctx in
1096       let goal = Cic.Meta(goalno, irl) in
1097       let proof = CicMetaSubst.apply_subst s goal in
1098       let green_proof, closed_proof =
1099         let b = is_a_green_cut proof in
1100         if not b then
1101           b, (* close_proof proof gty m ctx *) proof
1102         else
1103           b, proof
1104       in
1105       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
1106       if is_a_green_cut key then
1107         (* if the initia goal was closed, we cut alternatives *)
1108         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
1109         let orlist, fl = eat_head todo goalno fl orlist in
1110         let cache =
1111           if size < minsize then
1112             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
1113           else
1114           (* if the proof is closed we cache it *)
1115           if green_proof then cache_add_success cache key proof
1116           else (* cache_add_success cache key closed_proof *)
1117             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
1118         in
1119         cache, orlist, fl, true
1120       else
1121         let cache =
1122           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
1123           if size < minsize then
1124             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1125           (* if the substituted goal and the proof are closed we cache it *)
1126           if is_a_green_cut gty then
1127             if green_proof then cache_add_success cache gty proof
1128             else (* cache_add_success cache gty closed_proof *)
1129               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1130           else (*
1131             try
1132               let ty, _ =
1133                 CicTypeChecker.type_of_aux' ~subst:s
1134                   m ctx closed_proof CicUniv.oblivion_ugraph
1135               in
1136               if is_a_green_cut ty then
1137                 cache_add_success cache ty closed_proof
1138               else cache
1139             with
1140             | CicTypeChecker.TypeCheckerFailure _ ->*)
1141           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1142         in
1143         cache, orlist, fl, false
1144 ;;
1145 let close_failures (fl : fail list) (cache : cache) =
1146   List.fold_left
1147     (fun cache ((gno,depth,_),gty) ->
1148       debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1149       cache_add_failure cache gty depth)
1150     cache fl
1151 ;;
1152 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
1153   let entry = goalno, (canonical_ctx, t,ty) in
1154   assert_subst_are_disjoint subst [entry];
1155   let subst = entry :: subst in
1156   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1157   subst, metasenv
1158 ;;
1159
1160 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1161   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
1162 ;;
1163 let equational_case
1164   tables maxm cache depth fake_proof goalno goalty subst context
1165     flags
1166 =
1167   let active,passive,bag = tables in
1168   let ppterm = ppterm context in
1169   let status = (fake_proof,goalno) in
1170     if flags.use_only_paramod then
1171       begin
1172         debug_print (lazy ("PARAMODULATION SU: " ^
1173                          string_of_int goalno ^ " " ^ ppterm goalty ));
1174         let goal_steps, saturation_steps, timeout =
1175           max_int,max_int,flags.timeout
1176         in
1177
1178         match
1179           Saturation.given_clause bag maxm status active passive
1180             goal_steps saturation_steps timeout
1181         with
1182           | None, active, passive, maxmeta ->
1183               [], (active,passive,bag), cache, maxmeta, flags
1184           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1185             passive,maxmeta ->
1186               assert_subst_are_disjoint subst subst';
1187               let subst = subst@subst' in
1188               let open_goals =
1189                 order_new_goals metasenv subst open_goals ppterm
1190               in
1191               let open_goals =
1192                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1193               in
1194               incr candidate_no;
1195                       [(!candidate_no,proof),metasenv,subst,open_goals],
1196                 (active,passive,bag),
1197                 cache, maxmeta, flags
1198       end
1199     else
1200       begin
1201         debug_print
1202           (lazy
1203            ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1204         let res, maxmeta =
1205           Saturation.all_subsumed bag maxm status active passive
1206         in
1207         assert (maxmeta >= maxm);
1208         let res' =
1209           List.map
1210             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
1211                assert_subst_are_disjoint subst subst';
1212                let subst = subst@subst' in
1213                let open_goals =
1214                  order_new_goals metasenv subst open_goals ppterm
1215                in
1216                let open_goals =
1217                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1218                in
1219                incr candidate_no;
1220                  (!candidate_no,proof),metasenv,subst,open_goals)
1221             res
1222           in
1223           res', (active,passive,bag), cache, maxmeta, flags
1224       end
1225 ;;
1226
1227 let try_candidate
1228   goalty tables maxm subst fake_proof goalno depth context cand
1229 =
1230   let ppterm = ppterm context in
1231   try
1232     let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1233         (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1234         (fake_proof,goalno)
1235     in
1236     debug_print (lazy ("   OK: " ^ ppterm cand));
1237     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1238     let open_goals = order_new_goals metasenv subst open_goals ppterm in
1239     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1240     incr candidate_no;
1241     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
1242   with
1243     | ProofEngineTypes.Fail s -> None,tables, maxm
1244     | CicUnification.Uncertain s ->  None,tables, maxm
1245 ;;
1246
1247 let sort_new_elems =
1248  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
1249   List.length (prop_only l1) - List.length (prop_only l2))
1250 ;;
1251
1252 let applicative_case
1253   tables maxm depth subst fake_proof goalno goalty metasenv context universe
1254   cache
1255 =
1256   let candidates = get_candidates universe cache goalty in
1257   let tables, elems, maxm =
1258     List.fold_left
1259       (fun (tables,elems,maxm) cand ->
1260         match
1261           try_candidate goalty
1262             tables maxm subst fake_proof goalno depth context cand
1263         with
1264         | None, tables,maxm  -> tables,elems, maxm
1265         | Some x, tables, maxm -> tables,x::elems, maxm)
1266       (tables,[],maxm) candidates
1267   in
1268   let elems = sort_new_elems elems in
1269   elems, tables, cache, maxm
1270 ;;
1271
1272 let equational_and_applicative_case
1273   universe flags m s g gty tables cache maxm context
1274 =
1275   let goalno, depth, sort = g in
1276   let fake_proof = mk_fake_proof m s g gty context in
1277   if is_equational_case gty flags then
1278     let elems,tables,cache,maxm1, flags =
1279       equational_case tables maxm cache
1280         depth fake_proof goalno gty s context flags
1281     in
1282     let maxm = maxm1 in
1283     let more_elems, tables, cache, maxm1 =
1284       if flags.use_only_paramod then
1285         [],tables, cache, maxm
1286       else
1287         applicative_case
1288           tables maxm depth s fake_proof goalno
1289             gty m context universe cache
1290     in
1291     let maxm = maxm1 in
1292       elems@more_elems, tables, cache, maxm, flags
1293   else
1294     let elems, tables, cache, maxm =
1295       applicative_case tables maxm depth s fake_proof goalno
1296         gty m context universe cache
1297     in
1298       elems, tables, cache, maxm, flags
1299 ;;
1300 let rec condition_for_hint i = function
1301   | [] -> false
1302   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1303   | _::tl -> condition_for_hint i tl
1304 ;;
1305 let remove_s_from_fl (id,_,_) (fl : fail list) =
1306   let rec aux = function
1307     | [] -> []
1308     | ((id1,_,_),_)::tl when id = id1 -> tl
1309     | hd::tl ->  hd :: aux tl
1310   in
1311     aux fl
1312 ;;
1313
1314 let prunable_for_size flags s m todo =
1315   let rec aux b = function
1316     | (S _)::tl -> aux b tl
1317     | (D (_,_,T))::tl -> aux b tl
1318     | (D g)::tl ->
1319         (match calculate_goal_ty g s m with
1320           | None -> aux b tl
1321           | Some (canonical_ctx, gty) ->
1322             let gsize, _ =
1323               Utils.weight_of_term
1324                 ~consider_metas:false ~count_metas_occurrences:true gty in
1325             let newb = b || gsize > flags.maxgoalsizefactor in
1326             aux newb tl)
1327     | [] -> b
1328   in
1329     aux false todo
1330
1331 (*
1332 let prunable ty todo =
1333   let rec aux b = function
1334     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1335     | (D (_,_,T))::tl -> aux b tl
1336     | D _::_ -> false
1337     | [] -> b
1338   in
1339     aux false todo
1340 ;;
1341 *)
1342
1343 let prunable menv subst ty todo =
1344   let rec aux = function
1345     | (S(_,k,_,_))::tl ->
1346          (match Equality.meta_convertibility_subst k ty menv with
1347           | None -> aux tl
1348           | Some variant ->
1349                no_progress variant tl (* || aux tl*))
1350     | (D (_,_,T))::tl -> aux tl
1351     | _ -> false
1352   and no_progress variant = function
1353     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1354     | D ((n,_,P) as g)::tl ->
1355         (match calculate_goal_ty g subst menv with
1356            | None -> no_progress variant tl
1357            | Some (_, gty) ->
1358                (match calculate_goal_ty g variant menv with
1359                   | None -> assert false
1360                   | Some (_, gty') ->
1361                       if gty = gty' then
1362                          no_progress variant tl
1363                       else false))
1364     | _::tl -> no_progress variant tl
1365   in
1366     aux todo
1367
1368 ;;
1369 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1370   let s =
1371     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1372   in
1373   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1374 ;;
1375 let filter_prune_hint l =
1376   let prune = !prune_hint in
1377   prune_hint := []; (* possible race... *)
1378   if prune = [] then l
1379   else List.filter (condition_for_prune_hint prune) l
1380 ;;
1381 let auto_main tables maxm context flags universe cache elems =
1382   auto_context := context;
1383   let rec aux tables maxm flags cache (elems : status) =
1384 (*     pp_status context elems; *)
1385 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1386     auto_status := elems;
1387     check_pause ();
1388 *)
1389     let elems = filter_prune_hint elems in
1390     match elems with
1391     | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1392         debug_print (lazy "skip");
1393         (match !hint with
1394         | Some i when condition_for_hint i todo ->
1395             aux tables maxm flags cache orlist
1396         | _ ->
1397           hint := None;
1398           aux tables maxm flags cache elems)
1399     | [] ->
1400         (* complete failure *)
1401         debug_print (lazy "give up");
1402         Gaveup (tables, cache, maxm)
1403     | (m, s, _, _, [],_)::orlist ->
1404         (* complete success *)
1405         debug_print (lazy "success");
1406         Proved (m, s, orlist, tables, cache, maxm)
1407     | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
1408       when not flags.AutoTypes.do_types ->
1409         (* skip since not Prop, don't even check if closed by side-effect *)
1410         debug_print (lazy "skip existential goal");
1411         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1412     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1413         (* partial success, cache g and go on *)
1414         let cache, orlist, fl, sibling_pruned =
1415           add_to_cache_and_del_from_orlist_if_green_cut
1416             g s m cache key todo orlist fl context size minsize
1417         in
1418         debug_print (lazy (AutoCache.cache_print context cache));
1419         let fl = remove_s_from_fl g fl in
1420         let don = if sibling_pruned then don else op::don in
1421         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1422     | (m, s, size, don, todo, fl)::orlist
1423       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1424         debug_print (lazy ("FAIL: WIDTH"));
1425         (* too many goals in and generated by last th *)
1426         let cache = close_failures fl cache in
1427         aux tables maxm flags cache orlist
1428     | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1429         debug_print
1430           (lazy ("FAIL: SIZE: "^string_of_int size ^
1431             " > " ^ string_of_int flags.maxsize ));
1432         (* we already have a too large proof term *)
1433         let cache = close_failures fl cache in
1434         aux tables maxm flags cache orlist
1435     | _ when Unix.gettimeofday () > flags.timeout ->
1436         (* timeout *)
1437         debug_print (lazy ("FAIL: TIMEOUT"));
1438         Gaveup (tables, cache, maxm)
1439     | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
1440         (* attack g *)
1441         debug_print (lazy "attack goal");
1442         match calculate_goal_ty g s m with
1443         | None ->
1444             (* closed by side effect *)
1445             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1446             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1447         | Some (canonical_ctx, gty) ->
1448             let gsize, _ =
1449               Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1450             in
1451             if gsize > flags.maxgoalsizefactor then
1452               (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1453                aux tables maxm flags cache orlist)
1454             else if prunable_for_size flags s m todo then
1455                 (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
1456                  aux tables maxm flags cache orlist)
1457             else
1458             (* still to be proved *)
1459             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1460             match cache_examine cache gty with
1461             | Failed_in d when d >= depth ->
1462                 (* fail depth *)
1463                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1464                 let cache = close_failures fl cache in
1465                 aux tables maxm flags cache orlist
1466             | UnderInspection ->
1467                 (* fail loop *)
1468                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1469                 let cache = close_failures fl cache in
1470                 aux tables maxm flags cache orlist
1471             | Succeded t ->
1472                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1473                 let s, m = put_in_subst s m g canonical_ctx t gty in
1474                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1475             | Notfound
1476             | Failed_in _ when depth > 0 ->
1477                 ( (* more depth or is the first time we see the goal *)
1478                     if prunable m s gty todo then
1479                       (debug_print (lazy(
1480                          "FAIL: LOOP: one father is equal"));
1481                        aux tables maxm flags cache orlist)
1482                     else
1483                     let cache = cache_add_underinspection cache gty depth in
1484                     auto_status := status;
1485                     check_pause ();
1486                     debug_print
1487                       (lazy ("INSPECTING: " ^
1488                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1489                         CicPp.ppterm gty));
1490                     (* elems are possible computations for proving gty *)
1491                     let elems, tables, cache, maxm, flags =
1492                       equational_and_applicative_case
1493                         universe flags m s g gty tables cache maxm context
1494                     in
1495                     if elems = [] then
1496                       (* this goal has failed *)
1497                       let cache = close_failures ((g,gty)::fl) cache in
1498                       aux tables maxm flags cache orlist
1499                     else
1500                       (* elems = (cand,m,s,gl) *)
1501                       let size_gl l = List.length
1502                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1503                       in
1504                       let elems =
1505                         let inj_gl gl = List.map (fun g -> D g) gl in
1506                         let rec map = function
1507                           | [] -> assert false
1508                           | (cand,m,s,gl)::[] ->
1509                               (* in the last one we add the failure *)
1510                               let todo =
1511                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1512                               in
1513                               (* we are the last in OR, we fail on g and
1514                                * also on all failures implied by g *)
1515                               (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1516                               :: orlist
1517                           | (cand,m,s,gl)::tl ->
1518                               (* we add the S step after gl and before todo *)
1519                               let todo =
1520                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1521                               in
1522                               (* since we are not the last in OR, we do not
1523                                * imply failures *)
1524                               (m,s, size + size_gl gl, don, todo, []) :: map tl
1525                         in
1526                           map elems
1527                       in
1528                         aux tables maxm flags cache elems)
1529             | _ ->
1530                 (* no more depth *)
1531                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1532                 let cache = close_failures fl cache in
1533                 aux tables maxm flags cache orlist)
1534   in
1535     (aux tables maxm flags cache elems : auto_result)
1536 ;;
1537
1538
1539 let
1540   auto_all_solutions maxm tables universe cache context metasenv gl flags
1541 =
1542   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1543   let goals =
1544     List.map
1545       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1546   in
1547   let elems = [metasenv,[],1,[],goals,[]] in
1548   let rec aux tables maxm solutions cache elems flags =
1549     match auto_main tables maxm context flags universe cache elems with
1550     | Gaveup (tables,cache,maxm) ->
1551         solutions,cache,maxm
1552     | Proved (metasenv,subst,others,tables,cache,maxm) ->
1553         if Unix.gettimeofday () > flags.timeout then
1554           ((subst,metasenv)::solutions), cache, maxm
1555         else
1556           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1557   in
1558   let rc = aux tables maxm [] cache elems flags in
1559     match rc with
1560     | [],cache,maxm -> [],cache,maxm
1561     | solutions,cache,maxm ->
1562         let solutions =
1563           HExtlib.filter_map
1564             (fun (subst,newmetasenv) ->
1565               let opened =
1566                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1567               in
1568               if opened = [] then Some subst else None)
1569             solutions
1570         in
1571          solutions,cache,maxm
1572 ;;
1573
1574 (* }}} ****************** AUTO ***************)
1575
1576 let auto flags metasenv tables universe cache context metasenv gl =
1577   let initial_time = Unix.gettimeofday() in
1578   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1579   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1580   let elems = [metasenv,[],1,[],goals,[]] in
1581   match auto_main tables 0 context flags universe cache elems with
1582   | Proved (metasenv,subst,_, tables,cache,_) ->
1583       debug_print(lazy
1584         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1585       Some (subst,metasenv), cache
1586   | Gaveup (tables,cache,maxm) ->
1587       debug_print(lazy
1588         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1589       None,cache
1590 ;;
1591
1592 let applyS_tac ~dbd ~term ~params ~universe =
1593  ProofEngineTypes.mk_tactic
1594   (fun status ->
1595     try
1596       let proof, gl,_,_ =
1597        apply_smart ~dbd ~term ~subst:[] ~params ~universe status
1598       in
1599        proof, gl
1600     with
1601     | CicUnification.UnificationFailure msg
1602     | CicTypeChecker.TypeCheckerFailure msg ->
1603         raise (ProofEngineTypes.Fail msg))
1604
1605 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
1606   let _,metasenv,_subst,_,_, _ = proof in
1607   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1608   let universe = universe_of_params metasenv context universe univ in
1609   let flags = flags_of_params params () in
1610   let use_library = flags.use_library in
1611   let tables,cache,newmeta =
1612     init_cache_and_tables ~dbd use_library flags.use_only_paramod true
1613       false universe (proof, goal) in
1614   let tables,cache,newmeta =
1615     if flags.close_more then
1616       close_more
1617         tables newmeta context (proof, goal)
1618           auto_all_solutions universe cache
1619     else tables,cache,newmeta in
1620   let initial_time = Unix.gettimeofday() in
1621   let (_,oldmetasenv,_subst,_,_, _) = proof in
1622   hint := None;
1623   let elem =
1624     metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1625   in
1626   match auto_main tables newmeta context flags universe cache [elem] with
1627     | Proved (metasenv,subst,_, tables,cache,_) ->
1628         debug_print (lazy
1629           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1630         let proof,metasenv =
1631         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1632           proof goal subst metasenv
1633         in
1634         let opened =
1635           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1636             ~newmetasenv:metasenv
1637         in
1638           proof,opened
1639     | Gaveup (tables,cache,maxm) ->
1640         debug_print
1641           (lazy ("TIME:"^
1642             string_of_float(Unix.gettimeofday()-.initial_time)));
1643         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1644 ;;
1645
1646 let auto_tac ~dbd ~params ~universe =
1647   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1648
1649 let eq_of_goal = function
1650   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1651       uri
1652   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1653 ;;
1654
1655 (* performs steps of rewrite with the universe, obtaining if possible
1656  * a trivial goal *)
1657 let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
1658   let _,metasenv,_subst,_,_,_ = proof in
1659   let _,context,ty = CicUtil.lookup_meta goal metasenv in
1660   let steps = int_of_string (string params "steps" "1") in
1661   let universe = universe_of_params metasenv context universe univ in
1662   let eq_uri = eq_of_goal ty in
1663   let (active,passive,bag), cache, maxm =
1664      (* we take the whole universe (no signature filtering) *)
1665      init_cache_and_tables false true false true universe (proof,goal)
1666   in
1667   let initgoal = [], metasenv, ty in
1668   let table =
1669     let equalities = (Saturation.list_of_passive passive) in
1670     (* we demodulate using both actives passives *)
1671     List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
1672   in
1673   let env = metasenv,context,CicUniv.oblivion_ugraph in
1674   match Indexing.solve_demodulating bag env table initgoal steps with
1675   | Some (proof, metasenv, newty) ->
1676       let refl =
1677         match newty with
1678         | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
1679             Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
1680         | _ -> assert false
1681       in
1682       let proofterm,_ =
1683         Equality.build_goal_proof
1684           bag eq_uri proof refl newty [] context metasenv
1685       in
1686       ProofEngineTypes.apply_tactic
1687         (PrimitiveTactics.apply_tac ~term:proofterm) status
1688   | None ->
1689       raise
1690         (ProofEngineTypes.Fail (lazy
1691           ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
1692 ;;
1693 let solve_rewrite_tac ~params ~universe () =
1694   ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
1695 ;;
1696
1697 (* Demodulate thorem *)
1698 let open_type ty bo =
1699   let rec open_type_aux context ty k args =
1700     match ty with
1701       | Cic.Prod (n,s,t) ->
1702           let n' =
1703             FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
1704           let entry = match n' with
1705             | Cic.Name _    -> Some (n',(Cic.Decl s))
1706             | Cic.Anonymous -> None
1707           in
1708             open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
1709       | Cic.LetIn (n,s,sty,t) ->
1710           let entry = Some (n,(Cic.Def (s,sty)))
1711           in
1712             open_type_aux (entry::context) t (k+1) args
1713       | _  -> context, ty, args
1714   in
1715   let context, ty, args = open_type_aux [] ty 1 [] in
1716   match args with
1717     | [] -> context, ty, bo
1718     | _ -> context, ty, Cic.Appl (bo::args)
1719 ;;
1720
1721 let rec close_type bo ty context =
1722   match context with
1723     | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
1724     | Some (n,(Cic.Decl s))::tl ->
1725         close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
1726     | Some (n,(Cic.Def (s,sty)))::tl ->
1727         close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
1728     | _ -> assert false
1729 ;;
1730
1731 let is_subsumed univ context ty =
1732   let candidates = Universe.get_candidates univ ty in
1733     List.fold_left
1734       (fun res cand ->
1735          match res with
1736            | Some found -> Some found
1737            | None ->
1738                try
1739                  let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
1740                  let metasenv = [(0,context,ty)] in
1741                  let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
1742                  let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1743                    (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
1744                  in
1745                  let prop_goals, other = split_goals_in_prop metasenv subst open_goals in
1746                    if prop_goals = [] then Some cand else None
1747                with
1748                  | ProofEngineTypes.Fail s -> None
1749                  | CicUnification.Uncertain s ->  None
1750       ) None candidates
1751 ;;
1752
1753 let demodulate_theorem ~universe uri =
1754   let eq_uri =
1755     match LibraryObjects.eq_URI () with
1756       | Some (uri) -> uri
1757       | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1758   let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
1759   in
1760   let context,ty,bo =
1761     match obj with
1762       | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
1763       | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
1764   in
1765   if CicUtil.is_closed ty then
1766     raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
1767   let initgoal = [], [], ty in
1768   (* compute the signature *)
1769   let signature =
1770     let ty_set = MetadataConstraints.constants_of ty in
1771     let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
1772     let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
1773       MetadataQuery.close_with_types set [] context
1774   in
1775   (* retrieve equations from the universe universe *)
1776   let equations =
1777     retrieve_equations true signature universe AutoCache.cache_empty context []
1778   in
1779   debug_print
1780     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
1781   let eqs_and_types =
1782     HExtlib.filter_map
1783       (fun t ->
1784          let ty,_ =
1785            CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
1786          in
1787          (* retrieve_equations could also return flexible terms *)
1788          if is_an_equality ty then Some(t,ty)
1789          else
1790            try
1791              let ty' = unfold context ty in
1792              if is_an_equality ty' then Some(t,ty') else None
1793            with ProofEngineTypes.Fail _ -> None)
1794       equations
1795   in
1796   let bag = Equality.mk_equality_bag () in
1797
1798   let units, _, newmeta =
1799     partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
1800   in
1801   let table =
1802     List.fold_left
1803       (fun tbl eq -> Indexing.index tbl eq)
1804       Indexing.empty units
1805   in
1806   let changed,(newproof,newmetasenv, newty) =
1807     Indexing.demod bag
1808       ([],context,CicUniv.oblivion_ugraph) table initgoal in
1809   if changed then
1810     begin
1811       let oldproof = Equality.Exact bo in
1812       let proofterm,_ =
1813         Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
1814           eq_uri newproof oldproof ty [] context newmetasenv
1815       in
1816       if newmetasenv <> [] then
1817         raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
1818       else
1819         begin
1820           assert_proof_is_valid proofterm newmetasenv context newty;
1821           match is_subsumed universe context newty with
1822             | Some t -> raise
1823                 (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
1824             | None -> close_type proofterm newty context
1825         end
1826     end
1827   else (* if newty = ty then *)
1828     raise (ProofEngineTypes.Fail (lazy "no progress"))
1829   (*else ProofEngineTypes.apply_tactic
1830     (ReductionTactics.simpl_tac
1831       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1832 ;;
1833
1834
1835 (* NEW DEMODULATE *)
1836 let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
1837   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1838   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1839   let universe = universe_of_params metasenv context universe univ in
1840   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1841   let initgoal = [], metasenv, ty in
1842   let eq_uri =
1843     match LibraryObjects.eq_URI () with
1844       | Some (uri) -> uri
1845       | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1846   (* let eq_uri = eq_of_goal ty in *)
1847   let (active,passive,bag), cache, maxm =
1848      init_cache_and_tables
1849        ~dbd false false true true universe (proof,goal)
1850   in
1851   let equalities = (Saturation.list_of_passive passive) in
1852   (* we demodulate using both actives passives *)
1853   let table =
1854     List.fold_left
1855       (fun tbl eq -> Indexing.index tbl eq)
1856       (snd active) equalities
1857   in
1858   let changed,(newproof,newmetasenv, newty) =
1859     (* Indexing.demodulation_goal bag *)
1860       Indexing.demod bag
1861       (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
1862   in
1863   if changed then
1864     begin
1865       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1866       let proofterm,_ =
1867         Equality.build_goal_proof (~contextualize:false) bag
1868           eq_uri newproof opengoal ty [] context metasenv
1869       in
1870         let extended_metasenv = (maxm,context,newty)::metasenv in
1871         let extended_status =
1872           (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1873         let (status,newgoals) =
1874           ProofEngineTypes.apply_tactic
1875             (PrimitiveTactics.apply_tac ~term:proofterm)
1876             extended_status in
1877         (status,maxm::newgoals)
1878     end
1879   else (* if newty = ty then *)
1880     raise (ProofEngineTypes.Fail (lazy "no progress"))
1881   (*else ProofEngineTypes.apply_tactic
1882     (ReductionTactics.simpl_tac
1883       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1884 ;;
1885
1886 let demodulate_tac ~dbd ~params ~universe =
1887   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;
1888
1889 let pp_proofterm = Equality.pp_proofterm;;
1890
1891 let revision = "$Revision$";;
1892 let size_and_depth context metasenv t = 100, 100