diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 186 |
1 files changed, 92 insertions, 94 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 14f88728..fead921a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) open Util open Names @@ -22,6 +22,7 @@ open Nametab open Pp open Topconstr open Termops +open Namegen (*s Flags governing the computation of implicit arguments *) @@ -34,9 +35,9 @@ type implicits_flags = { maximal : bool } -(* les implicites sont stricts par défaut en v8 *) +(* les implicites sont stricts par défaut en v8 *) -let implicit_args = ref { +let implicit_args = ref { auto = false; strict = true; strongly_strict = false; @@ -72,7 +73,7 @@ let is_maximal_implicit_args () = !implicit_args.maximal let with_implicits flags f x = let oflags = !implicit_args in - try + try implicit_args := flags; let rslt = f x in implicit_args := oflags; @@ -169,7 +170,7 @@ let is_flexible_reference env bound depth f = let push_lift d (e,n) = (push_rel d e,n+1) let is_reversible_pattern bound depth f l = - isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & + isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & array_for_all (fun c -> isRel c & destRel c < depth) l & array_distinct l @@ -194,37 +195,35 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = | Evar _ -> () | _ -> iter_constr_with_full_binders push_lift (frec rig) ed c - in + in frec true (env,1) m; acc (* calcule la liste des arguments implicites *) -let concrete_name avoid_flags l env_names n all c = - if n = Anonymous & noccurn 1 c then - (Anonymous,l) +let find_displayed_name_in all avoid na b = + if all then + compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b else - let fresh_id = next_name_not_occuring avoid_flags n l env_names c in - let idopt = if not all && noccurn 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::l) + compute_displayed_name_in (RenamingElsewhereFor b) avoid na b let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> - let na',avoid' = concrete_name None avoid names na all b in + let na',avoid' = find_displayed_name_in all avoid na b in 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) - | _ -> + | _ -> let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in if contextual then add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v - in - match kind_of_term (whd_betadeltaiota env t) with + in + match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> - let na',avoid = concrete_name None [] [] na all b in + 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 | _ -> [] @@ -232,16 +231,16 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rec prepare_implicits f = function | [] -> [] | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit" - | (Name id, Some imp)::imps -> + | (Name id, Some imp)::imps -> let imps' = prepare_implicits f imps in - Some (id,imp,set_maximality imps' f.maximal) :: imps' + 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 +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) @@ -256,44 +255,44 @@ let compute_manual_implicits env flags t enriching l = else compute_implicits_gen false false false true true env t in let n = List.length autoimps in let try_forced k l = - try - let (id, (b, f)), l' = assoc_by_pos k l in - if f then + try + let (id, (b, fi, fo)), l' = assoc_by_pos k l in + if fo then let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual,b) + l', Some (id,Manual,(b,fi)) else l, None with Not_found -> l, None in - if not (list_distinct l) then + if not (list_distinct l) then 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 -> let l',imp,m = - try - let (b, f) = List.assoc (ExplByName id) l in - List.remove_assoc (ExplByName id) l, (Some Manual), (Some b) + try + let (b, fi, fo) = List.assoc (ExplByName id) l in + List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi)) with Not_found -> - try - let (id, (b, f)), l' = assoc_by_pos k l in - l', (Some Manual), (Some b) + try + let (id, (b, fi, fo)), l' = assoc_by_pos k l in + l', (Some Manual), (Some (b,fi)) with Not_found -> - l,imp, if enriching && imp <> None then Some flags.maximal else None + l,imp, if enriching && imp <> None then Some (flags.maximal,true) else None in let imps' = merge (k+1) l' imps in - let m = Option.map (set_maximality imps') m in + let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in Option.map (set_implicit id imp) m :: imps' | (Anonymous,imp)::imps -> let l', forced = try_forced k l in forced :: merge (k+1) l' imps | [] when l = [] -> [] | [] -> - List.iter (function - | ExplByName id,(b,forced) -> + 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 + if i<1 or i>n then error ("Bad implicit argument number: "^(string_of_int i)) else errorlabstrm "" @@ -307,19 +306,20 @@ let const v _ = v let compute_implicits_auto 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) option + (identifier * implicit_explanation * (maximal_insertion * force_inference)) option type implicits_list = implicit_status list @@ -332,7 +332,11 @@ let name_of_implicit = function | Some (id,_,_) -> id let maximal_insertion_of = function - | Some (_,_,b) -> b + | 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 *) @@ -361,7 +365,7 @@ let compute_constant_implicits flags manual cst = (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where - $i$ are the implicit arguments of the inductive and $v$ the array of + $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) let compute_mib_implicits flags manual kn = @@ -386,7 +390,7 @@ let compute_mib_implicits flags manual kn = let compute_all_mib_implicits flags manual kn = let imps = compute_mib_implicits flags manual kn in - List.flatten + List.flatten (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) @@ -401,25 +405,18 @@ let compute_var_implicits flags manual id = let compute_global_implicits flags manual = function | VarRef id -> compute_var_implicits flags manual id | ConstRef kn -> compute_constant_implicits flags manual kn - | IndRef (kn,i) -> + | IndRef (kn,i) -> let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps - | ConstructRef ((kn,i),j) -> + | ConstructRef ((kn,i),j) -> let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) -let list_split_at index l = - let rec aux i acc = function - tl when i = index -> (List.rev acc), tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - let merge_impls oldimpls newimpls = - let (before, news), olds = + let (before, news), olds = let len = List.length newimpls - List.length oldimpls in if len >= 0 then list_split_at len newimpls, oldimpls - else + else let before, after = list_split_at (-len) oldimpls in (before, newimpls), after in @@ -437,8 +434,8 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal | ImplConstant of constant * implicits_flags - | ImplMutualInductive of kernel_name * implicits_flags - | ImplInteractive of global_reference * implicits_flags * + | ImplMutualInductive of mutual_inductive * implicits_flags + | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request let implicits_table = ref Refmap.empty @@ -457,11 +454,11 @@ let cache_implicits o = let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) -let subst_implicits (_,subst,(req,l)) = +let subst_implicits (subst,(req,l)) = (ImplLocal,list_smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None) + List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, (true,true)) else None) (List.filter (fun (_,_,b,_) -> b = None) ctx) let section_segment_of_reference = function @@ -473,9 +470,9 @@ let section_segment_of_reference = function let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> + | ImplInteractive (ref,flags,exp) -> let vars = section_segment_of_reference ref in - let ref' = pop_global_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 Some (ImplInteractive (ref',flags,exp),l') | ImplConstant (con,flags) -> @@ -483,58 +480,61 @@ let discharge_implicits (_,(req,l)) = let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in Some (ImplConstant (con',flags),l') | ImplMutualInductive (kn,flags) -> - let l' = List.map (fun (gr, l) -> + let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in - (pop_global_reference gr, impls_of_context vars @ l)) l + ((if isVarRef gr then gr else pop_global_reference gr), + impls_of_context vars @ l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') let rebuild_implicits (req,l) = - let l' = match req with + match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> + | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in let newimpls = compute_constant_implicits flags [] con in - [ConstRef con, merge_impls oldimpls newimpls] + req, [ConstRef con, merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags [] kn in - let rec aux olds news = + let rec aux olds news = match olds, news with | (_, oldimpls) :: old, (gr, newimpls) :: tl -> (gr, merge_impls oldimpls newimpls) :: aux old tl | [], [] -> [] | _, _ -> assert false - in aux l newimpls + in req, aux l newimpls | ImplInteractive (ref,flags,o) -> + (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with - | ImplAuto -> + | ImplAuto -> let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags [] ref in [ref,merge_impls oldimpls newimpls] - | ImplManual m -> + | ImplManual m -> let oldimpls = snd (List.hd l) in - let auto = + let auto = if flags.auto then let newimpls = compute_global_implicits flags [] ref in merge_impls oldimpls newimpls else oldimpls in - let l' = merge_impls auto m in [ref,l'] - in (req,l') + let l' = merge_impls auto m in + [ref,l'] -let export_implicits (req,_ as x) = - if req = ImplLocal then None else Some x +let classify_implicits (req,_ as obj) = + if req = ImplLocal then Dispose else Substitute obj let (inImplicits, _) = - declare_object {(default_object "IMPLICITS") with + declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; - classify_function = (fun (_,x) -> Substitute x); + classify_function = classify_implicits; discharge_function = discharge_implicits; - rebuild_function = rebuild_implicits; - export_function = export_implicits } + rebuild_function = rebuild_implicits } + +let is_local local ref = local || isVarRef ref && is_in_section ref let declare_implicits_gen req flags ref = let imps = compute_global_implicits flags [] ref in @@ -542,10 +542,10 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in - let req = - if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in + let req = + if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in declare_implicits_gen req flags ref - + let declare_var_implicits id = let flags = !implicit_args in declare_implicits_gen ImplLocal flags (VarRef id) @@ -561,11 +561,11 @@ let declare_mib_implicits kn = (compute_mib_implicits flags [] kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) - + (* Declare manual implicits *) -type manual_explicitation = Topconstr.explicitation * (bool * bool) - -let compute_implicits_with_manual env typ enriching l = +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 declare_manual_implicits local ref ?enriching l = @@ -575,7 +575,7 @@ let declare_manual_implicits local ref ?enriching l = let enriching = Option.default flags.auto enriching in let l' = compute_manual_implicits env flags t enriching l in let req = - if local or isVarRef ref then ImplLocal + if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual l') in add_anonymous_leaf (inImplicits (req,[ref,l'])) @@ -584,9 +584,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if l = [] then () else declare_manual_implicits local ref ?enriching l -let lift_implicits n = - List.map (fun x -> - match fst x with +let lift_implicits n = + List.map (fun x -> + match fst x with ExplByPos (k, id) -> ExplByPos (k + n, id), snd x | _ -> x) @@ -596,10 +596,8 @@ let init () = implicits_table := Refmap.empty let freeze () = !implicits_table let unfreeze t = implicits_table := t -let _ = +let _ = Summary.declare_summary "implicits" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } |