+ let context,ty,bo =
+ match obj with
+ | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
+ | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
+ in
+ if CicUtil.is_closed ty then
+ raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
+ let initgoal = [], [], ty in
+ (* compute the signature *)
+ let signature =
+ let ty_set = MetadataConstraints.constants_of ty in
+ let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
+ let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
+ MetadataQuery.close_with_types set [] context
+ in
+ (* retrieve equations from the universe universe *)
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
+ let equations =
+ retrieve_equations true signature universe AutoCache.cache_empty context []
+ in
+ debug_print
+ (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
+ in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with ProofEngineTypes.Fail _ -> None)
+ equations
+ in
+ let bag = Equality.mk_equality_bag () in
+
+ let bag, units, _, newmeta =
+ partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
+ in
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ Indexing.empty units
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ Indexing.demod bag
+ ([],context,CicUniv.oblivion_ugraph) table initgoal in
+ if changed then
+ begin
+ let oldproof = Equality.Exact bo in
+ let proofterm,_ =
+ Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
+ eq_uri newproof oldproof ty [] context newmetasenv
+ in
+ if newmetasenv <> [] then
+ raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
+ else
+ begin
+ assert_proof_is_valid proofterm newmetasenv context newty;
+ match is_subsumed universe context newty with
+ | Some t -> raise
+ (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
+ | None -> close_type proofterm newty context
+ end
+ end
+ else (* if newty = ty then *)
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ (*else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
+;;
+
+
+(* NEW DEMODULATE *)
+let demodulate ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library:false ~use_context:true
+ automation_cache univ (proof,goal)
+ in
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
+ let active, passive, bag = tables in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let initgoal = [], metasenv, ty in
+ let equalities = (Saturation.list_of_passive passive) in
+ (* we demodulate using both actives passives *)
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
+ equalities;
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ (snd active) equalities
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ (* Indexing.demodulation_goal bag *)
+ Indexing.demod bag
+ (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
+ in
+ if changed then
+ begin
+ let maxm = CicMkImplicit.new_meta metasenv subst in
+ let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
+ let subst_candidates = List.map (fun (i,_,_) -> i) metasenv in
+ let subst_candidates = List.filter (fun x-> x <> goal) subst_candidates in
+ let proofterm, proto_subst =
+ Equality.build_goal_proof (~contextualize:false) bag
+ eq_uri newproof opengoal ty subst_candidates context metasenv
+ in
+ (* XXX understan what to do with proto subst *)
+ let metasenv = (maxm,context,newty)::metasenv in
+ let proofterm, _, metasenv, subst, _ =
+ CicRefine.type_of metasenv subst context proofterm
+ CicUniv.oblivion_ugraph
+ in
+ let extended_status = (curi,metasenv,subst,pbo,pty, attrs),goal in
+ let proof,gl =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) extended_status
+ in
+ proof,maxm::gl
+ end
+ else
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+;;
+
+let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ let all = bool flags "all" false in
+ if all then
+ solve_rewrite ~params ~automation_cache status
+ else
+ demodulate ~dbd ~params ~automation_cache status)
+;;
+(***************** applyS *******************)
+
+let apply_smart_aux
+ dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
+ context term' ty termty goal_arity
+=
+ let consthead,newmetasenv,arguments,_ =
+ TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
+ let term'' =
+ match arguments with
+ | [] -> term'
+ | _ -> Cic.Appl (term'::arguments)
+ in
+ let consthead =
+ let rec aux t = function
+ | [] ->
+ let t = CicReduction.normalize ~delta:false context t in
+ (match t, ty with
+ | Cic.Appl (hd1::_), Cic.Appl (hd2::_) when hd1 <> hd2 ->
+ let t = ProofEngineReduction.unfold context t in
+ (match t with
+ | Cic.Appl (hd1'::_) when hd1' = hd2 -> t
+ | _ -> raise (ProofEngineTypes.Fail (lazy "incompatible head")))
+ | _ -> t)
+ | arg :: tl ->
+ match CicReduction.whd context t with
+ | Cic.Prod (_,_,tgt) ->
+ aux (CicSubstitution.subst arg tgt) tl
+ | _ -> assert false
+ in
+ aux termty arguments
+ in
+ let goal_for_paramod =
+ match LibraryObjects.eq_URI () with
+ | Some uri ->
+ Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Implicit (Some `Type); consthead; ty]
+ | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ in
+ try
+ let goal_for_paramod, _, newmetasenv, subst, _ =
+ CicRefine.type_of newmetasenv subst context goal_for_paramod
+ CicUniv.oblivion_ugraph
+ in
+ let newmeta = CicMkImplicit.new_meta newmetasenv subst in
+ let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
+ let proof'' =
+ let uri,_,_,p,ty, attrs = proof in
+ uri,metasenv_for_paramod,subst,p,ty, attrs
+ in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+(*
+ prerr_endline ("------ prima di rewrite su ------ " ^ string_of_int goal);
+ prerr_endline ("menv:\n"^CicMetaSubst.ppmetasenv [] metasenv_for_paramod);
+ prerr_endline ("subst:\n"^CicMetaSubst.ppsubst
+ ~metasenv:(metasenv_for_paramod)
+ subst);
+*)
+
+ let (proof''',goals) =
+ ProofEngineTypes.apply_tactic
+ (EqualityTactics.rewrite_tac ~direction:`RightToLeft
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (Cic.Meta(newmeta,irl)) []) (proof'',goal)
+ in
+ let goal = match goals with [g] -> g | _ -> assert false in
+ let proof'''', _ =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac term'')
+ (proof''',goal)
+ in
+
+
+ let (_,m,_,_,_,_ as p) =
+ let pu,metasenv,subst,proof,px,py = proof'''' in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let proof'''' = pu,metasenv,subst,proof,px,py in
+ let univ, params = params in
+ let use_context = bool params "use_context" true in
+ let universe, (active,passive,bag), cache =
+ init_cache_and_tables ~use_library:false ~use_context
+ automation_cache univ (proof'''',newmeta)
+ in
+ match
+ Saturation.solve_narrowing bag (proof'''',newmeta) active passive
+ 2 (*0 infinity*)
+ with
+ | None, active, passive, bag ->
+ raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
+ | Some(subst',(pu,metasenv,_,proof,px, py),open_goals),active,
+ passive,bag ->
+ assert_subst_are_disjoint subst subst';
+ let subst = subst@subst' in
+ pu,metasenv,subst,proof,px,py
+ in
+
+(*
+ let (_,m,_,_,_,_ as p),_ =
+ solve_rewrite ~params ~automation_cache (proof'''',newmeta)
+ in
+*)
+
+ let open_goals =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m
+ in
+ p, open_goals
+ with
+ CicRefine.RefineFailure msg ->
+ raise (ProofEngineTypes.Fail msg)
+;;
+
+let apply_smart
+ ~dbd ~term ~automation_cache ~params (proof, goal)
+=
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (_,metasenv,subst,_,_, _) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let newmeta = CicMkImplicit.new_meta metasenv subst in
+ let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
+ match term with
+ C.Var (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Var (uri,exp_named_subst')
+ | C.Const (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | _ -> [],newmeta,[],term
+ in
+ let metasenv' = metasenv@newmetasenvfragment in
+ let termty,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv' ~subst context term' CicUniv.oblivion_ugraph
+ in
+ let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity =
+ let rec count_prods context ty =
+ match CicReduction.whd ~subst context ty with
+ | Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+ in
+ count_prods context ty
+ in
+ apply_smart_aux dbd automation_cache params proof goal
+ newmeta' metasenv' subst context term' ty termty goal_arity
+;;
+
+let applyS_tac ~dbd ~term ~params ~automation_cache =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ try
+ apply_smart ~dbd ~term ~params ~automation_cache status
+ with
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (ProofEngineTypes.Fail msg))
+;;
+
+
+(****************** AUTO ********************)
+
+let calculate_timeout flags =
+ if flags.timeout = 0. then
+ (debug_print (lazy "AUTO WITH NO TIMEOUT");
+ {flags with timeout = infinity})
+ else
+ flags
+;;
+let is_equational_case goalty flags =
+ let ensure_equational t =
+ if is_an_equational_goal t then true
+ else false
+ in
+ (flags.use_paramod && is_an_equational_goal goalty) ||
+ (flags.use_only_paramod && ensure_equational goalty)
+;;
+
+type menv = Cic.metasenv
+type subst = Cic.substitution
+type goal = ProofEngineTypes.goal * int * AutoTypes.sort
+let candidate_no = ref 0;;
+type candidate = int * Cic.term Lazy.t
+type cache = AutoCache.cache
+
+type fail =
+ (* the goal (mainly for depth) and key of the goal *)
+ goal * AutoCache.cache_key
+type op =
+ (* goal has to be proved *)
+ | D of goal
+ (* goal has to be cached as a success obtained using candidate as the first
+ * step *)
+ | S of goal * AutoCache.cache_key * candidate * int
+type elem =
+ (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
+ menv * subst * int * op list * op list * fail list
+type status =
+ (* list of computations that may lead to the solution: all op list will
+ * end with the same (S(g,_)) *)
+ elem list
+type auto_result =
+ (* menv, subst, alternatives, tables, cache *)
+ | Proved of menv * subst * elem list * AutomationCache.tables * cache
+ | Gaveup of AutomationCache.tables * cache
+
+
+(* the status exported to the external observer *)
+type auto_status =
+ (* context, (goal,candidate) list, and_list, history *)
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
+ (int * Cic.term * int) list * Cic.term Lazy.t list
+
+let d_prefix l =
+ let rec aux acc = function
+ | (D g)::tl -> aux (acc@[g]) tl
+ | _ -> acc
+ in
+ aux [] l
+;;
+let prop_only l =
+ List.filter (function (_,_,P) -> true | _ -> false) l
+;;
+
+let d_goals l =
+ let rec aux acc = function
+ | (D g)::tl -> aux (acc@[g]) tl
+ | (S _)::tl -> aux acc tl
+ | [] -> acc
+ in
+ aux [] l
+;;
+
+let calculate_goal_ty (goalno,_,_) s m =
+ try
+ let _,cc,goalty = CicUtil.lookup_meta goalno m in
+ (* XXX applicare la subst al contesto? *)
+ Some (cc, CicMetaSubst.apply_subst s goalty)
+ with CicUtil.Meta_not_found i when i = goalno -> None
+;;
+
+let calculate_closed_goal_ty (goalno,_,_) s =
+ try
+ let cc,_,goalty = List.assoc goalno s in
+ (* XXX applicare la subst al contesto? *)
+ Some (cc, CicMetaSubst.apply_subst s goalty)
+ with Not_found ->
+ None
+;;
+
+let pp_status ctx status =
+ if debug then
+ let names = Utils.names_of_context ctx in
+ let pp x =
+ let x =
+ ProofEngineReduction.replace
+ ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
+ ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
+ in
+ CicPp.pp x names
+ in
+ let string_of_do m s (gi,_,_ as g) d =
+ match calculate_goal_ty g s m with
+ | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
+ | None -> Printf.sprintf "D(%d, _, %d)" gi d
+ in
+ let string_of_s m su k (ci,ct) gi =
+ Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
+ in
+ let string_of_ol m su l =
+ String.concat " | "