aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/classes.ml505
-rw-r--r--toplevel/classes.mli65
-rw-r--r--toplevel/command.ml61
-rw-r--r--toplevel/command.mli12
-rw-r--r--toplevel/coqinit.ml1
-rw-r--r--toplevel/himsg.ml33
-rw-r--r--toplevel/himsg.mli3
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/vernacentries.ml44
-rw-r--r--toplevel/vernacexpr.ml30
-rw-r--r--toplevel/whelp.ml46
13 files changed, 733 insertions, 34 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 5a1b8b8b4..bad30a849 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -77,6 +77,8 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
| PretypeError(ctx,te) ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
+ | Typeclasses_errors.TypeClassError(env, te) ->
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
| InductiveError e ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
| RecursionSchemeError e ->
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
new file mode 100644
index 000000000..7ee4513d1
--- /dev/null
+++ b/toplevel/classes.ml
@@ -0,0 +1,505 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Termops
+open Sign
+open Entries
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Typeclasses_errors
+open Typeclasses
+open Libnames
+open Constrintern
+open Rawterm
+open Topconstr
+(*i*)
+
+let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
+(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
+let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+
+type binder_list = (identifier located * constr_expr) list
+
+let interp_binders_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) ((loc, i), t) ->
+ let n = Name i in
+ let t' = interp_binder_evars isevars env n t in
+ let d = (i,None,t') in
+ (push_named d env, i :: ids, d::params))
+ (env, avoid, []) l
+
+let interp_typeclass_context_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) (iid, bk, l) ->
+ let t' = interp_binder_evars isevars env (snd iid) l in
+ let i = match snd iid with
+ | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
+ | Name id -> id
+ in
+ let d = (i,None,t') in
+ (push_named d env, i :: ids, d::params))
+ (env, avoid, []) l
+
+let interp_constrs_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params) t ->
+ let t' = interp_binder_evars isevars env Anonymous t in
+ let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
+ let d = (id,None,t') in
+ (push_named d env, id :: ids, d::params))
+ (env, avoid, []) l
+
+let raw_assum_of_binders k =
+ List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t))
+
+let raw_assum_of_constrs k =
+ List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t))
+
+let raw_assum_of_anonymous_constrs k =
+ List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t))
+
+let decl_expr_of_binders =
+ List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t))
+
+let rec unfold n f acc =
+ match n with
+ | 0 -> f 0 acc
+ | n -> unfold (n - 1) f (f n acc)
+
+(* Declare everything in the parameters as implicit, and the class instance as well *)
+open Topconstr
+
+let declare_implicit_proj c proj =
+ let len = List.length c.cl_context + List.length c.cl_super + List.length c.cl_params in
+ let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in
+ let expls =
+ let rec aux i expls = function
+ [] -> expls
+ | (Name n, _) :: tl ->
+ let impl = ExplByPos (i, Some n), (true, true) in
+ aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl
+ | (Anonymous,_) :: _ -> assert(false)
+ in
+ aux 1 [] ctx
+ in Impargs.declare_manual_implicits true (ConstRef proj) true expls
+
+let declare_implicits cl =
+ let projs = Recordops.lookup_projections cl.cl_impl in
+ List.iter
+ (fun c ->
+ match c with
+ | None -> assert(false)
+ | Some p -> declare_implicit_proj cl p)
+ projs;
+ let indimps =
+ list_map_i
+ (fun i (na, b, t) -> ExplByPos (i, Some na), (false, true))
+ 1 (List.rev cl.cl_context)
+ in
+ Impargs.declare_manual_implicits true (IndRef cl.cl_impl) false indimps
+
+let rel_of_named_context subst l =
+ List.fold_right
+ (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
+ l ([], subst)
+
+let degenerate_decl (na,b,t) =
+ let id = match na with
+ | Name id -> id
+ | Anonymous -> anomaly "Unnamed record variable" in
+ match b with
+ | None -> (id, Entries.LocalAssum t)
+ | Some b -> (id, Entries.LocalDef b)
+
+
+let declare_structure env id idbuild params arity fields =
+ let nparams = List.length params and nfields = List.length fields in
+ let args = extended_rel_list nfields params in
+ let ind = applist (mkRel (1+nparams+nfields), args) in
+ let type_constructor = it_mkProd_or_LetIn ind fields in
+ let mie_ind =
+ { mind_entry_typename = id;
+ mind_entry_arity = arity;
+ mind_entry_consnames = [idbuild];
+ mind_entry_lc = [type_constructor] } in
+ let mie =
+ { mind_entry_params = List.map degenerate_decl params;
+ mind_entry_record = true;
+ mind_entry_finite = true;
+ mind_entry_inds = [mie_ind] } in
+ let kn = Command.declare_mutual_with_eliminations true mie in
+ let rsp = (kn,0) in (* This is ind path of idstruc *)
+ let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in
+ let _build = ConstructRef (rsp,1) in
+ Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+ rsp
+
+
+let mk_interning_data env na typ =
+ let impl =
+ if Impargs.is_implicit_args() then
+ Impargs.compute_implicits env typ
+ else []
+ in (na, ([], impl, Notation.compute_arguments_scope typ))
+
+let interp_fields_evars isevars env avoid l =
+ List.fold_left
+ (fun (env, ids, params, impls) ((loc, i), t) ->
+ let t' = interp_type_evars isevars env ~impls t in
+ let data = mk_interning_data env i t' in
+ let d = (i,None,t') in
+ (push_named d env, i :: ids, d::params, ([], data :: snd impls)))
+ (env, avoid, [], ([], [])) l
+
+let new_class id par ar sup props =
+ let env0 = Global.env() in
+ let isevars = ref (Evd.create_evar_defs Evd.empty) in
+ let avoid = Termops.ids_of_context env0 in
+
+ let env_params, avoid = env0, avoid in
+
+ (* Find the implicitly quantified variables *)
+ let gen_ctx, super = Implicit_quantifiers.resolve_class_binders (vars_of_env env0) sup in
+
+ let env_super_ctx, avoid, ctx_super_ctx = interp_binders_evars isevars env_params avoid gen_ctx in
+
+ (* Interpret the superclasses constraints *)
+ let env_super, avoid, ctx_super0 =
+ interp_typeclass_context_evars isevars env_super_ctx avoid super
+ in
+
+ let env_params, avoid, ctx_params = interp_binders_evars isevars env_super avoid par in
+
+ (* Interpret the arity *)
+ let arity = interp_type_evars isevars env_params (CSort (fst ar, snd ar)) in
+
+ (* let fullarity = it_mkProd_or_LetIn (it_mkProd_or_LetIn arity ctx_defs) ctx_params in*)
+
+ (* Interpret the definitions and propositions *)
+ let env_props, avoid, ctx_props, _ =
+ interp_fields_evars isevars env_params avoid props
+ in
+
+ (* Instantiate evars and check all are resolved *)
+ let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
+ let sigma = Evd.evars_of isevars in
+ let ctx_super_ctx = Implicit_quantifiers.nf_named_context sigma ctx_super_ctx in
+ let ctx_super = Implicit_quantifiers.nf_named_context sigma ctx_super0 in
+ let ctx_params = Implicit_quantifiers.nf_named_context sigma ctx_params in
+ let ctx_props = Implicit_quantifiers.nf_named_context sigma ctx_props in
+ let arity = Reductionops.nf_evar sigma arity in
+ let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
+ let kn =
+ let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
+ let params, subst = rel_of_named_context [] (ctx_params @ ctx_super @ ctx_super_ctx) in
+ let fields, _ = rel_of_named_context subst ctx_props in
+ List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
+ declare_structure env0 (snd id) idb params arity fields
+ in
+ let ctx_context, ctx_super =
+ let class_binders, regular_binders =
+ List.partition (fun (na, b, t) ->
+ Typeclasses.class_of_constr t <> None)
+ ctx_super_ctx
+ in
+ if (ctx_super_ctx = class_binders @ regular_binders) then
+ regular_binders, ctx_super @ class_binders
+ else ctx_super_ctx, ctx_super
+ in
+ let k =
+ { cl_name = snd id;
+ cl_context = ctx_context;
+ cl_super = ctx_super;
+ cl_params = ctx_params;
+ cl_props = ctx_props;
+ cl_impl = kn }
+ in
+ declare_implicits k;
+ add_class k
+
+open Decl_kinds
+open Entries
+
+let hint_db = "typeclass_instances"
+
+let add_instance_hint inst =
+ Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))])
+
+let declare_instance (_,id) =
+ add_instance_hint id
+
+type binder_def_list = (identifier located * identifier located list * constr_expr) list
+
+let binders_of_lidents l =
+ List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole loc)) l
+
+let subst_ids_in_named_context subst l =
+ let x, _ =
+ List.fold_right
+ (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k)
+ l ([], 1)
+ in x
+
+let subst_one_named inst ids t =
+ substnl inst 0 (substn_vars 1 ids t)
+
+let subst_named inst subst ctx =
+ let ids = List.map (fun (id, _, _) -> id) subst in
+ let ctx' = subst_ids_in_named_context ids ctx in
+ let ctx', _ =
+ List.fold_right
+ (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
+ ctx' ([], 0)
+ in ctx'
+
+let push_named_context = List.fold_right push_named
+
+let destClass c =
+ match kind_of_term c with
+ App (c, args) ->
+ (match kind_of_term c with
+ | Ind ind -> (try class_of_inductive ind, args with _ -> assert false)
+ | _ -> assert false)
+ | _ -> assert false
+
+let infer_super_instances env params params_ctx super =
+ let super = subst_named params params_ctx super in
+ List.fold_right
+ (fun (na, _, t) (sups, ids, supctx) ->
+ let t = subst_one_named sups ids t in
+ let inst =
+ try resolve_one_typeclass env t
+ with Not_found ->
+ let cl, args = destClass t in
+ no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args)
+ in
+ let d = (na, Some inst, t) in
+ inst :: sups, na :: ids, d :: supctx)
+ super ([], [], [])
+
+(* let evars_of_context ctx id n env = *)
+(* List.fold_right (fun (na, _, t) (n, env, nc) -> *)
+(* let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *)
+(* let d = (na, Some b, t) in *)
+(* (succ n, push_named d env, d :: nc)) *)
+(* ctx (n, env, []) *)
+
+let type_ctx_instance isevars env ctx inst subst =
+ List.fold_left2
+ (fun (subst, instctx) (na, _, t) ce ->
+ let t' = replace_vars subst t in
+ let c = interp_casted_constr_evars isevars env ce t' in
+ let d = na, Some c, t' in
+ (na, c) :: subst, d :: instctx)
+ (subst, []) (List.rev ctx) inst
+
+let substitution_of_constrs ctx cstrs =
+ List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
+
+let destClassApp cl =
+ match cl with
+ | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+ | _ -> raise Not_found
+
+let new_instance sup (instid, bk, cl) props =
+ let id, par = destClassApp cl in
+ let env = Global.env() in
+ let isevars = ref (Evd.create_evar_defs Evd.empty) in
+ let avoid = Termops.ids_of_context env in
+ let k =
+ try class_info (snd id)
+ with Not_found -> unbound_class env id
+ in
+ let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
+ let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
+ let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
+ let subst =
+ match bk with
+ Explicit ->
+ if List.length par <> List.length k.cl_context + List.length k.cl_params then
+ mismatched_params env par (k.cl_params @ k.cl_context);
+ let len = List.length k.cl_context in
+ let ctx, par = Util.list_chop len par in
+ let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in
+ let subst =
+ Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst
+ k.cl_super
+ in
+ if List.length par <> List.length k.cl_params then
+ mismatched_params env par k.cl_params;
+ let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst
+
+ | Implicit ->
+ let t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in
+ match kind_of_term t' with
+ App (c, args) ->
+ substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context)
+ (List.rev (Array.to_list args))
+ | _ -> assert false
+ in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let sigma = Evd.evars_of !isevars in
+ let env' = Implicit_quantifiers.nf_env sigma env' in
+ let subst = Typeclasses.nf_substitution sigma subst in
+ let subst, propsctx =
+ let props =
+ List.map (fun (x, l, d) ->
+ Topconstr.abstract_constr_expr d (binders_of_lidents l))
+ props
+ in
+ if List.length props <> List.length k.cl_props then
+ mismatched_props env' props k.cl_props;
+ type_ctx_instance isevars env' k.cl_props props subst
+ in
+ let app =
+ applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
+ in
+ let term = Termops.it_mkNamedLambda_or_LetIn (Termops.it_mkNamedLambda_or_LetIn app supctx) genctx in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let term = Evarutil.nf_isevar !isevars term in
+ let cdecl =
+ let kind = IsDefinition Instance in
+ let entry =
+ { const_entry_body = term;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = false }
+ in DefinitionEntry entry, kind
+ in
+ let id, cst =
+ let instid =
+ match snd instid with
+ Name id -> id
+ | Anonymous ->
+ let i = Nameops.add_suffix (snd id) "_instance_" in
+ Termops.next_global_ident_away false i (Termops.ids_of_context env)
+ in
+ instid, Declare.declare_constant instid cdecl
+ in
+ let inst =
+ { is_class = k;
+ is_name = id;
+(* is_params = paramsctx; (\* missing gen_ctx *\) *)
+(* is_super = superctx; *)
+ is_impl = cst;
+(* is_add_hint = (fun () -> add_instance_hint id); *)
+ }
+ in
+ add_instance_hint id;
+ add_instance inst
+
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+
+let solve_by_tac env evd evar evi t =
+ let goal = {it = evi; sigma = (Evd.evars_of evd) } in
+ let (res, valid) = t goal in
+ if res.it = [] then
+ let prooftree = valid [] in
+ let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in
+ if obls = [] then
+ let evd' = evars_reset_evd res.sigma evd in
+ let evd' = evar_define evar proofterm evd' in
+ evd', true
+ else evd, false
+ else evd, false
+
+let context l =
+ let env = Global.env() in
+ let isevars = ref (Evd.create_evar_defs Evd.empty) in
+ let avoid = Termops.ids_of_context env in
+ let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in
+ let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in
+ let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let sigma = Evd.evars_of !isevars in
+ let fullctx = Implicit_quantifiers.nf_named_context sigma (l @ ctx) in
+ List.iter (function (id,_,t) ->
+ Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id))
+ (List.rev fullctx)
+
+(* let init () = hints := [] *)
+(* let freeze () = !hints *)
+(* let unfreeze fs = hints := fs *)
+
+(* let _ = Summary.declare_summary "hints db" *)
+(* { Summary.freeze_function = freeze; *)
+(* Summary.unfreeze_function = unfreeze; *)
+(* Summary.init_function = init; *)
+(* Summary.survive_module = false; *)
+(* Summary.survive_section = true } *)
+
+open Libobject
+
+(* let cache (_, db) := hints := db *)
+
+(* let (input,output) = *)
+(* declare_object *)
+(* { (default_object "hints db") with *)
+(* cache_function = cache; *)
+(* load_function = (fun _ -> cache); *)
+(* open_function = (fun _ -> cache); *)
+(* classify_function = (fun (_,x) -> Keep x); *)
+(* export_function = (fun x -> Some x) } *)
+
+let tactic = ref Tacticals.tclIDTAC
+let tactic_expr = ref (Obj.magic ())
+
+let set_instantiation_tactic t =
+ tactic := Tacinterp.interp t; tactic_expr := t
+
+let freeze () = !tactic_expr
+let unfreeze t = set_instantiation_tactic t
+let init () =
+ set_instantiation_tactic (Tacexpr.TacId[])
+
+let cache (_, tac) =
+ set_instantiation_tactic tac
+
+let _ =
+ Summary.declare_summary "typeclasses instantiation tactic"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init;
+ Summary.survive_module = true;
+ Summary.survive_section = true }
+
+let (input,output) =
+ declare_object
+ { (default_object "type classes instantiation tactic state") with
+ cache_function = cache;
+ load_function = (fun _ -> cache);
+ open_function = (fun _ -> cache);
+ classify_function = (fun (_,x) -> Keep x);
+ export_function = (fun x -> Some x) }
+
+let set_instantiation_tactic t =
+ Lib.add_anonymous_leaf (input t)
+
+
+let initialize () =
+ if !tactic_expr = Tacexpr.TacId [] then
+ let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")) in
+ Library.require_library [qualid] None
+
+let _ =
+ Typeclasses.solve_instanciation_problem :=
+ (fun env -> initialize ();
+ fun evd ev evi ->
+ solve_by_tac env evd ev evi !tactic)
+
+
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
new file mode 100644
index 000000000..102f1b8b0
--- /dev/null
+++ b/toplevel/classes.mli
@@ -0,0 +1,65 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Topconstr
+open Util
+open Typeclasses
+open Implicit_quantifiers
+(*i*)
+
+type binder_list = (identifier located * constr_expr) list
+type binder_def_list = (identifier located * identifier located list * constr_expr) list
+
+val binders_of_lidents : identifier located list -> local_binder list
+
+val declare_implicit_proj : typeclass -> constant -> unit
+
+val infer_super_instances : env -> constr list ->
+ named_context -> named_context -> types list * identifier list * named_context
+
+val new_class : identifier located ->
+ binder_list ->
+ Vernacexpr.sort_expr located ->
+ typeclass_context ->
+ binder_list -> unit
+
+val new_instance :
+ typeclass_context ->
+ typeclass_constraint ->
+ binder_def_list ->
+ unit
+
+val context : typeclass_context -> unit
+
+val add_instance_hint : identifier -> unit
+
+val declare_instance : identifier located -> unit
+
+val set_instantiation_tactic : Tacexpr.raw_tactic_expr -> unit
+
+val mismatched_params : env -> constr_expr list -> named_context -> 'a
+
+val mismatched_props : env -> constr_expr list -> named_context -> 'a
+
+val solve_by_tac : env ->
+ Evd.evar_defs ->
+ Evd.evar ->
+ evar_info ->
+ Proof_type.tactic ->
+ Evd.evar_defs * bool
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 05ee50daf..445555251 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -46,21 +46,21 @@ open Goptions
open Mod_subst
open Evd
-let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
+let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
+let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
let rec abstract_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+ | LocalRawAssum (idl,k,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl
(abstract_constr_expr c bl)
let rec generalize_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+ | LocalRawAssum (idl,k,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl
(generalize_constr_expr c bl)
let rec under_binders env f n c =
@@ -103,10 +103,13 @@ let definition_message id =
let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
let sigma = Evd.empty in
let env = Global.env() in
- match comtypopt with
+ match comtypopt with
None ->
let b = abstract_constr_expr com bl in
- let j = interp_constr_judgment sigma env b in
+ let ib = intern_constr sigma env b in
+ let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+ let j = Default.understand_judgment sigma env ib in
+ imps,
{ const_entry_body = j.uj_val;
const_entry_type = None;
const_entry_opaque = opacity;
@@ -115,7 +118,10 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
(* We use a cast to avoid troubles with evars in comtyp *)
(* that can only be resolved knowing com *)
let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
- let (body,typ) = destSubCast (interp_constr sigma env b) in
+ let ib = intern_gen false sigma env b in
+ let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+ let (body,typ) = destSubCast (Default.understand_gen (OfType None) sigma env ib) in
+ imps,
{ const_entry_body = body;
const_entry_type = Some typ;
const_entry_opaque = opacity;
@@ -130,15 +136,18 @@ let red_constant_entry bl ce = function
(local_binders_length bl)
body }
-let declare_global_definition ident ce local =
+let declare_global_definition ident ce local imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
- if local = Local && Flags.is_verbose() then
- msg_warning (pr_id ident ++ str" is declared as a global definition");
- definition_message ident;
- ConstRef kn
+ let gr = ConstRef kn in
+ if Impargs.is_implicit_args () || imps <> [] then
+ declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ if local = Local && Flags.is_verbose() then
+ msg_warning (pr_id ident ++ str" is declared as a global definition");
+ definition_message ident;
+ gr
let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
- let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
+ let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
let ce' = red_constant_entry bl ce red_option in
let r = match local with
| Local when Lib.sections_are_opened () ->
@@ -152,7 +161,7 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
str" is not visible from current goals");
VarRef ident
| (Global|Local) ->
- declare_global_definition ident ce' local in
+ declare_global_definition ident ce' local imps in
hook local r
let syntax_definition ident c local onlyparse =
@@ -550,8 +559,8 @@ let eq_constr_expr c1 c2 =
(* Very syntactical equality *)
let eq_local_binder d1 d2 = match d1,d2 with
- | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) ->
- List.length nal1 = List.length nal2 &&
+ | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
+ List.length nal1 = List.length nal2 && k1 = k2 &&
List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
eq_constr_expr c1 c2
| LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
@@ -742,7 +751,7 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-let declare_fix boxed kind f def t =
+let declare_fix boxed kind f def t imps =
let ce = {
const_entry_body = def;
const_entry_type = Some t;
@@ -750,7 +759,11 @@ let declare_fix boxed kind f def t =
const_entry_boxed = boxed
} in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
- ConstRef kn
+ let gr = ConstRef kn in
+ if Impargs.is_implicit_args () || imps <> [] then
+ declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ gr
+
let prepare_recursive_declaration fixnames fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -766,6 +779,7 @@ let compute_possible_guardness_evidences (n,_) fixl fixtype =
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
+ (* FIXME, local_binders_length does not give the size of the final product if typeclasses are used *)
let m = local_binders_length fixl.fix_binders in
let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
@@ -778,6 +792,11 @@ let interp_recursive fixkind l boxed =
(* Interp arities allowing for unresolved types *)
let evdref = ref (Evd.create_evar_defs Evd.empty) in
+ let fiximps =
+ List.map
+ (fun x -> Implicit_quantifiers.implicits_of_binders x.fix_binders)
+ fixl
+ in
let fixctxs = List.map (interp_fix_context evdref env) fixl in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
@@ -816,7 +835,7 @@ let interp_recursive fixkind l boxed =
in
(* Declare the recursive definitions *)
- ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes);
+ ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps);
if_verbose ppnl (recursive_message kind indexes fixnames);
(* Declare notations *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3f7e50285..6b15479d7 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,7 +32,7 @@ open Redexpr
val declare_definition : identifier -> definition_kind ->
local_binder list -> red_expr option -> constr_expr ->
- constr_expr option -> declaration_hook -> unit
+ constr_expr option -> declaration_hook -> unit
val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
@@ -43,6 +43,16 @@ val declare_assumption : identifier located list ->
coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool
->unit
+val compute_interning_datas : Environ.env ->
+ 'a list ->
+ 'b list ->
+ Term.types list ->
+ 'a list *
+ ('b *
+ (Names.identifier list * Impargs.implicits_list *
+ Topconstr.scope_name option list))
+ list
+
val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
val declare_mutual_with_eliminations :
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8d9eabd7e..95ffeb44a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -71,6 +71,7 @@ let hm2 s =
(* The list of all theories in the standard library /!\ order does matter *)
let theories_dirs_map = [
"theories/Unicode", "Unicode" ;
+ "theories/Classes", "Classes" ;
"theories/Program", "Program" ;
"theories/FSets", "FSets" ;
"theories/IntMap", "IntMap" ;
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e381fe753..128091f44 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -21,6 +21,7 @@ open Sign
open Environ
open Pretype_errors
open Type_errors
+open Typeclasses_errors
open Indrec
open Reduction
open Cases
@@ -441,6 +442,38 @@ let explain_pretype_error env err =
| NoOccurrenceFound c -> explain_no_occurrence_found env c
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
+
+(* Typeclass errors *)
+
+let explain_unbound_class env (_,id) =
+ str "Unbound class name " ++ Nameops.pr_id id
+
+let explain_unbound_method env cid id =
+ str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++
+ Nameops.pr_id cid
+
+let pr_constr_exprs exprs =
+ hv 0 (List.fold_right
+ (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
+ exprs (mt ()))
+
+let explain_no_instance env (_,id) l =
+ str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
+ str "applied to arguments" ++ spc () ++
+ prlist_with_sep pr_spc (pr_lconstr_env env) l
+
+let explain_mismatched_contexts env c i j =
+ str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
+ hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++
+ hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
+
+let explain_typeclass_error env err =
+ match err with
+ | UnboundClass id -> explain_unbound_class env id
+ | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+ | NoInstance (id, l) -> explain_no_instance env id l
+ | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
+
(* Refiner errors *)
let explain_refiner_bad_type arg ty conclty =
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 05a52b8b7..d7a72bede 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -15,6 +15,7 @@ open Indtypes
open Environ
open Type_errors
open Pretype_errors
+open Typeclasses_errors
open Indrec
open Cases
open Logic
@@ -28,6 +29,8 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds
val explain_inductive_error : inductive_error -> std_ppcmds
+val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds
+
val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
val explain_refiner_error : refiner_error -> std_ppcmds
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e80001d25..73e4e42f7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -228,4 +228,5 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
let kinds,sp_projs = declare_projections rsp coers fields in
let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs)
+ Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+ kn
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 5074719bc..e322dcfd0 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -25,4 +25,4 @@ val declare_projections :
val definition_structure :
lident with_coercion * local_binder list *
- (local_decl_expr with_coercion) list * identifier * sorts -> unit
+ (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b71f9767e..0aea24d47 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -486,7 +486,7 @@ let vernac_record struc binders sort nameopt cfs =
| Sort s -> s
| _ -> user_err_loc
(constr_loc sort,"definition_structure", str "Sort expected") in
- Record.definition_structure (struc,binders,cfs,const,s)
+ ignore(Record.definition_structure (struc,binders,cfs,const,s))
(* Sections *)
@@ -522,6 +522,22 @@ let vernac_identity_coercion stre id qids qidt =
let source = cl_of_qualid qids in
Class.try_add_new_identity_coercion id stre source target
+(* Type classes *)
+let vernac_class id par ar sup props =
+ Classes.new_class id par ar sup props
+
+let vernac_instance sup inst props =
+ Classes.new_instance sup inst props
+
+let vernac_context l =
+ Classes.context l
+
+let vernac_declare_instance id =
+ Classes.declare_instance id
+
+(* Default tactics for solving evars management. *)
+let vernac_set_instantiation_tac tac =
+ Classes.set_instantiation_tactic tac
(***********)
(* Solving *)
@@ -656,9 +672,10 @@ let vernac_hints = Auto.add_hints
let vernac_syntactic_definition = Command.syntax_definition
-let vernac_declare_implicits local r = function
+let vernac_declare_implicits local r e = function
| Some imps ->
- Impargs.declare_manual_implicits local (global_with_alias r) imps
+ Impargs.declare_manual_implicits local (global_with_alias r) e
+ (List.map (fun (ex,b,f) -> ex, (b,f)) imps)
| None ->
Impargs.declare_implicits local (global_with_alias r)
@@ -712,6 +729,14 @@ let _ =
optread = Impargs.is_contextual_implicit_args;
optwrite = Impargs.make_contextual_implicit_args }
+(* let _ = *)
+(* declare_bool_option *)
+(* { optsync = true; *)
+(* optname = "forceable implicit arguments"; *)
+(* optkey = (SecondaryTable ("Forceable","Implicit")); *)
+(* optread = Impargs.is_forceable_implicit_args; *)
+(* optwrite = Impargs.make_forceable_implicit_args } *)
+
let _ =
declare_bool_option
{ optsync = true;
@@ -945,6 +970,8 @@ let vernac_print = function
| PrintOpaqueName qid -> msg (print_opaque_name qid)
| PrintGraph -> ppnl (Prettyp.print_graph())
| PrintClasses -> ppnl (Prettyp.print_classes())
+ | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
+ | PrintInstances c -> ppnl (Prettyp.print_instances c)
| PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
| PrintCoercions -> ppnl (Prettyp.print_coercions())
| PrintCoercionPaths (cls,clt) ->
@@ -1188,6 +1215,15 @@ let interp c = match c with
| VernacCoercion (str,r,s,t) -> vernac_coercion str r s t
| VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
+ (* Type classes *)
+ | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
+
+ | VernacInstance (sup, inst, props) -> vernac_instance sup inst props
+ | VernacContext sup -> vernac_context sup
+ | VernacDeclareInstance id -> vernac_declare_instance id
+
+ | VernacSetInstantiationTactic (tac) -> vernac_set_instantiation_tac tac
+
(* Solving *)
| VernacSolve (n,tac,b) -> vernac_solve n tac b
| VernacSolveExistential (n,c) -> vernac_solve_existential n c
@@ -1222,7 +1258,7 @@ let interp c = match c with
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
| VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
| VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
- | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
+ | VernacDeclareImplicits (local,qid,e,l) ->vernac_declare_implicits local qid e l
| VernacReserve (idl,c) -> vernac_reserve idl c
| VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
| VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c89393301..a5c04a561 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -48,6 +48,8 @@ type printable =
| PrintOpaqueName of reference
| PrintGraph
| PrintClasses
+ | PrintTypeClasses
+ | PrintInstances of reference
| PrintLtac of reference
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
@@ -145,10 +147,12 @@ type sort_expr = Rawterm.rawsort
type decl_notation = (string * constr_expr * scope_name option) option
type simple_binder = lident list * constr_expr
+type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
type constructor_expr = (lident * constr_expr) with_coercion
type inductive_expr =
lident * local_binder list * constr_expr * constructor_expr list
+
type definition_expr =
| ProveBody of local_binder list * constr_expr
| DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -220,6 +224,26 @@ type vernac_expr =
| VernacIdentityCoercion of strength * lident *
class_rawexpr * class_rawexpr
+ (* Type classes *)
+ | VernacClass of
+ lident * (* name *)
+ (lident * constr_expr) list * (* params *)
+ sort_expr located * (* arity *)
+ typeclass_context * (* super *)
+ (lident * constr_expr) list (* props *)
+
+ | VernacInstance of
+ typeclass_context * (* super *)
+ typeclass_constraint * (* instance name, class name, params *)
+ (lident * lident list * constr_expr) list (* props *)
+
+ | VernacContext of typeclass_context
+
+ | VernacDeclareInstance of
+ lident (* instance name *)
+
+ | VernacSetInstantiationTactic of raw_tactic_expr
+
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
module_binder list * (module_type_ast * bool)
@@ -260,12 +284,12 @@ type vernac_expr =
(* Commands *)
| VernacDeclareTacticDefinition of
- rec_flag * (lident * raw_tactic_expr) list
+ rec_flag * (lident * bool * raw_tactic_expr) list
| VernacHints of locality_flag * lstring list * hints
| VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
onlyparsing_flag
- | VernacDeclareImplicits of locality_flag * lreference *
- (explicitation * bool) list option
+ | VernacDeclareImplicits of locality_flag * lreference * bool *
+ (explicitation * bool * bool) list option
| VernacReserve of lident list * constr_expr
| VernacSetOpacity of opacity_flag * lreference list
| VernacUnsetOption of Goptions.option_name
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index c7a9774e0..d76c281be 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -151,12 +151,12 @@ let rec uri_of_constr c =
let inst,rest = merge (section_parameters f) args in
uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
url_list_with_sep " " uri_of_constr rest
- | RLambda (_,na,ty,c) ->
+ | RLambda (_,na,k,ty,c) ->
url_string "\\lambda "; url_of_name na; url_string ":";
uri_of_constr ty; url_string "."; uri_of_constr c
- | RProd (_,Anonymous,ty,c) ->
+ | RProd (_,Anonymous,k,ty,c) ->
uri_of_constr ty; url_string "\\to "; uri_of_constr c
- | RProd (_,Name id,ty,c) ->
+ | RProd (_,Name id,k,ty,c) ->
url_string "\\forall "; url_id id; url_string ":";
uri_of_constr ty; url_string "."; uri_of_constr c
| RLetIn (_,na,b,c) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 01:28:31 +0000