diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 316 |
1 files changed, 316 insertions, 0 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml new file mode 100644 index 00000000..b45e45c8 --- /dev/null +++ b/toplevel/autoinstance.ml @@ -0,0 +1,316 @@ +(************************************************************************) +(* 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:$ *) + +(*i*) +open Pp +open Printer +open Names +open Term +open Evd +open Sign +open Libnames +(*i*) + +(*s + * Automatic detection of (some) record instances + *) + +(* Datatype for wannabe-instances: a signature is a typeclass along + with the collection of evars corresponding to the parameters/fields + of the class. Each evar can be uninstantiated (we're still looking + for them) or defined (the instance for the field is fixed) *) +type signature = global_reference * evar list * evar_map + +type instance_decl_function = global_reference -> rel_context -> constr list -> unit + +(* + * Search algorithm + *) + +let rec subst_evar evar def n c = + match kind_of_term c with + | Evar (e,_) when e=evar -> lift n def + | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c + +let subst_evar_in_evm evar def evm = + Evd.fold + (fun ev evi acc -> + let evar_body = match evi.evar_body with + | Evd.Evar_empty -> Evd.Evar_empty + | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in + let evar_concl = subst_evar evar def 0 evi.evar_concl in + Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl} + ) evm empty + +(* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev : + * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated + * by this definition. *) + +let rec safe_define evm ev c = + if not (closedn (-1) c) then raise Termops.CannotFilter else +(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) + let evi = (Evd.find evm ev) in + let define_subst evm sigma = + Util.Intmap.fold + ( fun ev (e,c) evm -> + match kind_of_term c with Evar (i,_) when i=ev -> evm | _ -> + safe_define evm ev (lift (-List.length e) c) + ) sigma evm in + match evi.evar_body with + | Evd.Evar_defined def -> + define_subst evm (Termops.filtering [] Reduction.CUMUL def c) + | Evd.Evar_empty -> + let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in + let u = Libtypes.reduce (evar_concl evi) in + let evm = subst_evar_in_evm ev c evm in + define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u) + +let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = + let rec really_new_evar () = + let ev = Evarutil.new_untyped_evar() in + if Evd.is_evar evm ev then really_new_evar() else ev in + let add_gen_evar (cl,gen,evm) ev ty : signature = + let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in + (cl,ev::gen,evm) in + let rec mksubst b = function + | [] -> [] + | a::tl -> b::(mksubst (a::b) tl) in + let evl = List.map (fun _ -> really_new_evar()) ctx in + let evcl = List.map (fun i -> mkEvar (i,[||])) evl in + let substl = List.rev (mksubst [] (evcl)) in + let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in + let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in + sign,evcl + +(* TODO : for full proof-irrelevance in the search, provide a real + compare function for constr instead of Pervasive's one! *) +module SubstSet : Set.S with type elt = Termops.subst + = Set.Make (struct type t = Termops.subst + let compare = Util.Intmap.compare (Pervasives.compare) + end) + +(* searches instatiations in the library for just one evar [ev] of a + signature. [k] is called on each resulting signature *) +let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = + let ev_typ = Libtypes.reduce (evar_concl evi) in + let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in +(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*) + let substs = ref SubstSet.empty in + try List.iter + ( fun (gr,(pat,_),s) -> + let (_,genl,_) = Termops.decompose_prod_letin pat in + let genl = List.map (fun (_,_,t) -> t) genl in + let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in + let def = applistc (Libnames.constr_of_global gr) argl in +(* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() + ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) + (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) + try + let evm = safe_define evm ev def in + k (cl,gen,evm); + if sort_is_prop && SubstSet.mem s !substs then raise Exit; + substs := SubstSet.add s !substs + with Termops.CannotFilter -> () + ) (Libtypes.search_concl ev_typ) + with Exit -> () + +let evm_fold_rev f evm acc = + let l = Evd.fold (fun ev evi acc -> (ev,evi)::acc) evm [] in + List.fold_left (fun acc (ev,evi) -> f ev evi acc) acc l + +exception Continue of Evd.evar * Evd.evar_info + +(* searches matches for all the uninstantiated evars of evd in the + context. For each totally instantiated evar_map found, apply + k. *) +let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) = + try + evm_fold_rev + ( fun ev evi _ -> + if not (is_defined evm ev) && not (List.mem ev gen) then + raise (Continue (ev,evi)) + ) evm (); k (cl,gen,evm) + with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k) + +(* define all permutations of the evars to evd and call k on the + resulting evd *) +let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit) : unit = + let rec aux evm = List.iter + ( fun (ctx,ev) -> + let tyl = List.map (fun (_,_,t) -> t) ctx in + let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in + let def = applistc c argl in +(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) + try + if not (Evd.is_defined evm ev) then + let evm = safe_define evm ev def in + aux evm; k (cl,gen,evm) + with Termops.CannotFilter -> () + ) evl in + aux evm + +let new_inst_no = + let cnt = ref 0 in + fun () -> incr cnt; string_of_int !cnt + +let make_instance_ident gr = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no()) + +let new_instance_message ident typ def = + Flags.if_verbose + msgnl (str"new instance"++spc() + ++Nameops.pr_id ident++spc()++str":"++spc() + ++pr_constr typ++spc()++str":="++spc() + ++pr_constr def) + +open Entries + +let rec deep_refresh_universes c = + match kind_of_term c with + | Sort (Type _) -> Termops.new_Type() + | _ -> map_constr deep_refresh_universes c + +let declare_record_instance gr ctx params = + let ident = make_instance_ident gr in + let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in + let def = deep_refresh_universes def in + let ce = { const_entry_body=def; const_entry_type=None; + const_entry_opaque=false; const_entry_boxed=false } in + let cst = Declare.declare_constant ident + (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in + new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def + +let declare_class_instance gr ctx params = + let ident = make_instance_ident gr in + let cl = Typeclasses.class_info gr in + let (def,typ) = Typeclasses.instance_constructor cl params in + let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in + let def = deep_refresh_universes def in + let typ = deep_refresh_universes typ in + let ce = Entries.DefinitionEntry + { const_entry_type=Some typ; const_entry_body=def; + const_entry_opaque=false; const_entry_boxed=false } in + try + let cst = Declare.declare_constant ident + (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in + Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst)); + new_instance_message ident typ def + with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Cerrors.explain_exn e) + +let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t; + match kind_of_term t with + | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c + | _ -> () + +(* main search function: search for total instances containing gr, and + apply k to each of them *) +let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit = + let gr_c = Libnames.constr_of_global gr in + let (smap:(Libnames.global_reference * Evd.evar_map, + ('a * 'b * Term.constr) list * Evd.evar) + Gmapl.t ref) = ref Gmapl.empty in + iter_under_prod + ( fun ctx typ -> + List.iter + (fun ((cl,ev,evm),_,_) -> +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) + smap := Gmapl.add (cl,evm) (ctx,ev) !smap) + (Recordops.methods_matching typ) + ) [] deftyp; + Gmapl.iter + ( fun (cl,evm) evl -> + let f = if Typeclasses.is_class cl then + declare_class_instance else declare_record_instance in + complete_with_evars_permut (cl,[],evm) evl gr_c + (fun sign -> complete_signature (k f) sign) + ) !smap + +(* + * Interface with other parts: hooks & declaration + *) + + +let evar_definition evi = match evar_body evi with + Evar_empty -> assert false | Evar_defined c -> c + +let gen_sort_topo l evm = + let iter_evar f ev = + let rec aux c = match kind_of_term c with + Evar (e,_) -> f e + | _ -> iter_constr aux c in + aux (Evd.evar_concl (Evd.find evm ev)); + if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in + let r = ref [] in + let rec dfs ev = iter_evar dfs ev; + if not(List.mem ev !r) then r := ev::!r in + List.iter dfs l; List.rev !r + +(* register real typeclass instance given a totally defined evd *) +let declare_instance (k:global_reference -> rel_context -> constr list -> unit) + (cl,gen,evm:signature) = + let evm = Evarutil.nf_evars evm in + let gen = gen_sort_topo gen evm in + let (evm,gen) = List.fold_right + (fun ev (evm,gen) -> + if Evd.is_defined evm ev + then Evd.remove evm ev,gen + else evm,(ev::gen)) + gen (evm,[]) in +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) + let ngen = List.length gen in + let (_,ctx,evm) = List.fold_left + ( fun (i,ctx,evm) ev -> + let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in + let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in + (i-1,ctx,evm) + ) (ngen,[],evm) gen in + let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in + k cl ctx fields + +let autoinstance_opt = ref true + +let search_declaration gr = + if !autoinstance_opt && + not (Lib.is_modtype()) then + let deftyp = Global.type_of_global gr in + complete_signature_with_def gr deftyp declare_instance + +let search_record k cons sign = + if !autoinstance_opt && not (Lib.is_modtype()) then + complete_signature (declare_instance k) (cons,[],sign) + +(* +let dh_key = Profile.declare_profile "declaration_hook" +let ch_key = Profile.declare_profile "class_decl_hook" +let declaration_hook = Profile.profile1 dh_key declaration_hook +let class_decl_hook = Profile.profile1 ch_key class_decl_hook +*) + +(* + * Options and bookeeping + *) + +let begin_autoinstance () = + if not !autoinstance_opt then ( + autoinstance_opt := true; + ) + +let end_autoinstance () = + if !autoinstance_opt then ( + autoinstance_opt := false; + ) + +let _ = + Goptions.declare_bool_option + { Goptions.optsync=true; + Goptions.optkey=["Autoinstance"]; + Goptions.optname="automatic typeclass instance recognition"; + Goptions.optread=(fun () -> !autoinstance_opt); + Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) } |