(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* " let pr_orient _prc _prlc _prt = function | true -> Pp.mt () | false -> Pp.str " <-" ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "->" ] -> [ true ] | [ "<-" ] -> [ false ] | [ ] -> [ true ] END let pr_orient = pr_orient () () () let pr_int_list = Util.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 int_list_of_VList = function | VList l -> List.map (fun n -> coerce_to_int n) l | _ -> raise Not_found 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) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = Tacmach.project gl , interp_occs ist gl l 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 INTERPRETED BY interp_occs GLOBALIZED BY glob_occs SUBSTITUTED BY subst_occs RAW_TYPED AS occurrences_or_var RAW_PRINTED BY pr_occurrences GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences | [ ne_integer_list(l) ] -> [ ArgArg l ] | [ var(id) ] -> [ ArgVar id ] END let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c 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 subst_glob = Tacinterp.subst_glob_constr_and_expr ARGUMENT EXTEND glob 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 let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () | HypLocation (id,InHyp) -> str "in " ++ pr_id id | HypLocation (id,InHypTypeOnly) -> str "in (Type of " ++ pr_id id ++ str ")" | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id) let pr_place _ _ _ = pr_gen_place Nameops.pr_id let pr_hloc = pr_loc_place () () () let intern_place ist = function ConclLocation () -> ConclLocation () | HypLocation (id,hl) -> HypLocation (intern_hyp ist id,hl) let interp_place ist gl = function ConclLocation () -> ConclLocation () | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl) let interp_place ist gl p = Tacmach.project gl , interp_place ist gl p let subst_place subst pl = pl ARGUMENT EXTEND hloc PRINTED BY pr_place INTERPRETED BY interp_place GLOBALIZED BY intern_place SUBSTITUTED BY subst_place RAW_TYPED AS loc_place RAW_PRINTED BY pr_loc_place GLOB_TYPED AS loc_place GLOB_PRINTED BY pr_loc_place [ ] -> [ ConclLocation () ] | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> [ HypLocation ((Util.dummy_loc,id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ] 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 -> 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_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 = str "nat " ++ match natf with | Retroknowledge.NatType -> str "type" | Retroknowledge.NatPlus -> str "plus" | Retroknowledge.NatTimes -> str "times" let pr_r_n_field _ _ _ nf = str "binary N " ++ match nf with | Retroknowledge.NPositive -> str "positive" | Retroknowledge.NType -> str "type" | Retroknowledge.NTwice -> str "twice" | Retroknowledge.NTwicePlusOne -> str "twice plus one" | Retroknowledge.NPhi -> str "phi" | Retroknowledge.NPhiInv -> str "phi inv" | Retroknowledge.NPlus -> str "plus" | Retroknowledge.NTimes -> str "times" let pr_r_int31_field _ _ _ i31f = str "int31 " ++ match i31f with | Retroknowledge.Int31Bits -> str "bits" | Retroknowledge.Int31Type -> str "type" | Retroknowledge.Int31Twice -> str "twice" | Retroknowledge.Int31TwicePlusOne -> str "twice plus one" | Retroknowledge.Int31Phi -> str "phi" | Retroknowledge.Int31PhiInv -> str "phi inv" | Retroknowledge.Int31Plus -> str "plus" | Retroknowledge.Int31Times -> str "times" | _ -> assert false 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) ++ str "in " ++ str group ARGUMENT EXTEND retroknowledge_nat TYPED AS r_nat_field PRINTED BY pr_r_nat_field | [ "nat" "type" ] -> [ Retroknowledge.NatType ] | [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ] | [ "nat" "times" ] -> [ Retroknowledge.NatTimes ] END ARGUMENT EXTEND retroknowledge_binary_n TYPED AS r_n_field PRINTED BY pr_r_n_field | [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ] | [ "binary" "N" "type" ] -> [ Retroknowledge.NType ] | [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ] | [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ] | [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ] | [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ] | [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ] | [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ] END ARGUMENT EXTEND retroknowledge_int31 TYPED AS r_int31_field PRINTED BY pr_r_int31_field | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] | [ "int31" "type" ] -> [ Retroknowledge.Int31Type ] | [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ] | [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ] | [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ] | [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ] | [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ] | [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ] | [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ] | [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ] | [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ] | [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ] | [ "int31" "times" ] -> [ Retroknowledge.Int31Times ] | [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] | [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] | [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] | [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] | [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] END ARGUMENT EXTEND retroknowledge_field TYPED AS r_field PRINTED BY pr_retroknowledge_field (*| [ "equality" ] -> [ Retroknowledge.KEq ] | [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] | [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) | [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] END