diff options
Diffstat (limited to 'tactics/extraargs.ml4')
-rw-r--r-- | tactics/extraargs.ml4 | 114 |
1 files changed, 113 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 5a0b4b8c..3c7d76b2 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extraargs.ml4 8739 2006-04-26 22:23:37Z herbelin $ *) +(* $Id: extraargs.ml4 9076 2006-08-23 15:05:54Z jforest $ *) open Pp open Pcoq @@ -124,3 +124,115 @@ ARGUMENT EXTEND hloc END + + + + + + +(* Julien: Mise en commun des differentes version de replace with in by *) + +let pr_by_arg_tac _prc _prlc prtac opt_c = + match opt_c with + | None -> mt () + | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) + +ARGUMENT EXTEND by_arg_tac + TYPED AS tactic_opt + PRINTED BY pr_by_arg_tac +| [ "by" tactic3(c) ] -> [ Some c ] +| [ ] -> [ None ] +END + + +let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = + match lo,concl with + | Some [],true -> mt () + | None,true -> str "in" ++ spc () ++ str "*" + | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" + | Some l,_ -> + str "in" ++ spc () ++ + Util.prlist_with_sep spc pr_id l ++ + match concl with + | true -> spc () ++ str "|-" ++ spc () ++ str "*" + | _ -> mt () + + +let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id) + +let pr_in_arg_hyp_typed _ _ _ = pr_in_hyp Ppconstr.pr_id + + +let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id + +let pr_var_list_typed _ _ _ = pr_var_list_gen Ppconstr.pr_id + +let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id) + + +ARGUMENT EXTEND comma_var_lne + TYPED AS var list + PRINTED BY pr_var_list_typed + RAW_TYPED AS var list + RAW_PRINTED BY pr_var_list + GLOB_TYPED AS var list + GLOB_PRINTED BY pr_var_list +| [ var(x) ] -> [ [x] ] +| [ var(x) "," comma_var_lne(l) ] -> [x::l] +END + +ARGUMENT EXTEND comma_var_l + TYPED AS var list + PRINTED BY pr_var_list_typed + RAW_TYPED AS var list + RAW_PRINTED BY pr_var_list + GLOB_TYPED AS var list + GLOB_PRINTED BY pr_var_list +| [ comma_var_lne(l) ] -> [l] +| [] -> [ [] ] +END + +let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-" + +ARGUMENT EXTEND inconcl + TYPED AS bool + PRINTED BY pr_in_concl +| [ "|-" "*" ] -> [ true ] +| [ "|-" ] -> [ false ] +END + + + +ARGUMENT EXTEND in_arg_hyp + TYPED AS var list option * bool + PRINTED BY pr_in_arg_hyp_typed + RAW_TYPED AS var list option * bool + RAW_PRINTED BY pr_in_arg_hyp + GLOB_TYPED AS var list option * bool + GLOB_PRINTED BY pr_in_arg_hyp +| [ "in" "*" ] -> [(None,true)] +| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)] +| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in + Some l, onconcl + ] +| [ ] -> [ (Some [],true) ] +END + + +let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = + {Tacexpr.onhyps= + Util.option_map + (fun l -> + List.map + (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) + l + ) + hyps; + Tacexpr.onconcl=concl; + Tacexpr.concl_occs = []} + + +let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd +let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) + + |