diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 51 |
1 files changed, 38 insertions, 13 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 1bcff8695..5a44b5bdb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -169,7 +169,7 @@ let is_flexible_reference env bound depth f = | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true | Rel n -> (* since local definitions have been expanded *) false - | Const kn -> + | Const (kn,_) -> let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> @@ -214,6 +214,7 @@ let rec is_rigid_head t = match kind_of_term t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true | Case (_,_,f,_) -> is_rigid_head f + | Proj (p,c) -> true | App (f,args) -> (match kind_of_term f with | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) @@ -401,7 +402,14 @@ let compute_semi_auto_implicits env f manual t = let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst) + let cb = Environ.lookup_constant cst env in + let ty = cb.const_type in + let impls = compute_semi_auto_implicits env flags manual ty in + impls + (* match cb.const_proj with *) + (* | None -> impls *) + (* | Some {proj_npars = n} -> *) + (* List.map (fun (x,args) -> x, CList.skipn_at_least n args) impls *) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -413,14 +421,15 @@ let compute_mib_implicits flags manual kn = let mib = lookup_mind kn env in let ar = Array.to_list - (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> - (Name mip.mind_typename, None, type_of_inductive env (mib,mip))) + (Array.mapi (* No need to lift, arities contain no de Bruijn *) + (fun i mip -> + (** No need to care about constraints here *) + (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = type_of_inductive env (mib,mip) in + let ar = Global.type_of_global_unsafe (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) @@ -517,7 +526,7 @@ let section_segment_of_reference = function | ConstRef con -> section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> section_segment_of_mutual_inductive kn - | _ -> [] + | _ -> [], Univ.UContext.empty let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -532,24 +541,36 @@ let discharge_implicits (_,(req,l)) = | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> (try - let vars = section_segment_of_reference ref in + let vars,_ = section_segment_of_reference ref in + (* let isproj = *) + (* match ref with *) + (* | ConstRef cst -> is_projection cst (Global.env ()) *) + (* | _ -> false *) + (* in *) let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in - let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + let l' = + (* if isproj then [ref',snd (List.hd l)] *) + (* else *) + [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> (try let con' = pop_con con in - let vars = section_segment_of_constant con in + let vars,_ = section_segment_of_constant con in let extra_impls = impls_of_context vars in - let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + let newimpls = + (* if is_projection con (Global.env()) then (snd (List.hd l)) *) + (* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l)) + in + let l' = [ConstRef con',newimpls] in Some (ImplConstant (con',flags),l') with Not_found -> (* con not defined in this section *) Some (req,l)) | ImplMutualInductive (kn,flags) -> (try let l' = List.map (fun (gr, l) -> - let vars = section_segment_of_reference gr in + let vars,_ = section_segment_of_reference gr in let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), List.map (add_section_impls vars extra_impls) l)) l @@ -659,10 +680,14 @@ let check_rigidity isrigid = if not isrigid then errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") +let projection_implicits env p (x, impls) = + let pb = Environ.lookup_projection p env in + x, CList.skipn_at_least pb.Declarations.proj_npars impls + let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in - let t = Global.type_of_global ref in + let t = Global.type_of_global_unsafe ref in let enriching = Option.default flags.auto enriching in let isrigid,autoimpls = compute_auto_implicits env flags enriching t in let l' = match l with |