summaryrefslogtreecommitdiff
path: root/library/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.ml')
-rw-r--r--library/impargs.ml551
1 files changed, 551 insertions, 0 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
new file mode 100644
index 00000000..8a9429a4
--- /dev/null
+++ b/library/impargs.ml
@@ -0,0 +1,551 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: impargs.ml,v 1.59.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Util
+open Names
+open Libnames
+open Term
+open Reduction
+open Declarations
+open Environ
+open Inductive
+open Libobject
+open Lib
+open Nametab
+open Pp
+open Termops
+open Topconstr
+
+(*s Flags governing the computation of implicit arguments *)
+
+(* les implicites sont stricts par défaut en v8 *)
+let implicit_args = ref false
+let strict_implicit_args = ref (not !Options.v7)
+let contextual_implicit_args = ref false
+
+let implicit_args_out = ref false
+let strict_implicit_args_out = ref true
+let contextual_implicit_args_out = ref false
+
+let make_implicit_args flag =
+ implicit_args := flag;
+ if not !Options.v7_only then implicit_args_out := flag;
+ if !Options.translate_strict_impargs then
+ strict_implicit_args_out := not flag
+
+let make_strict_implicit_args flag =
+ strict_implicit_args := flag;
+ if not !Options.v7_only then strict_implicit_args_out := flag
+
+let make_contextual_implicit_args flag =
+ contextual_implicit_args := flag;
+ if not !Options.v7_only then contextual_implicit_args_out := flag
+
+let is_implicit_args () = !implicit_args
+let is_implicit_args_out () = !implicit_args_out
+let is_strict_implicit_args () = !strict_implicit_args
+let is_contextual_implicit_args () = !contextual_implicit_args
+
+type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
+
+let with_implicits ((a,b,c),(d,e,g)) f x =
+ let oa = !implicit_args in
+ let ob = !strict_implicit_args in
+ let oc = !contextual_implicit_args in
+ let od = !implicit_args_out in
+ let oe = !strict_implicit_args_out in
+ let og = !contextual_implicit_args_out in
+ try
+ implicit_args := a;
+ strict_implicit_args := b;
+ contextual_implicit_args := c;
+ implicit_args_out := d;
+ strict_implicit_args_out := e;
+ contextual_implicit_args_out := g;
+ let rslt = f x in
+ implicit_args := oa;
+ strict_implicit_args := ob;
+ contextual_implicit_args := oc;
+ implicit_args_out := od;
+ strict_implicit_args_out := oe;
+ contextual_implicit_args_out := og;
+ rslt
+ with e -> begin
+ implicit_args := oa;
+ strict_implicit_args := ob;
+ contextual_implicit_args := oc;
+ implicit_args_out := od;
+ strict_implicit_args_out := oe;
+ contextual_implicit_args_out := og;
+ raise e
+ end
+
+(*s Computation of implicit arguments *)
+
+(* We remember various information about why an argument is (automatically)
+ inferable as implicit
+
+- [DepRigid] means that the implicit argument can be found by
+ unification along a rigid path (we do not print the arguments of
+ this kind if there is enough arguments to infer them)
+
+- [DepFlex] means that the implicit argument can be found by unification
+ along a collapsable path only (e.g. as x in (P x) where P is another
+ argument) (we do (defensively) print the arguments of this kind)
+
+- [DepFlexAndRigid] means that the least argument from which the
+ implicit argument can be inferred is following a collapsable path
+ but there is a greater argument from where the implicit argument is
+ inferable following a rigid path (useful to know how to print a
+ partial application)
+
+ We also consider arguments inferable from the conclusion but it is
+ operational only if [conclusion_matters] is true.
+*)
+
+type argument_position =
+ | Conclusion
+ | Hyp of int
+
+type implicit_explanation =
+ | DepRigid of argument_position
+ | DepFlex of argument_position
+ | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+ | Manual
+
+let argument_less = function
+ | Hyp n, Hyp n' -> n<n'
+ | Hyp _, Conclusion -> true
+ | Conclusion, _ -> false
+
+let update pos rig (na,st) =
+ let e =
+ if rig then
+ match st with
+ | None -> DepRigid pos
+ | Some (DepRigid n as x) ->
+ if argument_less (pos,n) then DepRigid pos else x
+ | Some (DepFlexAndRigid (fpos,rpos) as x) ->
+ if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
+ if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
+ | Some (DepFlex fpos as x) ->
+ if argument_less (pos,fpos) or pos=fpos then DepRigid pos
+ else DepFlexAndRigid (fpos,pos)
+ | Some Manual -> assert false
+ else
+ match st with
+ | None -> DepFlex pos
+ | Some (DepRigid rpos as x) ->
+ if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x
+ | Some (DepFlexAndRigid (fpos,rpos) as x) ->
+ if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
+ | Some (DepFlex fpos as x) ->
+ if argument_less (pos,fpos) then DepFlex pos else x
+ | Some Manual -> assert false
+ in na, Some e
+
+(* modified is_rigid_reference with a truncated env *)
+let is_flexible_reference env bound depth f =
+ match kind_of_term f with
+ | 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 ->
+ let cb = Environ.lookup_constant kn env in
+ cb.const_body <> None & not cb.const_opaque
+ | Var id ->
+ let (_,value,_) = Environ.lookup_named id env in value <> None
+ | Ind _ | Construct _ -> false
+ | _ -> true
+
+let push_lift d (e,n) = (push_rel d e,n+1)
+
+(* Precondition: rels in env are for inductive types only *)
+let add_free_rels_until strict bound env m pos acc =
+ let rec frec rig (env,depth as ed) c =
+ match kind_of_term (whd_betadeltaiota env c) with
+ | Rel n when (n < bound+depth) & (n >= depth) ->
+ acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1))
+ | App (f,_) when rig & is_flexible_reference env bound depth f ->
+ if strict then () else
+ iter_constr_with_full_binders push_lift (frec false) ed c
+ | Case _ when rig ->
+ if strict then () else
+ iter_constr_with_full_binders push_lift (frec false) ed c
+ | _ ->
+ iter_constr_with_full_binders push_lift (frec rig) ed c
+ in
+ frec true (env,1) m; acc
+
+(* calcule la liste des arguments implicites *)
+
+let my_concrete_name avoid names t = function
+ | Anonymous -> Anonymous, avoid, Anonymous::names
+ | na ->
+ let id = Termops.next_name_not_occuring false na avoid names t in
+ Name id, id::avoid, Name id::names
+
+let compute_implicits_gen strict contextual 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' = Termops.concrete_name false avoid names na b in
+ add_free_rels_until strict 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 n env t Conclusion v
+ else v
+ in
+ match kind_of_term (whd_betadeltaiota env t) with
+ | Prod (na,a,b) ->
+ let na',avoid = Termops.concrete_name false [] [] na b in
+ let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
+ Array.to_list v
+ | _ -> []
+
+let compute_implicits output env t =
+ let strict =
+ (not output & !strict_implicit_args) or
+ (output & !strict_implicit_args_out) in
+ let contextual =
+ (not output & !contextual_implicit_args) or
+ (output & !contextual_implicit_args_out) in
+ let l = compute_implicits_gen strict contextual env t in
+ List.map (function
+ | (Name id, Some imp) -> Some (id,imp)
+ | (Anonymous, Some _) -> anomaly "Unnamed implicit"
+ | _ -> None) l
+
+type implicit_status =
+ (* None = Not implicit *)
+ (identifier * implicit_explanation) 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
+
+(* [in_ctx] means we now the expected type, [n] is the index of the argument *)
+let is_inferable_implicit in_ctx n = function
+ | None -> false
+ | Some (_,DepRigid (Hyp p)) -> n >= p
+ | Some (_,DepFlex (Hyp p)) -> false
+ | Some (_,DepFlexAndRigid (_,Hyp q)) -> n >= q
+ | Some (_,DepRigid Conclusion) -> in_ctx
+ | Some (_,DepFlex Conclusion) -> false
+ | Some (_,DepFlexAndRigid (_,Conclusion)) -> false
+ | Some (_,Manual) -> true
+
+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
+
+type strict_flag = bool (* true = strict *)
+type contextual_flag = bool (* true = contextual *)
+
+type implicits =
+ | Impl_auto of strict_flag * contextual_flag * implicits_list
+ | Impl_manual of implicits_list
+ | No_impl
+
+let auto_implicits env ty =
+ let impl =
+ if !implicit_args then
+ let l = compute_implicits false env ty in
+ Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
+ else
+ No_impl in
+ if Options.do_translate () then
+ impl,
+ if !implicit_args_out then
+ (let l = compute_implicits true env ty in
+ Impl_auto (!strict_implicit_args_out,!contextual_implicit_args_out,l))
+ else No_impl
+ else
+ impl, impl
+
+let list_of_implicits = function
+ | Impl_auto (_,_,l) -> l
+ | Impl_manual l -> l
+ | No_impl -> []
+
+(*s Constants. *)
+
+let constants_table = ref KNmap.empty
+
+let compute_constant_implicits kn =
+ let env = Global.env () in
+ let cb = lookup_constant kn env in
+ auto_implicits env (body_of_type cb.const_type)
+
+let constant_implicits sp =
+ try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl
+
+(*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
+ implicit arguments of the constructors. *)
+
+let inductives_table = ref Indmap.empty
+
+let constructors_table = ref Constrmap.empty
+
+let compute_mib_implicits kn =
+ let env = Global.env () in
+ 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, mip.mind_user_arity))
+ mib.mind_packets) in
+ let env_ar = push_rel_context ar env in
+ let imps_one_inductive i mip =
+ let ind = (kn,i) in
+ ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)),
+ Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
+ mip.mind_user_lc)
+ in
+ Array.mapi imps_one_inductive mib.mind_packets
+
+let inductive_implicits indp =
+ try Indmap.find indp !inductives_table with Not_found -> No_impl,No_impl
+
+let constructor_implicits consp =
+ try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl
+(*s Variables. *)
+
+let var_table = ref Idmap.empty
+
+let compute_var_implicits id =
+ let env = Global.env () in
+ let (_,_,ty) = lookup_named id env in
+ auto_implicits env ty
+
+let var_implicits id =
+ try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+
+(* Caching implicits *)
+
+let cache_implicits_decl (r,imps) =
+ match r with
+ | VarRef id ->
+ var_table := Idmap.add id imps !var_table
+ | ConstRef kn ->
+ constants_table := KNmap.add kn imps !constants_table
+ | IndRef indp ->
+ inductives_table := Indmap.add indp imps !inductives_table;
+ | ConstructRef consp ->
+ constructors_table := Constrmap.add consp imps !constructors_table
+
+let cache_implicits (_,l) = List.iter cache_implicits_decl l
+
+let subst_implicits_decl subst (r,imps as o) =
+ let r' = subst_global subst r in if r==r' then o else (r',imps)
+
+let subst_implicits (_,subst,l) =
+ list_smartmap (subst_implicits_decl subst) l
+
+let (in_implicits, _) =
+ declare_object {(default_object "IMPLICITS") with
+ cache_function = cache_implicits;
+ load_function = (fun _ -> cache_implicits);
+ subst_function = subst_implicits;
+ classify_function = (fun (_,x) -> Substitute x);
+ export_function = (fun x -> Some x) }
+
+(* Implicits of a global reference. *)
+
+let compute_global_implicits = function
+ | VarRef id -> compute_var_implicits id
+ | ConstRef kn -> compute_constant_implicits kn
+ | IndRef (kn,i) ->
+ let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+ | ConstructRef ((kn,i),j) ->
+ let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
+
+let declare_implicits_gen r =
+ add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
+
+let declare_implicits r =
+ with_implicits
+ ((true,!strict_implicit_args,!contextual_implicit_args),
+ (true,!strict_implicit_args_out,!contextual_implicit_args_out))
+ declare_implicits_gen r
+
+let declare_var_implicits id =
+ if !implicit_args or !implicit_args_out then
+ declare_implicits_gen (VarRef id)
+
+let declare_constant_implicits kn =
+ if !implicit_args or !implicit_args_out then
+ declare_implicits_gen (ConstRef kn)
+
+let declare_mib_implicits kn =
+ if !implicit_args or !implicit_args_out then
+ let imps = compute_mib_implicits kn in
+ let imps = array_map_to_list
+ (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
+ add_anonymous_leaf (in_implicits (List.flatten imps))
+
+let implicits_of_global_gen = function
+ | VarRef id -> var_implicits id
+ | ConstRef sp -> constant_implicits sp
+ | IndRef isp -> inductive_implicits isp
+ | ConstructRef csp -> constructor_implicits csp
+
+let implicits_of_global r =
+ let (imp_in,imp_out) = implicits_of_global_gen r in
+ list_of_implicits imp_in
+
+let implicits_of_global_out r =
+ let (imp_in,imp_out) = implicits_of_global_gen r in
+ list_of_implicits imp_out
+
+(* Declare manual implicits *)
+
+(*
+let check_range n = function
+ | loc,ExplByPos i ->
+ if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
+ | loc,ExplByName id ->
+()
+*)
+
+let rec list_remove a = function
+ | b::l when a = b -> l
+ | b::l -> b::list_remove a l
+ | [] -> raise Not_found
+
+let set_implicit id imp =
+ Some (id,match imp with None -> Manual | Some imp -> imp)
+
+let declare_manual_implicits r l =
+ let t = Global.type_of_global r in
+ let autoimps = compute_implicits_gen false true (Global.env()) t in
+ let n = List.length autoimps in
+ if not (list_distinct l) then
+ error ("Some parameters are referred more than once");
+(* List.iter (check_range n) l;*)
+(* let l = List.sort (-) l in*)
+ (* Compare with automatic implicits to recover printing data and names *)
+ let rec merge k l = function
+ | (Name id,imp)::imps ->
+ let l',imp =
+ try list_remove (ExplByPos k) l, set_implicit id imp
+ with Not_found ->
+ try list_remove (ExplByName id) l, set_implicit id imp
+ with Not_found ->
+ l, None in
+ imp :: merge (k+1) l' imps
+ | (Anonymous,imp)::imps ->
+ None :: merge (k+1) l imps
+ | [] when l = [] -> []
+ | _ ->
+ match List.hd l with
+ | ExplByName id ->
+ error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+ | ExplByPos i ->
+ 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") in
+ let l = Impl_manual (merge 1 l autoimps) in
+ let (_,oimp_out) = implicits_of_global_gen r in
+ let l = l, if !Options.v7_only then oimp_out else l in
+ add_anonymous_leaf (in_implicits [r,l])
+
+(* Tests if declared implicit *)
+
+let test = function
+ | No_impl | Impl_manual _ -> false,false,false
+ | Impl_auto (s,c,_) -> true,s,c
+
+let test_if_implicit find a =
+ try let b,c = find a in test b, test c
+ with Not_found -> (false,false,false),(false,false,false)
+
+let is_implicit_constant sp =
+ test_if_implicit (KNmap.find sp) !constants_table
+
+let is_implicit_inductive_definition indp =
+ test_if_implicit (Indmap.find (indp,0)) !inductives_table
+
+let is_implicit_var id =
+ test_if_implicit (Idmap.find id) !var_table
+
+(*s Registration as global tables *)
+
+let init () =
+ constants_table := KNmap.empty;
+ inductives_table := Indmap.empty;
+ constructors_table := Constrmap.empty;
+ var_table := Idmap.empty
+
+let freeze () =
+ (!constants_table, !inductives_table,
+ !constructors_table, !var_table)
+
+let unfreeze (ct,it,const,vt) =
+ constants_table := ct;
+ inductives_table := it;
+ constructors_table := const;
+ var_table := vt
+
+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 }
+
+(* Remark: flags implicit_args, contextual_implicit_args
+ are synchronized by the general options mechanism - see Vernacentries *)
+
+let init () =
+ (* strict_implicit_args_out must be not !Options.v7
+ but init is done before parsing *)
+ strict_implicit_args:=not !Options.v7;
+ implicit_args_out:=false;
+ (* strict_implicit_args_out needs to be not !Options.v7 or
+ Options.do_translate() but init is done before parsing *)
+ strict_implicit_args_out:=true;
+ contextual_implicit_args_out:=false
+
+let freeze () =
+ (!strict_implicit_args,
+ !implicit_args_out,!strict_implicit_args_out,!contextual_implicit_args_out)
+
+let unfreeze (b,d,e,f) =
+ strict_implicit_args := b;
+ implicit_args_out := d;
+ strict_implicit_args_out := e;
+ contextual_implicit_args_out := f
+
+let _ =
+ Summary.declare_summary "implicits-out-options"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = false;
+ Summary.survive_section = true }
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-15 16:02:17 +0000