diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 202 |
1 files changed, 60 insertions, 142 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 88271fd6..47987e9e 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -1,20 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp -open Pcoq open Genarg open Names open Tacexpr +open Taccoerce open Tacinterp -open Termops +open Misctypes +open Locus (* Rewriting orientation *) @@ -34,29 +35,35 @@ END let pr_orient = pr_orient () () () -let pr_int_list = Util.pr_sequence Pp.int +let pr_int_list = Pp.pr_sequence Pp.int let pr_int_list_full _prc _prlc _prt l = pr_int_list l -open Glob_term - let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x | ArgVar (loc, id) -> Nameops.pr_id id -let coerce_to_int = function - | VInteger n -> n - | v -> raise (CannotCoerceTo "an integer") +let occurrences_of = function + | [] -> NoOccurrences + | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + Errors.error "Illegal negative occurrence number."; + OnlyOccurrences nl + +let coerce_to_int v = match Value.to_int v with + | None -> raise (CannotCoerceTo "an integer") + | Some n -> n -let int_list_of_VList = function - | VList l -> List.map (fun n -> coerce_to_int n) l - | _ -> raise Not_found +let int_list_of_VList v = match Value.to_list v with +| Some l -> List.map (fun n -> coerce_to_int n) l +| _ -> raise (CannotCoerceTo "an integer") let interp_occs ist gl l = match l with | ArgArg x -> x | ArgVar (_,id as locid) -> - (try int_list_of_VList (List.assoc id ist.lfun) + (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = Tacmach.project gl , interp_occs ist gl l @@ -65,9 +72,6 @@ let glob_occs ist l = l let subst_occs evm l = l -type occurrences_or_var = int list or_var -type occurrences = int list - ARGUMENT EXTEND occurrences PRINTED BY pr_int_list_full @@ -93,9 +97,9 @@ let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) -let glob_glob = Tacinterp.intern_constr +let glob_glob = Tacintern.intern_constr -let subst_glob = Tacinterp.subst_glob_constr_and_expr +let subst_glob = Tacsubst.subst_glob_constr_and_expr ARGUMENT EXTEND glob PRINTED BY pr_globc @@ -109,14 +113,28 @@ ARGUMENT EXTEND glob GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen - [ lconstr(c) ] -> [ c ] + [ constr(c) ] -> [ c ] END +ARGUMENT EXTEND lglob + PRINTED BY pr_globc + + INTERPRETED BY interp_glob + GLOBALIZED BY glob_glob + SUBSTITUTED BY subst_glob + + RAW_TYPED AS constr_expr + RAW_PRINTED BY pr_gen + + GLOB_TYPED AS glob_constr_and_expr + GLOB_PRINTED BY pr_gen + [ lconstr(c) ] -> [ c ] +END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = identifier Util.located gen_place -type place = identifier gen_place +type loc_place = Id.t Loc.located gen_place +type place = Id.t gen_place let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () @@ -132,14 +150,14 @@ let pr_hloc = pr_loc_place () () () let intern_place ist = function ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (intern_hyp ist id,hl) + | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) -let interp_place ist gl = function +let interp_place ist env sigma = function ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl) + | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) let interp_place ist gl p = - Tacmach.project gl , interp_place ist gl p + Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p let subst_place subst pl = pl @@ -157,11 +175,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Util.dummy_loc,id),InHyp) ] + [ HypLocation ((Loc.ghost,id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ] + [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ] + [ HypLocation ((Loc.ghost,id),InHypValueOnly) ] END @@ -187,115 +205,16 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c -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 Util.pr_comma 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 - 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 - 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 - 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 pr_in_arg_hyp = pr_in_arg_hyp_typed () () () - -let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = - {Tacexpr.onhyps= - Option.map - (fun l -> - List.map - (fun id -> ( (all_occurrences_expr,trad_id id),InHyp)) - l - ) - hyps; - Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr} - - -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) - - -(* spiwack argument for the commands of the retroknowledge *) - -let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) = - Genarg.create_arg None "r_nat_field" -let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) = - Genarg.create_arg None "r_n_field" -let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) = - Genarg.create_arg None "r_int31_field" -let (wit_r_field, globwit_r_field, rawwit_r_field) = - Genarg.create_arg None "r_field" - (* spiwack: the print functions are incomplete, but I don't know what they are used for *) -let pr_r_nat_field _ _ _ natf = +let pr_r_nat_field natf = str "nat " ++ match natf with | Retroknowledge.NatType -> str "type" | Retroknowledge.NatPlus -> str "plus" | Retroknowledge.NatTimes -> str "times" -let pr_r_n_field _ _ _ nf = +let pr_r_n_field nf = str "binary N " ++ match nf with | Retroknowledge.NPositive -> str "positive" @@ -307,7 +226,7 @@ let pr_r_n_field _ _ _ nf = | Retroknowledge.NPlus -> str "plus" | Retroknowledge.NTimes -> str "times" -let pr_r_int31_field _ _ _ i31f = +let pr_r_int31_field i31f = str "int31 " ++ match i31f with | Retroknowledge.Int31Bits -> str "bits" @@ -320,16 +239,15 @@ let pr_r_int31_field _ _ _ i31f = | Retroknowledge.Int31Times -> str "times" | _ -> assert false -let pr_retroknowledge_field _ _ _ f = +let pr_retroknowledge_field f = match f with (* | Retroknowledge.KEq -> str "equality" | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) - | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field () () () i31f) ++ + | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ str "in " ++ str group -ARGUMENT EXTEND retroknowledge_nat -TYPED AS r_nat_field +VERNAC ARGUMENT EXTEND retroknowledge_nat PRINTED BY pr_r_nat_field | [ "nat" "type" ] -> [ Retroknowledge.NatType ] | [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ] @@ -337,8 +255,7 @@ PRINTED BY pr_r_nat_field END -ARGUMENT EXTEND retroknowledge_binary_n -TYPED AS r_n_field +VERNAC ARGUMENT EXTEND retroknowledge_binary_n PRINTED BY pr_r_n_field | [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ] | [ "binary" "N" "type" ] -> [ Retroknowledge.NType ] @@ -350,8 +267,7 @@ PRINTED BY pr_r_n_field | [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ] END -ARGUMENT EXTEND retroknowledge_int31 -TYPED AS r_int31_field +VERNAC ARGUMENT EXTEND retroknowledge_int31 PRINTED BY pr_r_int31_field | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] | [ "int31" "type" ] -> [ Retroknowledge.Int31Type ] @@ -369,15 +285,17 @@ PRINTED BY pr_r_int31_field | [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] | [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] | [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] +| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ] | [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] | [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] - +| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ] +| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ] +| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ] END -ARGUMENT EXTEND retroknowledge_field -TYPED AS r_field +VERNAC ARGUMENT EXTEND retroknowledge_field PRINTED BY pr_retroknowledge_field (*| [ "equality" ] -> [ Retroknowledge.KEq ] | [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] |