diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 17:19:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 17:19:41 +0000 |
| commit | 928287134ab9dd23258c395589f8633e422e939f (patch) | |
| tree | 192971793635b1057b78004b14df4ad5dfac9561 | |
| parent | c4ef643444acecdb4c08a74f37b9006ae060c5af (diff) | |
Globalisation des noms de tactiques dans les définitions de tactiques
pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
55 files changed, 1850 insertions, 1412 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b47632015..641ccf7fc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -90,6 +90,10 @@ let explain_internalisation_error = function | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po +let error_unbound_metanum loc n = + user_err_loc + (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound") + (**********************************************************************) (* Dump of globalization (to be used by coqdoc) *) @@ -453,8 +457,13 @@ let internalise isarity sigma env allow_soapp lvar c = Array.of_list (List.map (intern false env) cl)) | CHole loc -> RHole (loc, QuestionMark) - | CMeta (loc, n) when n >=0 or allow_soapp -> + | CMeta (loc, n) when allow_soapp = None or !interning_grammar -> RMeta (loc, n) + | CMeta (loc, n) when n >=0 -> + if List.mem n (out_some allow_soapp) then + RMeta (loc, n) + else + error_unbound_metanum loc n | CMeta (loc, _) -> raise (InternalisationError (loc,NegativeMetavariable)) | CSort (loc, s) -> @@ -559,20 +568,20 @@ let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c = allow_soapp (ltacvar,Environ.named_context env, []) c let interp_rawconstr sigma env c = - interp_rawconstr_gen false sigma env [] false ([],[]) c + interp_rawconstr_gen false sigma env [] (Some []) ([],[]) c let interp_rawtype sigma env c = - interp_rawconstr_gen true sigma env [] false ([],[]) c + interp_rawconstr_gen true sigma env [] (Some []) ([],[]) c let interp_rawtype_with_implicits sigma env impls c = - interp_rawconstr_gen true sigma env impls false ([],[]) c + interp_rawconstr_gen true sigma env impls (Some []) ([],[]) c (* (* The same as interp_rawconstr but with a list of variables which must not be globalized *) let interp_rawconstr_wo_glob sigma env lvar c = - interp_rawconstr_gen sigma env [] false lvar c + interp_rawconstr_gen sigma env [] (Some []) lvar c *) (*********************************************************************) @@ -621,7 +630,7 @@ type ltac_env = (* of instantiations (variables and metas) *) (* Note: typ is retyped *) let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp = - let c = interp_rawconstr_gen false sigma env [] false + let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta)) (List.map fst ltacvar,unbndltacvar) c and rtype lst = retype_list sigma env lst in understand_gen sigma env (rtype ltacvar) (rtype lmeta) exptyp c;; @@ -629,7 +638,7 @@ let interp_constr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp = (*Interprets a casted constr according to two lists of instantiations (variables and metas)*) let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp = - let c = interp_rawconstr_gen false sigma env [] false + let c = interp_rawconstr_gen false sigma env [] (Some (List.map fst lmeta)) (List.map fst ltacvar,unbndltacvar) c and rtype lst = retype_list sigma env lst in understand_gen_tcc sigma env (rtype ltacvar) (rtype lmeta) exptyp c;; @@ -637,86 +646,10 @@ let interp_openconstr_gen sigma env (ltacvar,unbndltacvar) lmeta c exptyp = let interp_casted_constr sigma env c typ = understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c) -(* To process patterns, we need a translation without typing at all. *) - -let rec pat_of_raw metas vars lvar = function - | RVar (_,id) -> - (try PRel (list_index (Name id) vars) - with Not_found -> - try List.assoc id lvar - with Not_found -> PVar id) - | RMeta (_,n) -> - metas := n::!metas; PMeta (Some n) - | RRef (_,r) -> - PRef r - (* Hack pour ne pas réécrire une interprétation complète des patterns*) - | RApp (_, RMeta (_,n), cl) when n<0 -> - PSoApp (- n, List.map (pat_of_raw metas vars lvar) cl) - | RApp (_,c,cl) -> - PApp (pat_of_raw metas vars lvar c, - Array.of_list (List.map (pat_of_raw metas vars lvar) cl)) - | RLambda (_,na,c1,c2) -> - PLambda (na, pat_of_raw metas vars lvar c1, - pat_of_raw metas (na::vars) lvar c2) - | RProd (_,na,c1,c2) -> - PProd (na, pat_of_raw metas vars lvar c1, - pat_of_raw metas (na::vars) lvar c2) - | RLetIn (_,na,c1,c2) -> - PLetIn (na, pat_of_raw metas vars lvar c1, - pat_of_raw metas (na::vars) lvar c2) - | RSort (_,s) -> - PSort s - | RHole _ -> - PMeta None - | RCast (_,c,t) -> - if_verbose warning "Cast not taken into account in constr pattern"; - pat_of_raw metas vars lvar c - | ROrderedCase (_,st,po,c,br) -> - PCase (st,option_app (pat_of_raw metas vars lvar) po, - pat_of_raw metas vars lvar c, - Array.map (pat_of_raw metas vars lvar) br) - | RCases (loc,po,[c],br) -> - PCase (Term.RegularStyle,option_app (pat_of_raw metas vars lvar) po, - pat_of_raw metas vars lvar c, - Array.init (List.length br) - (pat_of_raw_branch loc metas vars lvar br)) - | r -> - let loc = loc_of_rawconstr r in - user_err_loc (loc,"pattern_of_rawconstr", str "Not supported pattern") - -and pat_of_raw_branch loc metas vars lvar brs i = - let bri = List.filter - (function - (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1 - | (loc,_,_,_) -> - user_err_loc (loc,"pattern_of_rawconstr", - str "Not supported pattern")) brs in - match bri with - [(_,_,[PatCstr(_,_,lv,_)],br)] -> - let lna = - List.map - (function PatVar(_,na) -> na - | PatCstr(loc,_,_,_) -> - user_err_loc (loc,"pattern_of_rawconstr", - str "Not supported pattern")) lv in - let vars' = List.rev lna @ vars in - List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna - (pat_of_raw metas vars' lvar br) - | _ -> user_err_loc (loc,"pattern_of_rawconstr", - str "No unique branch for " ++ int (i+1) ++ - str"-th constructor") - - -let pattern_of_rawconstr lvar c = - let metas = ref [] in - let p = pat_of_raw metas [] lvar c in - (!metas,p) - let interp_constrpattern_gen sigma env (ltacvar,unbndltacvar) c = - let c = interp_rawconstr_gen false sigma env [] true + let c = interp_rawconstr_gen false sigma env [] None (List.map fst ltacvar,unbndltacvar) c in - let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) ltacvar in - pattern_of_rawconstr nlvar c + pattern_of_rawconstr c let interp_constrpattern sigma env c = interp_constrpattern_gen sigma env ([],[]) c @@ -726,7 +659,7 @@ let interp_aconstr vars a = (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = List.map (fun id -> (id,ref None)) vars in let c = for_grammar (internalise false Evd.empty (extract_ids env, [], []) - false (([],[]),Environ.named_context env,vl)) a in + (Some []) (([],[]),Environ.named_context env,vl)) a in (* Translate and check that [c] has all its free variables bound in [vars] *) let a = aconstr_of_rawconstr vars c in (* Returns [a] and the ordered list of variables with their scopes *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 5d66424c2..99e7d68bb 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -43,7 +43,7 @@ type ltac_env = (* Interprets global names, including syntactic defs and section variables *) val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> - bool -> ltac_sign -> constr_expr -> rawconstr + int list option -> ltac_sign -> constr_expr -> rawconstr (*s Composing the translation with typing *) val interp_constr : evar_map -> env -> constr_expr -> constr diff --git a/interp/genarg.ml b/interp/genarg.ml index b25908b42..0f2e031cc 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -39,6 +39,9 @@ type argument_type = | ExtraArgType of string type 'a or_var = ArgArg of 'a | ArgVar of identifier located +type 'a or_metanum = AN of 'a | MetaNum of int located +type 'a and_short_name = 'a * identifier option +type rawconstr_and_expr = rawconstr * constr_expr option (* Dynamics but tagged by a type expression *) @@ -53,57 +56,72 @@ let create_arg s = anomaly ("Genarg.create: already declared generic argument " ^ s); dyntab := s :: !dyntab; let t = ExtraArgType s in - (t,t) + (t,t,t) let exists_argtype s = List.mem s !dyntab type open_constr = Evd.evar_map * Term.constr -(*type open_rawconstr = Coqast.t*) -type open_rawconstr = constr_expr +type open_constr_expr = constr_expr +type open_rawconstr = rawconstr_and_expr let rawwit_bool = BoolArgType +let globwit_bool = BoolArgType let wit_bool = BoolArgType let rawwit_int = IntArgType +let globwit_int = IntArgType let wit_int = IntArgType let rawwit_int_or_var = IntOrVarArgType +let globwit_int_or_var = IntOrVarArgType let wit_int_or_var = IntOrVarArgType let rawwit_string = StringArgType +let globwit_string = StringArgType let wit_string = StringArgType let rawwit_ident = IdentArgType +let globwit_ident = IdentArgType let wit_ident = IdentArgType let rawwit_pre_ident = PreIdentArgType +let globwit_pre_ident = PreIdentArgType let wit_pre_ident = PreIdentArgType let rawwit_ref = RefArgType +let globwit_ref = RefArgType let wit_ref = RefArgType let rawwit_quant_hyp = QuantHypArgType +let globwit_quant_hyp = QuantHypArgType let wit_quant_hyp = QuantHypArgType let rawwit_sort = SortArgType +let globwit_sort = SortArgType let wit_sort = SortArgType let rawwit_constr = ConstrArgType +let globwit_constr = ConstrArgType let wit_constr = ConstrArgType let rawwit_constr_may_eval = ConstrMayEvalArgType +let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType let rawwit_tactic = TacticArgType +let globwit_tactic = TacticArgType let wit_tactic = TacticArgType let rawwit_casted_open_constr = CastedOpenConstrArgType +let globwit_casted_open_constr = CastedOpenConstrArgType let wit_casted_open_constr = CastedOpenConstrArgType let rawwit_constr_with_bindings = ConstrWithBindingsArgType +let globwit_constr_with_bindings = ConstrWithBindingsArgType let wit_constr_with_bindings = ConstrWithBindingsArgType let rawwit_red_expr = RedExprArgType +let globwit_red_expr = RedExprArgType let wit_red_expr = RedExprArgType let wit_list0 t = List0ArgType t @@ -167,17 +185,6 @@ let app_pair f1 f2 = function (u, Obj.repr (o1,o2)) | _ -> failwith "Genarg: not a pair" -let or_var_app f = function - | ArgArg x -> ArgArg (f x) - | ArgVar _ as x -> x - -let smash_var_app t f g = function - | ArgArg x -> f x - | ArgVar (_,id) -> - let (u, _ as x) = g id in - if t <> u then failwith "Genarg: a variable bound to a wrong type"; - x - let unquote x = x type an_arg_of_this_type = Obj.t diff --git a/interp/genarg.mli b/interp/genarg.mli index f1246b2cc..c938d4c51 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -16,10 +16,17 @@ open Rawterm open Topconstr type 'a or_var = ArgArg of 'a | ArgVar of identifier located +type 'a or_metanum = AN of 'a | MetaNum of int located +type 'a and_short_name = 'a * identifier option -type open_constr = Evd.evar_map * Term.constr -type open_rawconstr = constr_expr +(* In globalize tactics, we need to keep the initial constr_expr to recompute*) +(* in the environment by the effective calls to Intro, Inversion, etc *) +(* The constr_expr field is None in TacDef though *) +type rawconstr_and_expr = rawconstr * constr_expr option +type open_constr = Evd.evar_map * Term.constr +type open_constr_expr = constr_expr +type open_rawconstr = rawconstr_and_expr (* The route of a generic argument, from parsing to evaluation @@ -47,12 +54,12 @@ IntOrVarArgType int or_var int StringArgType string (parsed w/ "") string IdentArgType identifier identifier PreIdentArgType string (parsed w/o "") string -RefArgType reference global_reference -ConstrArgType constr_expr constr -ConstrMayEvalArgType constr_expr may_eval constr +RefArgType reference global_reference +ConstrArgType constr_expr constr +ConstrMayEvalArgType constr_expr may_eval constr QuantHypArgType quantified_hypothesis quantified_hypothesis TacticArgType raw_tactic_expr tactic -CastedOpenConstrArgType constr_expr open_constr +CastedOpenConstrArgType constr_expr open_constr ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings List0ArgType of argument_type List1ArgType of argument_type @@ -63,49 +70,64 @@ ExtraArgType of string '_a '_b type ('a,'co,'ta) abstract_argument_type val rawwit_bool : (bool,'co,'ta) abstract_argument_type +val globwit_bool : (bool,'co,'ta) abstract_argument_type val wit_bool : (bool,'co,'ta) abstract_argument_type val rawwit_int : (int,'co,'ta) abstract_argument_type +val globwit_int : (int,'co,'ta) abstract_argument_type val wit_int : (int,'co,'ta) abstract_argument_type val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type +val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type val rawwit_string : (string,'co,'ta) abstract_argument_type +val globwit_string : (string,'co,'ta) abstract_argument_type val wit_string : (string,'co,'ta) abstract_argument_type val rawwit_ident : (identifier,'co,'ta) abstract_argument_type +val globwit_ident : (identifier,'co,'ta) abstract_argument_type val wit_ident : (identifier,'co,'ta) abstract_argument_type val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type +val globwit_pre_ident : (string,'co,'ta) abstract_argument_type val wit_pre_ident : (string,'co,'ta) abstract_argument_type val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type +val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type val wit_ref : (global_reference,constr,'ta) abstract_argument_type val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type +val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type +val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type val wit_sort : (sorts,constr,'ta) abstract_argument_type val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type +val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr : (constr,constr,'ta) abstract_argument_type -val rawwit_constr_may_eval : (constr_expr may_eval,constr_expr,'ta) abstract_argument_type +val rawwit_constr_may_eval : ((constr_expr,reference or_metanum) may_eval,constr_expr,'ta) abstract_argument_type +val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) may_eval,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type -val rawwit_casted_open_constr : (open_rawconstr,constr_expr,'ta) abstract_argument_type +val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type +val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type +val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_metanum) red_expr_gen,constr_expr,'ta) abstract_argument_type +val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var or_metanum) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type (* TODO: transformer tactic en extra arg *) val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type +val globwit_tactic : ('ta,rawconstr_and_expr,'ta) abstract_argument_type val wit_tactic : ('ta,constr,'ta) abstract_argument_type val wit_list0 : @@ -159,8 +181,9 @@ val app_pair : polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel de create *) val create_arg : string -> - ('rawa,'rawco,'rawta) abstract_argument_type - * ('a,'co,'ta) abstract_argument_type + ('a,'co,'ta) abstract_argument_type + * ('globa,'globco,'globta) abstract_argument_type + * ('rawa,'rawco,'rawta) abstract_argument_type val exists_argtype : string -> bool diff --git a/library/nametab.ml b/library/nametab.ml index 372590911..ba3e7ff9f 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -348,8 +348,12 @@ let full_name_modtype qid = SpTab.user_name qid !the_modtypetab let locate_obj qid = SpTab.user_name qid !the_objtab +type ltac_constant = section_path let locate_tactic = locate_obj +let shortest_qualid_of_tactic sp = + SpTab.shortest_qualid Idset.empty sp !the_objtab + let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = diff --git a/library/nametab.mli b/library/nametab.mli index 9ee45a9ad..df433d145 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -101,7 +101,9 @@ val locate_section : qualid -> dir_path val locate_modtype : qualid -> kernel_name val locate_syntactic_definition : qualid -> kernel_name -val locate_tactic : qualid -> section_path +type ltac_constant = section_path +val locate_tactic : qualid -> ltac_constant +val shortest_qualid_of_tactic : ltac_constant -> qualid val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 4d6edda0e..0f4bc93a8 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -40,6 +40,29 @@ let rec make_rawwit loc = function <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> +let rec make_globwit loc = function + | BoolArgType -> <:expr< Genarg.globwit_bool >> + | IntArgType -> <:expr< Genarg.globwit_int >> + | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >> + | StringArgType -> <:expr< Genarg.globwit_string >> + | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> + | IdentArgType -> <:expr< Genarg.globwit_ident >> + | RefArgType -> <:expr< Genarg.globwit_ref >> + | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> + | SortArgType -> <:expr< Genarg.globwit_sort >> + | ConstrArgType -> <:expr< Genarg.globwit_constr >> + | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> + | TacticArgType -> <:expr< Genarg.globwit_tactic >> + | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> + | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> + | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> + | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> + | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >> + | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >> + | PairArgType (t1,t2) -> + <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >> + | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >> + let rec make_wit loc = function | BoolArgType -> <:expr< Genarg.wit_bool >> | IntArgType -> <:expr< Genarg.wit_int >> @@ -78,33 +101,57 @@ let make_rule loc (prods,act) = let (symbs,pil) = List.split prods in <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >> -let declare_tactic_argument for_v8 loc s typ pr f rawtyppr cl = +let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl = let interp = match f with - | None -> <:expr< Tacinterp.genarg_interp >> + | None -> <:expr< Tacinterp.interp_genarg >> + | Some f -> <:expr< $lid:f$>> in + let glob = match g with + | None -> <:expr< Tacinterp.intern_genarg >> + | Some f -> <:expr< $lid:f$>> in + let substitute = match h with + | None -> <:expr< Tacinterp.subst_genarg >> | Some f -> <:expr< $lid:f$>> in let rawtyp, rawpr = match rawtyppr with | None -> typ,pr | Some (t,p) -> t,p in + let globtyp, globpr = match globtyppr with + | None -> typ,pr + | Some (t,p) -> t,p in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in + let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< declare - value ($lid:"wit_"^s$, $lid:"rawwit_"^s$) = Genarg.create_arg $se$; + value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = + Genarg.create_arg $se$; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; - Tacinterp.add_genarg_interp $se$ + Tacinterp.add_interp_genarg $se$ + ((fun e x -> + (in_gen $globwit$ + (out_gen $make_globwit loc typ$ + ($glob$ e + (in_gen $make_rawwit loc rawtyp$ + (out_gen $rawwit$ x)))))), (fun ist gl x -> (in_gen $wit$ (out_gen $make_wit loc typ$ ($interp$ ist gl - (in_gen $make_rawwit loc rawtyp$ - (out_gen $rawwit$ x)))))); + (in_gen $make_globwit loc rawtyp$ + (out_gen $globwit$ x)))))), + (fun subst x -> + (in_gen $globwit$ + (out_gen $make_globwit loc typ$ + ($substitute$ subst + (in_gen $make_globwit loc rawtyp$ + (out_gen $globwit$ x))))))); Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; Pptactic.declare_extra_genarg_pprule $mlexpr_of_bool for_v8$ ($rawwit$, $lid:rawpr$) + ($globwit$, $lid:globpr$) ($wit$, $lid:pr$); end >> @@ -112,12 +159,11 @@ let declare_tactic_argument for_v8 loc s typ pr f rawtyppr cl = let declare_vernac_argument for_v8 loc s cl = let se = mlexpr_of_string s in let typ = ExtraArgType s in - let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< declare - value $lid:"rawwit_"^s$ = snd (Genarg.create_arg $se$); + value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; @@ -167,14 +213,20 @@ EXTEND "TYPED"; "AS"; typ = argtype; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; rawtyppr = - OPT [ "RAW"; "TYPED"; "AS"; t = argtype; - "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + (* Necessary if the globalized type is different from the final type *) + OPT [ "RAW_TYPED"; "AS"; t = argtype; + "RAW_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + globtyppr = + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_tactic_argument true loc s typ pr f rawtyppr l + declare_tactic_argument true loc s typ pr f g h rawtyppr globtyppr l | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> @@ -185,14 +237,19 @@ EXTEND "TYPED"; "AS"; typ = argtype; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; rawtyppr = - OPT [ "RAW"; "TYPED"; "AS"; t = argtype; - "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + globtyppr = + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_tactic_argument false loc s typ pr f rawtyppr l + declare_tactic_argument false loc s typ pr f g h rawtyppr globtyppr l | "V7"; "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> @@ -201,7 +258,11 @@ EXTEND declare_vernac_argument false loc s l ] ] ; argtype: - [ [ e = LIDENT -> fst (interp_entry_name loc e) ] ] + [ [ e = LIDENT -> fst (interp_entry_name loc e) + | e1 = LIDENT; "*"; e2 = LIDENT -> + let e1 = fst (interp_entry_name loc e1) in + let e2 = fst (interp_entry_name loc e2) in + PairArgType (e1, e2) ] ] ; argrule: [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d05827bfe..f5309fa39 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * constr_expr may_eval option * raw_tactic_arg) + (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -62,7 +62,7 @@ open Prelude let arg_of_expr = function TacArg a -> a - | e -> Tacexp e + | e -> Tacexp (e:raw_tactic_expr) (* Tactics grammar rules *) @@ -230,7 +230,7 @@ GEXTEND Gram | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) | "?" -> ConstrMayEval (ConstrTerm (CHole loc)) - | "?"; n = natural -> MetaNumArg (loc,n) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) | "'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 2caad4680..945009ae9 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * constr_expr may_eval option * raw_tactic_arg) + (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -60,7 +60,7 @@ end let arg_of_expr = function TacArg a -> a - | e -> Tacexp e + | e -> Tacexp (e:raw_tactic_expr) open Prelude @@ -136,7 +136,7 @@ GEXTEND Gram tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) | r = reference -> Reference r - | "?"; n = natural -> MetaNumArg (loc,n) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) | "()" -> TacVoid ] ] ; input_fun: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 787ccd07e..862bbd3dd 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -14,6 +14,7 @@ open Pcoq open Util open Tacexpr open Rawterm +open Genarg (* open grammar entries, possibly in quotified form *) ifdef Quotify then open Qast @@ -83,8 +84,8 @@ GEXTEND Gram ; (* Either an hypothesis or a ltac ref (variable or pattern metavariable) *) id_or_ltac_ref: - [ [ id = base_ident -> AN id - | "?"; n = natural -> MetaNum (loc,n) ] ] + [ [ id = base_ident -> Genarg.AN id + | "?"; n = natural -> Genarg.MetaNum (loc,n) ] ] ; (* Either a global ref or a ltac ref (variable or pattern metavariable) *) global_or_ltac_ref: diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index dade80611..725a3432f 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -14,6 +14,7 @@ open Pcoq open Util open Tacexpr open Rawterm +open Genarg let tactic_kw = [ "->"; "<-" ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 325d4f494..8558c2d2f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -151,7 +151,7 @@ module Tactic : open Rawterm val castedopenconstr : constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e - val constrarg : constr_expr may_eval Gram.Entry.e + val constrarg : (constr_expr,reference or_metanum) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 97c7d637b..d716e773b 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -312,10 +312,6 @@ open Genarg let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ prc c -let pr_metanum pr = function - | AN x -> pr x - | MetaNum (_,n) -> str "?" ++ int n - let pr_red_expr (pr_constr,pr_ref) = function | Red false -> str "Red" | Hnf -> str "Hnf" @@ -337,10 +333,10 @@ let pr_red_expr (pr_constr,pr_ref) = function | ExtraRedExpr (s,c) -> hov 1 (str s ++ pr_arg pr_constr c) -let rec pr_may_eval pr = function +let rec pr_may_eval pr pr2 = function | ConstrEval (r,c) -> hov 0 - (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_reference) r ++ + (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr2) r ++ spc () ++ str "in" ++ brk (1,1) ++ pr c) | ConstrContext ((_,id),c) -> hov 0 @@ -348,3 +344,5 @@ let rec pr_may_eval pr = function str "[" ++ pr c ++ str "]") | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c) | ConstrTerm c -> pr c + +let pr_rawconstr c = pr_constr (Constrextern.extern_rawconstr Idset.empty c) diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 6dd3d842c..ffb0146ae 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -37,4 +37,5 @@ val pr_sort : rawsort -> std_ppcmds val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds val pr_constr : constr_expr -> std_ppcmds val pr_cases_pattern : cases_pattern_expr -> std_ppcmds -val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds +val pr_may_eval : ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval -> std_ppcmds +val pr_rawconstr : rawconstr -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1bdd90d38..3c894dd84 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -31,42 +31,58 @@ let pr_occurrences = Ppconstr.pr_occurrences let prtac_tab_v7 = Hashtbl.create 17 let prtac_tab = Hashtbl.create 17 -let declare_extra_tactic_pprule for_v8 s f g = - Hashtbl.add prtac_tab_v7 s (f,g); - if for_v8 then Hashtbl.add prtac_tab s (f,g) +(* We need system F typing strength *) +type ('a,'b) gen_gram_prod_builder = + ('a,'b) generic_argument list -> + string * Egrammar.grammar_tactic_production list +let inst1 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (constr_expr,raw_tactic_expr) gen_gram_prod_builder) +let inst2 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (rawconstr * constr_expr option,glob_tactic_expr) gen_gram_prod_builder) +let inst3 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (Term.constr,glob_tactic_expr) gen_gram_prod_builder) + +let declare_extra_tactic_pprule for_v8 s f = + let f = inst1 f in + let g = inst2 f in + let h = inst3 f in + Hashtbl.add prtac_tab_v7 s (f,g,h); + if for_v8 then Hashtbl.add prtac_tab s (f,g,h) + +let p = prtac_tab +type 'a raw_extra_genarg_printer = + (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds +type 'a glob_extra_genarg_printer = + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds let genarg_pprule_v7 = ref Stringmap.empty let genarg_pprule = ref Stringmap.empty -let declare_extra_genarg_pprule for_v8 (rawwit, f) (wit, g) = +let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) = let s = match unquote wit with | ExtraArgType s -> s | _ -> error "Can declare a pretty-printing rule only for extra argument types" in - let f x = f (out_gen rawwit x) in - let g x = g (out_gen wit x) in - genarg_pprule_v7 := Stringmap.add s (f,g) !genarg_pprule_v7; + let f prc prtac x = f prc prtac (out_gen rawwit x) in + let g prc prtac x = g prc prtac (out_gen globwit x) in + let h prc prtac x = h prc prtac (out_gen wit x) in + genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7; if for_v8 then - genarg_pprule := Stringmap.add s (f,g) !genarg_pprule - -(* [pr_rawtac] is here to cheat with ML typing system, - gen_tactic_expr is polymorphic but with some occurrences of its - instance raw_tactic_expr in it; then pr_tactic should be - polymorphic but with some calls to instance of itself, what ML does - not accept; pr_rawtac0 denotes this instance of pr_tactic on - raw_tactic_expr *) - -let pr_rawtac = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) -let pr_rawtac0 = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) + genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule + +let pi1 (a,_,_) = a +let pi2 (_,a,_) = a +let pi3 (_,_,a) = a let pr_arg pr x = spc () ++ pr x -let pr_metanum pr = function +let pr_or_metanum pr = function | AN x -> pr x | MetaNum (_,n) -> str "?" ++ int n @@ -74,10 +90,22 @@ let pr_or_var pr = function | ArgArg x -> pr x | ArgVar (_,s) -> pr_id s -let pr_or_meta pr = function +let pr_or_metaid pr = function | AI x -> pr x | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" +let pr_and_short_name pr (c,_) = pr c + +let pr_located pr (loc,x) = pr x + +let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) + +let pr_evaluable_reference = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) + +let pr_inductive ind = pr_global (Libnames.IndRef ind) + let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id @@ -142,23 +170,23 @@ let pr_induction_arg prc = function | ElimOnIdent (_,id) -> pr_id id | ElimOnAnonHyp n -> int n -let pr_match_pattern = function - | Term a -> Ppconstr.pr_pattern a - | Subterm (None,a) -> str "[" ++ Ppconstr.pr_pattern a ++ str "]" - | Subterm (Some id,a) -> pr_id id ++ str "[" ++ Ppconstr.pr_pattern a ++ str "]" +let pr_match_pattern pr_pat = function + | Term a -> pr_pat a + | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]" + | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]" -let pr_match_hyps = function - | NoHypId mp -> str "_:" ++ pr_match_pattern mp - | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp +let pr_match_hyps pr_pat = function + | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp + | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp -let pr_match_rule m pr = function +let pr_match_rule m pr_pat pr = function | Pat ([],mp,t) when m -> - str "[" ++ pr_match_pattern mp ++ str "]" + str "[" ++ pr_match_pattern pr_pat mp ++ str "]" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t | Pat (rl,mp,t) -> str "[" ++ prlist_with_sep pr_semicolon - pr_match_hyps rl ++ spc () ++ - str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++ + (pr_match_hyps pr_pat) rl ++ spc () ++ + str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "]" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t @@ -203,16 +231,7 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -let rec pr_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> - spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> - pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - - -let rec pr_rawgen prc prtac x = +let rec pr_raw_generic prc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen rawwit_int x) @@ -224,52 +243,80 @@ let rec pr_rawgen prc prtac x = | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc) (out_gen rawwit_constr_may_eval x) + pr_arg (pr_may_eval prc (pr_or_metanum pr_reference)) + (out_gen rawwit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (prc,pr_metanum pr_reference)) (out_gen rawwit_red_expr x) + pr_arg (pr_red_expr + (prc,pr_or_metanum pr_reference)) (out_gen rawwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) | CastedOpenConstrArgType -> pr_arg prc (out_gen rawwit_casted_open_constr x) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc) - (out_gen rawwit_constr_with_bindings x) + pr_arg (pr_with_bindings prc) (out_gen rawwit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_rawgen prc prtac a ++ spc () ++ pr_rawgen prc - prtac b) + (fun a b -> pr_raw_generic prc prtac a ++ spc () ++ + pr_raw_generic prc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule else !genarg_pprule_v7 in - try fst (Stringmap.find s tab) x + try pi1 (Stringmap.find s tab) prc prtac x with Not_found -> str " [no printer for " ++ str s ++ str "] " -let pr_raw_extend prc prt s l = - let prg = pr_rawgen prc prt in - let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in - try - let (s,pl) = fst (Hashtbl.find tab s) l in - str s ++ pr_tacarg_using_rule prg (pl,l) - with Not_found -> - str "TODO(" ++ str s ++ prlist prg l ++ str ")" -open Closure - -let pr_evaluable_reference = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) +let rec pr_glob_generic prc prtac x = + match Genarg.genarg_tag x with + | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false") + | IntArgType -> pr_arg int (out_gen globwit_int x) + | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x) + | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\"" + | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x) + | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x) + | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x) + | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x) + | ConstrArgType -> pr_arg prc (out_gen globwit_constr x) + | ConstrMayEvalArgType -> + pr_arg (pr_may_eval prc + (pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_constr_may_eval x) + | QuantHypArgType -> + pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x) + | RedExprArgType -> + pr_arg (pr_red_expr + (prc,pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_red_expr x) + | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x) + | CastedOpenConstrArgType -> + pr_arg prc (out_gen globwit_casted_open_constr x) + | ConstrWithBindingsArgType -> + pr_arg (pr_with_bindings prc) (out_gen globwit_constr_with_bindings x) + | List0ArgType _ -> + hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) + | List1ArgType _ -> + hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prtac) (mt()) x) + | PairArgType _ -> + hov 0 + (fold_pair + (fun a b -> pr_glob_generic prc prtac a ++ spc () ++ + pr_glob_generic prc prtac b) + x) + | ExtraArgType s -> + let tab = if Options.do_translate() then !genarg_pprule + else !genarg_pprule_v7 in + try pi2 (Stringmap.find s tab) prc prtac x + with Not_found -> str " [no printer for " ++ str s ++ str "] " -let pr_inductive ind = pr_global (Libnames.IndRef ind) +open Closure -let rec pr_generic prtac x = +let rec pr_generic prc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen wit_int x) @@ -278,50 +325,57 @@ let rec pr_generic prtac x = | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) | RefArgType -> pr_arg pr_global (out_gen wit_ref x) - | SortArgType -> pr_arg Printer.prterm (Term.mkSort (out_gen wit_sort x)) - | ConstrArgType -> pr_arg Printer.prterm (out_gen wit_constr x) + | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x)) + | ConstrArgType -> pr_arg prc (out_gen wit_constr x) | ConstrMayEvalArgType -> - pr_arg Printer.prterm (out_gen wit_constr_may_eval x) + pr_arg prc (out_gen wit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (Printer.prterm,pr_evaluable_reference)) (out_gen wit_red_expr x) + pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) | CastedOpenConstrArgType -> - pr_arg Printer.prterm (snd (out_gen wit_casted_open_constr x)) + pr_arg prc (snd (out_gen wit_casted_open_constr x)) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings Printer.prterm) - (out_gen wit_constr_with_bindings x) + pr_arg (pr_with_bindings prc) (out_gen wit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_generic prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_generic prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_generic prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b) + (fun a b -> pr_generic prc prtac a ++ spc () ++ + pr_generic prc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule else !genarg_pprule_v7 in - try snd (Stringmap.find s tab) x - with Not_found -> str "[no printer for " ++ str s ++ str "]" + try pi3 (Stringmap.find s tab) prc prtac x + with Not_found -> str " [no printer for " ++ str s ++ str "]" -let pr_extend prt s l = - let prg = pr_generic prt in +let rec pr_tacarg_using_rule pr_gen = function + | Egrammar.TacTerm s :: l, al -> + spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) + | Egrammar.TacNonTerm _ :: l, a :: al -> + pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) + | [], [] -> mt () + | _ -> failwith "Inconsistent arguments of extended tactic" + +let pr_extend_gen proj prgen s l = let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in try - let (s,pl) = snd (Hashtbl.find tab s) l in - str s ++ pr_tacarg_using_rule prg (pl,l) + let (s,pl) = proj (Hashtbl.find tab s) l in + str s ++ pr_tacarg_using_rule prgen (pl,l) with Not_found -> - str s ++ prlist prg l + str s ++ prlist prgen l ++ str " (Generic printer)" -let make_pr_tac (pr_constr,pr_pattern,pr_cst,pr_ind,pr_ident,pr_extend) = +let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = let pr_bindings = pr_bindings pr_constr in let pr_with_bindings = pr_with_bindings pr_constr in -let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in +let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in let pr_constrarg c = spc () ++ pr_constr c in let pr_intarg n = spc () ++ int n in @@ -341,8 +395,8 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function - | TacExtend (_,s,l) -> pr_extend !pr_rawtac s l - | TacAlias (s,l,_) -> pr_extend !pr_rawtac s (List.map snd l) + | TacExtend (_,s,l) -> pr_extend pr_constr pr_tac s l + | TacAlias (s,l,_) -> pr_extend pr_constr pr_tac s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t @@ -420,7 +474,7 @@ and pr_atom1 = function hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c) | TacDecompose (l,c) -> hov 1 (str "Decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum pr_ind) l + hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum pr_ind) l ++ str "]")) | TacSpecialize (n,c) -> hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c) @@ -445,9 +499,9 @@ and pr_atom1 = function (* Context management *) | TacClear l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacClearBody l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacMove (b,(_,id1),(_,id2)) -> (* Rem: only b = true is available for users *) assert b; @@ -464,10 +518,10 @@ and pr_atom1 = function | TacRight l -> hov 1 (str "Right" ++ pr_bindings l) | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l) | TacAnyConstructor (Some t) -> - hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t) + hov 1 (str "Constructor" ++ pr_arg pr_tac0 t) | TacAnyConstructor None as t -> pr_atom0 t | TacConstructor (n,l) -> - hov 1 (str "Constructor" ++ pr_or_meta pr_intarg n ++ pr_bindings l) + hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l) (* Conversion *) | TacReduce (r,h) -> @@ -562,18 +616,18 @@ and pr6 = function (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc) ++ fnl () | TacMatch (t,lrul) -> - hov 0 (str "Match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc() + hov 0 (str "Match" ++ spc () ++ pr_may_eval pr_constr pr_cst t ++ spc() ++ str "With" ++ prlist (fun r -> fnl () ++ str "|" ++ spc () ++ - pr_match_rule true prtac r) + pr_match_rule true pr_pat prtac r) lrul) | TacMatchContext (lr,lrul) -> hov 0 ( str (if lr then "Match Reverse Context With" else "Match Context With") ++ prlist (fun r -> fnl () ++ str "|" ++ spc () ++ - pr_match_rule false prtac r) + pr_match_rule false pr_pat prtac r) lrul) | TacFun (lvar,body) -> hov 0 (str "Fun" ++ @@ -583,45 +637,58 @@ and pr6 = function and pr_tacarg0 = function | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>") - | MetaNumArg (_,n) -> str ("?" ^ string_of_int n ) | MetaIdArg (_,s) -> str ("$" ^ s) + | Identifier id -> pr_id id | TacVoid -> str "()" - | Reference r -> pr_reference r + | Reference r -> pr_ref r | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c - | ConstrMayEval c -> pr_may_eval pr_constr c + | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c | Integer n -> int n | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")" and pr_tacarg1 = function | TacCall (_,f,l) -> - hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) - | Tacexp t -> !pr_rawtac t + hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) + | Tacexp t -> pr_tac t | t -> pr_tacarg0 t and pr_tacarg x = pr_tacarg1 x and prtac x = pr6 x -in (prtac,pr0,pr_match_rule) +in (prtac,pr0,pr_match_rule false pr_pat pr_tac) -let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) = - make_pr_tac - (Ppconstr.pr_constr, - Ppconstr.pr_constr, - pr_metanum pr_reference, - pr_reference, - pr_or_meta (fun (loc,id) -> pr_id id), - pr_raw_extend Ppconstr.pr_constr) +let pr_raw_extend prc prtac = pr_extend_gen pi1 (pr_raw_generic prc prtac) +let pr_glob_extend prc prtac = pr_extend_gen pi2 (pr_glob_generic prc prtac) +let pr_extend prc prtac = pr_extend_gen pi3 (pr_generic prc prtac) + +let pr_and_constr_expr pr (c,_) = pr c + +let rec glob_printers = + (pr_glob_tactic, + pr_glob_tactic0, + pr_and_constr_expr Ppconstr.pr_rawconstr, + Printer.pr_pattern, + pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)), + pr_or_var pr_inductive, + pr_or_var pr_ltac_constant, + pr_located pr_id, + pr_glob_extend) -let _ = pr_rawtac := pr_raw_tactic -let _ = pr_rawtac0 := pr_raw_tactic0 +and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t + +and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t + +and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t let (pr_tactic,_,_) = make_pr_tac - (Printer.prterm, - Ppconstr.pr_constr, + (pr_glob_tactic, + pr_glob_tactic0, + Printer.prterm, + Printer.pr_pattern, pr_evaluable_reference, pr_inductive, + pr_ltac_constant, pr_id, pr_extend) - diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 186a726f6..055b5adf2 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -14,42 +14,70 @@ open Tacexpr open Pretyping open Proof_type open Topconstr +open Rawterm -(* if the boolean is false then the extension applies only to old syntax *) +val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_or_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds +val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds +val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds +val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds + +type 'a raw_extra_genarg_printer = + (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a glob_extra_genarg_printer = + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + + (* if the boolean is false then the extension applies only to old syntax *) val declare_extra_genarg_pprule : bool -> - ('a raw_abstract_argument_type * ('a -> std_ppcmds)) -> - ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit + ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> + ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> + ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit + +type ('a,'b) gen_gram_prod_builder = + ('a,'b) generic_argument list -> + string * Egrammar.grammar_tactic_production list -(* idem *) + (* if the boolean is false then the extension applies only to old syntax *) val declare_extra_tactic_pprule : - bool -> string -> - (raw_generic_argument list -> - string * Egrammar.grammar_tactic_production list) - -> (closed_generic_argument list -> - string * Egrammar.grammar_tactic_production list) - -> unit + bool -> string -> ('a,'b) gen_gram_prod_builder -> unit -val pr_match_pattern : pattern_expr match_pattern -> std_ppcmds +val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds -val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) -> - (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds +val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('a,'b) match_rule -> std_ppcmds -val pr_raw_tactic : raw_tactic_expr -> std_ppcmds +val pr_glob_tactic : glob_tactic_expr -> std_ppcmds val pr_tactic : Proof_type.tactic_expr -> std_ppcmds -val pr_rawgen: +val pr_glob_generic: + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + glob_generic_argument -> std_ppcmds + +val pr_raw_generic : (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds + val pr_raw_extend: (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> string -> - (constr_expr, raw_tactic_expr) generic_argument list -> - std_ppcmds + raw_generic_argument list -> std_ppcmds + +val pr_glob_extend: + (rawconstr_and_expr -> std_ppcmds) -> + (glob_tactic_expr -> std_ppcmds) -> string -> + glob_generic_argument list -> std_ppcmds + val pr_extend : - (raw_tactic_expr -> std_ppcmds) -> string -> - (Term.constr, raw_tactic_expr) generic_argument list -> - std_ppcmds + (Term.constr -> std_ppcmds) -> + (glob_tactic_expr -> std_ppcmds) -> string -> closed_generic_argument list -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 54b928ef8..f79148911 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -145,9 +145,9 @@ let mlexpr_of_intro_pattern = function let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) let mlexpr_of_or_metanum f = function - | Rawterm.AN a -> <:expr< Rawterm.AN $f a$ >> - | Rawterm.MetaNum (_,n) -> - <:expr< Rawterm.MetaNum $dloc$ $mlexpr_of_int n$ >> + | Genarg.AN a -> <:expr< Genarg.AN $f a$ >> + | Genarg.MetaNum (_,n) -> + <:expr< Genarg.MetaNum $dloc$ $mlexpr_of_int n$ >> let mlexpr_of_or_metaid f = function | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> @@ -449,7 +449,7 @@ let rec mlexpr_of_atomic_tactic = function *) | _ -> failwith "Quotation of atomic tactic expressions: TODO" -and mlexpr_of_tactic = function +and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function | Tacexpr.TacAtom (loc,t) -> <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >> | Tacexpr.TacThen (t1,t2) -> @@ -510,8 +510,6 @@ and mlexpr_of_tactic = function and mlexpr_of_tactic_arg = function | Tacexpr.MetaIdArg (loc,id) -> anti loc id - | Tacexpr.MetaNumArg (loc,n) -> - <:expr< Tacexpr.MetaNumArg $dloc$ $mlexpr_of_int n$ >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> | Tacexpr.Tacexp t -> diff --git a/parsing/search.ml b/parsing/search.ml index fc5792fa0..5e2fc7f2c 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -20,6 +20,7 @@ open Declare open Coqast open Environ open Pattern +open Matching open Printer open Libnames open Nametab @@ -131,9 +132,9 @@ let mk_rewrite_pattern2 eq pattern = let pattern_filter pat _ a c = try try - Pattern.is_matching pat (head c) + is_matching pat (head c) with _ -> - Pattern.is_matching + is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) with UserError _ -> false diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index a3d5f496e..a7da88b52 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -11,6 +11,7 @@ open Genarg open Q_util open Q_coqast +open Argextend let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = (0,0) @@ -35,35 +36,19 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l -let rec make_wit loc = function - | BoolArgType -> <:expr< Genarg.wit_bool >> - | IntArgType -> <:expr< Genarg.wit_int >> - | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | StringArgType -> <:expr< Genarg.wit_string >> - | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> - | IdentArgType -> <:expr< Genarg.wit_ident >> - | RefArgType -> <:expr< Genarg.wit_ref >> - | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> - | SortArgType -> <:expr< Genarg.wit_sort >> - | ConstrArgType -> <:expr< Genarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | TacticArgType -> <:expr< Genarg.wit_tactic >> - | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >> - let rec make_let e = function | [] -> e | TacNonTerm(loc,t,_,Some p)::l -> let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in - <:expr< let $lid:p$ = Genarg.out_gen $make_wit loc t$ $lid:p$ in $e$ >> + let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in + let v = + (* Special case for tactics which must be stored in algebraic + form to avoid marshalling closures and to be reprinted *) + if t = TacticArgType then + <:expr< ($v$, Tacinterp.eval_tactic $v$) >> + else v in + <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let e l let add_clause s (_,pt,e) l = @@ -95,6 +80,16 @@ let rec make_args = function <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> | _::l -> make_args l +let rec make_eval_tactic e = function + | [] -> e + | TacNonTerm(loc,TacticArgType,_,Some p)::l -> + let loc = join_loc loc (MLast.loc_of_expr e) in + let e = make_eval_tactic e l in + (* Special case for tactics which must be stored in algebraic + form to avoid marshalling closures and to be reprinted *) + <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >> + | _::l -> make_eval_tactic e l + let rec make_fun e = function | [] -> e | TacNonTerm(loc,_,_,Some p)::l -> @@ -142,7 +137,7 @@ let declare_tactic_v7 loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $e$ + Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> @@ -153,7 +148,7 @@ let declare_tactic_v7 loc s cl = open Pcoq; Egrammar.extend_tactic_grammar $se$ $gl$; let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se$ pp pp; + Pptactic.declare_extra_tactic_pprule False $se$ pp; end >> @@ -170,25 +165,26 @@ let declare_tactic loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $e$ + Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> in + let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in let se = mlexpr_of_string s in <:str_item< declare open Pcoq; - declare $list:List.map hide_tac cl'$ end; + declare $list:hidden$ end; try Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) with e -> Pp.pp (Cerrors.explain_exn e); Egrammar.extend_tactic_grammar $se'$ $gl'$; let pp' = fun [ $list:pl'$ ] in - Pptactic.declare_extra_tactic_pprule True $se'$ pp' pp'; + Pptactic.declare_extra_tactic_pprule True $se'$ pp'; Egrammar.extend_tactic_grammar $se'$ $gl$; let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se'$ pp pp; + Pptactic.declare_extra_tactic_pprule False $se'$ pp; end >> @@ -206,7 +202,8 @@ let rec interp_entry_name loc s = else if l > 4 & String.sub s (l-4) 4 = "_opt" then let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in OptArgType t, <:expr< Gramext.Sopt $g$ >> - else + else + let t, se = match Pcoq.entry_type (Pcoq.get_univ "prim") s with | Some _ as x -> x, <:expr< Prim. $lid:s$ >> diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index a910c1c06..3fad196f9 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -12,6 +12,7 @@ open Genarg open Q_util open Q_coqast open Ast +open Argextend let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = (0,0) @@ -35,29 +36,6 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l -let rec make_rawwit loc = function - | BoolArgType -> <:expr< Genarg.rawwit_bool >> - | IntArgType -> <:expr< Genarg.rawwit_int >> - | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >> - | StringArgType -> <:expr< Genarg.rawwit_string >> - | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> - | IdentArgType -> <:expr< Genarg.rawwit_ident >> - | RefArgType -> <:expr< Genarg.rawwit_ref >> - | SortArgType -> <:expr< Genarg.rawwit_sort >> - | ConstrArgType -> <:expr< Genarg.rawwit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> - | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> - | TacticArgType -> <:expr< Genarg.rawwit_tactic >> - | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> - let rec make_let e = function | [] -> e | VernacNonTerm(loc,t,_,Some p)::l -> diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 7af3a75dc..9dafda587 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -13,11 +13,10 @@ open Names open Libnames open Nameops open Term -open Termops -open Reductionops open Rawterm open Environ open Nametab +open Pp type constr_pattern = | PRef of global_reference @@ -149,234 +148,6 @@ let head_of_constr_reference c = match kind_of_term c with | Var id -> VarNode id | _ -> anomaly "Not a rigid reference" - -(* Second part : Given a term with second-order variables in it, - represented by Meta's, and possibly applied using [SOAPP] to - terms, this function will perform second-order, binding-preserving, - matching, in the case where the pattern is a pattern in the sense - of Dale Miller. - - ALGORITHM: - - Given a pattern, we decompose it, flattening Cast's and apply's, - recursing on all operators, and pushing the name of the binder each - time we descend a binder. - - When we reach a first-order variable, we ask that the corresponding - term's free-rels all be higher than the depth of the current stack. - - When we reach a second-order application, we ask that the - intersection of the free-rels of the term and the current stack be - contained in the arguments of the application, and in that case, we - construct a LAMBDA with the names on the stack. - - *) - -exception PatternMatchingFailure - -let constrain ((n : int),(m : constr)) sigma = - if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma - else raise PatternMatchingFailure - else - (n,m)::sigma - -let build_lambda toabstract stk (m : constr) = - let rec buildrec m p_0 p_1 = match p_0,p_1 with - | (_, []) -> m - | (n, (na,t)::tl) -> - if List.mem n toabstract then - buildrec (mkLambda (na,t,m)) (n+1) tl - else - buildrec (pop m) (n+1) tl - in - buildrec m 1 stk - -let memb_metavars m n = - match (m,n) with - | (None, _) -> true - | (Some mvs, n) -> List.mem n mvs - -let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 - -let matches_core convert allow_partial_app pat c = - let rec sorec stk sigma p t = - let cT = strip_outer_cast t in - match p,kind_of_term cT with - | PSoApp (n,args),m -> - let relargs = - List.map - (function - | PRel n -> n - | _ -> error "Only bound indices are currently allowed in second order pattern matching") - args in - let frels = Intset.elements (free_rels cT) in - if list_subset frels relargs then - constrain (n,build_lambda relargs stk cT) sigma - else - raise PatternMatchingFailure - - | PMeta (Some n), m -> - let depth = List.length stk in - let frels = Intset.elements (free_rels cT) in - if List.for_all (fun i -> i > depth) frels then - constrain (n,lift (-depth) cT) sigma - else - raise PatternMatchingFailure - - | PMeta None, m -> sigma - - | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma - - | PVar v1, Var v2 when v1 = v2 -> sigma - - | PRef ref, _ when constr_of_reference ref = cT -> sigma - - | PRel n1, Rel n2 when n1 = n2 -> sigma - - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma - - | PSort (RType _), Sort (Type _) -> sigma - - | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> - let p = Array.length args2 - Array.length args1 in - if p>=0 then - let args21, args22 = array_chop p args2 in - let sigma = - let depth = List.length stk in - let c = mkApp(c2,args21) in - let frels = Intset.elements (free_rels c) in - if List.for_all (fun i -> i > depth) frels then - constrain (n,lift (-depth) c) sigma - else - raise PatternMatchingFailure in - array_fold_left2 (sorec stk) sigma args1 args22 - else raise PatternMatchingFailure - - | PApp (c1,arg1), App (c2,arg2) -> - (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 - with Invalid_argument _ -> raise PatternMatchingFailure) - - | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 - - | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 - - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2 - - | PRef (ConstRef _ as ref), _ when convert <> None -> - let (env,evars) = out_some convert in - let c = constr_of_reference ref in - if is_conv env evars c cT then sigma - else raise PatternMatchingFailure - - | PCase (_,_,a1,br1), Case (_,_,a2,br2) -> - (* On ne teste pas le prédicat *) - if (Array.length br1) = (Array.length br2) then - array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2 - else - raise PatternMatchingFailure - (* À faire *) - | PFix f0, Fix f1 when f0 = f1 -> sigma - | PCoFix c0, CoFix c1 when c0 = c1 -> sigma - | _ -> raise PatternMatchingFailure - - in - Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c) - -let matches = matches_core None false - -let pmatches = matches_core None true - -(* To skip to the next occurrence *) -exception NextOccurrence of int - -(* Tells if it is an authorized occurrence *) -let authorized_occ nocc mres = - if nocc = 0 then mres - else raise (NextOccurrence nocc) - -(* Tries to match a subterm of [c] with [pat] *) -let rec sub_match nocc pat c = - match kind_of_term c with - | Cast (c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1] in - (lm,mkCast (List.hd lc, c2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in - (lm,mkCast (List.hd lc, c2))) - | Lambda (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1))) - | Prod (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1))) - | LetIn (x,c1,t2,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) - | App (c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le))) - | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le)))) - | Case (ci,hd,c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with - | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) - | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))) - | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ - | Rel _|Meta _|Var _|Sort _ -> - (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with - | PatternMatchingFailure -> raise (NextOccurrence nocc) - | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) - -(* Tries [sub_match] for all terms in the list *) -and try_sub_match nocc pat lc = - let rec try_sub_match_rec nocc pat lacc = function - | [] -> raise (NextOccurrence nocc) - | c::tl -> - (try - let (lm,ce) = sub_match nocc pat c in - (lm,lacc@(ce::tl)) - with - | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in - try_sub_match_rec nocc pat [] lc - -let is_matching pat n = - try let _ = matches pat n in true - with PatternMatchingFailure -> false - -let matches_conv env sigma = matches_core (Some (env,sigma)) false - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false - let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n @@ -402,3 +173,93 @@ let rec pattern_of_constr t = | Fix f -> PFix f | CoFix _ -> error "pattern_of_constr: (co)fix currently not supported" + +(* To process patterns, we need a translation without typing at all. *) + +let rec inst lvar = function + | PVar id as x -> (try List.assoc id lvar with Not_found -> x) + | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl) + | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl) + | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b) + | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b) + | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b) + | PCase (c,po,p,pl) -> + PCase (c,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl) + (* Non recursive *) + | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x + (* Bound to terms *) + | (PFix _ | PCoFix _ as r) -> + error ("Not instantiable pattern") + +let instantiate_pattern = inst + +let rec pat_of_raw metas vars = function + | RVar (_,id) -> + (try PRel (list_index (Name id) vars) + with Not_found -> PVar id) + | RMeta (_,n) -> + metas := n::!metas; PMeta (Some n) + | RRef (_,r) -> + PRef r + (* Hack pour ne pas réécrire une interprétation complète des patterns*) + | RApp (_, RMeta (_,n), cl) when n<0 -> + PSoApp (- n, List.map (pat_of_raw metas vars) cl) + | RApp (_,c,cl) -> + PApp (pat_of_raw metas vars c, + Array.of_list (List.map (pat_of_raw metas vars) cl)) + | RLambda (_,na,c1,c2) -> + PLambda (na, pat_of_raw metas vars c1, + pat_of_raw metas (na::vars) c2) + | RProd (_,na,c1,c2) -> + PProd (na, pat_of_raw metas vars c1, + pat_of_raw metas (na::vars) c2) + | RLetIn (_,na,c1,c2) -> + PLetIn (na, pat_of_raw metas vars c1, + pat_of_raw metas (na::vars) c2) + | RSort (_,s) -> + PSort s + | RHole _ -> + PMeta None + | RCast (_,c,t) -> + Options.if_verbose + Pp.warning "Cast not taken into account in constr pattern"; + pat_of_raw metas vars c + | ROrderedCase (_,st,po,c,br) -> + PCase (st,option_app (pat_of_raw metas vars) po, + pat_of_raw metas vars c, + Array.map (pat_of_raw metas vars) br) + | RCases (loc,po,[c],br) -> + PCase (Term.RegularStyle,option_app (pat_of_raw metas vars) po, + pat_of_raw metas vars c, + Array.init (List.length br) + (pat_of_raw_branch loc metas vars br)) + | r -> + let loc = loc_of_rawconstr r in + user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern") + +and pat_of_raw_branch loc metas vars brs i = + let bri = List.filter + (function + (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1 + | (loc,_,_,_) -> + user_err_loc (loc,"pattern_of_rawconstr", + Pp.str "Not supported pattern")) brs in + match bri with + [(_,_,[PatCstr(_,_,lv,_)],br)] -> + let lna = + List.map + (function PatVar(_,na) -> na + | PatCstr(loc,_,_,_) -> + user_err_loc (loc,"pattern_of_rawconstr", + Pp.str "Not supported pattern")) lv in + let vars' = List.rev lna @ vars in + List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna + (pat_of_raw metas vars' br) + | _ -> user_err_loc (loc,"pattern_of_rawconstr", + str "No unique branch for " ++ int (i+1) ++ + str"-th constructor") + +let pattern_of_rawconstr c = + let metas = ref [] in + let p = pat_of_raw metas [] c in + (!metas,p) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 4b8c0aa8d..11821a6a8 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -67,38 +67,11 @@ val head_of_constr_reference : Term.constr -> constr_label val pattern_of_constr : constr -> constr_pattern +(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into + a pattern; variables bound in [l] are replaced by the pattern to which they + are bound *) -exception PatternMatchingFailure +val pattern_of_rawconstr : Rawterm.rawconstr -> int list * constr_pattern -(* [matches pat c] matches [c] against [pat] and returns the resulting - assignment of metavariables; it raises [PatternMatchingFailure] if - not matchable; bindings are given in increasing order based on the - numbers given in the pattern *) -val matches : - constr_pattern -> constr -> (int * constr) list - -(* [is_matching pat c] just tells if [c] matches against [pat] *) - -val is_matching : - constr_pattern -> constr -> bool - -(* [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) - -val matches_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> (int * constr) list - -(* To skip to the next occurrence *) -exception NextOccurrence of int - -(* Tries to match a subterm of [c] with [pat] *) -val sub_match : - int -> constr_pattern -> constr -> ((int * constr) list * constr) - -(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) - -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool +val instantiate_pattern : + (identifier * constr_pattern) list -> constr_pattern -> constr_pattern diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 0075be7d8..0dcf90188 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -159,7 +159,6 @@ let map_rawconstr_with_binders_loc loc g f e = function | RDynamic (_,x) -> RDynamic (loc,x) *) -(* let rec subst_pat subst pat = match pat with | PatVar _ -> pat @@ -168,8 +167,7 @@ let rec subst_pat subst pat = and cpl' = list_smartmap (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) -*) -(* + let rec subst_raw subst raw = match raw with | RRef (loc,ref) -> @@ -244,7 +242,6 @@ let rec subst_raw subst raw = RCast (loc,r1',r2') | RDynamic _ -> raw -*) let loc_of_rawconstr = function | RRef (loc,_) -> loc @@ -284,10 +281,8 @@ type ('a,'b) red_expr_gen = | Pattern of 'a occurrences list | ExtraRedExpr of string * 'a -type 'a or_metanum = AN of 'a | MetaNum of int located - -type 'a may_eval = +type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a + | ConstrEval of ('a, 'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 7ac8a15b7..293667aed 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -98,9 +98,7 @@ val map_rawconstr_with_binders_loc : loc -> val loc_of_rawconstr : rawconstr -> loc -(* val subst_raw : Names.substitution -> rawconstr -> rawconstr -*) type 'a raw_red_flag = { rBeta : bool; @@ -123,10 +121,8 @@ type ('a,'b) red_expr_gen = | Pattern of 'a occurrences list | ExtraRedExpr of string * 'a -type 'a or_metanum = AN of 'a | MetaNum of int located - -type 'a may_eval = +type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a + | ConstrEval of ('a, 'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/proofs/logic.ml b/proofs/logic.ml index e9e1882f8..0c25e0ff8 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -50,10 +50,12 @@ type refiner_error = exception RefinerError of refiner_error +open Pretype_errors + let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _)) -> true + Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true | _ -> false let error_cannot_unify (m,n) = diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f4cf4640..b905c0a26 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -18,6 +18,8 @@ open Util open Tacexpr open Rawterm open Genarg +open Nametab +open Pattern (*i*) (* This module defines the structure of proof tree and the tactic type. So, it @@ -67,31 +69,33 @@ and validation = (proof_tree list -> proof_tree) and tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_expr and atomic_tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_atomic_tactic_expr and tactic_arg = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_arg type hyp_location = identifier Tacexpr.raw_hyp_location -type open_generic_argument = - (constr,raw_tactic_expr) generic_argument -type closed_generic_argument = - (constr,raw_tactic_expr) generic_argument - -type 'a closed_abstract_argument_type = - ('a,constr,raw_tactic_expr) abstract_argument_type diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index bf5d4f316..933740882 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -18,6 +18,8 @@ open Util open Tacexpr open Rawterm open Genarg +open Nametab +open Pattern (*i*) (* This module defines the structure of proof tree and the tactic type. So, it @@ -95,31 +97,32 @@ and validation = (proof_tree list -> proof_tree) and tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_expr and atomic_tactic_expr = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_atomic_tactic_expr and tactic_arg = (constr, + constr_pattern, evaluable_global_reference, inductive or_metanum, - identifier) + ltac_constant, + identifier, + glob_tactic_expr) Tacexpr.gen_tactic_arg type hyp_location = identifier Tacexpr.raw_hyp_location - -type open_generic_argument = - (constr,raw_tactic_expr) generic_argument -type closed_generic_argument = - (constr,raw_tactic_expr) generic_argument - -type 'a closed_abstract_argument_type = - ('a,constr,raw_tactic_expr) abstract_argument_type diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 61fc3f3b1..01787f7d9 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -856,7 +856,7 @@ open Pp let pr_tactic = function | Tacexpr.TacArg (Tacexpr.Tacexp t) -> - Pptactic.pr_raw_tactic t (*top tactic from tacinterp*) + Pptactic.pr_glob_tactic t (*top tactic from tacinterp*) | t -> Pptactic.pr_tactic t let pr_rule = function diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 146d4bd29..a2584773f 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -15,6 +15,7 @@ open Nametab open Rawterm open Util open Genarg +open Pattern type 'a or_metaid = AI of 'a | MetaId of loc * string @@ -29,6 +30,9 @@ type raw_red_flag = type raw_red_expr = (constr_expr, reference or_metanum) red_expr_gen +type glob_red_expr = + (rawconstr_and_expr, evaluable_global_reference or_var or_metanum) red_expr_gen + let make_red_flag = let rec add_flag red = function | [] -> red @@ -86,7 +90,7 @@ type ('a,'t) match_rule = | Pat of 'a match_context_hyps list * 'a match_pattern * 't | All of 't -type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr = +type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Basic tactics *) | TacIntroPattern of intro_pattern_expr list | TacIntrosUntil of quantified_hypothesis @@ -122,9 +126,6 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr = | TacDecomposeAnd of 'constr | TacDecomposeOr of 'constr | TacDecompose of 'ind list * 'constr -(* - | TacOldElim of 'constr -*) | TacSpecialize of int option * 'constr with_bindings | TacLApply of 'constr @@ -147,7 +148,7 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr = | TacLeft of 'constr substitution | TacRight of 'constr substitution | TacSplit of bool * 'constr substitution - | TacAnyConstructor of raw_tactic_expr option + | TacAnyConstructor of 'tac option | TacConstructor of int or_metaid * 'constr substitution (* Conversion *) @@ -161,76 +162,130 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* For ML extensions *) - | TacExtend of loc * string * ('constr,raw_tactic_expr) generic_argument list + | TacExtend of loc * string * ('constr,'tac) generic_argument list (* For syntax extensions *) | TacAlias of string * - (identifier * ('constr,raw_tactic_expr) generic_argument) list - * raw_tactic_expr - -and raw_tactic_expr = - (constr_expr,reference or_metanum,reference or_metanum,identifier located or_metaid) gen_tactic_expr - -and ('constr,'cst,'ind,'id) gen_tactic_expr = - | TacAtom of loc * ('constr,'cst,'ind,'id) gen_atomic_tactic_expr - | TacThen of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr - | TacThens of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr list - | TacFirst of ('constr,'cst,'ind,'id) gen_tactic_expr list - | TacSolve of ('constr,'cst,'ind,'id) gen_tactic_expr list - | TacTry of ('constr,'cst,'ind,'id) gen_tactic_expr - | TacOrelse of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr - | TacDo of int * ('constr,'cst,'ind,'id) gen_tactic_expr - | TacRepeat of ('constr,'cst,'ind,'id) gen_tactic_expr - | TacProgress of ('constr,'cst,'ind,'id) gen_tactic_expr - | TacAbstract of ('constr,'cst,'ind,'id) gen_tactic_expr * identifier option + (identifier * ('constr,'tac) generic_argument) list + * 'tac + +and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = + | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr + | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list + | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list + | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list + | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacDo of int * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option | TacId | TacFail of int * string - | TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr + | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr - | TacLetIn of (identifier located * constr_expr may_eval option * ('constr,'cst,'ind,'id) gen_tactic_arg) list * ('constr,'cst,'ind,'id) gen_tactic_expr - | TacLetCut of (identifier * constr_expr may_eval * ('constr,'cst,'ind,'id) gen_tactic_arg) list - | TacMatch of constr_expr may_eval * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list - | TacMatchContext of direction_flag * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list - | TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast - | TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg + | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacLetIn of (identifier located * ('constr,'cst) may_eval option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + | TacLetCut of (identifier * ('constr,'cst) may_eval * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list + | TacMatch of ('constr,'cst) may_eval * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast + | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg -and ('constr,'cst,'ind,'id) gen_tactic_fun_ast = - identifier option list * ('constr,'cst,'ind,'id) gen_tactic_expr +and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast = + identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr (* These are possible arguments of a tactic definition *) -and ('constr,'cst,'ind,'id) gen_tactic_arg = +and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | TacDynamic of loc * Dyn.t | TacVoid - | MetaNumArg of loc * int | MetaIdArg of loc * string - | ConstrMayEval of 'constr may_eval - | Reference of reference + | ConstrMayEval of ('constr,'cst) may_eval + | Identifier of identifier (* parsed under Reference (Ident _) *) + | Reference of 'ref | Integer of int | TacCall of loc * - reference * ('constr,'cst,'ind,'id) gen_tactic_arg list - | Tacexp of raw_tactic_expr + 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list + | Tacexp of 'tac + +type raw_tactic_expr = + (constr_expr, + pattern_expr, + reference or_metanum, + reference or_metanum, + reference, + identifier located or_metaid, + raw_tactic_expr) gen_tactic_expr type raw_atomic_tactic_expr = - (constr_expr, (* constr *) - reference or_metanum, (* evaluable reference *) - reference or_metanum, (* inductive *) - identifier located or_metaid (* identifier *) - ) gen_atomic_tactic_expr + (constr_expr, (* constr *) + pattern_expr, (* pattern *) + reference or_metanum, (* evaluable reference *) + reference or_metanum, (* inductive *) + reference, (* ltac reference *) + identifier located or_metaid, (* identifier *) + raw_tactic_expr) gen_atomic_tactic_expr type raw_tactic_arg = (constr_expr, + pattern_expr, reference or_metanum, reference or_metanum, - identifier located or_metaid) gen_tactic_arg + reference, + identifier located or_metaid, + raw_tactic_expr) gen_tactic_arg type raw_generic_argument = (constr_expr,raw_tactic_expr) generic_argument +(* Globalized tactics *) +type glob_tactic_expr = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var or_metanum, + inductive or_var or_metanum, + ltac_constant or_var, + identifier located, + glob_tactic_expr) gen_tactic_expr + +type glob_atomic_tactic_expr = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var or_metanum, + inductive or_var or_metanum, + ltac_constant or_var, + identifier located, + glob_tactic_expr) gen_atomic_tactic_expr + +type glob_tactic_arg = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var or_metanum, + inductive or_var or_metanum, + ltac_constant or_var, + identifier located, + glob_tactic_expr) gen_tactic_arg + +type glob_generic_argument = + (rawconstr_and_expr,glob_tactic_expr) generic_argument + type closed_raw_generic_argument = (constr_expr,raw_tactic_expr) generic_argument type 'a raw_abstract_argument_type = - ('a, constr_expr,raw_tactic_expr) abstract_argument_type + ('a,constr_expr,raw_tactic_expr) abstract_argument_type + +type 'a glob_abstract_argument_type = + ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type + +type open_generic_argument = + (Term.constr,glob_tactic_expr) generic_argument + +type closed_generic_argument = + (Term.constr,glob_tactic_expr) generic_argument + +type 'a closed_abstract_argument_type = + ('a,Term.constr,glob_tactic_expr) abstract_argument_type type declaration_hook = Decl_kinds.strength -> global_reference -> unit diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 9c0b77f58..42bbb8637 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -40,7 +40,7 @@ let help () = let goal_com g tac_ast = begin db_pr_goal g; - msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++ + msg (str "Going to execute:" ++ fnl () ++ (pr_glob_tactic tac_ast) ++ fnl ()) end @@ -114,7 +114,8 @@ let db_pattern_rule debug num r = if debug = DebugOn then begin msgnl (str "Pattern rule " ++ int num ++ str ":"); - msgnl (str "|" ++ spc () ++ pr_match_rule false pr_raw_tactic r) + msgnl (str "|" ++ spc () ++ + pr_match_rule false Printer.pr_pattern pr_glob_tactic r) end (* Prints the hypothesis pattern identifier if it exists *) @@ -150,7 +151,9 @@ let db_hyp_pattern_failure debug env hyp = if debug = DebugOn then msgnl (str ("The pattern hypothesis"^(hyp_bound (fst hyp))^ " cannot match: ") ++ - pr_match_pattern (pp_match_pattern env (snd hyp))) + pr_match_pattern + (Printer.pr_pattern_env env (names_of_rel_context env)) + (snd hyp)) (* Prints a matching failure message for a rule *) let db_matching_failure debug = diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 82f01f461..f859b31dd 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -27,14 +27,14 @@ type debug_info = (* Prints the state and waits *) val debug_prompt : - goal sigma -> debug_info -> Tacexpr.raw_tactic_expr -> debug_info + goal sigma -> debug_info -> Tacexpr.glob_tactic_expr -> debug_info (* Prints a constr *) val db_constr : debug_info -> env -> constr -> unit (* Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (pattern_expr,raw_tactic_expr) match_rule -> unit + debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit (* Prints a matched hypothesis *) val db_matched_hyp : diff --git a/tactics/auto.ml b/tactics/auto.ml index 9eb192f4d..8788f7208 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -20,6 +20,7 @@ open Evd open Reduction open Typing open Pattern +open Matching open Tacmach open Proof_type open Pfedit @@ -48,7 +49,7 @@ type auto_tactic = | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *) | Unfold_nth of global_reference (* Hint Unfold *) - | Extern of raw_tactic_expr (* Hint Extern *) + | Extern of glob_tactic_expr (* Hint Extern *) type pri_auto_tactic = { hname : identifier; (* name of the hint *) @@ -311,6 +312,11 @@ let cache_autohint (_,(name,hintlist)) = add_hint name hintlist list_smartmap recalc_hint hintlist *) +let forward_subst_tactic = + ref (fun _ -> failwith "subst_tactic is not installed for Auto") + +let set_extern_subst_tactic f = forward_subst_tactic := f + let subst_autohint (_,subst,(name,hintlist as obj)) = let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in let trans_data data code = @@ -343,8 +349,10 @@ let subst_autohint (_,subst,(name,hintlist as obj)) = let ref' = subst_global subst ref in if ref==ref' then data else trans_data data (Unfold_nth ref') - | Extern _ -> - anomaly "Extern hints cannot be substituted!!!" + | Extern tac -> + let tac' = !forward_subst_tactic subst tac in + if tac==tac' then data else + trans_data data (Extern tac') in if lab' == lab && data' == data then hint else (lab',data') @@ -356,7 +364,6 @@ let subst_autohint (_,subst,(name,hintlist as obj)) = let classify_autohint (_,((name,hintlist) as obj)) = match hintlist with [] -> Dispose - | (_,{code=Extern _})::_ -> Keep obj (* TODO! should be changed *) | _ -> Substitute obj let export_autohint x = Some x @@ -415,7 +422,6 @@ let add_extern name pri (patmetas,pat) tacast dbname = let add_externs name pri pat tacast dbnames = List.iter (add_extern name pri pat tacast) dbnames - let add_trivials env sigma l dbnames = List.iter (fun dbname -> @@ -423,6 +429,10 @@ let add_trivials env sigma l dbnames = inAutoHint(dbname, List.map (make_trivial env sigma) l))) dbnames +let forward_intern_tac = + ref (fun _ -> failwith "intern_tac is not installed for Auto") + +let set_extern_intern_tac f = forward_intern_tac := f let add_hints dbnames h = let dbnames = if dbnames = [] then ["core"] else dbnames in match h with @@ -461,6 +471,7 @@ let add_hints dbnames h = add_resolves env sigma lcons dbnames | HintsExtern (hintname, pri, patcom, tacexp) -> let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in + let tacexp = !forward_intern_tac (fst pat) tacexp in add_externs hintname pri pat tacexp dbnames (**************************************************************************) @@ -474,7 +485,7 @@ let fmt_autotactic = function | Res_pf_THEN_trivial_fail (c,clenv) -> (str"Apply " ++ prterm c ++ str" ; Trivial") | Unfold_nth c -> (str"Unfold " ++ pr_global c) - | Extern coqast -> (str "Extern " ++ Pptactic.pr_raw_tactic coqast) + | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac) let fmt_hint v = (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) @@ -605,16 +616,16 @@ si après Intros la conclusion matche le pattern. (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) -let forward_tac_interp = - ref (fun _ -> failwith "tac_interp is not installed for Auto") +let forward_interp_tactic = + ref (fun _ -> failwith "interp_tactic is not installed for Auto") -let set_extern_interp f = forward_tac_interp := f +let set_extern_interp f = forward_interp_tactic := f let conclPattern concl pat tac gl = let constr_bindings = - try Pattern.matches pat concl + try matches pat concl with PatternMatchingFailure -> error "conclPattern" in - !forward_tac_interp constr_bindings tac gl + !forward_interp_tactic constr_bindings tac gl (**************************************************************************) (* The Trivial tactic *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 4cd017e5f..5fe5ebb86 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -28,7 +28,7 @@ type auto_tactic = | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *) | Unfold_nth of global_reference (* Hint Unfold *) - | Extern of Tacexpr.raw_tactic_expr (* Hint Extern *) + | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) open Rawterm @@ -114,11 +114,18 @@ val make_resolve_hyp : (* [make_extern name pri pattern tactic_expr] *) val make_extern : - identifier -> int -> constr_pattern -> Tacexpr.raw_tactic_expr + identifier -> int -> constr_pattern -> Tacexpr.glob_tactic_expr -> constr_label * pri_auto_tactic val set_extern_interp : - ((int * constr) list -> Tacexpr.raw_tactic_expr -> tactic) -> unit + ((int * constr) list -> Tacexpr.glob_tactic_expr -> tactic) -> unit + +val set_extern_intern_tac : + (int list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit + +val set_extern_subst_tactic : + (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) + -> unit (* Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints *) @@ -137,7 +144,7 @@ val unify_resolve : (constr * unit clausenv) -> tactic [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr_pattern -> Tacexpr.raw_tactic_expr -> tactic +val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tactic (* The Auto tactic *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 419d9c43c..b0fce4679 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -128,6 +128,7 @@ open Tacticals open Libobject open Library open Pattern +open Matching open Ast open Pcoq open Tacexpr @@ -149,7 +150,7 @@ type located_destructor_pattern = type destructor_data = { d_pat : located_destructor_pattern; d_pri : int; - d_code : identifier option * raw_tactic_expr (* should be of phylum tactic *) + d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *) } type t = (identifier,destructor_data) Nbtermdn.t @@ -204,9 +205,16 @@ let ((inDD : destructor_data_object->obj), declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); + (* TODO: substitution *) export_function = export_dd } + +let forward_intern_tac = + ref (fun _ -> failwith "intern_tac is not installed for DHyp") + +let set_extern_intern_tac f = forward_intern_tac := f let add_destructor_hint na loc pat pri code = + let code = !forward_intern_tac code in let code = begin match loc, code with | HypLocation _, TacFun ([id],body) -> (id,body) @@ -240,10 +248,10 @@ let match_dpat dp cls gls = (matches concld.d_sort (pf_type_of gls (pf_concl gls))) | _ -> error "ApplyDestructor" -let forward_tac_interp = - ref (fun _ -> failwith "tac_interp is not installed for DHyp") +let forward_interp_tactic = + ref (fun _ -> failwith "interp_tactic is not installed for DHyp") -let set_extern_interp f = forward_tac_interp := f +let set_extern_interp f = forward_interp_tactic := f let applyDestructor cls discard dd gls = let mvb = @@ -251,7 +259,7 @@ let applyDestructor cls discard dd gls = with PatternMatchingFailure -> error "No match" in let tac = match cls, dd.d_code with | Some id, (Some x, tac) -> - let arg = Reference (Ident (dummy_loc,id)) in + let arg = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in TacLetIn ([(dummy_loc, x), None, arg], tac) | None, (None, tac) -> tac | _, (Some _,_) -> error "Destructor expects an hypothesis" @@ -263,7 +271,7 @@ let applyDestructor cls discard dd gls = | (None,ConclLocation _) -> tclIDTAC | _ -> error "ApplyDestructor" in - tclTHEN (!forward_tac_interp tac) discard_0 gls + tclTHEN (!forward_interp_tactic tac) discard_0 gls (* [DHyp id gls] diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 2015f6053..b4ecfeac8 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -11,11 +11,13 @@ (*i*) open Names open Tacmach +open Tacexpr (*i*) (* Programmable destruction of hypotheses and conclusions. *) -val set_extern_interp : (Tacexpr.raw_tactic_expr -> tactic) -> unit +val set_extern_interp : (glob_tactic_expr -> tactic) -> unit +val set_extern_intern_tac : (raw_tactic_expr -> glob_tactic_expr) -> unit (* val dHyp : identifier -> tactic @@ -27,4 +29,4 @@ val h_auto_tdb : int option -> tactic val add_destructor_hint : identifier -> (bool,unit) Tacexpr.location -> - Topconstr.constr_expr -> int -> Tacexpr.raw_tactic_expr -> unit + Topconstr.constr_expr -> int -> raw_tactic_expr -> unit diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 442f18c45..2bd30c5eb 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -355,34 +355,36 @@ open Genarg (* Hint bases *) +let pr_hintbases _prc _prt = function + | None -> str " with *" + | Some [] -> mt () + | Some l -> str " with " ++ Util.prlist str l + +ARGUMENT EXTEND hintbases + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ "with" "*" ] -> [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +(* let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases" let hintbases = create_generic_entry "hintbases" rawwit_hintbases -let _ = Tacinterp.add_genarg_interp "hintbases" +let _ = Tacinterp.add_interp_genarg "hintbases" (fun ist gl x -> (in_gen wit_hintbases (out_gen (wit_opt (wit_list0 wit_string)) - (Tacinterp.genarg_interp ist gl + (Tacinterp.interp_genarg ist gl (in_gen (wit_opt (wit_list0 rawwit_string)) (out_gen rawwit_hintbases x)))))) -GEXTEND Gram - GLOBAL: hintbases; - hintbases: - [ [ "with"; "*" -> None - | "with"; l = LIST1 IDENT -> Some l - | -> Some [] ] ]; -END - -let pr_hintbases = function - | None -> str " with *" - | Some [] -> mt () - | Some l -> str " with " ++ Util.prlist str l - let _ = Pptactic.declare_extra_genarg_pprule true (rawwit_hintbases, pr_hintbases) (wit_hintbases, pr_hintbases) +*) (* V8 TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] -> diff --git a/tactics/elim.ml b/tactics/elim.ml index 85ff09f5c..9ced398dd 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -128,7 +128,7 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls -let inj x = Rawterm.AN x +let inj x = Genarg.AN x let h_decompose l c = Refiner.abstract_tactic (TacDecompose (List.map inj l,c)) (decompose_these c l) diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 8a13925c9..a14a7b2de 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -27,6 +27,7 @@ open Hiddentac open Equality open Auto open Pattern +open Matching open Hipattern open Proof_trees open Proof_type @@ -125,7 +126,7 @@ let solveArg a1 a2 tac g = let solveLeftBranch rectype g = match try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g) - with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!" + with PatternMatchingFailure -> error "Unexpected conclusion!" with | _ :: lhs :: rhs :: _ -> let (mib,mip) = Global.lookup_inductive rectype in @@ -147,7 +148,7 @@ let hd_app c = match kind_of_term c with let decideGralEquality g = match try matches (build_coq_eqdec_pattern ()) (pf_concl g) - with Pattern.PatternMatchingFailure -> + with PatternMatchingFailure -> error "The goal does not have the expected form" with | (_,typ) :: _ -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 3c3b6e7cf..f1c39f319 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -29,6 +29,7 @@ open Logic open Evar_refiner open Wcclausenv open Pattern +open Matching open Hipattern open Tacexpr open Tacticals diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index fd732563a..37b8b3356 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -19,88 +19,27 @@ open Genarg let _ = Metasyntax.add_token_obj "<-" let _ = Metasyntax.add_token_obj "->" -let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-" +let pr_orient _prc _prt = function true -> Pp.str " ->" | false -> Pp.str " <-" ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "->" ] -> [ true ] | [ "<-" ] -> [ false ] | [ ] -> [ true ] END -(* -let wit_orient, rawwit_orient = Genarg.create_arg "orient" -let orient = Pcoq.create_generic_entry "orient" rawwit_orient -let _ = Tacinterp.add_genarg_interp "orient" - (fun ist x -> - (in_gen wit_orient - (out_gen wit_bool - (Tacinterp.genarg_interp ist - (in_gen wit_bool - (out_gen rawwit_orient x)))))) - -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" - -GEXTEND Gram - GLOBAL: orient; - orient: - [ [ "->" -> true - | "<-" -> false - | -> true ] ]; -END - -let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-" - -let _ = - Pptactic.declare_extra_genarg_pprule - (rawwit_orient, pr_orient) - (wit_orient, pr_orient) -*) (* with_constr *) open Tacinterp -let pr_with_constr_gen prc = function +let pr_with_constr_gen prc _prtac = function | None -> Pp.mt () | Some c -> Pp.str " with" ++ prc c -let rawpr_with_constr = pr_with_constr_gen Ppconstr.pr_constr -let pr_with_constr = pr_with_constr_gen Printer.prterm - ARGUMENT EXTEND with_constr TYPED AS constr_opt - PRINTED BY pr_with_constr - INTERPRETED BY genarg_interp - RAW TYPED AS constr_opt - RAW PRINTED BY rawpr_with_constr + PRINTED BY pr_with_constr_gen + INTERPRETED BY interp_genarg + GLOBALIZED BY intern_genarg | [ "with" constr(c) ] -> [ Some c ] | [ ] -> [ None ] END - -(* -let wit_with_constr, rawwit_with_constr = Genarg.create_arg "with_constr" -let with_constr = Pcoq.create_generic_entry "with_constr" rawwit_with_constr -let _ = Tacinterp.add_genarg_interp "with_constr" - (fun ist x -> - (in_gen wit_with_constr - (out_gen (wit_opt wit_constr) - (Tacinterp.genarg_interp ist - (in_gen (wit_opt rawwit_constr) - (out_gen rawwit_with_constr x)))))) - -GEXTEND Gram - GLOBAL: with_constr; - with_constr: - [ [ "with"; c = Constr.constr -> Some c - | -> None ] ]; -END - -let pr_with_constr prc = function - | None -> Pp.mt () - | Some c -> Pp.str " with" ++ prc c - -let _ = - Pptactic.declare_extra_genarg_pprule - (rawwit_with_constr, pr_with_constr Ppconstr.pr_constr) - (wit_with_constr, pr_with_constr Printer.prterm) -*) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0915a2d9d..47c8319f1 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -18,9 +18,6 @@ open Extraargs (* Equality *) open Equality -(* V8 TACTIC EXTEND rewrite - [ "rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c] -END*) TACTIC EXTEND Rewrite [ "Rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c] END @@ -86,13 +83,13 @@ let h_injHyp id = h_injection (Some id) TACTIC EXTEND ConditionalRewrite [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ] - -> [ conditional_rewrite b (Tacinterp.interp tac) c ] + -> [ conditional_rewrite b (snd tac) c ] END TACTIC EXTEND ConditionalRewriteIn [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) "in" ident(h) ] - -> [ conditional_rewrite_in b h (Tacinterp.interp tac) c ] + -> [ conditional_rewrite_in b h (snd tac) c ] END TACTIC EXTEND DependentRewrite @@ -134,13 +131,6 @@ TACTIC EXTEND Inversion -> [ dinv (Some false) c id ] END -(* V8 TACTIC EXTEND inversionclear -| [ "inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ] -| [ "inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ] - -> [ invIn_gen (Some true) id l] -| [ "dependent" "inversion_clear" quantified_hypothesis(id) with_constr(c) ] - -> [ dinv (Some true) c id ] -END*) TACTIC EXTEND InversionClear | [ "Inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ] | [ "Inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ] @@ -164,7 +154,7 @@ TACTIC EXTEND Autorewrite [ "AutoRewrite" "[" ne_preident_list(l) "]" ] -> [ autorewrite Refiner.tclIDTAC l ] | [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] -> - [ autorewrite (Tacinterp.interp t) l ] + [ autorewrite (snd t) l ] END let add_rewrite_hint name ort t lcsr = diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 3e6542853..a502b4110 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -60,7 +60,7 @@ let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) (* Context management *) -let inj x = AN x +let inj x = Genarg.AN x let h_clear l = abstract_tactic (TacClear (List.map inj l)) (clear l) let h_clear_body l = abstract_tactic (TacClearBody (List.map inj l)) (clear_body l) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 53ffa7a35..c11fd1699 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -21,6 +21,7 @@ open Environ open Proof_trees open Clenv open Pattern +open Matching open Coqlib open Declarations diff --git a/tactics/inv.ml b/tactics/inv.ml index 7ea582692..233c149cb 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -33,6 +33,7 @@ open Elim open Equality open Typing open Pattern +open Matching open Rawterm let collect_meta_variables c = diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4 index 11958a0ea..0c8f9bb4a 100644 --- a/tactics/newtauto.ml4 +++ b/tactics/newtauto.ml4 @@ -226,12 +226,12 @@ let lfo_wrap n gl= TACTIC EXTEND NewIntuition [ "NewIntuition" ] -> [ newtauto true default_stac ] - |[ "NewIntuition" tactic(t)] -> [ newtauto true (interp t) ] + |[ "NewIntuition" tactic(t)] -> [ newtauto true (snd t) ] END TACTIC EXTEND Intuition1 [ "Intuition1" ] -> [ newtauto false default_stac ] - |[ "Intuition1" tactic(t)] -> [ newtauto false (interp t) ] + |[ "Intuition1" tactic(t)] -> [ newtauto false (snd t) ] END TACTIC EXTEND NewTauto diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c28e21e79..c77a18db4 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -16,6 +16,7 @@ open Entries open Dyn open Libobject open Pattern +open Matching open Pp open Rawterm open Sign @@ -68,7 +69,7 @@ type value = | VTactic of loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *) | VRTactic of (goal list sigma * validation) (* For Match results *) (* Not a true value *) - | VFun of (identifier * value) list * identifier option list *raw_tactic_expr + | VFun of (identifier*value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int | VIdentifier of identifier (* idents which are not bound, as in "Intro H" *) @@ -243,7 +244,7 @@ let coerce_to_inductive = function (* Summary and Object declaration *) let mactab = ref Gmap.empty -let lookup qid = Gmap.find (locate_tactic qid) !mactab +let lookup r = Gmap.find r !mactab let _ = let init () = mactab := Gmap.empty in @@ -256,14 +257,34 @@ let _ = Summary.survive_section = false } (* Interpretation of extra generic arguments *) -type genarg_interp_type = - interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument -let extragenargtab = ref (Gmap.empty : (string,genarg_interp_type) Gmap.t) -let add_genarg_interp id f = extragenargtab := Gmap.add id f !extragenargtab -let lookup_genarg_interp id = +type glob_sign = { + ltacvars : identifier list * identifier list; + (* ltac variables and the subset of vars introduced by Intro/Let/... *) + ltacrecvars : (identifier * ltac_constant) list; + (* ltac recursive names *) + metavars : int list; + (* metavariables introduced by patterns *) + gsigma : Evd.evar_map; + genv : Environ.env } + +type interp_genarg_type = + (glob_sign -> raw_generic_argument -> glob_generic_argument) * + (interp_sign -> goal sigma -> glob_generic_argument -> + closed_generic_argument) * + (Names.substitution -> glob_generic_argument -> glob_generic_argument) + +let extragenargtab = + ref (Gmap.empty : (string,interp_genarg_type) Gmap.t) +let add_interp_genarg id f = + extragenargtab := Gmap.add id f !extragenargtab +let lookup_genarg id = try Gmap.find id !extragenargtab with Not_found -> failwith ("No interpretation function found for entry "^id) +let lookup_genarg_glob id = let (f,_,_) = lookup_genarg id in f +let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f +let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f + (* Unboxes VRec *) let unrec = function | VRec v -> !v @@ -275,19 +296,34 @@ let unrec = function (* We have identifier <| global_reference <| constr *) -let find_ident id (lfun,_,_,env) = - List.mem id lfun or - List.mem id (ids_of_named_context (Environ.named_context env)) +let find_ident id sign = + List.mem id (fst sign.ltacvars) or + List.mem id (ids_of_named_context (Environ.named_context sign.genv)) + +let find_recvar qid sign = List.assoc qid sign.ltacrecvars + +(* a "var" is a ltac var or a var introduced by an intro tactic *) +let find_var id sign = List.mem id (fst sign.ltacvars) + +(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *) +let find_ctxvar id sign = List.mem id (snd sign.ltacvars) -(* Globalize a name which can be fresh *) -let glob_ident l ist id = +(* a "ltacvar" is an ltac var (Let-In/Fun/...) *) +let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign) + +let find_hyp id sign = + List.mem id (ids_of_named_context (Environ.named_context sign.genv)) + +(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *) +(* be fresh in which case it is binding later on *) +let intern_ident l ist id = (* We use identifier both for variables and new names; thus nothing to do *) - if find_ident id ist then () else l:=id::!l; + if find_ident id ist then () else l:=(id::fst !l,id::snd !l); id -let glob_name l ist = function +let intern_name l ist = function | Anonymous -> Anonymous - | Name id -> Name (glob_ident l ist id) + | Name id -> Name (intern_ident l ist id) let vars_of_ist (lfun,_,_,env) = List.fold_left (fun s id -> Idset.add id s) @@ -301,150 +337,187 @@ let get_current_context () = let strict_check = ref false (* Globalize a name which must be bound -- actually just check it is bound *) -let glob_hyp ist (loc,id) = +let intern_hyp ist (loc,id) = let (_,env) = get_current_context () in if (not !strict_check) or find_ident id ist then id else -(* - try let _ = lookup (make_short_qualid id) in id - with Not_found -> -*) Pretype_errors.error_var_not_found_loc loc id -let glob_lochyp ist (_loc,_ as locid) = (loc,glob_hyp ist locid) +let intern_lochyp ist (_loc,_ as locid) = (loc,intern_hyp ist locid) let error_unbound_metanum loc n = user_err_loc - (loc,"glob_qualid_or_metanum", str "?" ++ int n ++ str " is unbound") + (loc,"intern_qualid_or_metanum", str "?" ++ int n ++ str " is unbound") -let glob_metanum (_,lmeta,_,_) loc n = - if List.mem n lmeta then n else error_unbound_metanum loc n +let intern_metanum sign loc n = + if List.mem n sign.metavars then n else error_unbound_metanum loc n -let glob_hyp_or_metanum ist = function - | AN id -> AN (glob_hyp ist (loc,id)) - | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n) +let intern_hyp_or_metanum ist = function + | AN id -> AN (intern_hyp ist (loc,id)) + | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n) -let glob_qualid_or_metanum ist = function - | AN qid -> AN (Qualid(loc, - shortest_qualid_of_global (vars_of_ist ist) (Nametab.global qid))) - | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n) +let intern_inductive ist = function + | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) + | r -> ArgArg (Nametab.global_inductive r) -let glob_reference ist = function - | Ident (loc,id) as r when find_ident id ist -> r - | r -> Qualid (loc, - shortest_qualid_of_global (vars_of_ist ist) (Nametab.global r)) +let intern_or_metanum f ist = function + | AN x -> AN (f ist x) + | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n) -let glob_ltac_qualid ist ref = - let (loc,qid) = qualid_of_reference ref in - try Qualid (loc,qualid_of_sp (locate_tactic qid)) - with Not_found -> glob_reference ist ref +let intern_global_reference ist = function + | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id) + | r -> ArgArg (loc,Nametab.global r) -let glob_ltac_reference strict ist = function - | Ident (_loc,id) when not strict or find_ident id ist -> Ident (loc,id) - | r -> glob_ltac_qualid ist r +let intern_tac_ref ist = function + | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id) + | Ident (loc,id) -> + ArgArg + (try find_recvar id ist + with Not_found -> locate_tactic (make_short_qualid id)) + | r -> + let (loc,qid) = qualid_of_reference r in + ArgArg (locate_tactic qid) + +let intern_tactic_reference ist r = + try intern_tac_ref ist r + with Not_found -> + let (loc,qid) = qualid_of_reference r in + error_global_not_found_loc loc qid + +let intern_constr_reference strict ist = function + | Ident (loc,id) as x when find_hyp id ist -> + RVar (loc,id), if strict then None else Some (CRef x) + | r -> + let loc,qid = qualid_of_reference r in + RRef (loc,Nametab.locate qid), (*Long names can't be Intro's names*) None + +let intern_reference strict ist r = + try Reference (intern_tac_ref ist r) + with Not_found -> + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + with Not_found -> + match r with + | Ident (loc,id) when not strict -> Identifier id + | _ -> + let (loc,qid) = qualid_of_reference r in + error_global_not_found_loc loc qid -let rec glob_intro_pattern lf ist = function +let rec intern_intro_pattern lf ist = function | IntroOrAndPattern l -> - IntroOrAndPattern (List.map (List.map (glob_intro_pattern lf ist)) l) + IntroOrAndPattern (List.map (List.map (intern_intro_pattern lf ist)) l) | IntroWildcard -> IntroWildcard | IntroIdentifier id -> - IntroIdentifier (glob_ident lf ist id) + IntroIdentifier (intern_ident lf ist id) -let glob_quantified_hypothesis ist x = +let intern_quantified_hypothesis ist x = (* We use identifier both for variables and quantified hyps (no way to statically check the existence of a quantified hyp); thus nothing to do *) x -let glob_constr (lfun,_,sigma,env) c = - let _ = +let intern_constr {ltacvars=lfun; metavars=lmatch; gsigma=sigma; genv=env} c = + let c' = Constrintern.for_grammar (Constrintern.interp_rawconstr_gen false - sigma env [] false (lfun,[])) c - in c + sigma env [] (Some lmatch) (fst lfun,[])) c + in (c',if !strict_check then None else Some c) (* Globalize bindings *) -let glob_binding ist (loc,b,c) = - (loc,glob_quantified_hypothesis ist b,glob_constr ist c) +let intern_binding ist (loc,b,c) = + (loc,intern_quantified_hypothesis ist b,intern_constr ist c) -let glob_bindings ist = function +let intern_bindings ist = function | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map (glob_constr ist) l) - | ExplicitBindings l -> ExplicitBindings (List.map (glob_binding ist) l) + | ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l) + | ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l) -let glob_constr_with_bindings ist (c,bl) = - (glob_constr ist c, glob_bindings ist bl) +let intern_constr_with_bindings ist (c,bl) = + (intern_constr ist c, intern_bindings ist bl) -let glob_clause_pattern ist (l,occl) = +let intern_clause_pattern ist (l,occl) = let rec check = function | (hyp,l) :: rest -> let (_loc,_ as id) = skip_metaid hyp in - (AI(loc,glob_hyp ist id),l)::(check rest) + ((loc,intern_hyp ist id),l)::(check rest) | [] -> [] in (l,check occl) -let glob_induction_arg ist = function - | ElimOnConstr c -> ElimOnConstr (glob_constr ist c) +let intern_induction_arg ist = function + | ElimOnConstr c -> ElimOnConstr (intern_constr ist c) | ElimOnAnonHyp n as x -> x | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id) (* Globalizes a reduction expression *) -let glob_evaluable_or_metanum ist = function - | AN qid -> AN (glob_reference ist qid) - | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n) - -let glob_unfold ist (l,qid) = (l,glob_evaluable_or_metanum ist qid) - -let glob_flag ist red = - { red with rConst = List.map (glob_evaluable_or_metanum ist) red.rConst } - -let glob_constr_occurrence ist (l,c) = (l,glob_constr ist c) - -let glob_redexp ist = function - | Unfold l -> Unfold (List.map (glob_unfold ist) l) - | Fold l -> Fold (List.map (glob_constr ist) l) - | Cbv f -> Cbv (glob_flag ist f) - | Lazy f -> Lazy (glob_flag ist f) - | Pattern l -> Pattern (List.map (glob_constr_occurrence ist) l) - | Simpl o -> Simpl (option_app (glob_constr_occurrence ist) o) +let intern_evaluable_or_metanum ist = function + | AN qid -> + let e = match qid with + | Ident (loc,id) when find_ctxvar id ist -> + ArgArg (EvalVarRef id, Some id) + | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id) + | r -> + let e = match fst (intern_constr_reference true ist r) with + | RRef (_,ConstRef c) -> EvalConstRef c + | RRef (_,VarRef c) | RVar (_,c) -> EvalVarRef c + | _ -> error_not_evaluable (pr_reference r) in + let short_name = match r with + | Ident (_,id) when not !strict_check -> Some id + | _ -> None in + ArgArg (e,short_name) + in AN e + | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n) + +let intern_unfold ist (l,qid) = (l,intern_evaluable_or_metanum ist qid) + +let intern_flag ist red = + { red with rConst = List.map (intern_evaluable_or_metanum ist) red.rConst } + +let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c) + +let intern_redexp ist = function + | Unfold l -> Unfold (List.map (intern_unfold ist) l) + | Fold l -> Fold (List.map (intern_constr ist) l) + | Cbv f -> Cbv (intern_flag ist f) + | Lazy f -> Lazy (intern_flag ist f) + | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) + | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o) | (Red _ | Hnf as r) -> r - | ExtraRedExpr (s,c) -> ExtraRedExpr (s, glob_constr ist c) + | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c) (* Interprets an hypothesis name *) -let glob_hyp_location ist = function +let intern_hyp_location ist = function | InHyp id -> let (_loc,_ as id) = skip_metaid id in - InHyp (AI(loc,glob_hyp ist id)) + InHyp (loc,intern_hyp ist id) | InHypType id -> let (_loc,_ as id) = skip_metaid id in - InHypType (AI(loc,glob_hyp ist id)) + InHypType (loc,intern_hyp ist id) (* Reads a pattern *) -let glob_pattern evc env lfun = function +let intern_pattern evc env lfun = function | Subterm (ido,pc) -> let lfun = List.map (fun id -> (id, mkVar id)) lfun in - let (metas,_) = interp_constrpattern_gen evc env (lfun,[]) pc in - metas, Subterm (ido,pc) + let (metas,pat) = interp_constrpattern_gen evc env (lfun,[]) pc in + metas, Subterm (ido,pat) | Term pc -> let lfun = List.map (fun id -> (id, mkVar id)) lfun in - let (metas,_) = interp_constrpattern_gen evc env (lfun,[]) pc in - metas, Term pc + let (metas,pat) = interp_constrpattern_gen evc env (lfun,[]) pc in + metas, Term pat -let glob_constr_may_eval ist = function - | ConstrEval (r,c) -> ConstrEval (glob_redexp ist r,glob_constr ist c) +let intern_constr_may_eval ist = function + | ConstrEval (r,c) -> ConstrEval (intern_redexp ist r,intern_constr ist c) | ConstrContext (locid,c) -> - ConstrContext ((loc,glob_hyp ist locid),glob_constr ist c) - | ConstrTypeOf c -> ConstrTypeOf (glob_constr ist c) - | ConstrTerm c -> ConstrTerm (glob_constr ist c) + ConstrContext ((loc,intern_hyp ist locid),intern_constr ist c) + | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c) + | ConstrTerm c -> ConstrTerm (intern_constr ist c) (* Reads the hypotheses of a Match Context rule *) -let rec glob_match_context_hyps evc env lfun = function +let rec intern_match_context_hyps evc env lfun = function | (NoHypId mp)::tl -> - let metas1, pat = glob_pattern evc env lfun mp in - let lfun, metas2, hyps = glob_match_context_hyps evc env lfun tl in + let metas1, pat = intern_pattern evc env lfun mp in + let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in lfun, metas1@metas2, (NoHypId pat)::hyps | (Hyp ((_,s) as locs,mp))::tl -> - let metas1, pat = glob_pattern evc env lfun mp in - let lfun, metas2, hyps = glob_match_context_hyps evc env lfun tl in + let metas1, pat = intern_pattern evc env lfun mp in + let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in s::lfun, metas1@metas2, Hyp (locs,pat)::hyps | [] -> lfun, [], [] @@ -459,7 +532,7 @@ let extract_names lrc = (fun ((loc,name),_) l -> if List.mem name l then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times"); + (loc, "intern_tactic", str "This variable is bound several times"); name::l) lrc [] @@ -472,236 +545,244 @@ let extract_let_names lrc = name::l) lrc [] -(* Globalizes tactics *) -let rec glob_atomic lf (_,_,_,_ as ist) = function +(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) +let rec intern_atomic lf ist x = + match (x:raw_atomic_tactic_expr) with (* Basic tactics *) | TacIntroPattern l -> - TacIntroPattern (List.map (glob_intro_pattern lf ist) l) - | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp) + TacIntroPattern (List.map (intern_intro_pattern lf ist) l) + | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) | TacIntroMove (ido,ido') -> - TacIntroMove (option_app (glob_ident lf ist) ido, - option_app (fun (_loc,_ as x) -> (loc,glob_hyp ist x)) ido') + TacIntroMove (option_app (intern_ident lf ist) ido, + option_app (fun (_loc,_ as x) -> (loc,intern_hyp ist x)) ido') | TacAssumption -> TacAssumption - | TacExact c -> TacExact (glob_constr ist c) - | TacApply cb -> TacApply (glob_constr_with_bindings ist cb) + | TacExact c -> TacExact (intern_constr ist c) + | TacApply cb -> TacApply (intern_constr_with_bindings ist cb) | TacElim (cb,cbo) -> - TacElim (glob_constr_with_bindings ist cb, - option_app (glob_constr_with_bindings ist) cbo) - | TacElimType c -> TacElimType (glob_constr ist c) - | TacCase cb -> TacCase (glob_constr_with_bindings ist cb) - | TacCaseType c -> TacCaseType (glob_constr ist c) - | TacFix (idopt,n) -> TacFix (option_app (glob_ident lf ist) idopt,n) + TacElim (intern_constr_with_bindings ist cb, + option_app (intern_constr_with_bindings ist) cbo) + | TacElimType c -> TacElimType (intern_constr ist c) + | TacCase cb -> TacCase (intern_constr_with_bindings ist cb) + | TacCaseType c -> TacCaseType (intern_constr ist c) + | TacFix (idopt,n) -> TacFix (option_app (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> - let f (id,n,c) = (glob_ident lf ist id,n,glob_constr ist c) in - TacMutualFix (glob_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (option_app (glob_ident lf ist) idopt) + let f (id,n,c) = (intern_ident lf ist id,n,intern_constr ist c) in + TacMutualFix (intern_ident lf ist id, n, List.map f l) + | TacCofix idopt -> TacCofix (option_app (intern_ident lf ist) idopt) | TacMutualCofix (id,l) -> - let f (id,c) = (glob_ident lf ist id,glob_constr ist c) in - TacMutualCofix (glob_ident lf ist id, List.map f l) - | TacCut c -> TacCut (glob_constr ist c) + let f (id,c) = (intern_ident lf ist id,intern_constr ist c) in + TacMutualCofix (intern_ident lf ist id, List.map f l) + | TacCut c -> TacCut (intern_constr ist c) | TacTrueCut (ido,c) -> - TacTrueCut (option_app (glob_ident lf ist) ido, glob_constr ist c) - | TacForward (b,na,c) -> TacForward (b,glob_name lf ist na,glob_constr ist c) - | TacGeneralize cl -> TacGeneralize (List.map (glob_constr ist) cl) - | TacGeneralizeDep c -> TacGeneralizeDep (glob_constr ist c) + TacTrueCut (option_app (intern_ident lf ist) ido, intern_constr ist c) + | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c) + | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) + | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) | TacLetTac (id,c,clp) -> - TacLetTac (id,glob_constr ist c,glob_clause_pattern ist clp) - | TacInstantiate (n,c) -> TacInstantiate (n,glob_constr ist c) + let id = intern_ident lf ist id in + TacLetTac (id,intern_constr ist c,intern_clause_pattern ist clp) + | TacInstantiate (n,c) -> TacInstantiate (n,intern_constr ist c) (* Automation tactics *) | TacTrivial l -> TacTrivial l | TacAuto (n,l) -> TacAuto (n,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,(_loc,_ as id)) -> - TacDestructHyp(b,(loc,glob_hyp ist id)) + TacDestructHyp(b,(loc,intern_hyp ist id)) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) | TacDAuto (n,p) -> TacDAuto (n,p) (* Derived basic tactics *) - | TacOldInduction h -> TacOldInduction (glob_quantified_hypothesis ist h) + | TacOldInduction h -> TacOldInduction (intern_quantified_hypothesis ist h) | TacNewInduction (c,cbo,ids) -> - TacNewInduction (glob_induction_arg ist c, - option_app (glob_constr_with_bindings ist) cbo, - List.map (List.map (glob_ident lf ist)) ids) - | TacOldDestruct h -> TacOldDestruct (glob_quantified_hypothesis ist h) + TacNewInduction (intern_induction_arg ist c, + option_app (intern_constr_with_bindings ist) cbo, + List.map (List.map (intern_ident lf ist)) ids) + | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h) | TacNewDestruct (c,cbo,ids) -> - TacNewDestruct (glob_induction_arg ist c, - option_app (glob_constr_with_bindings ist) cbo, - List.map (List.map (glob_ident lf ist)) ids) + TacNewDestruct (intern_induction_arg ist c, + option_app (intern_constr_with_bindings ist) cbo, + List.map (List.map (intern_ident lf ist)) ids) | TacDoubleInduction (h1,h2) -> - let h1 = glob_quantified_hypothesis ist h1 in - let h2 = glob_quantified_hypothesis ist h2 in + let h1 = intern_quantified_hypothesis ist h1 in + let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) - | TacDecomposeAnd c -> TacDecomposeAnd (glob_constr ist c) - | TacDecomposeOr c -> TacDecomposeOr (glob_constr ist c) + | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c) + | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c) | TacDecompose (l,c) -> - let l = List.map (glob_qualid_or_metanum ist) l in - TacDecompose (l,glob_constr ist c) - | TacSpecialize (n,l) -> TacSpecialize (n,glob_constr_with_bindings ist l) - | TacLApply c -> TacLApply (glob_constr ist c) + let l = List.map (intern_or_metanum intern_inductive ist) l in + TacDecompose (l,intern_constr ist c) + | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l) + | TacLApply c -> TacLApply (intern_constr ist c) (* Context management *) - | TacClear l -> TacClear (List.map (glob_hyp_or_metanum ist) l) - | TacClearBody l -> TacClearBody (List.map (glob_hyp_or_metanum ist) l) + | TacClear l -> TacClear (List.map (intern_hyp_or_metanum ist) l) + | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metanum ist) l) | TacMove (dep,id1,id2) -> - TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2) - | TacRename (id1,id2) -> TacRename (glob_lochyp ist id1, glob_lochyp ist id2) + TacMove (dep,intern_lochyp ist id1,intern_lochyp ist id2) + | TacRename (id1,id2) -> TacRename (intern_lochyp ist id1, intern_lochyp ist id2) (* Constructors *) - | TacLeft bl -> TacLeft (glob_bindings ist bl) - | TacRight bl -> TacRight (glob_bindings ist bl) - | TacSplit (b,bl) -> TacSplit (b,glob_bindings ist bl) - | TacAnyConstructor t -> TacAnyConstructor (option_app (glob_tactic ist) t) - | TacConstructor (n,bl) -> TacConstructor (n, glob_bindings ist bl) + | TacLeft bl -> TacLeft (intern_bindings ist bl) + | TacRight bl -> TacRight (intern_bindings ist bl) + | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl) + | TacAnyConstructor t -> TacAnyConstructor (option_app (intern_tactic ist) t) + | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl) (* Conversion *) | TacReduce (r,cl) -> - TacReduce (glob_redexp ist r, List.map (glob_hyp_location ist) cl) + TacReduce (intern_redexp ist r, List.map (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> - TacChange (option_app (glob_constr_occurrence ist) occl, - glob_constr ist c, List.map (glob_hyp_location ist) cl) + TacChange (option_app (intern_constr_occurrence ist) occl, + intern_constr ist c, List.map (intern_hyp_location ist) cl) (* Equivalence relations *) | TacReflexivity -> TacReflexivity | TacSymmetry -> TacSymmetry - | TacTransitivity c -> TacTransitivity (glob_constr ist c) + | TacTransitivity c -> TacTransitivity (intern_constr ist c) (* For extensions *) | TacExtend (_loc,opn,l) -> let _ = lookup_tactic opn in - TacExtend (loc,opn,List.map (glob_genarg ist) l) - | TacAlias (_,l,body) as t -> - (* failwith "TacAlias globalisation: TODO" *) - t + TacExtend (loc,opn,List.map (intern_genarg ist) l) + | TacAlias (s,l,body) -> + TacAlias (s,List.map (fun (id,a) -> (id,intern_genarg ist a)) l,intern_tactic ist body) -and glob_tactic ist tac = snd (glob_tactic_seq ist tac) +and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) -and glob_tactic_seq (lfun,lmeta,sigma,env as ist) = function +and intern_tactic_seq ist = function | TacAtom (_loc,t) -> - let lf = ref lfun in - let t = glob_atomic lf ist t in + let lf = ref ist.ltacvars in + let t = intern_atomic lf ist t in !lf, TacAtom (loc, t) - | TacFun tacfun -> lfun, TacFun (glob_tactic_fun ist tacfun) + | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun) | TacLetRecIn (lrc,u) -> let names = extract_names lrc in - let ist = (names@lfun,lmeta,sigma,env) in - let lrc = List.map (fun (n,b) -> (n,glob_tactic_fun ist b)) lrc in - lfun, TacLetRecIn (lrc,glob_tactic ist u) + let (l1,l2) = ist.ltacvars in + let ist = { ist with ltacvars = (names@l1,l2) } in + let lrc = List.map (fun (n,b) -> (n,intern_tactic_fun ist b)) lrc in + ist.ltacvars, TacLetRecIn (lrc,intern_tactic ist u) | TacLetIn (l,u) -> - let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist) - c,glob_tacarg !strict_check ist b)) l in - let ist' = ((extract_let_names l)@lfun,lmeta,sigma,env) in - lfun, TacLetIn (l,glob_tactic ist' u) + let l = List.map + (fun (n,c,b) -> + (n,option_app (intern_constr_may_eval ist) c, intern_tacarg !strict_check ist b)) l in + let (l1,l2) = ist.ltacvars in + let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in + ist.ltacvars, TacLetIn (l,intern_tactic ist' u) | TacLetCut l -> - let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg !strict_check - ist t) in - lfun, TacLetCut (List.map f l) + let f (n,c,t) = (n,intern_constr_may_eval ist c,intern_tacarg !strict_check ist t) in + ist.ltacvars, TacLetCut (List.map f l) | TacMatchContext (lr,lmr) -> - lfun, TacMatchContext(lr, glob_match_rule ist lmr) + ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr) | TacMatch (c,lmr) -> - lfun, TacMatch (glob_constr_may_eval ist c,glob_match_rule ist lmr) - | TacId -> lfun, TacId - | TacFail _ as x -> lfun, x - | TacProgress tac -> lfun, TacProgress (glob_tactic ist tac) - | TacAbstract (tac,s) -> lfun, TacAbstract (glob_tactic ist tac,s) + ist.ltacvars, TacMatch (intern_constr_may_eval ist c,intern_match_rule ist lmr) + | TacId -> ist.ltacvars, TacId + | TacFail _ as x -> ist.ltacvars, x + | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac) + | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s) | TacThen (t1,t2) -> - let lfun', t1 = glob_tactic_seq ist t1 in - let lfun'', t2 = glob_tactic_seq (lfun',lmeta,sigma,env) t2 in + let lfun', t1 = intern_tactic_seq ist t1 in + let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in lfun'', TacThen (t1,t2) | TacThens (t,tl) -> - let lfun', t = glob_tactic_seq ist t in + let lfun', t = intern_tactic_seq ist t in (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *) - lfun', TacThens (t, List.map (glob_tactic (lfun',lmeta,sigma,env)) tl) - | TacDo (n,tac) -> lfun, TacDo (n,glob_tactic ist tac) - | TacTry tac -> lfun, TacTry (glob_tactic ist tac) - | TacInfo tac -> lfun, TacInfo (glob_tactic ist tac) - | TacRepeat tac -> lfun, TacRepeat (glob_tactic ist tac) + lfun', + TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl) + | TacDo (n,tac) -> ist.ltacvars, TacDo (n,intern_tactic ist tac) + | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac) + | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac) + | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac) | TacOrelse (tac1,tac2) -> - lfun, TacOrelse (glob_tactic ist tac1,glob_tactic ist tac2) - | TacFirst l -> lfun, TacFirst (List.map (glob_tactic ist) l) - | TacSolve l -> lfun, TacSolve (List.map (glob_tactic ist) l) - | TacArg a -> lfun, TacArg (glob_tacarg true ist a) + ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2) + | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l) + | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l) + | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a) -and glob_tactic_fun (lfun,lmeta,sigma,env) (var,body) = - let lfun' = List.rev_append (filter_some var) lfun in - (var,glob_tactic (lfun',lmeta,sigma,env) body) +and intern_tactic_fun ist (var,body) = + let (l1,l2) = ist.ltacvars in + let lfun' = List.rev_append (filter_some var) l1 in + (var,intern_tactic { ist with ltacvars = (lfun',l2) } body) -and glob_tacarg strict ist = function +and intern_tacarg strict ist = function | TacVoid -> TacVoid - | Reference r -> Reference (glob_ltac_reference strict ist r) + | Reference r -> intern_reference strict ist r + | Identifier id -> anomaly "Not used only in raw_tactic_expr" | Integer n -> Integer n - | ConstrMayEval c -> ConstrMayEval (glob_constr_may_eval ist c) - | MetaNumArg (_loc,n) -> MetaNumArg (loc,glob_metanum ist loc n) + | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) | MetaIdArg (_loc,_) -> error_syntactic_metavariables_not_allowed loc | TacCall (_loc,f,l) -> TacCall (_loc, - glob_ltac_reference strict ist f, - List.map (glob_tacarg !strict_check ist) l) - | Tacexp t -> Tacexp (glob_tactic ist t) + intern_tactic_reference ist f, + List.map (intern_tacarg !strict_check ist) l) + | Tacexp t -> Tacexp (intern_tactic ist t) | TacDynamic(_,t) as x -> (match tag t with - | "tactic"|"value"|"constr" -> x - | s -> anomaly_loc (loc, "Tacinterp.val_interp", + | "tactic" | "value" | "constr" -> x + | s -> anomaly_loc (loc, "", str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) -and glob_match_rule (lfun,lmeta,sigma,env as ist) = function +and intern_match_rule ist = function | (All tc)::tl -> - (All (glob_tactic ist tc))::(glob_match_rule ist tl) + All (intern_tactic ist tc) :: (intern_match_rule ist tl) | (Pat (rl,mp,tc))::tl -> - let lfun',metas1,hyps = glob_match_context_hyps Evd.empty env lfun rl in - let metas2,pat = glob_pattern Evd.empty env lfun mp in + let {ltacvars=(lfun,l2); metavars=lmeta; gsigma=sigma; genv=env} = ist in + let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in + let metas2,pat = intern_pattern sigma env lfun mp in let metas = list_uniquize (metas1@metas2@lmeta) in - (Pat (hyps,pat,glob_tactic (lfun',metas,sigma,env) tc)) - ::(glob_match_rule ist tl) + let ist' = { ist with ltacvars = (lfun',l2); metavars = metas } in + Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl) | [] -> [] -and glob_genarg ist x = +and intern_genarg ist x = match genarg_tag x with - | BoolArgType -> in_gen rawwit_bool (out_gen rawwit_bool x) - | IntArgType -> in_gen rawwit_int (out_gen rawwit_int x) + | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x) + | IntArgType -> in_gen globwit_int (out_gen rawwit_int x) | IntOrVarArgType -> let f = function - | ArgVar (_loc,id) -> ArgVar (loc,glob_hyp ist (loc,id)) + | ArgVar (_loc,id) -> ArgVar (loc,intern_hyp ist (loc,id)) | ArgArg n as x -> x in - in_gen rawwit_int_or_var (f (out_gen rawwit_int_or_var x)) + in_gen globwit_int_or_var (f (out_gen rawwit_int_or_var x)) | StringArgType -> - in_gen rawwit_string (out_gen rawwit_string x) + in_gen globwit_string (out_gen rawwit_string x) | PreIdentArgType -> - in_gen rawwit_pre_ident (out_gen rawwit_pre_ident x) + in_gen globwit_pre_ident (out_gen rawwit_pre_ident x) | IdentArgType -> - in_gen rawwit_ident (glob_hyp ist (dummy_loc,out_gen rawwit_ident x)) + in_gen globwit_ident (intern_hyp ist (dummy_loc,out_gen rawwit_ident x)) | RefArgType -> - in_gen rawwit_ref (glob_ltac_reference !strict_check ist - (out_gen rawwit_ref x)) + in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x)) | SortArgType -> - in_gen rawwit_sort (out_gen rawwit_sort x) + in_gen globwit_sort (out_gen rawwit_sort x) | ConstrArgType -> - in_gen rawwit_constr (glob_constr ist (out_gen rawwit_constr x)) + in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x)) | ConstrMayEvalArgType -> - in_gen rawwit_constr_may_eval (glob_constr_may_eval ist - (out_gen rawwit_constr_may_eval x)) + in_gen globwit_constr_may_eval + (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x)) | QuantHypArgType -> - in_gen rawwit_quant_hyp - (glob_quantified_hypothesis ist (out_gen rawwit_quant_hyp x)) + in_gen globwit_quant_hyp + (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x)) | RedExprArgType -> - in_gen rawwit_red_expr (glob_redexp ist (out_gen rawwit_red_expr x)) + in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x)) | TacticArgType -> - in_gen rawwit_tactic (glob_tactic ist (out_gen rawwit_tactic x)) + in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x)) | CastedOpenConstrArgType -> - in_gen rawwit_casted_open_constr - (glob_constr ist (out_gen rawwit_casted_open_constr x)) + in_gen globwit_casted_open_constr + (intern_constr ist (out_gen rawwit_casted_open_constr x)) | ConstrWithBindingsArgType -> - in_gen rawwit_constr_with_bindings - (glob_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) - | List0ArgType _ -> app_list0 (glob_genarg ist) x - | List1ArgType _ -> app_list1 (glob_genarg ist) x - | OptArgType _ -> app_opt (glob_genarg ist) x - | PairArgType _ -> app_pair (glob_genarg ist) (glob_genarg ist) x - | ExtraArgType s -> x + in_gen globwit_constr_with_bindings + (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) + | List0ArgType _ -> app_list0 (intern_genarg ist) x + | List1ArgType _ -> app_list1 (intern_genarg ist) x + | OptArgType _ -> app_opt (intern_genarg ist) x + | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x + | ExtraArgType s -> lookup_genarg_glob s ist x -(**** End Globalization ****) +(************* End globalization ************) + +(***************************************************************************) +(* Evaluation/interpretation *) (* Associates variables with values and gives the remaining variables and values *) @@ -722,12 +803,14 @@ let give_context ctxt = function | None -> [] | Some id -> [id,VConstr_context ctxt] -(* Reads a pattern *) +(* Reads a pattern by substituing vars of lfun *) +let eval_pattern lfun c = + let lvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lfun in + instantiate_pattern lvar c + let read_pattern evc env lfun = function - | Subterm (ido,pc) -> - Subterm (ido,snd (interp_constrpattern_gen evc env lfun pc)) - | Term pc -> - Term (snd (interp_constrpattern_gen evc env lfun pc)) + | Subterm (ido,pc) -> Subterm (ido,eval_pattern lfun pc) + | Term pc -> Term (eval_pattern lfun pc) (* Reads the hypotheses of a Match Context rule *) let rec read_match_context_hyps evc env lfun lidh = function @@ -748,8 +831,8 @@ let rec read_match_context_hyps evc env lfun lidh = function let rec read_match_rule evc env lfun = function | (All tc)::tl -> (All tc)::(read_match_rule evc env lfun tl) | (Pat (rl,mp,tc))::tl -> - (Pat (read_match_context_hyps evc env lfun [] rl, - read_pattern evc env lfun mp,tc)) + Pat (read_match_context_hyps evc env lfun [] rl, + read_pattern evc env lfun mp,tc) ::(read_match_rule evc env lfun tl) | [] -> [] @@ -778,7 +861,7 @@ let rec verify_metas_coherence gl lcm = function (* Tries to match a pattern and a constr *) let apply_matching pat csr = try - (Pattern.matches pat csr) + (matches pat csr) with PatternMatchingFailure -> raise No_match @@ -799,7 +882,7 @@ let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt = | Term t -> (try let lmeta = - verify_metas_coherence gl lmatch (Pattern.matches t hyp) in + verify_metas_coherence gl lmatch (matches t hyp) in (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None) with | PatternMatchingFailure | Not_coherent_metas -> apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl) @@ -855,8 +938,7 @@ let constr_to_qid loc c = let check_clause_pattern ist gl (l,occl) = let sign = pf_hyps gl in let rec check acc = function - | (hyp,l) :: rest -> - let _,hyp = skip_metaid hyp in + | ((_,hyp),l) :: rest -> if List.mem hyp acc then error ("Hypothesis "^(string_of_id hyp)^" occurs twice"); if not (mem_named_context hyp sign) then @@ -927,13 +1009,13 @@ let eval_variable ist gl (loc,id) = else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found") -let hyp_interp = eval_variable +let interp_hyp = eval_variable let eval_name ist = function | Anonymous -> Anonymous | Name id -> Name (eval_ident ist id) -let hyp_or_metanum_interp ist gl = function +let interp_hyp_or_metanum ist gl = function | AN id -> eval_variable ist gl (dummy_loc,id) | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch) @@ -954,33 +1036,38 @@ let eval_ref ist env = function try unrec (List.assoc id ist.lfun) with Not_found -> interp_pure_qualid false env (loc,make_short_qualid id) -let reference_interp ist env qid = - let v = eval_ref ist env qid in - coerce_to_reference env v - -let pf_reference_interp ist gl = reference_interp ist (pf_env gl) - -(* Interprets a qualified name. This can be a metavariable to be injected *) -let qualid_or_metanum_interp ist = function - | AN qid -> qid - | MetaNum (loc,n) -> constr_to_qid loc (List.assoc n ist.lmatch) - -let eval_ref_or_metanum ist gl = function - | AN qid -> eval_ref ist gl qid - | MetaNum (loc,n) -> VConstr (List.assoc n ist.lmatch) - -let interp_evaluable_or_metanum ist env c = - let c = eval_ref_or_metanum ist env c in - coerce_to_evaluable_ref env c - -let interp_inductive_or_metanum ist gl c = - let c = eval_ref_or_metanum ist (pf_env gl) c in - coerce_to_inductive c +let interp_reference ist env = function + | ArgArg (_,r) -> r + | ArgVar (loc,id) -> coerce_to_reference env (unrec (List.assoc id ist.lfun)) + +let pf_interp_reference ist gl = interp_reference ist (pf_env gl) + +let interp_inductive_or_metanum ist = function + | MetaNum (loc,n) -> + coerce_to_inductive (VConstr (List.assoc n ist.lmatch)) + | AN r -> match r with + | ArgArg r -> r + | ArgVar (_,id) -> + coerce_to_inductive (unrec (List.assoc id ist.lfun)) + +let interp_evaluable_or_metanum ist env = function + | MetaNum (loc,n) -> + coerce_to_evaluable_ref env (VConstr (List.assoc n ist.lmatch)) + | AN r -> match r with + | ArgArg (r,Some id) -> + (* Maybe [id] has been introduced by Intro-like tactics *) + (try match Environ.lookup_named id env with + | (_,Some _,_) -> EvalVarRef id + | _ -> error_not_evaluable (pr_id id) + with Not_found -> r) + | ArgArg (r,None) -> r + | ArgVar (_,id) -> + coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun)) (* Interprets an hypothesis name *) let interp_hyp_location ist gl = function - | InHyp id -> InHyp (hyp_interp ist gl (skip_metaid id)) - | InHypType id -> InHypType (hyp_interp ist gl (skip_metaid id)) + | InHyp id -> InHyp (interp_hyp ist gl id) + | InHypType id -> InHypType (interp_hyp ist gl id) let eval_opt_ident ist = option_app (eval_ident ist) @@ -997,57 +1084,74 @@ let rec constr_list_aux env = function let constr_list ist env = constr_list_aux env ist.lfun -let interp_constr ocl ist sigma env c = - interp_constr_gen sigma env (constr_list ist env) ist.lmatch c ocl +let retype_list sigma env lst = + List.fold_right (fun (x,csr) a -> + try (x,Retyping.get_judgment_of env sigma csr)::a with + | Anomaly _ -> a) lst [] + +let interp_casted_constr ocl ist sigma env (c,ce) = + let (l1,l2) = constr_list ist env in + let rtype lst = retype_list sigma env lst in + let csr = + match ce with + | None -> + Pretyping.understand_gen sigma env (rtype l1) (rtype ist.lmatch) ocl c + (* If at toplevel (ce<>None), the error can be due to an incorrect + context at globalization time: we retype with the now known + intros/lettac/inversion hypothesis names *) + | Some c -> interp_constr_gen sigma env (l1,l2) ist.lmatch c ocl + in + db_constr ist.debug env csr; + csr -let interp_openconstr ist gl c ocl = - interp_openconstr_gen (project gl) (pf_env gl) - (constr_list ist (pf_env gl)) ist.lmatch c ocl +let interp_constr ist sigma env c = + interp_casted_constr None ist sigma env c -let pf_interp_constr ist gl = - interp_constr None ist (project gl) (pf_env gl) +(* Interprets an open constr expression casted by the current goal *) +let pf_interp_casted_openconstr ist gl (c,ce) = + let sigma = project gl in + let env = pf_env gl in + let (ltacvar,l) = constr_list ist env in + let rtype lst = retype_list sigma env lst in + let ocl = Some (pf_concl gl) in + match ce with + | None -> + Pretyping.understand_gen_tcc sigma env (rtype ltacvar) (rtype ist.lmatch) + ocl c + (* If at toplevel (ce<>None), the error can be due to an incorrect + context at globalization time: we retype with the now known + intros/lettac/inversion hypothesis names *) + | Some c -> interp_openconstr_gen sigma env (ltacvar,l) ist.lmatch c ocl (* Interprets a constr expression *) -let constr_interp ist sigma env c = - let csr = interp_constr None ist sigma env c in - begin - db_constr ist.debug env csr; - csr - end - -let pf_constr_interp ist gl c = constr_interp ist (project gl) (pf_env gl) c +let pf_interp_constr ist gl = + interp_constr ist (project gl) (pf_env gl) (* Interprets a constr expression casted by the current goal *) -let cast_constr_interp ist gl c = - let csr = interp_constr (Some (pf_concl gl)) ist (project gl) (pf_env gl) c in - db_constr ist.debug (pf_env gl) csr; - csr - -(* Interprets an open constr expression casted by the current goal *) -let cast_openconstr_interp ist gl c = - interp_openconstr ist gl c (Some (pf_concl gl)) +let pf_interp_casted_constr ist gl c = + interp_casted_constr (Some(pf_concl gl)) ist (project gl) (pf_env gl) c (* Interprets a reduction expression *) -let unfold_interp ist env (l,qid) = +let interp_unfold ist env (l,qid) = (l,interp_evaluable_or_metanum ist env qid) -let flag_interp ist env red = +let interp_flag ist env red = { red with rConst = List.map (interp_evaluable_or_metanum ist env) red.rConst } -let pattern_interp ist sigma env (l,c) = (l,constr_interp ist sigma env c) +let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c) -let pf_pattern_interp ist gl = pattern_interp ist (project gl) (pf_env gl) +let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl) let redexp_interp ist sigma env = function - | Unfold l -> Unfold (List.map (unfold_interp ist env) l) - | Fold l -> Fold (List.map (constr_interp ist sigma env) l) - | Cbv f -> Cbv (flag_interp ist env f) - | Lazy f -> Lazy (flag_interp ist env f) - | Pattern l -> Pattern (List.map (pattern_interp ist sigma env) l) - | Simpl o -> Simpl (option_app (pattern_interp ist sigma env) o) + | Unfold l -> Unfold (List.map (interp_unfold ist env) l) + | Fold l -> Fold (List.map (interp_constr ist sigma env) l) + | Cbv f -> Cbv (interp_flag ist env f) + | Lazy f -> Lazy (interp_flag ist env f) + | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) + | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o) | (Red _ | Hnf as r) -> r - | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist sigma env c) + | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c) let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl) @@ -1062,13 +1166,13 @@ let interp_may_eval f ist gl = function subst_meta [-1,ic] ctxt with | Not_found -> - user_err_loc (loc, "constr_interp", + user_err_loc (loc, "interp_may_eval", str "Unbound context identifier" ++ pr_id s)) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) | ConstrTerm c -> f ist gl c (* Interprets a constr expression possibly to first evaluate *) -let constr_interp_may_eval ist gl c = +let interp_constr_may_eval ist gl c = let csr = interp_may_eval pf_interp_constr ist gl c in begin db_constr ist.debug (pf_env gl) csr; @@ -1095,45 +1199,42 @@ let interp_quantified_hypothesis ist gl = function with Not_found -> NamedHyp id let interp_induction_arg ist gl = function - | ElimOnConstr c -> ElimOnConstr (pf_constr_interp ist gl c) + | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c) | ElimOnAnonHyp n as x -> x | ElimOnIdent (loc,id) -> if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr (pf_constr_interp ist gl (CRef (Ident (loc,id)))) + else ElimOnConstr (pf_interp_constr ist gl (RVar (loc,id),None)) -let binding_interp ist gl (loc,b,c) = - (loc,interp_quantified_hypothesis ist gl b,pf_constr_interp ist gl c) +let interp_binding ist gl (loc,b,c) = + (loc,interp_quantified_hypothesis ist gl b,pf_interp_constr ist gl c) -let bindings_interp ist gl = function +let interp_bindings ist gl = function | NoBindings -> NoBindings -| ImplicitBindings l -> ImplicitBindings (List.map (pf_constr_interp ist gl) l) -| ExplicitBindings l -> ExplicitBindings (List.map (binding_interp ist gl) l) +| ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr ist gl) l) +| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l) let interp_constr_with_bindings ist gl (c,bl) = - (pf_constr_interp ist gl c, bindings_interp ist gl bl) - -(* Interprets a l-tac expression into a value *) -let rec val_interp ist gl tac = - - let value_interp ist = - match tac with - (* Immediate evaluation *) - | TacFun (it,body) -> VFun (ist.lfun,it,body) - | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u - | TacLetIn (l,u) -> - let addlfun = letin_interp ist gl l in - val_interp { ist with lfun=addlfun@ist.lfun } gl u - | TacMatchContext (lr,lmr) -> match_context_interp ist gl lr lmr - | TacMatch (c,lmr) -> match_interp ist gl c lmr - | TacArg a -> tacarg_interp ist gl a - (* Delayed evaluation *) - | t -> VTactic (dummy_loc,eval_tactic ist t) - in - match ist.debug with - | DebugOn | Run _ -> - let debug = debug_prompt gl ist.debug tac in - value_interp {ist with debug=debug} - | _ -> value_interp ist + (pf_interp_constr ist gl c, interp_bindings ist gl bl) + +(* Interprets an l-tac expression into a value *) +let rec val_interp ist gl (tac:glob_tactic_expr) = + + let ist = match ist.debug with + | DebugOn | Run _ -> {ist with debug = debug_prompt gl ist.debug tac } + | _ -> ist in + + match tac with + (* Immediate evaluation *) + | TacFun (it,body) -> VFun (ist.lfun,it,body) + | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u + | TacLetIn (l,u) -> + let addlfun = interp_letin ist gl l in + val_interp { ist with lfun=addlfun@ist.lfun } gl u + | TacMatchContext (lr,lmr) -> match_context_interp ist gl lr lmr + | TacMatch (c,lmr) -> match_interp ist gl c lmr + | TacArg a -> interp_tacarg ist gl a + (* Delayed evaluation *) + | t -> VTactic (dummy_loc,eval_tactic ist t) and eval_tactic ist = function | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl @@ -1145,41 +1246,33 @@ and eval_tactic ist = function | TacMatch (c,lmr) -> assert false | TacId -> tclIDTAC | TacFail (n,s) -> tclFAIL n s - | TacProgress tac -> tclPROGRESS (tactic_interp ist tac) - | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (tactic_interp ist tac) - | TacThen (t1,t2) -> tclTHEN (tactic_interp ist t1) (tactic_interp ist t2) + | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) + | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac) + | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2) | TacThens (t,tl) -> - tclTHENS (tactic_interp ist t) (List.map (tactic_interp ist) tl) - | TacDo (n,tac) -> tclDO n (tactic_interp ist tac) - | TacTry tac -> tclTRY (tactic_interp ist tac) - | TacInfo tac -> tclINFO (tactic_interp ist tac) - | TacRepeat tac -> tclREPEAT (tactic_interp ist tac) + tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl) + | TacDo (n,tac) -> tclDO n (interp_tactic ist tac) + | TacTry tac -> tclTRY (interp_tactic ist tac) + | TacInfo tac -> tclINFO (interp_tactic ist tac) + | TacRepeat tac -> tclREPEAT (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> - tclORELSE (tactic_interp ist tac1) (tactic_interp ist tac2) - | TacFirst l -> tclFIRST (List.map (tactic_interp ist) l) - | TacSolve l -> tclSOLVE (List.map (tactic_interp ist) l) + tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacFirst l -> tclFIRST (List.map (interp_tactic ist) l) + | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l) | TacArg a -> assert false -and interp_ltac_qualid is_applied ist gl (loc,qid as lqid) = - try - let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) in - if is_applied then v else locate_tactic_call loc v - with - Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid - and interp_ltac_reference isapplied ist gl = function - | Ident (loc,id) -> - (try unrec (List.assoc id ist.lfun) - with | Not_found -> - interp_ltac_qualid isapplied ist gl (loc,make_short_qualid id)) - | Qualid qid -> interp_ltac_qualid isapplied ist gl qid + | ArgVar (loc,id) -> unrec (List.assoc id ist.lfun) + | ArgArg qid -> + let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) in + if isapplied then v else locate_tactic_call loc v -and tacarg_interp ist gl = function +and interp_tacarg ist gl = function | TacVoid -> VVoid | Reference r -> interp_ltac_reference false ist gl r | Integer n -> VInteger n - | ConstrMayEval c -> VConstr (constr_interp_may_eval ist gl c) - | MetaNumArg (_,n) -> VConstr (List.assoc n ist.lmatch) + | Identifier id -> VIdentifier id + | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) | MetaIdArg (loc,id) -> (try (* $id can occur in Grammar tactic... *) (unrec (List.assoc (id_of_string id) ist.lfun)) @@ -1187,14 +1280,20 @@ and tacarg_interp ist gl = function | Not_found -> error_syntactic_metavariables_not_allowed loc) | TacCall (loc,f,l) -> let fv = interp_ltac_reference true ist gl f - and largs = List.map (tacarg_interp ist gl) l in + and largs = List.map (interp_tacarg ist gl) l in List.iter check_is_value largs; - app_interp ist gl fv largs loc + interp_app ist gl fv largs loc | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> let tg = (tag t) in if tg = "tactic" then - let f = (tactic_out t) in val_interp ist gl (f ist) + let f = (tactic_out t) in + val_interp ist gl + (intern_tactic { + ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = []; + metavars = List.map fst ist.lmatch; + gsigma = project gl; genv = pf_env gl } + (f ist)) else if tg = "value" then value_out t else if tg = "constr" then @@ -1204,18 +1303,18 @@ and tacarg_interp ist gl = function (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) (* Interprets an application node *) -and app_interp ist gl fv largs loc = +and interp_app ist gl fv largs loc = match fv with | VFun(olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then let v = val_interp { ist with lfun=newlfun@olfun } gl body in if lval=[] then locate_tactic_call loc v - else app_interp ist gl v lval loc + else interp_app ist gl v lval loc else VFun(newlfun@olfun,lvar,body) | _ -> - user_err_loc (loc, "Tacinterp.app_interp", + user_err_loc (loc, "Tacinterp.interp_app", (str"Illegal tactic application")) (* Gives the tactic corresponding to the tactic value *) @@ -1227,9 +1326,9 @@ and tactic_of_value vle g = | _ -> raise NotTactic (* Evaluation with FailError catching *) -and eval_with_fail interp tac goal = +and eval_with_fail ist tac goal = try - (match interp goal tac with + (match val_interp ist goal tac with | VTactic (loc,tac) -> VRTactic (catch_error loc tac goal) | a -> a) with @@ -1254,15 +1353,15 @@ and letrec_interp ist gl lrc u = end (* Interprets the clauses of a LetIn *) -and letin_interp ist gl = function +and interp_letin ist gl = function | [] -> [] | ((loc,id),None,t)::tl -> - let v = tacarg_interp ist gl t in + let v = interp_tacarg ist gl t in check_is_value v; - (id,v):: (letin_interp ist gl tl) + (id,v):: (interp_letin ist gl tl) | ((loc,id),Some com,tce)::tl -> let typ = interp_may_eval pf_interp_constr ist gl com - and v = tacarg_interp ist gl tce in + and v = interp_tacarg ist gl tce in let csr = try constr_of_value (pf_env gl) v @@ -1277,16 +1376,16 @@ and letin_interp ist gl = function pft with | NotTactic -> delete_proof (dummy_loc,id); - errorlabstrm "Tacinterp.letin_interp" + errorlabstrm "Tacinterp.interp_letin" (str "Term or fully applied tactic expected in Let") - in (id,VConstr (mkCast (csr,typ)))::(letin_interp ist gl tl) + in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl) (* Interprets the clauses of a LetCut *) and letcut_interp ist = function | [] -> tclIDTAC | (id,c,tce)::tl -> fun gl -> - let typ = constr_interp_may_eval ist gl c - and v = tacarg_interp ist gl tce in + let typ = interp_constr_may_eval ist gl c + and v = interp_tacarg ist gl tce in let csr = try constr_of_value (pf_env gl) v @@ -1300,7 +1399,7 @@ and letcut_interp ist = function pft with | NotTactic -> delete_proof (dummy_loc,id); - errorlabstrm "Tacinterp.letin_interp" + errorlabstrm "Tacinterp.interp_letin" (str "Term or fully applied tactic expected in Let") in let cutt = h_cut typ @@ -1314,8 +1413,7 @@ and match_context_interp ist g lr lmr = let (lgoal,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in if mhyps = [] then - eval_with_fail - (val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch}) + eval_with_fail {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch} mt goal else apply_hyps_context ist env goal mt lgoal mhyps hyps @@ -1331,7 +1429,7 @@ and match_context_interp ist g lr lmr = | (All t)::tl -> begin db_mc_pattern_success ist.debug; - try eval_with_fail (val_interp ist) t goal + try eval_with_fail ist t goal with e when is_match_catchable e -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl end @@ -1349,8 +1447,7 @@ and match_context_interp ist g lr lmr = if mhyps = [] then begin db_mc_pattern_success ist.debug; - eval_with_fail (val_interp - {ist with lmatch=lgoal@ist.lmatch}) mt goal + eval_with_fail {ist with lmatch=lgoal@ist.lmatch} mt goal end else apply_hyps_context ist env goal mt lgoal mhyps hyps @@ -1369,7 +1466,8 @@ and match_context_interp ist g lr lmr = with e when is_match_catchable e -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" + errorlabstrm "Tacinterp.apply_match_context" (str + "No matching clauses for Match Context") (v 0 (str "No matching clauses for Match Context" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Debug On\" for more info)" @@ -1377,7 +1475,7 @@ and match_context_interp ist g lr lmr = end in let env = pf_env g in apply_match_context ist env g 0 lmr - (read_match_rule (project g) env (constr_list ist env) lmr) + (read_match_rule (project g) env (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env goal mt lgmatch mhyps hyps = @@ -1394,8 +1492,8 @@ and apply_hyps_context ist env goal mt lgmatch mhyps hyps = if tl = [] then begin db_mc_pattern_success ist.debug; - eval_with_fail (val_interp {ist with lfun=lfun@lid@lc@ist.lfun; - lmatch=lmatch@lm@ist.lmatch}) mt goal + eval_with_fail {ist with lfun=lfun@lid@lc@ist.lfun; + lmatch=lmatch@lm@ist.lmatch} mt goal end else let nextlhyps = @@ -1420,48 +1518,49 @@ and apply_hyps_context ist env goal mt lgmatch mhyps hyps = apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None (* Interprets extended tactic generic arguments *) -and genarg_interp ist goal x = +and interp_genarg ist goal x = match genarg_tag x with - | BoolArgType -> in_gen wit_bool (out_gen rawwit_bool x) - | IntArgType -> in_gen wit_int (out_gen rawwit_int x) + | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x) + | IntArgType -> in_gen wit_int (out_gen globwit_int x) | IntOrVarArgType -> let f = function | ArgVar locid -> eval_integer ist.lfun locid | ArgArg n as x -> x in - in_gen wit_int_or_var (f (out_gen rawwit_int_or_var x)) + in_gen wit_int_or_var (f (out_gen globwit_int_or_var x)) | StringArgType -> - in_gen wit_string (out_gen rawwit_string x) + in_gen wit_string (out_gen globwit_string x) | PreIdentArgType -> - in_gen wit_pre_ident (out_gen rawwit_pre_ident x) + in_gen wit_pre_ident (out_gen globwit_pre_ident x) | IdentArgType -> - in_gen wit_ident (eval_ident ist (out_gen rawwit_ident x)) + in_gen wit_ident (eval_ident ist (out_gen globwit_ident x)) | RefArgType -> - in_gen wit_ref (pf_reference_interp ist goal (out_gen rawwit_ref x)) + in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x)) | SortArgType -> in_gen wit_sort (destSort - (pf_constr_interp ist goal (CSort (dummy_loc,out_gen rawwit_sort x)))) + (pf_interp_constr ist goal + (RSort (dummy_loc,out_gen globwit_sort x), None))) | ConstrArgType -> - in_gen wit_constr (pf_constr_interp ist goal (out_gen rawwit_constr x)) + in_gen wit_constr (pf_interp_constr ist goal (out_gen globwit_constr x)) | ConstrMayEvalArgType -> - in_gen wit_constr_may_eval (constr_interp_may_eval ist goal (out_gen rawwit_constr_may_eval x)) + in_gen wit_constr_may_eval (interp_constr_may_eval ist goal (out_gen globwit_constr_may_eval x)) | QuantHypArgType -> in_gen wit_quant_hyp - (interp_quantified_hypothesis ist goal (out_gen rawwit_quant_hyp x)) + (interp_quantified_hypothesis ist goal (out_gen globwit_quant_hyp x)) | RedExprArgType -> - in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen rawwit_red_expr x)) - | TacticArgType -> in_gen wit_tactic (out_gen rawwit_tactic x) + in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x)) + | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x) | CastedOpenConstrArgType -> in_gen wit_casted_open_constr - (cast_openconstr_interp ist goal (out_gen rawwit_casted_open_constr x)) + (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x)) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings - (interp_constr_with_bindings ist goal (out_gen rawwit_constr_with_bindings x)) - | List0ArgType _ -> app_list0 (genarg_interp ist goal) x - | List1ArgType _ -> app_list1 (genarg_interp ist goal) x - | OptArgType _ -> app_opt (genarg_interp ist goal) x - | PairArgType _ -> app_pair (genarg_interp ist goal) (genarg_interp ist goal) x - | ExtraArgType s -> lookup_genarg_interp s ist goal x + (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x)) + | List0ArgType _ -> app_list0 (interp_genarg ist goal) x + | List1ArgType _ -> app_list1 (interp_genarg ist goal) x + | OptArgType _ -> app_opt (interp_genarg ist goal) x + | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x + | ExtraArgType s -> lookup_interp_genarg s ist goal x (* Interprets the Match expressions *) and match_interp ist g constr lmr = @@ -1489,16 +1588,16 @@ and match_interp ist g constr lmr = | _ -> errorlabstrm "Tacinterp.apply_match" (str "No matching clauses for Match") in - let csr = constr_interp_may_eval ist g constr in + let csr = interp_constr_may_eval ist g constr in let env = pf_env g in - let ilr = read_match_rule (project g) env (constr_list ist env) lmr in + let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in apply_match ist csr ilr (* Interprets tactic expressions : returns a "tactic" *) -and tactic_interp ist tac gl = +and interp_tactic ist tac gl = try tactic_of_value (val_interp ist gl tac) gl with | NotTactic -> - errorlabstrm "Tacinterp.tac_interp" (str + errorlabstrm "Tacinterp.interp_tactic" (str "Must be a command or must give a tactic value") (* Interprets a primitive tactic *) @@ -1512,43 +1611,46 @@ and interp_atomic ist gl = function h_intro_move (option_app (eval_ident ist) ido) (option_app (fun x -> eval_variable ist gl x) ido') | TacAssumption -> h_assumption - | TacExact c -> h_exact (cast_constr_interp ist gl c) + | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb) | TacElim (cb,cbo) -> h_elim (interp_constr_with_bindings ist gl cb) (option_app (interp_constr_with_bindings ist gl) cbo) - | TacElimType c -> h_elim_type (pf_constr_interp ist gl c) + | TacElimType c -> h_elim_type (pf_interp_constr ist gl c) | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb) - | TacCaseType c -> h_case_type (pf_constr_interp ist gl c) + | TacCaseType c -> h_case_type (pf_interp_constr ist gl c) | TacFix (idopt,n) -> h_fix (eval_opt_ident ist idopt) n | TacMutualFix (id,n,l) -> - let f (id,n,c) = (eval_ident ist id,n,pf_constr_interp ist gl c) in + let f (id,n,c) = (eval_ident ist id,n,pf_interp_constr ist gl c) in h_mutual_fix (eval_ident ist id) n (List.map f l) | TacCofix idopt -> h_cofix (eval_opt_ident ist idopt) | TacMutualCofix (id,l) -> - let f (id,c) = (eval_ident ist id,pf_constr_interp ist gl c) in + let f (id,c) = (eval_ident ist id,pf_interp_constr ist gl c) in h_mutual_cofix (eval_ident ist id) (List.map f l) - | TacCut c -> h_cut (pf_constr_interp ist gl c) - | TacTrueCut (ido,c) -> h_true_cut (eval_opt_ident ist ido) (pf_constr_interp ist gl c) - | TacForward (b,na,c) -> h_forward b (eval_name ist na) (pf_constr_interp ist gl c) - | TacGeneralize cl -> h_generalize (List.map (pf_constr_interp ist gl) cl) - | TacGeneralizeDep c -> h_generalize_dep (pf_constr_interp ist gl c) + | TacCut c -> h_cut (pf_interp_constr ist gl c) + | TacTrueCut (ido,c) -> + h_true_cut (eval_opt_ident ist ido) (pf_interp_constr ist gl c) + | TacForward (b,na,c) -> + h_forward b (eval_name ist na) (pf_interp_constr ist gl c) + | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl) + | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (id,c,clp) -> let clp = check_clause_pattern ist gl clp in - h_let_tac (eval_ident ist id) (pf_constr_interp ist gl c) clp - | TacInstantiate (n,c) -> h_instantiate n (pf_constr_interp ist gl c) + h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp + | TacInstantiate (n,c) -> h_instantiate n (pf_interp_constr ist gl c) (* Automation tactics *) | TacTrivial l -> Auto.h_trivial l | TacAuto (n, l) -> Auto.h_auto n l | TacAutoTDB n -> Dhyp.h_auto_tdb n - | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (hyp_interp ist gl id) + | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p) -> Auto.h_dauto (n,p) (* Derived basic tactics *) - | TacOldInduction h -> h_old_induction (interp_quantified_hypothesis ist gl h) + | TacOldInduction h -> + h_old_induction (interp_quantified_hypothesis ist gl h) | TacNewInduction (c,cbo,ids) -> h_new_induction (interp_induction_arg ist gl c) (option_app (interp_constr_with_bindings ist gl) cbo) @@ -1562,79 +1664,367 @@ and interp_atomic ist gl = function let h1 = interp_quantified_hypothesis ist gl h1 in let h2 = interp_quantified_hypothesis ist gl h2 in Elim.h_double_induction h1 h2 - | TacDecomposeAnd c -> Elim.h_decompose_and (pf_constr_interp ist gl c) - | TacDecomposeOr c -> Elim.h_decompose_or (pf_constr_interp ist gl c) + | TacDecomposeAnd c -> Elim.h_decompose_and (pf_interp_constr ist gl c) + | TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c) | TacDecompose (l,c) -> - let l = List.map (interp_inductive_or_metanum ist gl) l in - Elim.h_decompose l (pf_constr_interp ist gl c) - | TacSpecialize (n,l) -> h_specialize n (interp_constr_with_bindings ist gl l) - | TacLApply c -> h_lapply (pf_constr_interp ist gl c) + let l = List.map (interp_inductive_or_metanum ist) l in + Elim.h_decompose l (pf_interp_constr ist gl c) + | TacSpecialize (n,l) -> + h_specialize n (interp_constr_with_bindings ist gl l) + | TacLApply c -> h_lapply (pf_interp_constr ist gl c) (* Context management *) - | TacClear l -> h_clear (List.map (hyp_or_metanum_interp ist gl) l) - | TacClearBody l -> h_clear_body (List.map (hyp_or_metanum_interp ist gl) l) + | TacClear l -> h_clear (List.map (interp_hyp_or_metanum ist gl) l) + | TacClearBody l -> h_clear_body (List.map (interp_hyp_or_metanum ist gl) l) | TacMove (dep,id1,id2) -> - h_move dep (hyp_interp ist gl id1) (hyp_interp ist gl id2) + h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2) | TacRename (id1,id2) -> - h_rename (hyp_interp ist gl id1) (eval_ident ist (snd id2)) + h_rename (interp_hyp ist gl id1) (eval_ident ist (snd id2)) (* Constructors *) - | TacLeft bl -> h_left (bindings_interp ist gl bl) - | TacRight bl -> h_right (bindings_interp ist gl bl) - | TacSplit (_,bl) -> h_split (bindings_interp ist gl bl) + | TacLeft bl -> h_left (interp_bindings ist gl bl) + | TacRight bl -> h_right (interp_bindings ist gl bl) + | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl) | TacAnyConstructor t -> abstract_tactic (TacAnyConstructor t) - (Tactics.any_constructor (option_app (tactic_interp ist) t)) + (Tactics.any_constructor (option_app (interp_tactic ist) t)) | TacConstructor (n,bl) -> - h_constructor (skip_metaid n) (bindings_interp ist gl bl) + h_constructor (skip_metaid n) (interp_bindings ist gl bl) (* Conversion *) | TacReduce (r,cl) -> h_reduce (pf_redexp_interp ist gl r) (List.map (interp_hyp_location ist gl) cl) | TacChange (occl,c,cl) -> - h_change (option_app (pf_pattern_interp ist gl) occl) - (pf_constr_interp ist gl c) (List.map (interp_hyp_location ist gl) cl) + h_change (option_app (pf_interp_pattern ist gl) occl) + (pf_interp_constr ist gl c) (List.map (interp_hyp_location ist gl) cl) (* Equivalence relations *) | TacReflexivity -> h_reflexivity | TacSymmetry -> h_symmetry - | TacTransitivity c -> h_transitivity (pf_constr_interp ist gl c) + | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) (* For extensions *) | TacExtend (loc,opn,l) -> - fun gl -> vernac_tactic (opn,List.map (genarg_interp ist gl) l) gl + fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl | TacAlias (_,l,body) -> fun gl -> let f x = match genarg_tag x with | IdentArgType -> - let id = out_gen rawwit_ident x in + let id = out_gen globwit_ident x in (try VConstr (mkVar (eval_variable ist gl (dummy_loc,id))) with Not_found -> VIdentifier id) - | RefArgType -> VConstr (constr_of_reference (pf_reference_interp ist gl (out_gen rawwit_ref x))) - | ConstrArgType -> VConstr (pf_constr_interp ist gl (out_gen rawwit_constr x)) + | RefArgType -> + VConstr (constr_of_reference + (pf_interp_reference ist gl (out_gen globwit_ref x))) + | ConstrArgType -> + VConstr (pf_interp_constr ist gl (out_gen globwit_constr x)) | ConstrMayEvalArgType -> - VConstr (constr_interp_may_eval ist gl (out_gen rawwit_constr_may_eval x)) + VConstr + (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) | _ -> failwith "This generic type is not supported in alias" in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in tactic_of_value (val_interp { ist with lfun=lfun } gl body) gl -(* Interprets tactic arguments *) -let interp_tacarg sign ast = val_interp sign ast - (* Initial call for interpretation *) -let tac_interp lfun lmatch debug t = - tactic_interp { lfun=lfun; lmatch=lmatch; debug=debug } t +let interp_tac_gen lfun lmatch debug t gl = + interp_tactic { lfun=lfun; lmatch=lmatch; debug=debug } + (intern_tactic { + ltacvars = (List.map fst lfun, []); ltacrecvars = []; + metavars = List.map fst lmatch; + gsigma = project gl; genv = pf_env gl } t) gl -let interp = fun t -> tac_interp [] [] (get_debug()) t (* Side-effect *) +let eval_tactic t = interp_tactic { lfun=[]; lmatch=[]; debug=get_debug() } t + +let interp t = interp_tac_gen [] [] (get_debug()) t (* Hides interpretation for pretty-print *) let hide_interp t ot gl = - let te = glob_tactic ([],[],project gl,pf_env gl) t in + let ist = { ltacvars = ([],[]); ltacrecvars = []; metavars = []; + gsigma = project gl; genv = pf_env gl } in + let te = intern_tactic ist t in + let t = eval_tactic te in match ot with - | None -> abstract_tactic_expr (TacArg (Tacexp t)) (interp t) gl - | Some t' -> - abstract_tactic_expr (TacArg (Tacexp t)) (tclTHEN (interp t) t') gl + | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl + | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl + +(***************************************************************************) +(* Substitution at module closing time *) + +let subst_quantified_hypothesis _ x = x + +let subst_inductive subst (kn,i) = (subst_kn subst kn,i) + +let subst_rawconstr subst (c,e) = + assert (e=None); (* e<>None only for toplevel tactics *) + (subst_raw subst c,None) + +let subst_binding subst (loc,b,c) = + (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c) + +let subst_bindings subst = function + | NoBindings -> NoBindings + | ImplicitBindings l -> ImplicitBindings (List.map (subst_rawconstr subst) l) + | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l) + +let subst_raw_with_bindings subst (c,bl) = + (subst_rawconstr subst c, subst_bindings subst bl) + +let subst_induction_arg subst = function + | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c) + | ElimOnAnonHyp n as x -> x + | ElimOnIdent id as x -> x + +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (subst_kn subst kn) + +let subst_and_short_name f (c,n) = + assert (n=None); (* since tacdef are strictly globalized *) + (f c,None) + +let subst_or_metanum f = function + | AN x -> AN (f x) + | MetaNum (_loc,n) -> MetaNum (loc,n) + +let subst_or_var f = function + | ArgVar _ as x -> x + | ArgArg (x) -> ArgArg (f x) + +let subst_located f (_loc,id) = (loc,f id) + +let subst_reference subst r = (* TODO: subst ltac global names *) r + +let subst_global_reference subst = + subst_or_var (subst_located (subst_global subst)) + +let subst_evaluable subst = + subst_or_metanum (subst_or_var + (subst_and_short_name (subst_evaluable_reference subst))) + +let subst_unfold subst (l,e) = + (l,subst_evaluable subst e) + +let subst_flag subst red = + { red with rConst = List.map (subst_evaluable subst) red.rConst } + +let subst_constr_occurrence subst (l,c) = (l,subst_rawconstr subst c) + +let subst_redexp subst = function + | Unfold l -> Unfold (List.map (subst_unfold subst) l) + | Fold l -> Fold (List.map (subst_rawconstr subst) l) + | Cbv f -> Cbv (subst_flag subst f) + | Lazy f -> Lazy (subst_flag subst f) + | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) + | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o) + | (Red _ | Hnf as r) -> r + | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c) + +let subst_raw_may_eval subst = function + | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c) + | ConstrContext (locid,c) -> ConstrContext (locid,subst_rawconstr subst c) + | ConstrTypeOf c -> ConstrTypeOf (subst_rawconstr subst c) + | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c) + +let subst_match_pattern subst = function + | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc) + | Term pc -> Term (subst_pattern subst pc) + +let rec subst_match_context_hyps subst = function + | NoHypId mp :: tl -> + NoHypId (subst_match_pattern subst mp) + :: subst_match_context_hyps subst tl + | Hyp (locs,mp) :: tl -> + Hyp (locs,subst_match_pattern subst mp) + :: subst_match_context_hyps subst tl + | [] -> [] + +let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with + (* Basic tactics *) + | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x + | TacAssumption as x -> x + | TacExact c -> TacExact (subst_rawconstr subst c) + | TacApply cb -> TacApply (subst_raw_with_bindings subst cb) + | TacElim (cb,cbo) -> + TacElim (subst_raw_with_bindings subst cb, + option_app (subst_raw_with_bindings subst) cbo) + | TacElimType c -> TacElimType (subst_rawconstr subst c) + | TacCase cb -> TacCase (subst_raw_with_bindings subst cb) + | TacCaseType c -> TacCaseType (subst_rawconstr subst c) + | TacFix (idopt,n) as x -> x + | TacMutualFix (id,n,l) -> + TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l) + | TacCofix idopt as x -> x + | TacMutualCofix (id,l) -> + TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) + | TacCut c -> TacCut (subst_rawconstr subst c) + | TacTrueCut (ido,c) -> TacTrueCut (ido, subst_rawconstr subst c) + | TacForward (b,na,c) -> TacForward (b,na,subst_rawconstr subst c) + | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) + | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) + | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) + | TacInstantiate (n,c) -> TacInstantiate (n,subst_rawconstr subst c) + + (* Automation tactics *) + | TacTrivial l -> TacTrivial l + | TacAuto (n,l) -> TacAuto (n,l) + | TacAutoTDB n -> TacAutoTDB n + | TacDestructHyp (b,id) -> TacDestructHyp(b,id) + | TacDestructConcl -> TacDestructConcl + | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) + | TacDAuto (n,p) -> TacDAuto (n,p) + + (* Derived basic tactics *) + | TacOldInduction h as x -> x + | TacNewInduction (c,cbo,ids) -> + TacNewInduction (subst_induction_arg subst c, + option_app (subst_raw_with_bindings subst) cbo, ids) + | TacOldDestruct h as x -> x + | TacNewDestruct (c,cbo,ids) -> + TacNewDestruct (subst_induction_arg subst c, + option_app (subst_raw_with_bindings subst) cbo, ids) + | TacDoubleInduction (h1,h2) as x -> x + | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) + | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) + | TacDecompose (l,c) -> + let l = + List.map (subst_or_metanum (subst_or_var (subst_inductive subst))) l in + TacDecompose (l,subst_rawconstr subst c) + | TacSpecialize (n,l) -> TacSpecialize (n,subst_raw_with_bindings subst l) + | TacLApply c -> TacLApply (subst_rawconstr subst c) + + (* Context management *) + | TacClear l as x -> x + | TacClearBody l as x -> x + | TacMove (dep,id1,id2) as x -> x + | TacRename (id1,id2) as x -> x + + (* Constructors *) + | TacLeft bl -> TacLeft (subst_bindings subst bl) + | TacRight bl -> TacRight (subst_bindings subst bl) + | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl) + | TacAnyConstructor t -> TacAnyConstructor (option_app (subst_tactic subst) t) + | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl) + + (* Conversion *) + | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) + | TacChange (occl,c,cl) -> + TacChange (option_app (subst_constr_occurrence subst) occl, + subst_rawconstr subst c, cl) + + (* Equivalence relations *) + | TacReflexivity | TacSymmetry as x -> x + | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c) + + (* For extensions *) + | TacExtend (_loc,opn,l) -> + let _ = lookup_tactic opn in + TacExtend (loc,opn,List.map (subst_genarg subst) l) + | TacAlias (s,l,body) -> + TacAlias (s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,subst_tactic subst body) + +and subst_tactic subst (t:glob_tactic_expr) = match t with + | TacAtom (_loc,t) -> TacAtom (loc, subst_atomic subst t) + | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun) + | TacLetRecIn (lrc,u) -> + let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in + TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr)) + | TacLetIn (l,u) -> + let l = List.map (fun (n,c,b) -> (n,option_app (subst_raw_may_eval subst) c,subst_tacarg subst b)) l in + TacLetIn (l,subst_tactic subst u) + | TacLetCut l -> + let f (n,c,t) = (n,subst_raw_may_eval subst c,subst_tacarg subst t) in + TacLetCut (List.map f l) + | TacMatchContext (lr,lmr) -> + TacMatchContext(lr, subst_match_rule subst lmr) + | TacMatch (c,lmr) -> + TacMatch (subst_raw_may_eval subst c,subst_match_rule subst lmr) + | TacId | TacFail _ as x -> x + | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr) + | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s) + | TacThen (t1,t2) -> + TacThen (subst_tactic subst t1,subst_tactic subst t2) + | TacThens (t,tl) -> + TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) + | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac) + | TacTry tac -> TacTry (subst_tactic subst tac) + | TacInfo tac -> TacInfo (subst_tactic subst tac) + | TacRepeat tac -> TacRepeat (subst_tactic subst tac) + | TacOrelse (tac1,tac2) -> + TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) + | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) + | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) + | TacArg a -> TacArg (subst_tacarg subst a) + +and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) + +and subst_tacarg subst = function + | TacVoid -> TacVoid + | Reference r -> Reference (subst_or_var (subst_reference subst) r) + | Identifier id -> Identifier id + | Integer n -> Integer n + | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) + | MetaIdArg (_loc,_) -> error_syntactic_metavariables_not_allowed loc + | TacCall (_loc,f,l) -> + TacCall (_loc, + subst_or_var (subst_reference subst) f, + List.map (subst_tacarg subst) l) + | Tacexp t -> Tacexp (subst_tactic subst t) + | TacDynamic(_,t) as x -> + (match tag t with + | "tactic" | "value" | "constr" -> x + | s -> anomaly_loc (loc, "Tacinterp.val_interp", + str "Unknown dynamic: <" ++ str s ++ str ">")) + +(* Reads the rules of a Match Context or a Match *) +and subst_match_rule subst = function + | (All tc)::tl -> + (All (subst_tactic subst tc))::(subst_match_rule subst tl) + | (Pat (rl,mp,tc))::tl -> + let hyps = subst_match_context_hyps subst rl in + let pat = subst_match_pattern subst mp in + Pat (hyps,pat,subst_tactic subst tc) + ::(subst_match_rule subst tl) + | [] -> [] + +and subst_genarg subst (x:glob_generic_argument) = + match genarg_tag x with + | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x) + | IntArgType -> in_gen globwit_int (out_gen globwit_int x) + | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x) + | StringArgType -> in_gen globwit_string (out_gen globwit_string x) + | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x) + | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x) + | RefArgType -> + in_gen globwit_ref (subst_global_reference subst + (out_gen globwit_ref x)) + | SortArgType -> + in_gen globwit_sort (out_gen globwit_sort x) + | ConstrArgType -> + in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x)) + | ConstrMayEvalArgType -> + in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x)) + | QuantHypArgType -> + in_gen globwit_quant_hyp + (subst_quantified_hypothesis subst (out_gen globwit_quant_hyp x)) + | RedExprArgType -> + in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) + | TacticArgType -> + in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x)) + | CastedOpenConstrArgType -> + in_gen globwit_casted_open_constr + (subst_rawconstr subst (out_gen globwit_casted_open_constr x)) + | ConstrWithBindingsArgType -> + in_gen globwit_constr_with_bindings + (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x)) + | List0ArgType _ -> app_list0 (subst_genarg subst) x + | List1ArgType _ -> app_list1 (subst_genarg subst) x + | OptArgType _ -> app_opt (subst_genarg subst) x + | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x + | ExtraArgType s -> lookup_genarg_subst s subst x + +(***************************************************************************) +(* Tactic registration *) (* For bad tactic calls *) let bad_tactic_args s = @@ -1651,10 +2041,15 @@ let cache_md (_,defs) = List.iter (fun (sp,_) -> Nametab.push_tactic (Until 1) sp) defs; List.iter add (List.map register_tacdef defs) +let subst_md (_,subst,defs) = + List.map (fun (sp,t) -> (sp,subst_tactic subst t)) defs + let (inMD,outMD) = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; open_function = (fun i o -> if i=1 then cache_md o); + subst_function = subst_md; + classify_function = (fun (_,o) -> Substitute o); export_function = (fun x -> Some x)} (* Adds a definition for tactics in the table *) @@ -1666,18 +2061,42 @@ let make_absolute_name (loc,id) = ++ pr_sp sp); sp +let make_empty_glob_sign () = + { ltacvars = ([],[]); ltacrecvars = []; + metavars = []; gsigma = Evd.empty; genv = Global.env() } + let add_tacdef isrec tacl = - let lfun = List.map (fun ((loc,id),_) -> id) tacl in - let ist = ((if isrec then lfun else []), [], Evd.empty, Global.env()) in - let tacl = List.map (fun (id,tac) -> (make_absolute_name id,tac)) tacl in - let tacl = List.map (fun (id,def) -> (id,glob_tactic ist def)) tacl in - let _ = Lib.add_leaf (List.hd lfun) (inMD tacl) in + let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in + let ist = + {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in + let gtacl = + List.map2 (fun (_,sp) (_,def) -> + (sp,Options.with_option strict_check (intern_tactic ist) def)) + rfun tacl in + let id0 = fst (List.hd rfun) in + let _ = Lib.add_leaf id0 (inMD gtacl) in List.iter - (fun id -> Options.if_verbose msgnl (pr_id id ++ str " is defined")) lfun + (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined")) + rfun + +(***************************************************************************) +(* Other entry points *) + +let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x let interp_redexp env evc r = let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in - redexp_interp ist evc env r - -let _ = Auto.set_extern_interp (fun l -> tac_interp [] l (get_debug())) -let _ = Dhyp.set_extern_interp interp + let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = evc } in + redexp_interp ist evc env (intern_redexp gist r) + +(***************************************************************************) +(* Backwarding recursive needs of tactic glob/interp/eval functions *) + +let _ = Auto.set_extern_interp + (fun l -> interp_tactic {lfun=[];lmatch=l;debug=get_debug()}) +let _ = Auto.set_extern_intern_tac + (fun l -> intern_tactic {(make_empty_glob_sign()) with metavars=l}) +let _ = Auto.set_extern_subst_tactic subst_tactic +let _ = Dhyp.set_extern_interp eval_tactic +let _ = Dhyp.set_extern_intern_tac + (fun t -> intern_tactic (make_empty_glob_sign()) t) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index d3c57c45b..e36c89377 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -25,7 +25,7 @@ open Topconstr type value = | VTactic of Util.loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *) | VRTactic of (goal list sigma * validation) - | VFun of (identifier * value) list * identifier option list *raw_tactic_expr + | VFun of (identifier * value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int | VIdentifier of identifier @@ -67,33 +67,46 @@ val add_tacdef : bool -> (identifier Util.located * raw_tactic_expr) list -> unit (* Adds an interpretation function for extra generic arguments *) -val add_genarg_interp : +type glob_sign = { + ltacvars : identifier list * identifier list; + ltacrecvars : (identifier * Nametab.ltac_constant) list; + metavars : int list; + gsigma : Evd.evar_map; + genv : Environ.env } + +val add_interp_genarg : string -> - (interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument) -> unit + (glob_sign -> raw_generic_argument -> glob_generic_argument) * + (interp_sign -> goal sigma -> glob_generic_argument -> + closed_generic_argument) * + (Names.substitution -> glob_generic_argument -> glob_generic_argument) + -> unit -val genarg_interp : - interp_sign -> goal sigma -> raw_generic_argument -> closed_generic_argument +val interp_genarg : + interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument -(* Interprets any expression *) -val val_interp : interp_sign -> goal sigma -> raw_tactic_expr -> value +val intern_genarg : + glob_sign -> raw_generic_argument -> glob_generic_argument + +val subst_genarg : + Names.substitution -> glob_generic_argument -> glob_generic_argument -(* -(* Interprets tactic arguments *) -val interp_tacarg : interp_sign -> raw_tactic_expr -> value -*) +(* Interprets any expression *) +val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value (* Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Tacred.red_expr (* Interprets tactic expressions *) -val tac_interp : (identifier * value) list -> (int * constr) list -> +val interp_tac_gen : (identifier * value) list -> (int * constr) list -> debug_info -> raw_tactic_expr -> tactic -(* Interprets constr expressions *) -val constr_interp : interp_sign -> Evd.evar_map -> Environ.env -> constr_expr -> constr - (* Initial call for interpretation *) +val glob_tactic : raw_tactic_expr -> glob_tactic_expr + +val eval_tactic : glob_tactic_expr -> tactic + val interp : raw_tactic_expr -> tactic (* Hides interpretation for pretty-print *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f6be87bcf..6978efdba 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -24,6 +24,7 @@ open Refiner open Tacmach open Clenv open Pattern +open Matching open Evar_refiner open Wcclausenv diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index bf9059c75..dd5268720 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -24,10 +24,10 @@ open Util let is_empty ist = if (is_empty_type (List.assoc 1 ist.lmatch)) then - <:tactic<ElimType ?1;Assumption>> - else - <:tactic<Fail>> - + <:tactic<Idtac>> + else + <:tactic<Fail>> + let is_unit ist = if (is_unit_type (List.assoc 1 ist.lmatch)) then <:tactic<Idtac>> @@ -65,7 +65,7 @@ let axioms ist = <:tactic< Match Reverse Context With |[|- ?1] -> $t_is_unit;Constructor 1 - |[_:?1 |- ?] -> $t_is_empty + |[_:?1 |- ?] -> $t_is_empty;ElimType ?1;Assumption |[_:?1 |- ?1] -> Assumption>> @@ -108,11 +108,12 @@ let simplif ist = | [|- (?1 ? ?)] -> $t_is_conj;Split); $t_not_dep_intros)>> -let rec tauto_intuit t_reduce t_solver ist = +let rec tauto_intuit t_reduce solver ist = let t_axioms = tacticIn axioms and t_simplif = tacticIn simplif and t_is_disj = tacticIn is_disj - and t_tauto_intuit = tacticIn (tauto_intuit t_reduce t_solver) in + and t_tauto_intuit = tacticIn (tauto_intuit t_reduce solver) in + let t_solver = Tacexpr.TacArg (valueIn (VTactic (dummy_loc,solver))) in <:tactic< ($t_simplif;$t_axioms Orelse @@ -153,12 +154,12 @@ let intuition_gen tac = let simplif_gen = interp (tacticIn simplif) let tauto g = - try intuition_gen <:tactic<Fail>> g + try intuition_gen (interp <:tactic<Fail>>) g with Refiner.FailError _ | UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >] -let default_intuition_tac = <:tactic< Auto with * >> +let default_intuition_tac = interp <:tactic< Auto with * >> let q_elim tac= <:tactic< @@ -170,7 +171,7 @@ let rec lfo n gl= if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else let p=if n<0 then n else (n-1) in let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in - intuition_gen lfo_rec gl + intuition_gen (interp lfo_rec) gl let lfo_wrap n gl= try lfo n gl @@ -188,7 +189,7 @@ END TACTIC EXTEND Intuition | [ "Intuition" ] -> [ intuition_gen default_intuition_tac ] -| [ "Intuition" tactic(t) ] -> [ intuition_gen t ] +| [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ] END TACTIC EXTEND LinearIntuition diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index af9de6b43..726f521c1 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -671,7 +671,7 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) omodv8 sc toks = if onlyparse then None else let r = interp_rawconstr_gen - false Evd.empty (Global.env()) [] false (vars,[]) c in + false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in Some (make_old_pp_rule ppn ppsymbols pptyps r notation scope vars) in (* Declare the interpretation *) let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index eee2042a0..96c65b54c 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -456,6 +456,11 @@ let pr_lconstr_env env c = pr ltop (transf env c) let pr_constr c = pr_constr_env (Global.env()) c let pr_lconstr c = pr_lconstr_env (Global.env()) c +let pr_rawconstr_env env c = + pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) +let pr_lrawconstr_env env c = + pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) + let anonymize_binder na c = if Options.do_translate() then Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env())) @@ -495,10 +500,6 @@ let pr_red_flag pr r = open Genarg -let pr_metanum pr = function - | AN x -> pr x - | MetaNum (_,n) -> str "?" ++ int n - let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function @@ -524,11 +525,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | ExtraRedExpr (s,c) -> hov 1 (str s ++ pr_arg pr_constr c) -let rec pr_may_eval prc prlc = function +let rec pr_may_eval prc prlc pr2 = function | ConstrEval (r,c) -> hov 0 (str "eval" ++ brk (1,1) ++ - pr_red_expr (prc,prlc,pr_metanum pr_reference) r ++ + pr_red_expr (prc,prlc,pr2) r ++ str " in" ++ spc() ++ prlc c) | ConstrContext ((_,id),c) -> hov 0 diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index fe1c560ca..9cd75607b 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -19,6 +19,7 @@ open Coqast open Topconstr open Names open Util +open Genarg val extract_lam_binders : constr_expr -> (name located list * constr_expr) list * constr_expr @@ -51,6 +52,9 @@ val pr_lconstr_env : env -> constr_expr -> std_ppcmds val pr_cases_pattern : cases_pattern_expr -> std_ppcmds val pr_binders : (name located list * constr_expr) list -> std_ppcmds val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds -val pr_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval + -> std_ppcmds val pr_metaid : identifier -> std_ppcmds + +val pr_rawconstr_env : env -> rawconstr -> std_ppcmds +val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 38cbc3109..157999b10 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -21,34 +21,17 @@ open Rawterm open Topconstr open Genarg open Libnames - -(* [pr_rawtac] is here to cheat with ML typing system, - gen_tactic_expr is polymorphic but with some occurrences of its - instance raw_tactic_expr in it; then pr_tactic should be - polymorphic but with some calls to instance of itself, what ML does - not accept; pr_rawtac0 denotes this instance of pr_tactic on - raw_tactic_expr *) - -let pr_rawtac = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : env -> raw_tactic_expr -> std_ppcmds) -let pr_rawtac0 = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : env -> raw_tactic_expr -> std_ppcmds) +open Pptactic let pr_arg pr x = spc () ++ pr x -let pr_metanum pr = function - | AN x -> pr x - | MetaNum (_,n) -> str "?" ++ int n +let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) -let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar (_,s) -> pr_id s +let pr_evaluable_reference = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> pr_global Idset.empty (Libnames.ConstRef sp) -let pr_or_meta pr = function - | AI x -> pr x - | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" +let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -116,22 +99,22 @@ let pr_induction_arg prc = function | ElimOnIdent (_,id) -> pr_id id | ElimOnAnonHyp n -> int n -let pr_match_pattern = function - | Term a -> pr_pattern a - | Subterm (None,a) -> str "[" ++ pr_pattern a ++ str "]" - | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pattern a ++ str "]" +let pr_match_pattern pr_pat = function + | Term a -> pr_pat a + | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]" + | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]" -let pr_match_hyps = function - | NoHypId mp -> str "_:" ++ pr_match_pattern mp - | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp +let pr_match_hyps pr_pat = function + | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp + | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp -let pr_match_rule m pr = function +let pr_match_rule m pr pr_pat = function | Pat ([],mp,t) when m -> - str "[" ++ pr_match_pattern mp ++ str "]" + str "[" ++ pr_match_pattern pr_pat mp ++ str "]" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t | Pat (rl,mp,t) -> - str "[" ++ prlist_with_sep (fun () -> str",") pr_match_hyps rl ++ - spc () ++ str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ + str "[" ++ prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++ + spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "] =>" ++ brk (1,4) ++ pr t | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t @@ -139,20 +122,20 @@ let pr_funvar = function | None -> spc () ++ str "()" | Some id -> spc () ++ pr_id id -let pr_let_clause k pr = function +let pr_let_clause k pr prc pr_cst = function | ((_,id),None,t) -> hov 0 (str k ++ pr_id id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t)) | ((_,id),Some c,t) -> hv 0 (str k ++ pr_id id ++ str" :" ++ brk(1,2) ++ - pr_may_eval pr_constr pr_constr c ++ + pr_may_eval prc prc pr_cst c ++ str " :=" ++ brk (1,1) ++ pr (TacArg t)) -let pr_let_clauses pr = function +let pr_let_clauses pr prc pr_cst = function | hd::tl -> hv 0 - (pr_let_clause "let " pr hd ++ spc () ++ - prlist_with_sep spc (pr_let_clause "with " pr) tl) + (pr_let_clause "let " pr prc pr_cst hd ++ spc () ++ + prlist_with_sep spc (pr_let_clause "with " pr prc pr_cst) tl) | [] -> anomaly "LetIn must declare at least one binding" let pr_rec_clause pr ((_,id),(l,t)) = @@ -181,15 +164,16 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -open Closure +let rec pr_tacarg_using_rule pr_gen = function + | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) + | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) + | [], [] -> mt () + | _ -> failwith "Inconsistent arguments of extended tactic" -let pr_evaluable_reference vars = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global vars (Libnames.ConstRef sp) -let pr_inductive vars ind = pr_global vars (Libnames.IndRef ind) +open Closure -let make_pr_tac (pr_constr,pr_lconstr,pr_cst,pr_ind,pr_ident,pr_extend) = +let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = let pr_bindings env = pr_bindings (pr_constr env) in let pr_ex_bindings env = pr_bindings_gen true (pr_constr env) in @@ -197,6 +181,7 @@ let pr_with_bindings env = pr_with_bindings (pr_constr env) in let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in let pr_constrarg env c = spc () ++ pr_constr env c in let pr_lconstrarg env c = spc () ++ pr_lconstr env c in + let pr_intarg n = spc () ++ int n in (* Printing tactics as arguments *) @@ -216,10 +201,9 @@ let rec pr_atom0 env = function (* Main tactic printer *) and pr_atom1 env = function | TacExtend (_,s,l) -> - pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s l + pr_extend (pr_constr env) (pr_tac env) s l | TacAlias (s,l,_) -> - pr_extend (Ppconstrnew.pr_constr_env env) (!pr_rawtac env) s - (List.map snd l) + pr_extend (pr_constr env) (pr_tac env) s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 env t @@ -304,7 +288,7 @@ and pr_atom1 env = function | TacDecompose (l,c) -> let vars = Termops.vars_of_env env in hov 1 (str "decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum (pr_ind vars)) l + hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum (pr_ind vars)) l ++ str "]" ++ pr_lconstrarg env c)) | TacSpecialize (n,c) -> hov 1 (str "specialize " ++ pr_opt int n ++ pr_with_bindings env c) @@ -329,9 +313,9 @@ and pr_atom1 env = function (* Context management *) | TacClear l -> - hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacClearBody l -> - hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacMove (b,(_,id1),(_,id2)) -> (* Rem: only b = true is available for users *) assert b; @@ -349,10 +333,10 @@ and pr_atom1 env = function | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l) | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l) | TacAnyConstructor (Some t) -> - hov 1 (str "constructor" ++ pr_arg (!pr_rawtac0 env) t) + hov 1 (str "constructor" ++ pr_arg (pr_tac0 env) t) | TacAnyConstructor None as t -> pr_atom0 env t | TacConstructor (n,l) -> - hov 1 (str "constructor" ++ pr_or_meta pr_intarg n ++ + hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l) (* Conversion *) @@ -406,18 +390,18 @@ let rec pr_tac env inherited tac = llet | TacLetIn (llc,u) -> v 0 - (hv 0 (pr_let_clauses (pr_tac env ltop) llc ++ str " in") ++ + (hv 0 (pr_let_clauses (pr_tac env ltop) (pr_constr env) pr_cst llc ++ + str " in") ++ fnl () ++ pr_tac env (llet,E) u), llet | TacLetCut llc -> assert false | TacMatch (t,lrul) -> hov 0 (str "match " ++ - pr_may_eval (Ppconstrnew.pr_constr_env env) - (Ppconstrnew.pr_lconstr_env env) t + pr_may_eval (pr_constr env) (pr_lconstr env) pr_cst t ++ str " with" ++ prlist (fun r -> fnl () ++ str "| " ++ - pr_match_rule true (pr_tac env ltop) r) + pr_match_rule true (pr_tac env ltop) pr_pat r) lrul ++ fnl() ++ str "end"), lmatch @@ -426,7 +410,7 @@ let rec pr_tac env inherited tac = str (if lr then "match reverse context with" else "match context with") ++ prlist (fun r -> fnl () ++ str "| " ++ - pr_match_rule false (pr_tac env ltop) r) + pr_match_rule false (pr_tac env ltop) pr_pat r) lrul ++ fnl() ++ str "end"), lmatch @@ -472,13 +456,13 @@ let rec pr_tac env inherited tac = str "solve" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet | TacId -> str "idtac", latom | TacAtom (_,t) -> hov 1 (pr_atom1 env t), ltatom - | TacArg(Tacexp e) -> !pr_rawtac0 env e, latom + | TacArg(Tacexp e) -> pr_tac0 env e, latom | TacArg(ConstrMayEval (ConstrTerm c)) -> str "'" ++ pr_constr env c, latom | TacArg(ConstrMayEval c) -> - pr_may_eval (pr_constr env) (pr_lconstr env) c, leval + pr_may_eval (pr_constr env) (pr_lconstr env) pr_cst c, leval | TacArg(Integer n) -> int n, latom | TacArg(TacCall(_,f,l)) -> - hov 1 (pr_reference f ++ spc () ++ + hov 1 (pr_ref f ++ spc () ++ prlist_with_sep spc (pr_tacarg env) l), lcall | TacArg a -> pr_tacarg env a, latom @@ -488,10 +472,10 @@ let rec pr_tac env inherited tac = and pr_tacarg env = function | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>") - | MetaNumArg (_,n) -> str ("?" ^ string_of_int n ) | MetaIdArg (_,s) -> str ("$" ^ s) + | Identifier id -> pr_id id | TacVoid -> str "()" - | Reference r -> pr_reference r + | Reference r -> pr_ref r | ConstrMayEval (ConstrTerm c) -> pr_constr env c | (ConstrMayEval _|TacCall _|Tacexp _|Integer _) as a -> str "'" ++ pr_tac env (latom,E) (TacArg a) @@ -500,18 +484,63 @@ in ((fun env -> pr_tac env ltop), (fun env -> pr_tac env (latom,E)), pr_match_rule) -let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) = - make_pr_tac - (Ppconstrnew.pr_constr_env, +let pi1 (a,_,_) = a +let pi2 (_,a,_) = a +let pi3 (_,_,a) = a + +let rec raw_printers = + (pr_raw_tactic, + pr_raw_tactic0, + Ppconstrnew.pr_constr_env, Ppconstrnew.pr_lconstr_env, - pr_metanum pr_reference, + Ppconstrnew.pr_pattern, + pr_or_metanum pr_reference, (fun _ -> pr_reference), - pr_or_meta (fun (loc,id) -> pr_id id), + pr_reference, + pr_or_metaid (pr_located pr_id), Pptactic.pr_raw_extend) -let _ = pr_rawtac := pr_raw_tactic -let _ = pr_rawtac0 := pr_raw_tactic0 +and pr_raw_tactic env (t:raw_tactic_expr) = + pi1 (make_pr_tac raw_printers) env t + +and pr_raw_tactic0 env t = + pi2 (make_pr_tac raw_printers) env t + +and pr_raw_match_rule env t = + pi3 (make_pr_tac raw_printers) env t + +let pr_and_constr_expr pr (c,_) = pr c + +let rec glob_printers = + (pr_glob_tactic, + pr_glob_tactic0, + (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env env)), + (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env env)), + Printer.pr_pattern, + pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)), + (fun vars -> pr_or_var (pr_inductive vars)), + pr_or_var pr_ltac_constant, + pr_located pr_id, + Pptactic.pr_glob_extend) -let pr_gen env = - Pptactic.pr_rawgen (Ppconstrnew.pr_constr_env env) - (pr_raw_tactic env) +and pr_glob_tactic env (t:glob_tactic_expr) = + pi1 (make_pr_tac glob_printers) env t + +and pr_glob_tactic0 env t = + pi2 (make_pr_tac glob_printers) env t + +and pr_glob_match_rule env t = + pi3 (make_pr_tac glob_printers) env t + +let (pr_tactic,_,_) = + make_pr_tac + (pr_glob_tactic, + pr_glob_tactic0, + Printer.prterm_env, + Printer.prterm_env, + Printer.pr_pattern, + pr_evaluable_reference, + pr_inductive, + pr_ltac_constant, + pr_id, + Pptactic.pr_extend) diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli index 41fc97da9..e6772405f 100644 --- a/translate/pptacticnew.mli +++ b/translate/pptacticnew.mli @@ -15,5 +15,7 @@ open Proof_type open Topconstr val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds -val pr_gen : Environ.env -> - (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds + +val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds + +val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index de0abed00..8e7aa2fc1 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -26,11 +26,22 @@ open Libnames open Ppextend open Topconstr +open Tacinterp + +(* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *) +let pr_raw_tactic_env l env t = + Pptacticnew.pr_raw_tactic env t + +let pr_gen env t = + Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env) + (Pptacticnew.pr_raw_tactic env) t + let pr_raw_tactic tac = - Pptacticnew.pr_raw_tactic (Global.env()) tac + pr_raw_tactic_env [] (Global.env()) tac + let pr_raw_tactic_goal n tac = let (_,env) = Pfedit.get_goal_context n in - Pptacticnew.pr_raw_tactic env tac + pr_raw_tactic_env [] env tac let pr_lconstr_goal n c = let (_,env) = Pfedit.get_goal_context n in Ppconstrnew.pr_lconstr_env env c @@ -451,7 +462,7 @@ let rec pr_vernac = function | None -> mt() | Some r -> str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_metanum pr_reference) r ++ + pr_red_expr (pr_constr, pr_lconstr, Pptactic.pr_or_metanum pr_reference) r ++ str" in" ++ spc() in let pr_def_body = function | DefineBody (bl,red,c,d) -> @@ -635,7 +646,9 @@ let rec pr_vernac = function b | _ -> mt(), body in pr_located pr_id id ++ ppb ++ str" :=" ++ brk(1,1) ++ - pr_raw_tactic body in + pr_raw_tactic_env + (List.map (fun ((_,id),_) -> (id,Lib.make_path id)) l) + (Global.env()) body in hov 1 ((if rc then str "Recursive " else mt()) ++ str "Tactic Definition " ++ @@ -676,7 +689,7 @@ let rec pr_vernac = function let pr_mayeval r c = match r with | Some r0 -> hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_metanum pr_reference) r0 ++ + pr_red_expr (pr_constr,pr_lconstr,Pptactic.pr_or_metanum pr_reference) r0 ++ spc() ++ str"in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) in pr_mayeval r c @@ -734,7 +747,7 @@ let rec pr_vernac = function and pr_extend s cl = let pr_arg a = - try Pptacticnew.pr_gen (Global.env()) a + try pr_gen (Global.env()) a with Failure _ -> str ("<error in "^s^">") in try let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in @@ -744,7 +757,7 @@ and pr_extend s cl = (fun (strm,args) pi -> match pi with Egrammar.TacNonTerm _ -> - (strm ++ Pptacticnew.pr_gen (Global.env()) (List.hd args), + (strm ++ pr_gen (Global.env()) (List.hd args), List.tl args) | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) (str hd,cl) rl in |