helm/software/components/tactics/auto.ml

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