aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml39
-rw-r--r--interp/implicit_quantifiers.ml53
-rw-r--r--interp/implicit_quantifiers.mli14
-rw-r--r--interp/topconstr.ml6
-rw-r--r--interp/topconstr.mli3
5 files changed, 76 insertions, 39 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9b8f62aa0..cfa88f3cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -696,17 +696,8 @@ let push_loc_name_env lvar (ids,unb,tmpsc,scopes as env) loc = function
let intern_generalized_binder intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
let ty =
if t then ty else
- let is_class =
- try
- let (loc, r, _ as clapp) = Implicit_quantifiers.destClassAppExpl ty in
- let (loc, qid) = qualid_of_reference r in
- let gr = Nametab.locate qid in
- if Typeclasses.is_class gr then Some (clapp, gr) else None
- with Not_found -> None
- in
- match is_class with
- | None -> ty
- | Some (clapp, gr) -> Implicit_quantifiers.full_class_binder ids clapp gr
+ Implicit_quantifiers.implicit_application ids
+ Implicit_quantifiers.combine_params_freevar ty
in
let ty = intern_type (ids,true,tmpsc,sc) ty in
let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty in
@@ -731,6 +722,30 @@ let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl)
((name_fold Idset.add na ids,unb,ts,sc),
(na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
+ let c = intern (ids,true,tmp_scope,scopes) c in
+ let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
+ let env', c' =
+ let abs =
+ let pi =
+ match ak with
+ | Some AbsPi -> true
+ | None when tmp_scope = Some Notation.type_scope
+ || List.mem Notation.type_scope scopes -> true
+ | _ -> false
+ in
+ if pi then
+ (fun (id, loc') acc ->
+ RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+ else
+ (fun (id, loc') acc ->
+ RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+ in
+ List.fold_right (fun (id, loc as lid) (env, acc) ->
+ let env' = push_loc_name_env lvar env loc (Name id) in
+ (env', abs lid acc)) fvs (env,c)
+ in c'
+
(**********************************************************************)
(* Utilities for application *)
@@ -897,6 +912,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CNotation (_,"( _ )",([a],[])) -> intern env a
| CNotation (loc,ntn,args) ->
intern_notation intern env loc ntn args
+ | CGeneralization (loc,b,a,c) ->
+ intern_generalization intern env lvar loc b a c
| CPrim (loc, p) ->
let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
Dumpglob.dump_notation_location (fst (unloc loc)) df;
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4daf21955..876af8f54 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -200,14 +200,12 @@ let combine_params avoid fn applied needed =
| (x,_) :: _, [] ->
user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
-
-let combine_params_freevar avoid applied needed =
- combine_params avoid
- (fun avoid (_, (na, _, _)) ->
- let id' = next_name_away_from na avoid in
- (CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
- applied needed
+let combine_params_freevar =
+ fun avoid (_, (na, _, _)) ->
+ let id' = next_name_away_from na avoid in
+ (CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
+
let destClassApp cl =
match cl with
| CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
@@ -221,19 +219,34 @@ let destClassAppExpl cl =
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-let full_class_binder env (loc, id, l) gr =
- let avoid =
- Idset.union env (ids_of_list
- (free_vars_of_constr_expr (CApp (loc, (None, mkRefC id), l)) ~bound:env []))
- in
- let c, avoid =
- let c = class_info gr in
- let (ci, rd) = c.cl_context in
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params_freevar avoid l pars in
- CAppExpl (loc, (None, id), args), avoid
- in c
-
+let implicit_application env ?(allow_partial=true) f ty =
+ let is_class =
+ try
+ let (loc, r, _ as clapp) = destClassAppExpl ty in
+ let (loc, qid) = qualid_of_reference r in
+ let gr = Nametab.locate qid in
+ if Typeclasses.is_class gr then Some (clapp, gr) else None
+ with Not_found -> None
+ in
+ match is_class with
+ | None -> ty
+ | Some ((loc, id, par), gr) ->
+ let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+ let c, avoid =
+ let c = class_info gr in
+ let (ci, rd) = c.cl_context in
+ if not allow_partial then
+ begin
+ let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in
+ if needlen <> applen then
+ Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+ end;
+ let pars = List.rev (List.combine ci rd) in
+ let args, avoid = combine_params avoid f par pars in
+ CAppExpl (loc, (None, id), args), avoid
+ in c
+
let implicits_of_rawterm l =
let rec aux i c =
match c with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 744b45272..593427209 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -43,13 +43,11 @@ val free_vars_of_binders :
val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
-val combine_params : Names.Idset.t ->
+val combine_params_freevar :
+ Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+ Topconstr.constr_expr * Names.Idset.t
+
+val implicit_application : Idset.t -> ?allow_partial:bool ->
(Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
Topconstr.constr_expr * Names.Idset.t) ->
- (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
- ((global_reference * bool) option * Term.rel_declaration) list ->
- Topconstr.constr_expr list * Names.Idset.t
-
-val full_class_binder : Idset.t ->
- loc * reference * (constr_expr * explicitation located option) list ->
- global_reference -> constr_expr
+ constr_expr -> constr_expr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 935d95fc5..c0b81c90c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -608,6 +608,8 @@ type explicitation = ExplByPos of int * identifier option | ExplByName of identi
type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool
+type abstraction_kind = AbsLambda | AbsPi
+
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
@@ -648,6 +650,7 @@ type constr_expr =
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_expr notation_substitution
+ | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -715,6 +718,7 @@ let constr_loc = function
| CSort (loc,_) -> loc
| CCast (loc,_,_) -> loc
| CNotation (loc,_,_) -> loc
+ | CGeneralization (loc,_,_,_) -> loc
| CPrim (loc,_) -> loc
| CDelimiters (loc,_,_) -> loc
| CDynamic _ -> dummy_loc
@@ -798,6 +802,7 @@ let fold_constr_expr_with_binders g f n acc = function
| CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
| CCast (loc,a,CastCoerce) -> f n acc a
| CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
+ | CGeneralization (_,_,_,c) -> f n acc c
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
@@ -910,6 +915,7 @@ let map_constr_expr_with_binders g f e = function
| CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
| CNotation (loc,n,(l,ll)) ->
CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
+ | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b2d74beed..0064d238d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -104,6 +104,8 @@ type binder_kind =
(* Inner binding, outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
+type abstraction_kind = AbsLambda | AbsPi
+
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
@@ -144,6 +146,7 @@ type constr_expr =
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_expr notation_substitution
+ | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 08:57:50 +0000