diff options
| -rw-r--r-- | library/impargs.ml | 11 | ||||
| -rw-r--r-- | library/impargs.mli | 11 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 12 | ||||
| -rw-r--r-- | toplevel/classes.ml | 46 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 |
5 files changed, 49 insertions, 33 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 4272f413a..687374c59 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -257,9 +257,7 @@ let rec assoc_by_pos k = function | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl | [] -> raise Not_found -let compute_manual_implicits flags ref enriching l = - let t = Global.type_of_global ref in - let env = Global.env () in +let compute_manual_implicits flags env t enriching l = let autoimps = if enriching then compute_implicits_flags env flags true t else compute_implicits_gen false false false true true env t in @@ -517,9 +515,14 @@ let declare_mib_implicits kn = (* Declare manual implicits *) type manual_explicitation = Topconstr.explicitation * (bool * bool) +let compute_implicits_with_manual env typ enriching l = + compute_manual_implicits !implicit_args env typ enriching l + let declare_manual_implicits local ref enriching l = let flags = !implicit_args in - let l' = compute_manual_implicits flags ref enriching l in + let env = Global.env () in + let t = Global.type_of_global ref in + let l' = compute_manual_implicits flags env t enriching l in let req = if local or isVarRef ref then ImplNoDischarge else ImplInteractive(ref,flags,ImplManual l') diff --git a/library/impargs.mli b/library/impargs.mli index 22c1ea23c..a9e6ccb91 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -55,6 +55,12 @@ val positions_of_implicits : implicits_list -> int list for an object of the given type in the given env *) val compute_implicits : env -> types -> implicits_list +(* A [manual_explicitation] is a tuple of a positional or named explicitation with + maximal insertion and forcing flags. *) +type manual_explicitation = Topconstr.explicitation * (bool * bool) + +val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list + (*s Computation of implicits (done using the global environment). *) val declare_var_implicits : variable -> unit @@ -63,13 +69,8 @@ val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : bool -> global_reference -> unit -(* A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion and forcing flags. *) -type manual_explicitation = Topconstr.explicitation * (bool * bool) - (* Manual declaration of which arguments are expected implicit *) val declare_manual_implicits : bool -> global_reference -> bool -> manual_explicitation list -> unit val implicits_of_global : global_reference -> implicits_list - diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 16e8de970..c514d3234 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -61,8 +61,16 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0). (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) -Notation in_right := (@right _ _ _). -Notation in_left := (@left _ _ _). + +(** These type arguments should be infered from the context. *) + +Implicit Arguments left [[A]]. +Implicit Arguments right [[B]]. + +(** Hide proofs and generates obligations when put in a term. *) + +Notation left := (left _ _). +Notation right := (right _ _). (** Extraction directives *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7ee4513d1..f3db79833 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -84,7 +84,7 @@ let rec unfold n f acc = (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr -let declare_implicit_proj c proj = +let declare_implicit_proj c proj imps = let len = List.length c.cl_context + List.length c.cl_super + List.length c.cl_params in let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in let expls = @@ -96,16 +96,18 @@ let declare_implicit_proj c proj = | (Anonymous,_) :: _ -> assert(false) in aux 1 [] ctx - in Impargs.declare_manual_implicits true (ConstRef proj) true expls + in + let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in + Impargs.declare_manual_implicits true (ConstRef proj) true expls -let declare_implicits cl = +let declare_implicits impls cl = let projs = Recordops.lookup_projections cl.cl_impl in - List.iter - (fun c -> + List.iter2 + (fun c imps -> match c with | None -> assert(false) - | Some p -> declare_implicit_proj cl p) - projs; + | Some p -> declare_implicit_proj cl p imps) + projs impls; let indimps = list_map_i (fun i (na, b, t) -> ExplByPos (i, Some na), (false, true)) @@ -149,22 +151,24 @@ let declare_structure env id idbuild params arity fields = Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); rsp +let interp_type_evars evdref env ?(impls=([],[])) typ = + let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in + let imps = Implicit_quantifiers.implicits_of_rawterm typ' in + imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' + -let mk_interning_data env na typ = - let impl = - if Impargs.is_implicit_args() then - Impargs.compute_implicits env typ - else [] +let mk_interning_data env na impls typ = + let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls in (na, ([], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env avoid l = List.fold_left - (fun (env, ids, params, impls) ((loc, i), t) -> - let t' = interp_type_evars isevars env ~impls t in - let data = mk_interning_data env i t' in + (fun (env, uimpls, ids, params, impls) ((loc, i), t) -> + let impl, t' = interp_type_evars isevars env ~impls t in + let data = mk_interning_data env i impl t' in let d = (i,None,t') in - (push_named d env, i :: ids, d::params, ([], data :: snd impls))) - (env, avoid, [], ([], [])) l + (push_named d env, impl :: uimpls, i :: ids, d::params, ([], data :: snd impls))) + (env, [], avoid, [], ([], [])) l let new_class id par ar sup props = let env0 = Global.env() in @@ -186,12 +190,12 @@ let new_class id par ar sup props = let env_params, avoid, ctx_params = interp_binders_evars isevars env_super avoid par in (* Interpret the arity *) - let arity = interp_type_evars isevars env_params (CSort (fst ar, snd ar)) in + let _arity_imps, arity = interp_type_evars isevars env_params (CSort (fst ar, snd ar)) in (* let fullarity = it_mkProd_or_LetIn (it_mkProd_or_LetIn arity ctx_defs) ctx_params in*) (* Interpret the definitions and propositions *) - let env_props, avoid, ctx_props, _ = + let env_props, prop_impls, avoid, ctx_props, _ = interp_fields_evars isevars env_params avoid props in @@ -229,7 +233,7 @@ let new_class id par ar sup props = cl_props = ctx_props; cl_impl = kn } in - declare_implicits k; + declare_implicits (List.rev prop_impls) k; add_class k open Decl_kinds @@ -345,7 +349,7 @@ let new_instance sup (instid, bk, cl) props = let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst | Implicit -> - let t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in + let _imps, t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in match kind_of_term t' with App (c, args) -> substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 102f1b8b0..ec494622c 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -28,7 +28,7 @@ type binder_def_list = (identifier located * identifier located list * constr_ex val binders_of_lidents : identifier located list -> local_binder list -val declare_implicit_proj : typeclass -> constant -> unit +val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> unit val infer_super_instances : env -> constr list -> named_context -> named_context -> types list * identifier list * named_context |