diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 40 | ||||
| -rw-r--r-- | interp/constrintern.mli | 16 |
2 files changed, 48 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 156d155667..49b719bdb5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1144,17 +1144,36 @@ let intern_pattern env patt = let intern_ltac isarity ltacvars sigma env c = intern_gen isarity sigma env ~ltacvars:ltacvars c +type manual_implicits = (explicitation * (bool * bool)) list + +let implicits_of_rawterm l = + let rec aux i c = + match c with + RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true)) :: rest + else rest + | RLetIn (loc, na, t, b) -> aux i b + | _ -> [] + in aux 1 l + (*********************************************************************) (* Functions to parse and interpret constructions *) let interp_gen kind sigma env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - Default.understand_gen kind sigma env - (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c) + let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in + Default.understand_gen kind sigma env c let interp_constr sigma env c = - interp_gen (OfType None) sigma env c + interp_gen (OfType None) sigma env c let interp_type sigma env ?(impls=([],[])) c = interp_gen IsType sigma env ~impls c @@ -1168,9 +1187,20 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) +let interp_constr_evars_gen_impls evdref env ?(impls=([],[])) kind c = + let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let imps = implicits_of_rawterm c in + Default.understand_tcc_evars evdref env kind c, imps + let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = - Default.understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c) + let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + Default.understand_tcc_evars evdref env kind c + +let interp_casted_constr_evars_impls evdref env ?(impls=([],[])) c typ = + interp_constr_evars_gen_impls evdref env ~impls (OfType (Some typ)) c + +let interp_type_evars_impls evdref env ?(impls=([],[])) c = + interp_constr_evars_gen_impls evdref env IsType ~impls c let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f4272a2b19..9f3a815ee0 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -45,6 +45,8 @@ type var_internalisation_data = type implicits_env = (identifier * var_internalisation_data) list type full_implicits_env = identifier list * implicits_env +type manual_implicits = (explicitation * (bool * bool)) list + type ltac_sign = identifier list * unbound_ltac_var_map (*s Internalisation performs interpretation of global names and notations *) @@ -74,14 +76,22 @@ val interp_gen : typing_constraint -> evar_map -> env -> val interp_constr : evar_map -> env -> constr_expr -> constr -val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> - constr_expr -> types -> constr - val interp_type : evar_map -> env -> ?impls:full_implicits_env -> constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> + constr_expr -> types -> constr + +(* Accepting evars and giving back the manual implicits in addition. *) + +val interp_casted_constr_evars_impls : evar_defs ref -> env -> + ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits + +val interp_type_evars_impls : evar_defs ref -> env -> ?impls:full_implicits_env -> + constr_expr -> types * manual_implicits + val interp_casted_constr_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr |