+let debug_print s = () (* prerr_endline s;; *)
+
+let given_clause dbd ?tables maxm ?auto cache subst flags status =
+ prerr_endline ("given_clause " ^ string_of_int maxm);
+ let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout =
+ match tables with
+ | None ->
+ let bag, equalities, cache, maxmeta =
+ Saturation.find_equalities dbd status ?auto true cache
+ in
+ let passive = Saturation.make_passive equalities in
+ let active = Saturation.make_active [] in
+ let goal_steps, saturation_steps, timeout =
+ if flags.use_only_paramod then max_int,max_int,flags.timeout
+ else 82, 82, infinity
+ in
+ let maxm = max maxm maxmeta in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ | Some (active,passive,bag,oldcache) ->
+ let bag, equalities, cache, maxm =
+ if cache_size oldcache <> cache_size cache then
+ Saturation.saturate_more bag active maxm status true ?auto cache
+ else
+ bag, [], cache, maxm
+ in
+ let minsteps = List.length equalities in
+ let passive = Saturation.add_to_passive equalities passive in
+ let goal_steps, saturation_steps, timeout =
+ if flags.use_only_paramod then max_int,max_int,flags.timeout
+ else max 30 minsteps, minsteps, infinity
+ in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ in
+ let res,a,p, maxmeta =
+ Saturation.given_clause bag maxmeta status active passive
+ goal_steps saturation_steps timeout
+ in
+ res,a,p,bag,cache,maxmeta
+;;
+
+(* {{{ **************** applyS *******************)
+
+let new_metasenv_and_unify_and_t
+ dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
+=
+ let (consthead,newmetasenv,arguments,_) =
+ ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ let term'' =
+ match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
+ in
+ let proof',oldmetasenv =
+ let (puri,metasenv,pbo,pty) = proof in
+ (puri,newmetasenv,pbo,pty),metasenv
+ in
+ let goal_for_paramod =
+ match LibraryObjects.eq_URI () with
+ | Some uri ->
+ Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
+ | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ 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 = proof' in uri,metasenv_for_paramod,p,ty in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ 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 subst, (proof'''', _), _ =
+ PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
+ in
+ match
+ let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
+ let flags =
+ {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
+ in
+ given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta)
+ with
+ | None, active, passive, bag,_,_ ->
+ raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
+ | Some (_,proof''''',_), active, passive,bag,_,_ ->
+ subst,proof''''',
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
+;;
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+
+let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (_,metasenv,_,_) = 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' context term' CicUniv.empty_ugraph
+ in
+ let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity = count_prods context ty in
+ let subst, proof, gl, active, passive =
+ new_metasenv_and_unify_and_t dbd proof goal ?tables
+ newmeta' metasenv' context term' ty termty goal_arity
+ in
+ subst, proof, gl, active, passive
+;;
+
+(* }}} **************** applyS **************)
+
+(* {{{ ***************** AUTO ********************)