diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 320 |
1 files changed, 0 insertions, 320 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml deleted file mode 100644 index ff09f73d..00000000 --- a/toplevel/autoinstance.ml +++ /dev/null @@ -1,320 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*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_secctx = None; - const_entry_type=None; - const_entry_opaque=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 (Option.get 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_secctx = None; - const_entry_body= def; - const_entry_opaque=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 when Errors.noncritical e -> - msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print 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_evar_map 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.optdepr=false; - 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()) } |