diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 105 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | interp/genarg.ml | 35 | ||||
| -rw-r--r-- | interp/genarg.mli | 43 |
4 files changed, 74 insertions, 111 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b476320150..641ccf7fc5 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 5d66424c24..99e7d68bbc 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 b25908b42e..0f2e031cc7 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 f1246b2cc6..c938d4c516 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 |