Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: classes.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i*)
module CVars = Vars
open Names
open EConstr
open CErrors
open Util
open Typeclasses_errors
open Typeclasses
open Libnames
open Globnames
open Constrintern
open Constrexpr
open Context.Rel.Declaration
open Class_tactics

module RelDecl = Context.Rel.Declaration
(*i*)

open Decl_kinds
open Entries

let refine_instance = ref false

let () = Goptions.(declare_bool_option {
  optdepr  = true;
  optname  = "definition of instances by refining";
  optkey   = ["Refine";"Instance";"Mode"];
  optread  = (fun () -> !refine_instance);
  optwrite = (fun b -> refine_instance := b)
})

let set_typeclass_transparency c local b =
  Hints.add_hints ~local [typeclasses_db]
    (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))

let classes_transparent_state () =
  try
    Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)
  with Not_found -> TransparentState.empty

let () =
  Hook.set Typeclasses.add_instance_hint_hook
    (fun inst path local info poly ->
     let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
       | IsGlobal gr -> Hints.IsGlobRef gr
     in
     Flags.silently (fun () ->
       Hints.add_hints ~local [typeclasses_db]
   (Hints.HintsResolveEntry
      [info, poly, false, Hints.PathHints path, inst'])) ());
  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
  Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state

let intern_info {hint_priority;hint_pattern} =
  let env = Global.env() in
  let sigma = Evd.from_env env in
  let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in
  {hint_priority;hint_pattern}

(** TODO: add subinstances *)
let existing_instance glob g info =
  let c = Nametab.global g in
  let info = Option.default Hints.empty_hint_info info in
  let info = intern_info info in
  let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in
  let _, r = Term.decompose_prod_assum instance in
    match class_of_constr Evd.empty (EConstr.of_constr r) with
      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
      | None -> user_err ?loc:g.CAst.loc
                         ~hdr:"declare_instance"
                         (Pp.str "Constant does not build instances of a declared type class.")

let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m

(* Declare everything in the parameters as implicit, and the class instance as well *)

let type_ctx_instance ~program_mode env sigma ctx inst subst =
  let open Vars in
  let rec aux (sigma, subst, instctx) l = function
    decl :: ctx ->
      let t' = substl subst (RelDecl.get_type decl) in
      let (sigma, c'), l =
match decl with
        | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l
        | LocalDef (_,b,_) -> (sigma, substl subst b), l
      in
      let d = RelDecl.get_name decl, Some c', t' in
        aux (sigma, c' :: subst, d :: instctx) l ctx
    | [] -> sigma, subst
  in aux (sigma, subst, []) inst (List.rev ctx)

let id_of_class cl =
  match cl.cl_impl with
    | ConstRef kn -> Label.to_id @@ Constant.label kn
    | IndRef (kn,i) ->
let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
   mip.(0).Declarations.mind_typename
    | _ -> assert false

let instance_hook k info global imps ?hook cst =
  Impargs.maybe_declare_manual_implicits false cst imps;
  let info = intern_info info in
  Typeclasses.declare_instance (Some info) (not global) cst;
  (match hook with Some h -> h cst | None -> ())

let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
  let kind = IsDefinition Instance in
  let sigma =
    let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
                                 (CVars.universes_of_constr term) in
    Evd.restrict_universe_context sigma levels
  in
  let uctx = Evd.check_univ_decl ~poly sigma decl in
  let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
  let cdecl = (DefinitionEntry entry, kind) in
  let kn = Declare.declare_constant id cdecl in
  Declare.definition_message id;
  Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
  instance_hook k info global imps ?hook (ConstRef kn)

let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
  let subst = List.fold_left2
      (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
      [] subst (snd k.cl_context)
  in
  let (_, ty_constr) = instance_constructor (k,u) subst in
  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
  let sigma = Evd.minimize_universes sigma in
  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
  let univs = Evd.check_univ_decl ~poly sigma decl in
  let termtype = to_constr sigma termtype in
  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
      (ParameterEntry
         (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
  in
  Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
  instance_hook k pri global imps (ConstRef cst)

let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
  if program_mode then
    let hook _ _ vis gr =
      let cst = match gr with ConstRef kn -> kn | _ -> assert false in
      Impargs.declare_manual_implicits false gr imps;
      let pri = intern_info pri in
      Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
    in
    let obls, constr, typ =
      match term with
      | Some t ->
        let obls, _, constr, typ =
          Obligations.eterm_obligations env id sigma 0 t termtype
        in obls, Some constr, typ
      | None -> [||], None, termtype
    in
    let hook = Lemmas.mk_hook hook in
    let ctx = Evd.evar_universe_context sigma in
    let _progress = Obligations.add_definition id ?term:constr
              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
    pstate
  else
    Some Flags.(silently (fun () ->
        (* spiwack: it is hard to reorder the actions to do
           the pretyping after the proof has opened. As a
           consequence, we use the low-level primitives to code
           the refinement manually.*)
        let gls = List.rev (Evd.future_goals sigma) in
        let sigma = Evd.reset_future_goals sigma in
        let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype)
          ~hook:(Lemmas.mk_hook
             (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
        (* spiwack: I don't know what to do with the status here. *)
        let pstate =
          if not (Option.is_empty term) then
            let init_refine =
              Tacticals.New.tclTHENLIST [
                Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
                Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
                Tactics.New.reduce_after_refine;
              ]
            in
            let pstate, _ = Pfedit.by init_refine pstate in
            pstate
          else
            let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
            pstate
        in
        match tac with
        | Some tac ->
          let pstate, _ = Pfedit.by tac pstate in
          pstate
        | None ->
          pstate) ())

let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
  let props =
    match props with
    | Some (true, { CAst.v = CRecord fs }) ->
      if List.length fs > List.length k.cl_props then
        mismatched_props env' (List.map snd fs) k.cl_props;
      Some (Inl fs)
    | Some (_, t) -> Some (Inr t)
    | None ->
      if program_mode then Some (Inl [])
      else None
  in
  let subst, sigma =
    match props with
    | None ->
      (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
    | Some (Inr term) ->
      let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in
      Some (Inr (c, subst)), sigma
    | Some (Inl props) ->
      let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
      let props, rest =
        List.fold_left
          (fun (props, rest) decl ->
             if is_local_assum decl then
               try
                 let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
                   | Name id, {CAst.v=id'} -> Id.equal id id'
                   | Anonymous, _ -> false
                 in
                 let (loc_mid, c) = List.find is_id rest in
                 let rest' = List.filter (fun v -> not (is_id v)) rest
                 in
                 let {CAst.loc;v=mid} = get_id loc_mid in
                 List.iter (fun (n, _, x) ->
                     if Name.equal n (Name mid) then
                       Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs;
                 c :: props, rest'
               with Not_found ->
                 ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
             else props, rest)
          ([], props) k.cl_props
      in
      match rest with
      | (n, _) :: _ ->
        unbound_method env' sigma k.cl_impl (get_id n)
      | _ ->
        let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
        let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
        Some (Inl res), sigma
  in
  let term, termtype =
    match subst with
    | None -> let termtype = it_mkProd_or_LetIn cty ctx in
      None, termtype
    | Some (Inl subst) ->
      let subst = List.fold_left2
          (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
          [] subst (k.cl_props @ snd k.cl_context)
      in
      let (app, ty_constr) = instance_constructor (k,u) subst in
      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
      let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
      Some term, termtype
    | Some (Inr (def, subst)) ->
      let termtype = it_mkProd_or_LetIn cty ctx in
      let term = it_mkLambda_or_LetIn def ctx in
      Some term, termtype
  in
  let sigma = Evarutil.nf_evar_map sigma in
  let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in
  (* Try resolving fields that are typeclasses automatically. *)
  let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
  let sigma = Evarutil.nf_evar_map_undefined sigma in
  (* Beware of this step, it is required as to minimize universes. *)
  let sigma = Evd.minimize_universes sigma in
  (* Check that the type is free of evars now. *)
  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
  let termtype = to_constr sigma termtype in
  let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
  let pstate =
    if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
      (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
       None)
    else if program_mode || refine || Option.is_empty props then
      declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
    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 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
  in
  let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
  let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in
  let len = Context.Rel.nhyps ctx in
  let imps = imps @ Impargs.lift_implicits len imps' in
  let ctx', c = decompose_prod_assum sigma c' in
  let ctx'' = ctx' @ ctx in
  let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
  let u_s = EInstance.kind sigma u in
  let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
  let args = List.map of_constr args in
  let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
  let _, args =
    List.fold_right (fun decl (args, args') ->
        match decl with
        | LocalAssum _ -> (List.tl args, List.hd args :: args')
        | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
      cl_context (args, [])
  in
  let sigma = Evarutil.nf_evar_map sigma in
  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) ?(refine= !refine_instance) ~program_mode
    poly ctx (instid, bk, 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
  in
  let id =
    match instid with
    | Name id -> id
    | Anonymous ->
      let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
      Namegen.next_global_ident_away i (Termops.vars_of_env env)
  in
  let env' = push_rel_context ctx env in
  do_instance ~pstate env env' sigma ?hook ~refine ~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 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
  in
  do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid

let named_of_rel_context l =
  let open Vars in
  let acc, ctx =
    List.fold_right
      (fun decl (subst, ctx) ->
        let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
let d = match decl with
          | LocalAssum (_,t) -> id, None, substl subst t
          | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
   (mkVar id :: subst, d :: ctx))
      l ([], [])
  in ctx

let context ~pstate poly l =
  let env = Global.env() in
  let sigma = Evd.from_env env in
  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
  (* Note, we must use the normalized evar from now on! *)
  let sigma = Evd.minimize_universes sigma in
  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
  let ctx =
    try named_of_rel_context fullctx
    with e when CErrors.noncritical e ->
      user_err Pp.(str "Anonymous variables not allowed in contexts.")
  in
  let univs =
    match ctx with
    | [] -> assert false
    | [_] -> Evd.univ_entry ~poly sigma
    | _::_::_ ->
      if Lib.sections_are_opened ()
      then
        (* More than 1 variable in a section: we can't associate
           universes to any specific variable so we declare them
           separately. *)
        begin
          let uctx = Evd.universe_context_set sigma in
          Declare.declare_universe_context poly uctx;
          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
          else Monomorphic_entry Univ.ContextSet.empty
        end
      else if poly then
        (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
        Evd.univ_entry ~poly sigma
      else
        (* Multiple monomorphic axioms: declare universes separately
           to avoid redeclaring them. *)
        begin
          let uctx = Evd.universe_context_set sigma in
          Declare.declare_universe_context poly uctx;
          Monomorphic_entry Univ.ContextSet.empty
        end
  in
  let fn status (id, b, t) =
    let b, t = Option.map (to_constr sigma) b, to_constr sigma t in
    if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
      (* Declare the universe context once *)
      let decl = match b with
      | None ->
        (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
      | Some b ->
        let entry = Declare.definition_entry ~univs ~types:t b in
        (DefinitionEntry entry, IsAssumption Logical)
      in
      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
        match class_of_constr sigma (of_constr t) with
| Some (rels, ((tc,_), args) as _cl) ->
            add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
            status
     (* declare_subclasses (ConstRef cst) cl *)
| None -> status
    else
      let test (x, _) = match x with
      | ExplByPos (_, Some id') -> Id.equal id id'
      | _ -> false
      in
      let impl = List.exists test impls in
      let decl = (Discharge, poly, Definitional) in
      let nstatus = match b with
      | None ->
        pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
               Declaremods.NoInline (CAst.make id))
      | Some b ->
        let decl = (Discharge, poly, Definition) in
        let entry = Declare.definition_entry ~univs ~types:t b in
        let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
        Lib.sections_are_opened () || Lib.is_modtype_strict ()
      in
status && nstatus
  in
  List.fold_left fn true (List.rev ctx)

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.