diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 24 | ||||
| -rw-r--r-- | vernac/classes.mli | 45 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 8 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 20 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 16 |
6 files changed, 53 insertions, 66 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 5a7f60584a..ea66234993 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -494,21 +494,8 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate -let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = +let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in - let tclass, ids = - match bk with - | Decl_kinds.Implicit -> - Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false - (fun avoid (clname, _) -> - match clname with - | Some cl -> - let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in - t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl - | Explicit -> cl, Id.Set.empty - in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass @@ -535,14 +522,13 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl - let new_instance ~pstate ?(global=false) ~program_mode - poly ctx (instid, bk, cl) props + poly instid ctx cl props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ~generalize ctx pl bk cl + interp_instance_context ~program_mode env ~generalize ctx pl cl in let id = match instid with @@ -555,10 +541,10 @@ let new_instance ~pstate ?(global=false) ~program_mode do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props -let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = +let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ctx pl bk cl + interp_instance_context ~program_mode env ctx pl cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid diff --git a/vernac/classes.mli b/vernac/classes.mli index 57bb9ce312..8d5f3e3a06 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -46,28 +46,29 @@ val declare_instance_constant : unit val new_instance : - pstate:Proof_global.t option -> - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - Vernacexpr.typeclass_constraint -> - (bool * constr_expr) option -> - ?generalize:bool -> - ?tac:unit Proofview.tactic -> - ?hook:(GlobRef.t -> unit) -> - Hints.hint_info_expr -> - (* May open a proof *) - Id.t * Proof_global.t option - -val declare_new_instance : - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - ident_decl * Decl_kinds.binding_kind * constr_expr -> - Hints.hint_info_expr -> - unit + pstate:Proof_global.t option + -> ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) option + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Proof_global.t option (* May open a proof *) + +val declare_new_instance + : ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> ident_decl + -> local_binder_expr list + -> constr_expr + -> Hints.hint_info_expr + -> unit (** {6 Low level interface used by Add Morphism, do not use } *) val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 6438b48e32..b2db64f74c 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -723,11 +723,11 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (fst namesup,snd namesup,t,props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> @@ -888,9 +888,9 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info -> - { VernacDeclareInstance (bl, (id, expl, t), info) } + { VernacDeclareInstance (id, bl, t, info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f2332bab8b..2e97a169cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -911,7 +911,7 @@ open Pputils spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (sup, (instid, bk, cl), props, info) -> + | VernacInstance (instid, sup, cl, props, info) -> return ( hov 1 ( keyword "Instance" ++ @@ -920,7 +920,6 @@ open Pputils | { v = Anonymous }, _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++ (match props with | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" @@ -929,13 +928,12 @@ open Pputils | None -> mt())) ) - | VernacDeclareInstance (sup, (instid, bk, cl), info) -> + | VernacDeclareInstance (instid, sup, cl, info) -> return ( hov 1 ( keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info) ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 697bb788ac..828356d31d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1062,18 +1062,18 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts sup inst props pri = +let vernac_instance ~atts name bl t props pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; + Dumpglob.dump_constraint (fst name) false "inst"; let program_mode = atts.program in - Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri + Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri -let vernac_declare_instance ~atts sup inst pri = +let vernac_declare_instance ~atts id bl inst pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; - Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri + Dumpglob.dump_definition (fst id) false "inst"; + Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri let vernac_context ~poly l = if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -2377,10 +2377,10 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = pstate (* Type classes *) - | VernacInstance (sup, inst, props, info) -> - snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info) - | VernacDeclareInstance (sup, inst, info) -> - with_def_attributes ~atts vernac_declare_instance sup inst info; + | VernacInstance (name, bl, t, props, info) -> + snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info) + | VernacDeclareInstance (id, bl, inst, info) -> + with_def_attributes ~atts vernac_declare_instance id bl inst info; pstate | VernacContext sup -> let () = vernac_context ~poly:(only_polymorphism atts) sup in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 23633e39ab..f946e0596e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -303,15 +303,17 @@ type nonrec vernac_expr = (* Type classes *) | VernacInstance of - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Hints.hint_info_expr + name_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + (bool * constr_expr) option * (* body (bool=true when using {}) *) + Hints.hint_info_expr | VernacDeclareInstance of - local_binder_expr list * (* super *) - (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *) - Hints.hint_info_expr + ident_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + Hints.hint_info_expr | VernacContext of local_binder_expr list |