From 306463170dc9b3e93959de32044c8b280b83f821 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jun 2005 15:00:38 +0000 Subject: [PATCH] support for goal patterns --- helm/matita/matitaEngine.ml | 100 +++++++++--------------------------- 1 file changed, 24 insertions(+), 76 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 14eab882c..a9c85e7d8 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -65,65 +65,17 @@ let tactic_of_ast = function *) | TacticAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) - | TacticAst.ReduceAt (_,reduction_kind,ident,path) -> - ProofEngineTypes.mk_tactic - (fun (((_,metasenv,_,_),goal) as status) -> - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let where, also_in_hypotheses = - if ident = "goal" then - ty, false - else - let hyp = - try - List.find (function - | Some (Cic.Name name,entry) when name = ident -> true - | _ -> false) - context - with - Not_found -> - raise (ProofEngineTypes.Fail - (ident ^ " is not an hypothesis")) - in - (match hyp with - | Some (_, Cic.Decl term) -> term - | Some (_, Cic.Def (term,ty)) -> term - | None -> assert false),true - in - let pointers = CicUtil.select ~term:where ~context:path in - (match reduction_kind with - | `Normalize -> - ProofEngineTypes.apply_tactic - (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers)) - status - | `Reduce -> - ProofEngineTypes.apply_tactic - (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers)) - status - | `Simpl -> - ProofEngineTypes.apply_tactic - (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers)) - status - | `Whd -> - ProofEngineTypes.apply_tactic - (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers)) - status)) - | TacticAst.Reduce (_,reduction_kind,opts) -> - let terms, also_in_hypotheses = - match opts with - | Some (l,`Goal) -> Some l, false - | Some (l,`Everywhere) -> Some l, true - | None -> None, false - in + | TacticAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with - | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms - | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms - | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms - | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) - | TacticAst.Rewrite (_,dir,t,ident) -> + | `Normalize -> Tactics.normalize ~pattern + | `Reduce -> Tactics.reduce ~pattern + | `Simpl -> Tactics.simpl ~pattern + | `Whd -> Tactics.whd ~pattern) + | TacticAst.Rewrite (_, dir, t, pattern) -> if dir = `Left then - EqualityTactics.rewrite_tac ~term:t + EqualityTactics.rewrite_tac ~where:pattern ~term:t () else - EqualityTactics.rewrite_back_tac ~term:t + EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () | TacticAst.FwdSimpl (_, name) -> Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ()) | TacticAst.LApply (_, term, substs) -> @@ -413,6 +365,15 @@ let disambiguate_obj status obj = in status, cic +let disambiguate_pattern aliases (hyp_paths ,goal_path) = + let interp path = Disambiguate.interpretate_path [] aliases path in + let goal_path = + match goal_path with + | None -> None + | Some path -> Some (interp path) in + let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in + (hyp_paths ,goal_path) + let disambiguate_tactic status = function | TacticAst.Transitivity (loc, term) -> let status, cic = disambiguate_term status term in @@ -457,29 +418,16 @@ let disambiguate_tactic status = function | TacticAst.Injection of 'ident | TacticAst.Replace_pattern of 'term pattern * 'term *) - | TacticAst.LetIn (loc,term,name) -> + | TacticAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in status, TacticAst.LetIn (loc,term,name) - | TacticAst.ReduceAt (loc, reduction_kind, ident, path) -> - let path = Disambiguate.interpretate_path [] status.aliases path in - status, TacticAst.ReduceAt(loc, reduction_kind, ident, path) - | TacticAst.Reduce (loc, reduction_kind, opts) -> - let status, opts = - match opts with - | None -> status, None - | Some (l,pat) -> - let status, l = - List.fold_right (fun t (status,acc) -> - let status',t' = disambiguate_term status t in - status', t'::acc) - l (status,[]) - in - status, Some (l, pat) - in - status, TacticAst.Reduce (loc, reduction_kind, opts) - | TacticAst.Rewrite (loc,dir,t,ident) -> + | TacticAst.Reduce (loc, reduction_kind, pattern) -> + let pattern = disambiguate_pattern status.aliases pattern in + status, TacticAst.Reduce(loc, reduction_kind, pattern) + | TacticAst.Rewrite (loc, dir, t, pattern) -> let status, term = disambiguate_term status t in - status, TacticAst.Rewrite (loc,dir,term,ident) + let pattern = disambiguate_pattern status.aliases pattern in + status, TacticAst.Rewrite (loc, dir, term, pattern) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) -- 2.39.2