From: Ferruccio Guidi Date: Thu, 31 Aug 2006 08:56:16 +0000 (+0000) Subject: fixing the semantics of subst X-Git-Tag: make_still_working~6958 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=14dc1c8085e0aa49a606f78655f693184827f72b;p=helm.git fixing the semantics of subst --- diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index fd6e7c59f..8760f36ef 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -191,7 +191,9 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit in (proof',goals) with (* FG: this should be PET.Fail _ *) - TC.TypeCheckerFailure _ -> PET.apply_tactic P.letout_tac status + TC.TypeCheckerFailure _ -> + let msg = lazy "rewrite: nothing to rewrite" in + raise (PET.Fail msg) in ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality) @@ -364,16 +366,20 @@ let transitivity_tac ~term = (* FG: subst tactic *********************************************************) +(* FG: This should be replaced by T.try_tactic *) +let try_tactic ~tactic = + let try_tactic status = + try PET.apply_tactic tactic status with + | PET.Fail _ -> PET.apply_tactic T.id_tac status + in + PET.mk_tactic try_tactic + let msg0 = lazy "Subst: not found in context" let msg1 = lazy "Subst: not a simple equality" let msg2 = lazy "Subst: recursive equation" let subst_tac ~hyp = let hole = C.Implicit (Some `Hole) in - let map self = function - | Some (C.Name s, _) when s <> self -> Some (s, hole) - | _ -> None - in let subst_tac status = let (proof, goal) = status in let (_, metasenv, _, _) = proof in @@ -390,27 +396,27 @@ let subst_tac ~hyp = when LO.is_eq_URI uri -> `RightToLeft, i, t | _ -> raise (PET.Fail msg1) in + let rewrite pattern = + try_tactic ~tactic:(rewrite_tac ~direction ~pattern what) + in let var = match PEH.get_name context i with | Some name -> name | None -> raise (PET.Fail msg0) in if DTI.does_not_occur i t then () else raise (PET.Fail msg2); - let pattern = None, PEH.list_rev_map_filter (map hyp) context, Some hole in - let start = rewrite_tac ~direction ~pattern what in - let continuation = PESR.clear ~hyps:[hyp; var] in - let tac = T.then_ ~start ~continuation in - PET.apply_tactic tac status + let map self = function + | Some (C.Name s, _) when s <> self -> + Some (rewrite (None, [(s, hole)], None)) + | _ -> None + in + let rew_hips = PEH.list_rev_map_filter (map hyp) context in + let rew_concl = rewrite (None, [], Some hole) in + let clear = PESR.clear ~hyps:[hyp; var] in + let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in + PET.apply_tactic (T.seq ~tactics) status in PET.mk_tactic subst_tac -(* FG: This should be replaced by T.try_tactic *) -let try_tactic ~tactic = - let try_tactic status = - try PET.apply_tactic tactic status with - | PET.Fail _ -> PET.apply_tactic T.id_tac status - in - PET.mk_tactic try_tactic - let subst_tac = let subst hyp = try_tactic ~tactic:(subst_tac hyp) in let map = function