-let eq_of_goal = function
- | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
- uri
- | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
-;;
-
-(* performs steps of rewrite with the universe, obtaining if possible
- * a trivial goal *)
-let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)=
- let _,metasenv,_subst,_,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let steps = int_of_string (string params "steps" "1") in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
- let eq_uri = eq_of_goal ty in
- let (active,passive,bag), cache, maxm =
- (* we take the whole universe (no signature filtering) *)
- init_cache_and_tables false true false true universe (proof,goal)
- in
- let initgoal = [], metasenv, ty in
- let table =
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
- in
- let env = metasenv,context,CicUniv.oblivion_ugraph in
- match Indexing.solve_demodulating bag env table initgoal steps with
- | Some (proof, metasenv, newty) ->
- let refl =
- match newty with
- | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
- Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
- | _ -> assert false
- in
- let proofterm,_ =
- Equality.build_goal_proof
- bag eq_uri proof refl newty [] context metasenv
- in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm) status
- | None ->
- raise
- (ProofEngineTypes.Fail (lazy
- ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
-;;
-let solve_rewrite_tac ~params ~automation_cache () =
- ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params)
-;;
-
-(* Demodulate thorem *)
-let open_type ty bo =
- let rec open_type_aux context ty k args =
- match ty with
- | Cic.Prod (n,s,t) ->
- let n' =
- FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
- let entry = match n' with
- | Cic.Name _ -> Some (n',(Cic.Decl s))
- | Cic.Anonymous -> None
- in
- open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
- | Cic.LetIn (n,s,sty,t) ->
- let entry = Some (n,(Cic.Def (s,sty)))
- in
- open_type_aux (entry::context) t (k+1) args
- | _ -> context, ty, args
- in
- let context, ty, args = open_type_aux [] ty 1 [] in
- match args with
- | [] -> context, ty, bo
- | _ -> context, ty, Cic.Appl (bo::args)
-;;
-
-let rec close_type bo ty context =
- match context with
- | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
- | Some (n,(Cic.Decl s))::tl ->
- close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
- | Some (n,(Cic.Def (s,sty)))::tl ->
- close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
- | _ -> assert false
-;;
-
-let is_subsumed univ context ty =
- let candidates = Universe.get_candidates univ ty in
- List.fold_left
- (fun res cand ->
- match res with
- | Some found -> Some found
- | None ->
- try
- let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
- let metasenv = [(0,context,ty)] in
- let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
- let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
- (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
- in
- let prop_goals, other = split_goals_in_prop metasenv subst open_goals in
- if prop_goals = [] then Some cand else None
- with
- | ProofEngineTypes.Fail s -> None
- | CicUnification.Uncertain s -> None
- ) None candidates
-;;
-
-let demodulate_theorem ~automation_cache uri =
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- 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 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_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], metasenv, ty in
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- (* let eq_uri = eq_of_goal ty in *)
- let (active,passive,bag), cache, maxm =
- init_cache_and_tables
- ~dbd false false true true universe (proof,goal)
- 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 opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
- let proofterm,_ =
- Equality.build_goal_proof (~contextualize:false) bag
- eq_uri newproof opengoal ty [] context metasenv
- in
- let extended_metasenv = (maxm,context,newty)::metasenv in
- let extended_status =
- (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
- let (status,newgoals) =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- extended_status in
- (status,maxm::newgoals)
- 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*)
-;;
-
-let demodulate_tac ~dbd ~params ~automation_cache =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);;
-