From: Claudio Sacerdoti Coen Date: Mon, 6 Apr 2009 20:40:43 +0000 (+0000) Subject: New tactic clear; new syntax # _; to introduce and immediately clear an X-Git-Tag: make_still_working~4111 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c950d8cfe400f6b68eee7a67c555549db3a4d36;p=helm.git New tactic clear; new syntax # _; to introduce and immediately clear an hypothesis. --- diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 660edb2f5..8121968e9 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,5 +1,10 @@ v8Parser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: v8Parser.cmo: types.cmo options.cmo v8Parser.cmi v8Parser.cmx: types.cmx options.cmx v8Parser.cmi v8Lexer.cmo: v8Parser.cmi options.cmo diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b20ca85ba..8f37c918e 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -189,6 +189,7 @@ EXTEND | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> GrafiteAst.NElim (loc, what, where) | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n) + | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_") | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_") | SYMBOL "*"; n=IDENT -> GrafiteAst.NCase1 (loc,n) diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 5d08f2d21..bb269130e 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index f79b45841..8c5dcae76 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -27,7 +27,7 @@ let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -(* let pp _ = ();; *) +let pp _ = ();; let wrap_exc msg = function | NCicUnification.Uncertain _ -> Uncertain msg diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 22f896f21..3000b7311 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -86,7 +86,7 @@ let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -(* let pp _ = ();; *) +let pp _ = ();; let fix_sorts swap metasenv subst context meta t = let rec aux () = function diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 52a82af69..250d50ce3 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -305,10 +305,33 @@ let elim_tac ~what ~where status = status ;; +let find_in_context name context = + let rec aux acc = function + | [] -> raise Not_found + | (hd,_) :: tl when hd = name -> acc + | _ :: tl -> aux (acc + 1) tl + in + aux 1 context +;; + +let clear name status goal = + let goalty = get_goalty status goal in + let j = + try find_in_context name (ctx_of goalty) + with Not_found -> fail (lazy ("hypothesis '" ^ name ^ "' not found")) in + let n,h,metasenv,subst,o = status.pstatus in + let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal [j] in + { status with pstatus = n,h,metasenv,subst,o } +;; + +let clear_tac name = distribute_tac (clear name);; + let intro_tac name = - exact_tac - ("",0,(CicNotationPt.Binder (`Lambda, - (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit))) + block_tac + [ exact_tac + ("",0,(CicNotationPt.Binder (`Lambda, + (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit))); + if name = "_" then clear_tac name else fun x -> x ] ;; let cases ~what status goal =