diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 270 |
1 files changed, 181 insertions, 89 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 19f7e094e..615b568b3 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -27,14 +27,12 @@ open Namegen type implicits_flags = { auto : bool; (* automatic or manual only *) strict : bool; (* true = strict *) - strongly_strict : bool; (* true = strongly strict *) + strongly_strict : bool; (* true = strongly strict *) reversible_pattern : bool; contextual : bool; (* true = contextual *) maximal : bool } -(* les implicites sont stricts par défaut en v8 *) - let implicit_args = ref { auto = false; strict = true; @@ -196,6 +194,17 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = in frec true (env,1) m; acc +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 + | App (f,args) -> + (match kind_of_term f with + | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) + | _ -> is_rigid_head f) + | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ + | Prod _ | Meta _ | Cast _ -> assert false + (* calcule la liste des arguments implicites *) let find_displayed_name_in all avoid na b = @@ -205,6 +214,7 @@ let find_displayed_name_in all avoid na b = compute_displayed_name_in (RenamingElsewhereFor b) avoid na b let compute_implicits_gen strict strongly_strict revpat contextual all env t = + let rigid = ref true in let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with @@ -213,6 +223,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) | _ -> + rigid := is_rigid_head t; let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in if contextual then @@ -223,8 +234,66 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na b in let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in - Array.to_list v - | _ -> [] + !rigid, Array.to_list v + | _ -> true, [] + +let compute_implicits_flags env f all t = + compute_implicits_gen + (f.strict or f.strongly_strict) f.strongly_strict + f.reversible_pattern f.contextual all env t + +let compute_auto_implicits env flags enriching t = + if enriching then compute_implicits_flags env flags true t + else compute_implicits_gen false false false true true env t + +(* Extra information about implicit arguments *) + +type maximal_insertion = bool (* true = maximal contextual insertion *) +type force_inference = bool (* true = always infer, never turn into evar/subgoal *) + +type implicit_status = + (* None = Not implicit *) + (identifier * implicit_explanation * (maximal_insertion * force_inference)) option + +type implicit_side_condition = DefaultImpArgs | LessArgsThan of int + +type implicits_list = implicit_side_condition * implicit_status list + +let is_status_implicit = function + | None -> false + | _ -> true + +let name_of_implicit = function + | None -> anomaly "Not an implicit argument" + | Some (id,_,_) -> id + +let maximal_insertion_of = function + | Some (_,_,(b,_)) -> b + | None -> anomaly "Not an implicit argument" + +let force_inference_of = function + | Some (_, _, (_, b)) -> b + | None -> anomaly "Not an implicit argument" + +(* [in_ctx] means we know the expected type, [n] is the index of the argument *) +let is_inferable_implicit in_ctx n = function + | None -> false + | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p + | Some (_,DepFlex (Hyp p),_) -> false + | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q + | Some (_,DepRigid Conclusion,_) -> in_ctx + | Some (_,DepFlex Conclusion,_) -> false + | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx + | Some (_,Manual,_) -> true + +let positions_of_implicits (_,impls) = + let rec aux n = function + [] -> [] + | Some _ :: l -> n :: aux (n+1) l + | None :: l -> aux (n+1) l + in aux 1 impls + +(* Manage user-given implicit arguments *) let rec prepare_implicits f = function | [] -> [] @@ -234,11 +303,6 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let compute_implicits_flags env f all t = - compute_implicits_gen - (f.strict or f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env t - let set_implicit id imp insmax = (id,(match imp with None -> Manual | Some imp -> imp),insmax) @@ -247,11 +311,20 @@ 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 env flags 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 - let n = List.length autoimps in +let check_correct_manual_implicits autoimps l = + List.iter (function + | ExplByName id,(b,fi,forced) -> + if not forced then + error ("Wrong or non-dependent implicit argument name: "^(string_of_id id)^".") + | ExplByPos (i,_id),_t -> + if i<1 or i>List.length autoimps then + error ("Bad implicit argument number: "^(string_of_int i)^".") + else + errorlabstrm "" + (str "Cannot set implicit argument number " ++ int i ++ + str ": it has no name.")) l + +let set_manual_implicits env flags enriching autoimps l = let try_forced k l = try let (id, (b, fi, fo)), l' = assoc_by_pos k l in @@ -262,7 +335,7 @@ let compute_manual_implicits env flags t enriching l = with Not_found -> l, None in if not (list_distinct l) then - error ("Some parameters are referred more than once"); + error ("Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> @@ -285,79 +358,28 @@ let compute_manual_implicits env flags t enriching l = forced :: merge (k+1) l' imps | [] when l = [] -> [] | [] -> - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) - | ExplByPos (i,_id),_t -> - if i<1 or i>n then - error ("Bad implicit argument number: "^(string_of_int i)) - else - errorlabstrm "" - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name")) - l; [] + check_correct_manual_implicits autoimps l; + [] in merge 1 l autoimps -let compute_implicits_auto env f manual t = +let compute_semi_auto_implicits env f manual t = match manual with | [] -> if not f.auto then [] - else let l = compute_implicits_flags env f false t in - prepare_implicits f l - | _ -> compute_manual_implicits env f t f.auto manual - -let compute_implicits env t = compute_implicits_auto env !implicit_args [] t - -type maximal_insertion = bool (* true = maximal contextual insertion *) -type force_inference = bool (* true = always infer, never turn into evar/subgoal *) - -type implicit_status = - (* None = Not implicit *) - (identifier * implicit_explanation * (maximal_insertion * force_inference)) option - -type implicits_list = implicit_status list - -let is_status_implicit = function - | None -> false - | _ -> true - -let name_of_implicit = function - | None -> anomaly "Not an implicit argument" - | Some (id,_,_) -> id - -let maximal_insertion_of = function - | Some (_,_,(b,_)) -> b - | None -> anomaly "Not an implicit argument" - -let force_inference_of = function - | Some (_, _, (_, b)) -> b - | None -> anomaly "Not an implicit argument" - -(* [in_ctx] means we know the expected type, [n] is the index of the argument *) -let is_inferable_implicit in_ctx n = function - | None -> false - | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p - | Some (_,DepFlex (Hyp p),_) -> false - | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q - | Some (_,DepRigid Conclusion,_) -> in_ctx - | Some (_,DepFlex Conclusion,_) -> false - | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx - | Some (_,Manual,_) -> true + else let _,l = compute_implicits_flags env f false t in + [DefaultImpArgs, prepare_implicits f l] + | _ -> + let _,autoimpls = compute_auto_implicits env f f.auto t in + [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] -let positions_of_implicits = - let rec aux n = function - [] -> [] - | Some _ :: l -> n :: aux (n+1) l - | None :: l -> aux (n+1) l - in aux 1 +let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t (*s Constants. *) let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_implicits_auto env flags manual (Typeops.type_of_constant env cst) + compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -377,9 +399,9 @@ let compute_mib_implicits flags manual kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,compute_implicits_auto env flags manual ar), + ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c)) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets @@ -394,7 +416,7 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - compute_implicits_auto env flags manual ty + compute_semi_auto_implicits env flags manual ty (* Implicits of a global reference. *) @@ -408,12 +430,15 @@ let compute_global_implicits flags manual = function (* Merge a manual explicitation with an implicit_status list *) -let merge_impls oldimpls newimpls = - List.map2 (fun orig ni -> +let merge_one_impls_block (cond,oldimpls) (_,newimpls) = + cond, List.map2 (fun orig ni -> match orig with | Some (_, Manual, _) -> orig | _ -> ni) oldimpls newimpls +let merge_impls oldimpls newimpls = + List.map2 merge_one_impls_block oldimpls newimpls + (* Caching implicits *) type implicit_interactive_request = @@ -456,23 +481,35 @@ let section_segment_of_reference = function section_segment_of_mutual_inductive kn | _ -> [] +let adjust_side_condition p = function + | LessArgsThan n -> LessArgsThan (n+p) + | DefaultImpArgs -> DefaultImpArgs + +let add_section_impls vars extra_impls (cond,impls)= + let p = List.length vars - List.length extra_impls in + adjust_side_condition p cond, extra_impls @ impls + let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> let vars = section_segment_of_reference ref in let ref' = if isVarRef ref then ref else pop_global_reference ref in - let l' = [ref', impls_of_context vars @ snd (List.hd l)] 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 Some (ImplInteractive (ref',flags,exp),l') | ImplConstant (con,flags) -> let con' = pop_con con in - let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] 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 Some (ImplConstant (con',flags),l') | ImplMutualInductive (kn,flags) -> let l' = List.map (fun (gr, l) -> 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), - impls_of_context vars @ l)) l + List.map (add_section_impls vars extra_impls) l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') @@ -504,7 +541,9 @@ let rebuild_implicits (req,l) = let oldimpls = snd (List.hd l) in if flags.auto then let newimpls = compute_global_implicits flags [] ref in - [ref, merge_impls oldimpls newimpls] + assert (List.tl newimpls = []); + let newimpls = List.map (fun _ -> List.hd newimpls) oldimpls in + [ref,merge_impls oldimpls newimpls] else [ref,oldimpls] @@ -552,14 +591,42 @@ let declare_mib_implicits kn = type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) let compute_implicits_with_manual env typ enriching l = - compute_manual_implicits env !implicit_args typ enriching l + let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in + set_manual_implicits env !implicit_args enriching autoimpls l + +let check_inclusion l = + (* Check strict inclusion *) + let rec aux = function + | n1::(n2::_ as nl) -> + if n1 <= n2 then + error "Sequences of implicit arguments must be of different lengths"; + aux nl + | _ -> () in + aux (List.map (fun (imps,_) -> List.length imps) l) + +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 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 enriching = Option.default flags.auto enriching in - let l' = compute_manual_implicits env flags t enriching l in + let isrigid,autoimpls = compute_auto_implicits env flags enriching t in + let l' = match l with + | [] -> assert false + | [l] -> + [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + | _ -> + check_rigidity isrigid; + let l = List.map (fun imps -> (imps,List.length imps)) l in + let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in + check_inclusion l; + let nargs = List.length autoimpls in + List.map (fun (imps,n) -> + (LessArgsThan (nargs-n), + set_manual_implicits env flags enriching autoimpls imps)) l in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual) @@ -568,7 +635,14 @@ let declare_manual_implicits local ref ?enriching l = let maybe_declare_manual_implicits local ref ?enriching l = if l = [] then () - else declare_manual_implicits local ref ?enriching l + else declare_manual_implicits local ref ?enriching [l] + +let extract_impargs_data impls = + let rec aux p = function + | (DefaultImpArgs, imps)::_ -> [None,imps] + | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l + | [] -> [] in + aux 0 impls let lift_implicits n = List.map (fun x -> @@ -576,6 +650,24 @@ let lift_implicits n = ExplByPos (k, id) -> ExplByPos (k + n, id), snd x | _ -> x) +let make_implicits_list l = [DefaultImpArgs, l] + +let rec drop_first_implicits p = function + | _,[] as x -> x + | DefaultImpArgs,imp::impls -> + drop_first_implicits (p-1) (DefaultImpArgs,impls) + | LessArgsThan n,imp::impls -> + let n = if is_status_implicit imp then n-1 else n in + drop_first_implicits (p-1) (LessArgsThan n,impls) + +let rec select_impargs_size n = function + | [] -> [] + | [_, impls] | (DefaultImpArgs, impls)::_ -> impls + | (LessArgsThan p, impls)::l -> + if n <= p then impls else select_impargs_size n l + +let rec select_stronger_impargs = function [] -> [] | (_,impls)::_ -> impls + (*s Registration as global tables *) let init () = implicits_table := Refmap.empty |