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      prerr_endline "chiamo given clause";
 617      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
 618        max_int max_int flags.timeout
 619  with
 620  | None, _,_,_ ->
 621      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 622  | Some (_,proof''''',_), active,passive,_  ->
 623      prerr_endline "torno";
 624
 625      proof''''',
 626      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 627        ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
 628 ;;
 629
 630 let rec count_prods context ty =
 631  match CicReduction.whd context ty with
 632     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 633   | _ -> 0
 634
 635 let apply_smart
 636   ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal)
 637 =
 638  let module T = CicTypeChecker in
 639  let module R = CicReduction in
 640  let module C = Cic in
 641   let (_,metasenv,_subst,_,_, _) = proof in
 642   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 643   let flags = flags_of_params params ~for_applyS:true () in
 644   let universe = universe_of_params metasenv context universe univ in
 645   let newmeta = CicMkImplicit.new_meta metasenv subst in
 646    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 647     match term with
 648        C.Var (uri,exp_named_subst) ->
 649         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 650          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 651           exp_named_subst
 652         in
 653          exp_named_subst_diff,newmeta',newmetasenvfragment,
 654           C.Var (uri,exp_named_subst')
 655      | C.Const (uri,exp_named_subst) ->
 656         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 657          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 658           exp_named_subst
 659         in
 660          exp_named_subst_diff,newmeta',newmetasenvfragment,
 661           C.Const (uri,exp_named_subst')
 662      | C.MutInd (uri,tyno,exp_named_subst) ->
 663         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 664          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 665           exp_named_subst
 666         in
 667          exp_named_subst_diff,newmeta',newmetasenvfragment,
 668           C.MutInd (uri,tyno,exp_named_subst')
 669      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 670         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 671          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 672           exp_named_subst
 673         in
 674          exp_named_subst_diff,newmeta',newmetasenvfragment,
 675           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 676      | _ -> [],newmeta,[],term
 677    in
 678    let metasenv' = metasenv@newmetasenvfragment in
 679    let termty,_ =
 680      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
 681    in
 682    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 683    let goal_arity = count_prods context ty in
 684    let proof, gl, active, passive =
 685     new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
 686      newmeta' metasenv' context term' ty termty goal_arity
 687    in
 688     proof, gl, active, passive
 689 ;;
 690
 691 (****************** AUTO ********************)
 692
 693 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 694 let ugraph = CicUniv.oblivion_ugraph;;
 695 let typeof = CicTypeChecker.type_of_aux';;
 696 let ppterm ctx t =
 697   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 698   CicPp.pp t names
 699 ;;
 700 let is_in_prop context subst metasenv ty =
 701   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
 702   is_propositional context sort
 703 ;;
 704
 705 exception NotConvertible;;
 706
 707 let check_proof_is_valid proof metasenv context goalty =
 708   if debug then
 709     begin
 710       try
 711         let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
 712         let b,_ = CicReduction.are_convertible context ty goalty u in
 713         if not b then raise NotConvertible else b
 714       with _ ->
 715         let names =
 716           List.map (function None -> None | Some (x,_) -> Some x) context
 717         in
 718           debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
 719           (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *)
 720           debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
 721           debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
 722         false
 723     end
 724   else true
 725 ;;
 726
 727 let assert_proof_is_valid proof metasenv context goalty =
 728   assert (check_proof_is_valid proof metasenv context goalty)
 729 ;;
 730
 731 let assert_subst_are_disjoint subst subst' =
 732   if debug then
 733     assert(List.for_all
 734              (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 735              subst)
 736   else ()
 737 ;;
 738
 739 let split_goals_in_prop metasenv subst gl =
 740   List.partition
 741     (fun g ->
 742       let _,context,ty = CicUtil.lookup_meta g metasenv in
 743       try
 744         let sort,u = typeof ~subst metasenv context ty ugraph in
 745         is_propositional context sort
 746       with
 747       | CicTypeChecker.AssertFailure s
 748       | CicTypeChecker.TypeCheckerFailure s ->
 749           debug_print
 750             (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
 751           debug_print s;
 752           false)
 753     (* FIXME... they should type! *)
 754     gl
 755 ;;
 756
 757 let split_goals_with_metas metasenv subst gl =
 758   List.partition
 759     (fun g ->
 760       let _,context,ty = CicUtil.lookup_meta g metasenv in
 761       let ty = CicMetaSubst.apply_subst subst ty in
 762       CicUtil.is_meta_closed ty)
 763     gl
 764 ;;
 765
 766 let order_new_goals metasenv subst open_goals ppterm =
 767   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 768   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
 769   let closed_type, open_type = split_goals_with_metas metasenv subst rest in
 770   let open_goals =
 771     (List.map (fun x -> x,P) (open_prop @ closed_prop))
 772     @
 773     (List.map (fun x -> x,T) (open_type @ closed_type))
 774   in
 775   let tys =
 776     List.map
 777       (fun (i,sort) ->
 778         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
 779   in
 780   debug_print (lazy ("   OPEN: "^
 781     String.concat "\n"
 782       (List.map
 783          (function
 784             | (i,t,P) -> string_of_int i   ^ ":"^ppterm t^ "Prop"
 785             | (i,t,T) -> string_of_int i  ^ ":"^ppterm t^ "Type")
 786          tys)));
 787   open_goals
 788 ;;
 789
 790 let is_an_equational_goal = function
 791   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 792   | _ -> false
 793 ;;
 794
 795 (*
 796 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
 797 *)
 798
 799 let calculate_timeout flags =
 800     if flags.timeout = 0. then
 801       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 802        {flags with timeout = infinity})
 803     else
 804       flags
 805 ;;
 806 let is_equational_case goalty flags =
 807   let ensure_equational t =
 808     if is_an_equational_goal t then true
 809     else false
 810     (*
 811       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 812       raise (ProofEngineTypes.Fail (lazy msg))
 813     *)
 814   in
 815   (flags.use_paramod && is_an_equational_goal goalty) ||
 816   (flags.use_only_paramod && ensure_equational goalty)
 817 ;;
 818 (*
 819 let cache_add_success sort cache k v =
 820   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 821   cache k
 822 ;;
 823 *)
 824
 825 type menv = Cic.metasenv
 826 type subst = Cic.substitution
 827 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 828 let candidate_no = ref 0;;
 829 type candidate = int * Cic.term Lazy.t
 830 type cache = AutoCache.cache
 831 type tables =
 832   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
 833
 834 type fail =
 835   (* the goal (mainly for depth) and key of the goal *)
 836   goal * AutoCache.cache_key
 837 type op =
 838   (* goal has to be proved *)
 839   | D of goal
 840   (* goal has to be cached as a success obtained using candidate as the first
 841    * step *)
 842   | S of goal * AutoCache.cache_key * candidate * int
 843 type elem =
 844   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
 845   menv * subst * int * op list * op list * fail list
 846 type status =
 847   (* list of computations that may lead to the solution: all op list will
 848    * end with the same (S(g,_)) *)
 849   elem list
 850 type auto_result =
 851   (* menv, subst, alternatives, tables, cache, maxmeta *)
 852   | Proved of menv * subst * elem list * tables * cache * int
 853   | Gaveup of tables * cache * int
 854
 855
 856 (* the status exported to the external observer *)
 857 type auto_status =
 858   (* context, (goal,candidate) list, and_list, history *)
 859   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 860   (int * Cic.term * int) list * Cic.term Lazy.t list
 861
 862 let d_prefix l =
 863   let rec aux acc = function
 864     | (D g)::tl -> aux (acc@[g]) tl
 865     | _ -> acc
 866   in
 867     aux [] l
 868 ;;
 869 let prop_only l =
 870   List.filter (function (_,_,P) -> true | _ -> false) l
 871 ;;
 872
 873 let d_goals l =
 874   let rec aux acc = function
 875     | (D g)::tl -> aux (acc@[g]) tl
 876     | (S _)::tl -> aux acc tl
 877     | [] -> acc
 878   in
 879     aux [] l
 880 ;;
 881
 882 let calculate_goal_ty (goalno,_,_) s m =
 883   try
 884     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 885     (* XXX applicare la subst al contesto? *)
 886     Some (cc, CicMetaSubst.apply_subst s goalty)
 887   with CicUtil.Meta_not_found i when i = goalno -> None
 888 ;;
 889
 890 let calculate_closed_goal_ty (goalno,_,_) s =
 891   try
 892     let cc,_,goalty = List.assoc goalno s in
 893     (* XXX applicare la subst al contesto? *)
 894     Some (cc, CicMetaSubst.apply_subst s goalty)
 895   with Not_found -> None
 896 ;;
 897
 898 let pp_status ctx status =
 899   if debug then
 900   let names = Utils.names_of_context ctx in
 901   let pp x =
 902     let x =
 903       ProofEngineReduction.replace
 904         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 905           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 906     in
 907     CicPp.pp x names
 908   in
 909   let string_of_do m s (gi,_,_ as g) d =
 910     match calculate_goal_ty g s m with
 911     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 912     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 913   in
 914   let string_of_s m su k (ci,ct) gi =
 915     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 916   in
 917   let string_of_ol m su l =
 918     String.concat " | "
 919       (List.map
 920         (function
 921           | D (g,d,s) -> string_of_do m su (g,d,s) d
 922           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 923         l)
 924   in
 925   let string_of_fl m s fl =
 926     String.concat " | "
 927       (List.map (fun ((i,_,_),ty) ->
 928          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 929   in
 930   let rec aux = function
 931     | [] -> ()
 932     | (m,s,_,_,ol,fl)::tl ->
 933         Printf.eprintf "< [%s] ;;; [%s]>\n"
 934           (string_of_ol m s ol) (string_of_fl m s fl);
 935         aux tl
 936   in
 937     Printf.eprintf "-------------------------- status -------------------\n";
 938     aux status;
 939     Printf.eprintf "-----------------------------------------------------\n";
 940 ;;
 941
 942 let auto_status = ref [] ;;
 943 let auto_context = ref [];;
 944 let in_pause = ref false;;
 945 let pause b = in_pause := b;;
 946 let cond = Condition.create ();;
 947 let mutex = Mutex.create ();;
 948 let hint = ref None;;
 949 let prune_hint = ref [];;
 950
 951 let step _ = Condition.signal cond;;
 952 let give_hint n = hint := Some n;;
 953 let give_prune_hint hint =
 954   prune_hint := hint :: !prune_hint
 955 ;;
 956
 957 let check_pause _ =
 958   if !in_pause then
 959     begin
 960       Mutex.lock mutex;
 961       Condition.wait cond mutex;
 962       Mutex.unlock mutex
 963     end
 964 ;;
 965
 966 let get_auto_status _ =
 967   let status = !auto_status in
 968   let and_list,elems,last =
 969     match status with
 970     | [] -> [],[],[]
 971     | (m,s,_,don,gl,fail)::tl ->
 972         let and_list =
 973           HExtlib.filter_map
 974             (fun (id,d,_ as g) ->
 975               match calculate_goal_ty g s m with
 976               | Some (_,x) -> Some (id,x,d) | None -> None)
 977             (d_goals gl)
 978         in
 979         let rows =
 980           (* these are the S goalsin the or list *)
 981           let orlist =
 982             List.map
 983               (fun (m,s,_,don,gl,fail) ->
 984                 HExtlib.filter_map
 985                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 986                   (List.rev don @ gl))
 987               status
 988           in
 989           (* this function eats id from a list l::[id,x] returning x, l *)
 990           let eat_tail_if_eq id l =
 991             let rec aux (s, l) = function
 992               | [] -> s, l
 993               | ((id1,_,_),k1,c)::tl when id = id1 ->
 994                   (match s with
 995                   | None -> aux (Some c,l) tl
 996                   | Some _ -> assert false)
 997               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 998             in
 999             let c, l = aux (None, []) l in
1000             c, List.rev l
1001           in
1002           let eat_in_parallel id l =
1003             let rec aux (b,eaten, new_l as acc) l =
1004               match l with
1005               | [] -> acc
1006               | l::tl ->
1007                   match eat_tail_if_eq id l with
1008                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
1009                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
1010             in
1011             aux ([],[],[]) l
1012           in
1013           let rec eat_all rows l =
1014             match l with
1015             | [] -> rows
1016             | elem::or_list ->
1017                 match List.rev elem with
1018                 | ((to_eat,depth,_),k,_)::next_lunch ->
1019                     let b, eaten, l = eat_in_parallel to_eat l in
1020                     let eaten = HExtlib.list_uniq eaten in
1021                     let eaten = List.rev eaten in
1022                     let b = true (* List.hd (List.rev b) *) in
1023                     let rows = rows @ [to_eat,k,b,depth,eaten] in
1024                     eat_all rows l
1025                 | [] -> eat_all rows or_list
1026           in
1027           eat_all [] (List.rev orlist)
1028         in
1029         let history =
1030           HExtlib.filter_map
1031             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
1032             gl
1033         in
1034 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
1035         and_list, rows, history
1036   in
1037   !auto_context, elems, and_list, last
1038 ;;
1039
1040 (* Works if there is no dependency over proofs *)
1041 let is_a_green_cut goalty =
1042   CicUtil.is_meta_closed goalty
1043 ;;
1044 let rec first_s = function
1045   | (D _)::tl -> first_s tl
1046   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
1047   | [] -> None
1048 ;;
1049 let list_union l1 l2 =
1050   (* TODO ottimizzare compare *)
1051   HExtlib.list_uniq (List.sort compare (l1 @ l1))
1052 ;;
1053 let rec eq_todo l1 l2 =
1054   match l1,l2 with
1055   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
1056   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
1057     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
1058       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
1059   | [],[] -> true
1060   | _ -> false
1061 ;;
1062 let eat_head todo id fl orlist =
1063   let rec aux acc = function
1064   | [] -> [], acc
1065   | (m, s, _, _, todo1, fl1)::tl as orlist ->
1066       let rec aux1 todo1 =
1067         match first_s todo1 with
1068         | None -> orlist, acc
1069         | Some (((gno,_,_),_,_,_), todo11) ->
1070             (* TODO confronto tra todo da ottimizzare *)
1071             if gno = id && eq_todo todo11 todo then
1072               aux (list_union fl1 acc) tl
1073             else
1074               aux1 todo11
1075       in
1076        aux1 todo1
1077   in
1078     aux fl orlist
1079 ;;
1080 let close_proof p ty menv context =
1081   let metas =
1082     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
1083   in
1084   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
1085   naif_closure p menv context
1086 ;;
1087 (* XXX capire bene quando aggiungere alla cache *)
1088 let add_to_cache_and_del_from_orlist_if_green_cut
1089   g s m cache key todo orlist fl ctx size minsize
1090 =
1091   let cache = cache_remove_underinspection cache key in
1092   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
1093    * canonico! XXX *)
1094   match calculate_closed_goal_ty g s with
1095   | None -> assert false
1096   | Some (canonical_ctx , gty) ->
1097       let goalno,depth,sort = g in
1098       let irl = mk_irl canonical_ctx in
1099       let goal = Cic.Meta(goalno, irl) in
1100       let proof = CicMetaSubst.apply_subst s goal in
1101       let green_proof, closed_proof =
1102         let b = is_a_green_cut proof in
1103         if not b then
1104           b, (* close_proof proof gty m ctx *) proof
1105         else
1106           b, proof
1107       in
1108       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
1109       if is_a_green_cut key then
1110         (* if the initia goal was closed, we cut alternatives *)
1111         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
1112         let orlist, fl = eat_head todo goalno fl orlist in
1113         let cache =
1114           if size < minsize then
1115             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
1116           else
1117           (* if the proof is closed we cache it *)
1118           if green_proof then cache_add_success cache key proof
1119           else (* cache_add_success cache key closed_proof *)
1120             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
1121         in
1122         cache, orlist, fl, true
1123       else
1124         let cache =
1125           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
1126           if size < minsize then
1127             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1128           (* if the substituted goal and the proof are closed we cache it *)
1129           if is_a_green_cut gty then
1130             if green_proof then cache_add_success cache gty proof
1131             else (* cache_add_success cache gty closed_proof *)
1132               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1133           else (*
1134             try
1135               let ty, _ =
1136                 CicTypeChecker.type_of_aux' ~subst:s
1137                   m ctx closed_proof CicUniv.oblivion_ugraph
1138               in
1139               if is_a_green_cut ty then
1140                 cache_add_success cache ty closed_proof
1141               else cache
1142             with
1143             | CicTypeChecker.TypeCheckerFailure _ ->*)
1144           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1145         in
1146         cache, orlist, fl, false
1147 ;;
1148 let close_failures (fl : fail list) (cache : cache) =
1149   List.fold_left
1150     (fun cache ((gno,depth,_),gty) ->
1151       debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1152       cache_add_failure cache gty depth)
1153     cache fl
1154 ;;
1155 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
1156   let entry = goalno, (canonical_ctx, t,ty) in
1157   assert_subst_are_disjoint subst [entry];
1158   let subst = entry :: subst in
1159   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1160   subst, metasenv
1161 ;;
1162
1163 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1164   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
1165 ;;
1166 let equational_case
1167   tables maxm cache depth fake_proof goalno goalty subst context
1168     flags
1169 =
1170   let active,passive,bag = tables in
1171   let ppterm = ppterm context in
1172   let status = (fake_proof,goalno) in
1173     if flags.use_only_paramod then
1174       begin
1175         debug_print (lazy ("PARAMODULATION SU: " ^
1176                          string_of_int goalno ^ " " ^ ppterm goalty ));
1177         let goal_steps, saturation_steps, timeout =
1178           max_int,max_int,flags.timeout
1179         in
1180
1181         match
1182           Saturation.given_clause bag maxm status active passive
1183             goal_steps saturation_steps timeout
1184         with
1185           | None, active, passive, maxmeta ->
1186               [], (active,passive,bag), cache, maxmeta, flags
1187           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1188             passive,maxmeta ->
1189               assert_subst_are_disjoint subst subst';
1190               let subst = subst@subst' in
1191               let open_goals =
1192                 order_new_goals metasenv subst open_goals ppterm
1193               in
1194               let open_goals =
1195                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1196               in
1197               incr candidate_no;
1198                       [(!candidate_no,proof),metasenv,subst,open_goals],
1199                 (active,passive,bag),
1200                 cache, maxmeta, flags
1201       end
1202     else
1203       begin
1204         debug_print
1205           (lazy
1206            ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1207         let res, maxmeta =
1208           Saturation.all_subsumed bag maxm status active passive
1209         in
1210         assert (maxmeta >= maxm);
1211         let res' =
1212           List.map
1213             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
1214                assert_subst_are_disjoint subst subst';
1215                let subst = subst@subst' in
1216                let open_goals =
1217                  order_new_goals metasenv subst open_goals ppterm
1218                in
1219                let open_goals =
1220                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1221                in
1222                incr candidate_no;
1223                  (!candidate_no,proof),metasenv,subst,open_goals)
1224             res
1225           in
1226           res', (active,passive,bag), cache, maxmeta, flags
1227       end
1228 ;;
1229
1230 let try_candidate
1231   goalty tables maxm subst fake_proof goalno depth context cand
1232 =
1233   let ppterm = ppterm context in
1234   try
1235     let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1236         (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1237         (fake_proof,goalno)
1238     in
1239     debug_print (lazy ("   OK: " ^ ppterm cand));
1240     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1241     let open_goals = order_new_goals metasenv subst open_goals ppterm in
1242     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1243     incr candidate_no;
1244     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
1245   with
1246     | ProofEngineTypes.Fail s -> None,tables, maxm
1247     | CicUnification.Uncertain s ->  None,tables, maxm
1248 ;;
1249
1250 let sort_new_elems =
1251  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
1252   List.length (prop_only l1) - List.length (prop_only l2))
1253 ;;
1254
1255 let applicative_case
1256   tables maxm depth subst fake_proof goalno goalty metasenv context universe
1257   cache
1258 =
1259   let candidates = get_candidates universe cache goalty in
1260   let tables, elems, maxm =
1261     List.fold_left
1262       (fun (tables,elems,maxm) cand ->
1263         match
1264           try_candidate goalty
1265             tables maxm subst fake_proof goalno depth context cand
1266         with
1267         | None, tables,maxm  -> tables,elems, maxm
1268         | Some x, tables, maxm -> tables,x::elems, maxm)
1269       (tables,[],maxm) candidates
1270   in
1271   let elems = sort_new_elems elems in
1272   elems, tables, cache, maxm
1273 ;;
1274
1275 let equational_and_applicative_case
1276   universe flags m s g gty tables cache maxm context
1277 =
1278   let goalno, depth, sort = g in
1279   let fake_proof = mk_fake_proof m s g gty context in
1280   if is_equational_case gty flags then
1281     let elems,tables,cache,maxm1, flags =
1282       equational_case tables maxm cache
1283         depth fake_proof goalno gty s context flags
1284     in
1285     let maxm = maxm1 in
1286     let more_elems, tables, cache, maxm1 =
1287       if flags.use_only_paramod then
1288         [],tables, cache, maxm
1289       else
1290         applicative_case
1291           tables maxm depth s fake_proof goalno
1292             gty m context universe cache
1293     in
1294     let maxm = maxm1 in
1295       elems@more_elems, tables, cache, maxm, flags
1296   else
1297     let elems, tables, cache, maxm =
1298       applicative_case tables maxm depth s fake_proof goalno
1299         gty m context universe cache
1300     in
1301       elems, tables, cache, maxm, flags
1302 ;;
1303 let rec condition_for_hint i = function
1304   | [] -> false
1305   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1306   | _::tl -> condition_for_hint i tl
1307 ;;
1308 let remove_s_from_fl (id,_,_) (fl : fail list) =
1309   let rec aux = function
1310     | [] -> []
1311     | ((id1,_,_),_)::tl when id = id1 -> tl
1312     | hd::tl ->  hd :: aux tl
1313   in
1314     aux fl
1315 ;;
1316
1317 let prunable_for_size flags s m todo =
1318   let rec aux b = function
1319     | (S _)::tl -> aux b tl
1320     | (D (_,_,T))::tl -> aux b tl
1321     | (D g)::tl ->
1322         (match calculate_goal_ty g s m with
1323           | None -> aux b tl
1324           | Some (canonical_ctx, gty) ->
1325             let gsize, _ =
1326               Utils.weight_of_term
1327                 ~consider_metas:false ~count_metas_occurrences:true gty in
1328             let newb = b || gsize > flags.maxgoalsizefactor in
1329             aux newb tl)
1330     | [] -> b
1331   in
1332     aux false todo
1333
1334 (*
1335 let prunable ty todo =
1336   let rec aux b = function
1337     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1338     | (D (_,_,T))::tl -> aux b tl
1339     | D _::_ -> false
1340     | [] -> b
1341   in
1342     aux false todo
1343 ;;
1344 *)
1345
1346 let prunable menv subst ty todo =
1347   let rec aux = function
1348     | (S(_,k,_,_))::tl ->
1349          (match Equality.meta_convertibility_subst k ty menv with
1350           | None -> aux tl
1351           | Some variant ->
1352                no_progress variant tl (* || aux tl*))
1353     | (D (_,_,T))::tl -> aux tl
1354     | _ -> false
1355   and no_progress variant = function
1356     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1357     | D ((n,_,P) as g)::tl ->
1358         (match calculate_goal_ty g subst menv with
1359            | None -> no_progress variant tl
1360            | Some (_, gty) ->
1361                (match calculate_goal_ty g variant menv with
1362                   | None -> assert false
1363                   | Some (_, gty') ->
1364                       if gty = gty' then
1365                          no_progress variant tl
1366                       else false))
1367     | _::tl -> no_progress variant tl
1368   in
1369     aux todo
1370
1371 ;;
1372 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1373   let s =
1374     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1375   in
1376   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1377 ;;
1378 let filter_prune_hint l =
1379   let prune = !prune_hint in
1380   prune_hint := []; (* possible race... *)
1381   if prune = [] then l
1382   else List.filter (condition_for_prune_hint prune) l
1383 ;;
1384 let auto_main tables maxm context flags universe cache elems =
1385   auto_context := context;
1386   let rec aux tables maxm flags cache (elems : status) =
1387 (*     pp_status context elems; *)
1388 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1389     auto_status := elems;
1390     check_pause ();
1391 *)
1392     let elems = filter_prune_hint elems in
1393     match elems with
1394     | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1395         debug_print (lazy "skip");
1396         (match !hint with
1397         | Some i when condition_for_hint i todo ->
1398             aux tables maxm flags cache orlist
1399         | _ ->
1400           hint := None;
1401           aux tables maxm flags cache elems)
1402     | [] ->
1403         (* complete failure *)
1404         debug_print (lazy "give up");
1405         Gaveup (tables, cache, maxm)
1406     | (m, s, _, _, [],_)::orlist ->
1407         (* complete success *)
1408         debug_print (lazy "success");
1409         Proved (m, s, orlist, tables, cache, maxm)
1410     | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
1411       when not flags.AutoTypes.do_types ->
1412         (* skip since not Prop, don't even check if closed by side-effect *)
1413         debug_print (lazy "skip existential goal");
1414         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1415     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1416         (* partial success, cache g and go on *)
1417         let cache, orlist, fl, sibling_pruned =
1418           add_to_cache_and_del_from_orlist_if_green_cut
1419             g s m cache key todo orlist fl context size minsize
1420         in
1421         debug_print (lazy (AutoCache.cache_print context cache));
1422         let fl = remove_s_from_fl g fl in
1423         let don = if sibling_pruned then don else op::don in
1424         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1425     | (m, s, size, don, todo, fl)::orlist
1426       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1427         debug_print (lazy ("FAIL: WIDTH"));
1428         (* too many goals in and generated by last th *)
1429         let cache = close_failures fl cache in
1430         aux tables maxm flags cache orlist
1431     | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1432         debug_print
1433           (lazy ("FAIL: SIZE: "^string_of_int size ^
1434             " > " ^ string_of_int flags.maxsize ));
1435         (* we already have a too large proof term *)
1436         let cache = close_failures fl cache in
1437         aux tables maxm flags cache orlist
1438     | _ when Unix.gettimeofday () > flags.timeout ->
1439         (* timeout *)
1440         debug_print (lazy ("FAIL: TIMEOUT"));
1441         Gaveup (tables, cache, maxm)
1442     | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
1443         (* attack g *)
1444         debug_print (lazy "attack goal");
1445         match calculate_goal_ty g s m with
1446         | None ->
1447             (* closed by side effect *)
1448             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1449             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1450         | Some (canonical_ctx, gty) ->
1451             let gsize, _ =
1452               Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1453             in
1454             if gsize > flags.maxgoalsizefactor then
1455               (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1456                aux tables maxm flags cache orlist)
1457             else if prunable_for_size flags s m todo then
1458                 (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
1459                  aux tables maxm flags cache orlist)
1460             else
1461             (* still to be proved *)
1462             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1463             match cache_examine cache gty with
1464             | Failed_in d when d >= depth ->
1465                 (* fail depth *)
1466                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1467                 let cache = close_failures fl cache in
1468                 aux tables maxm flags cache orlist
1469             | UnderInspection ->
1470                 (* fail loop *)
1471                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1472                 let cache = close_failures fl cache in
1473                 aux tables maxm flags cache orlist
1474             | Succeded t ->
1475                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1476                 let s, m = put_in_subst s m g canonical_ctx t gty in
1477                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1478             | Notfound
1479             | Failed_in _ when depth > 0 ->
1480                 ( (* more depth or is the first time we see the goal *)
1481                     if prunable m s gty todo then
1482                       (debug_print (lazy(
1483                          "FAIL: LOOP: one father is equal"));
1484                        aux tables maxm flags cache orlist)
1485                     else
1486                     let cache = cache_add_underinspection cache gty depth in
1487                     auto_status := status;
1488                     check_pause ();
1489                     debug_print
1490                       (lazy ("INSPECTING: " ^
1491                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1492                         CicPp.ppterm gty));
1493                     (* elems are possible computations for proving gty *)
1494                     let elems, tables, cache, maxm, flags =
1495                       equational_and_applicative_case
1496                         universe flags m s g gty tables cache maxm context
1497                     in
1498                     if elems = [] then
1499                       (* this goal has failed *)
1500                       let cache = close_failures ((g,gty)::fl) cache in
1501                       aux tables maxm flags cache orlist
1502                     else
1503                       (* elems = (cand,m,s,gl) *)
1504                       let size_gl l = List.length
1505                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1506                       in
1507                       let elems =
1508                         let inj_gl gl = List.map (fun g -> D g) gl in
1509                         let rec map = function
1510                           | [] -> assert false
1511                           | (cand,m,s,gl)::[] ->
1512                               (* in the last one we add the failure *)
1513                               let todo =
1514                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1515                               in
1516                               (* we are the last in OR, we fail on g and
1517                                * also on all failures implied by g *)
1518                               (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1519                               :: orlist
1520                           | (cand,m,s,gl)::tl ->
1521                               (* we add the S step after gl and before todo *)
1522                               let todo =
1523                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1524                               in
1525                               (* since we are not the last in OR, we do not
1526                                * imply failures *)
1527                               (m,s, size + size_gl gl, don, todo, []) :: map tl
1528                         in
1529                           map elems
1530                       in
1531                         aux tables maxm flags cache elems)
1532             | _ ->
1533                 (* no more depth *)
1534                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1535                 let cache = close_failures fl cache in
1536                 aux tables maxm flags cache orlist)
1537   in
1538     (aux tables maxm flags cache elems : auto_result)
1539 ;;
1540
1541
1542 let
1543   auto_all_solutions maxm tables universe cache context metasenv gl flags
1544 =
1545   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1546   let goals =
1547     List.map
1548       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1549   in
1550   let elems = [metasenv,[],1,[],goals,[]] in
1551   let rec aux tables maxm solutions cache elems flags =
1552     match auto_main tables maxm context flags universe cache elems with
1553     | Gaveup (tables,cache,maxm) ->
1554         solutions,cache,maxm
1555     | Proved (metasenv,subst,others,tables,cache,maxm) ->
1556         if Unix.gettimeofday () > flags.timeout then
1557           ((subst,metasenv)::solutions), cache, maxm
1558         else
1559           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1560   in
1561   let rc = aux tables maxm [] cache elems flags in
1562     match rc with
1563     | [],cache,maxm -> [],cache,maxm
1564     | solutions,cache,maxm ->
1565         let solutions =
1566           HExtlib.filter_map
1567             (fun (subst,newmetasenv) ->
1568               let opened =
1569                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1570               in
1571               if opened = [] then Some subst else None)
1572             solutions
1573         in
1574          solutions,cache,maxm
1575 ;;
1576
1577 (* }}} ****************** AUTO ***************)
1578
1579 let auto flags metasenv tables universe cache context metasenv gl =
1580   let initial_time = Unix.gettimeofday() in
1581   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1582   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1583   let elems = [metasenv,[],1,[],goals,[]] in
1584   match auto_main tables 0 context flags universe cache elems with
1585   | Proved (metasenv,subst,_, tables,cache,_) ->
1586       debug_print(lazy
1587         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1588       Some (subst,metasenv), cache
1589   | Gaveup (tables,cache,maxm) ->
1590       debug_print(lazy
1591         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1592       None,cache
1593 ;;
1594
1595 let applyS_tac ~dbd ~term ~params ~universe =
1596  ProofEngineTypes.mk_tactic
1597   (fun status ->
1598     try
1599       let proof, gl,_,_ =
1600        apply_smart ~dbd ~term ~subst:[] ~params ~universe status
1601       in
1602        proof, gl
1603     with
1604     | CicUnification.UnificationFailure msg
1605     | CicTypeChecker.TypeCheckerFailure msg ->
1606         raise (ProofEngineTypes.Fail msg))
1607
1608 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
1609   let _,metasenv,_subst,_,_, _ = proof in
1610   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1611   let universe = universe_of_params metasenv context universe univ in
1612   let flags = flags_of_params params () in
1613   let use_library = flags.use_library in
1614   let tables,cache,newmeta =
1615     init_cache_and_tables ~dbd use_library flags.use_only_paramod true
1616       false universe (proof, goal) in
1617   let tables,cache,newmeta =
1618     if flags.close_more then
1619       close_more
1620         tables newmeta context (proof, goal)
1621           auto_all_solutions universe cache
1622     else tables,cache,newmeta in
1623   let initial_time = Unix.gettimeofday() in
1624   let (_,oldmetasenv,_subst,_,_, _) = proof in
1625   hint := None;
1626   let elem =
1627     metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1628   in
1629   match auto_main tables newmeta context flags universe cache [elem] with
1630     | Proved (metasenv,subst,_, tables,cache,_) ->
1631         debug_print (lazy
1632           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1633         let proof,metasenv =
1634         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1635           proof goal subst metasenv
1636         in
1637         let opened =
1638           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1639             ~newmetasenv:metasenv
1640         in
1641           proof,opened
1642     | Gaveup (tables,cache,maxm) ->
1643         debug_print
1644           (lazy ("TIME:"^
1645             string_of_float(Unix.gettimeofday()-.initial_time)));
1646         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1647 ;;
1648
1649 let auto_tac ~dbd ~params ~universe =
1650   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1651
1652 let eq_of_goal = function
1653   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1654       uri
1655   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1656 ;;
1657
1658 (* performs steps of rewrite with the universe, obtaining if possible
1659  * a trivial goal *)
1660 let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
1661   let _,metasenv,_subst,_,_,_ = proof in
1662   let _,context,ty = CicUtil.lookup_meta goal metasenv in
1663   let steps = int_of_string (string params "steps" "1") in
1664   let universe = universe_of_params metasenv context universe univ in
1665   let eq_uri = eq_of_goal ty in
1666   let (active,passive,bag), cache, maxm =
1667      (* we take the whole universe (no signature filtering) *)
1668      init_cache_and_tables false true false true universe (proof,goal)
1669   in
1670   let initgoal = [], metasenv, ty in
1671   let table =
1672     let equalities = (Saturation.list_of_passive passive) in
1673     (* we demodulate using both actives passives *)
1674     List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
1675   in
1676   let env = metasenv,context,CicUniv.oblivion_ugraph in
1677   match Indexing.solve_demodulating bag env table initgoal steps with
1678   | Some (proof, metasenv, newty) ->
1679       let refl =
1680         match newty with
1681         | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
1682             Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
1683         | _ -> assert false
1684       in
1685       let proofterm,_ =
1686         Equality.build_goal_proof
1687           bag eq_uri proof refl newty [] context metasenv
1688       in
1689       ProofEngineTypes.apply_tactic
1690         (PrimitiveTactics.apply_tac ~term:proofterm) status
1691   | None ->
1692       raise
1693         (ProofEngineTypes.Fail (lazy
1694           ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
1695 ;;
1696 let solve_rewrite_tac ~params ~universe () =
1697   ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
1698 ;;
1699
1700 (* Demodulate thorem *)
1701 let open_type ty bo =
1702   let rec open_type_aux context ty k args =
1703     match ty with
1704       | Cic.Prod (n,s,t) ->
1705           let n' =
1706             FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
1707           let entry = match n' with
1708             | Cic.Name _    -> Some (n',(Cic.Decl s))
1709             | Cic.Anonymous -> None
1710           in
1711             open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
1712       | Cic.LetIn (n,s,sty,t) ->
1713           let entry = Some (n,(Cic.Def (s,sty)))
1714           in
1715             open_type_aux (entry::context) t (k+1) args
1716       | _  -> context, ty, args
1717   in
1718   let context, ty, args = open_type_aux [] ty 1 [] in
1719   match args with
1720     | [] -> context, ty, bo
1721     | _ -> context, ty, Cic.Appl (bo::args)
1722 ;;
1723
1724 let rec close_type bo ty context =
1725   match context with
1726     | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
1727     | Some (n,(Cic.Decl s))::tl ->
1728         close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
1729     | Some (n,(Cic.Def (s,sty)))::tl ->
1730         close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
1731     | _ -> assert false
1732 ;;
1733
1734 let is_subsumed univ context ty =
1735   let candidates = Universe.get_candidates univ ty in
1736     List.fold_left
1737       (fun res cand ->
1738          match res with
1739            | Some found -> Some found
1740            | None ->
1741                try
1742                  let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
1743                  let metasenv = [(0,context,ty)] in
1744                  let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
1745                  let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1746                    (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
1747                  in
1748                  let prop_goals, other = split_goals_in_prop metasenv subst open_goals in
1749                    if prop_goals = [] then Some cand else None
1750                with
1751                  | ProofEngineTypes.Fail s -> None
1752                  | CicUnification.Uncertain s ->  None
1753       ) None candidates
1754 ;;
1755
1756 let demodulate_theorem ~universe uri =
1757   let eq_uri =
1758     match LibraryObjects.eq_URI () with
1759       | Some (uri) -> uri
1760       | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1761   let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
1762   in
1763   let context,ty,bo =
1764     match obj with
1765       | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
1766       | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
1767   in
1768   if CicUtil.is_closed ty then
1769     raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
1770   let initgoal = [], [], ty in
1771   (* compute the signature *)
1772   let signature =
1773     let ty_set = MetadataConstraints.constants_of ty in
1774     let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
1775     let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
1776       MetadataQuery.close_with_types set [] context
1777   in
1778   (* retrieve equations from the universe universe *)
1779   let equations =
1780     retrieve_equations true signature universe AutoCache.cache_empty context []
1781   in
1782   debug_print
1783     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
1784   let eqs_and_types =
1785     HExtlib.filter_map
1786       (fun t ->
1787          let ty,_ =
1788            CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
1789          in
1790          (* retrieve_equations could also return flexible terms *)
1791          if is_an_equality ty then Some(t,ty)
1792          else
1793            try
1794              let ty' = unfold context ty in
1795              if is_an_equality ty' then Some(t,ty') else None
1796            with ProofEngineTypes.Fail _ -> None)
1797       equations
1798   in
1799   let bag = Equality.mk_equality_bag () in
1800
1801   let units, _, newmeta =
1802     partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
1803   in
1804   let table =
1805     List.fold_left
1806       (fun tbl eq -> Indexing.index tbl eq)
1807       Indexing.empty units
1808   in
1809   let changed,(newproof,newmetasenv, newty) =
1810     Indexing.demod bag
1811       ([],context,CicUniv.oblivion_ugraph) table initgoal in
1812   if changed then
1813     begin
1814       let oldproof = Equality.Exact bo in
1815       let proofterm,_ =
1816         Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
1817           eq_uri newproof oldproof ty [] context newmetasenv
1818       in
1819       if newmetasenv <> [] then
1820         raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
1821       else
1822         begin
1823           assert_proof_is_valid proofterm newmetasenv context newty;
1824           match is_subsumed universe context newty with
1825             | Some t -> raise
1826                 (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
1827             | None -> close_type proofterm newty context
1828         end
1829     end
1830   else (* if newty = ty then *)
1831     raise (ProofEngineTypes.Fail (lazy "no progress"))
1832   (*else ProofEngineTypes.apply_tactic
1833     (ReductionTactics.simpl_tac
1834       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1835 ;;
1836
1837
1838 (* NEW DEMODULATE *)
1839 let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
1840   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1841   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1842   let universe = universe_of_params metasenv context universe univ in
1843   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1844   let initgoal = [], metasenv, ty in
1845   let eq_uri =
1846     match LibraryObjects.eq_URI () with
1847       | Some (uri) -> uri
1848       | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1849   (* let eq_uri = eq_of_goal ty in *)
1850   let (active,passive,bag), cache, maxm =
1851      init_cache_and_tables
1852        ~dbd false false true true universe (proof,goal)
1853   in
1854   let equalities = (Saturation.list_of_passive passive) in
1855   (* we demodulate using both actives passives *)
1856   let table =
1857     List.fold_left
1858       (fun tbl eq -> Indexing.index tbl eq)
1859       (snd active) equalities
1860   in
1861   let changed,(newproof,newmetasenv, newty) =
1862     (* Indexing.demodulation_goal bag *)
1863       Indexing.demod bag
1864       (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
1865   in
1866   if changed then
1867     begin
1868       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1869       let proofterm,_ =
1870         Equality.build_goal_proof (~contextualize:false) bag
1871           eq_uri newproof opengoal ty [] context metasenv
1872       in
1873         let extended_metasenv = (maxm,context,newty)::metasenv in
1874         let extended_status =
1875           (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1876         let (status,newgoals) =
1877           ProofEngineTypes.apply_tactic
1878             (PrimitiveTactics.apply_tac ~term:proofterm)
1879             extended_status in
1880         (status,maxm::newgoals)
1881     end
1882   else (* if newty = ty then *)
1883     raise (ProofEngineTypes.Fail (lazy "no progress"))
1884   (*else ProofEngineTypes.apply_tactic
1885     (ReductionTactics.simpl_tac
1886       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1887 ;;
1888
1889 let demodulate_tac ~dbd ~params ~universe =
1890   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;
1891
1892 let pp_proofterm = Equality.pp_proofterm;;
1893
1894 let revision = "$Revision$";;
1895 let size_and_depth context metasenv t = 100, 100