products/sources/formale Sprachen/C/Cephes/ldouble/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: .project   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)         *)
(************************************************************************)

(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml
   as part of the rebuilding of Coq around a purely functional
   abstract type-checker, Nov 1999 *)

(* This module implements kernel-level discharching of local
   declarations over global constants and inductive types *)

open Util
open Names
open Term
open Constr
open Declarations
open Univ
open Context

module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration

(*s Cooking the constants. *)

type my_global_reference =
  | ConstRef of Constant.t
  | IndRef of inductive
  | ConstructRef of constructor

module RefHash =
struct
  type t = my_global_reference
  let equal gr1 gr2 = match gr1, gr2 with
  | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
  | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
  | _ -> false
  open Hashset.Combine
  let hash = function
  | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
  | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
end

module RefTable = Hashtbl.Make(RefHash)

let instantiate_my_gr gr u =
  match gr with
  | ConstRef c -> mkConstU (c, u)
  | IndRef i -> mkIndU (i, u)
  | ConstructRef c -> mkConstructU (c, u)

let share cache r (cstl,knl) =
  try RefTable.find cache r
  with Not_found ->
  let (u,l) =
    match r with
    | IndRef (kn,_i) ->
        Mindmap.find kn knl
    | ConstructRef ((kn,_i),_j) ->
        Mindmap.find kn knl
    | ConstRef cst ->
        Cmap.find cst cstl in
  let c = (u, Array.map mkVar l) in
  RefTable.add cache r c;
  c

let share_univs cache r u l =
  let (u', args) = share cache r l in
    mkApp (instantiate_my_gr r (Instance.append u' u), args)

let update_case_info cache ci modlist =
  try
    let (_u,l) = share cache (IndRef ci.ci_ind) modlist in
    { ci with ci_npar = ci.ci_npar + Array.length l }
  with Not_found ->
    ci

let is_empty_modlist (cm, mm) =
  Cmap.is_empty cm && Mindmap.is_empty mm

let expmod_constr cache modlist c =
  let share_univs = share_univs cache in
  let update_case_info = update_case_info cache in
  let rec substrec c =
    match kind c with
      | Case (ci,p,t,br) ->
   Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))

      | Ind (ind,u) ->
   (try
     share_univs (IndRef ind) u modlist
    with
     | Not_found -> Constr.map substrec c)

      | Construct (cstr,u) ->
   (try
      share_univs (ConstructRef cstr) u modlist
    with
     | Not_found -> Constr.map substrec c)

      | Const (cst,u) ->
   (try
     share_univs (ConstRef cst) u modlist
    with
     | Not_found -> Constr.map substrec c)

      | Proj (p, c') ->
        let map cst npars =
          let _, newpars = Mindmap.find cst (snd modlist) in
          (cst, npars + Array.length newpars)
        in
        let p' = try Projection.map_npars map p with Not_found -> p in
        let c'' = substrec c' in
        if p == p' && c' == c'' then c else mkProj (p', c'')

  | _ -> Constr.map substrec c

  in
  if is_empty_modlist modlist then c
  else substrec c

(** Transforms a named context into a rel context. Also returns the list of
    variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to
    abstract a term that lived in that context. *)
let abstract_context hyps =
  let fold decl (ctx, subst) =
    let id, decl = match decl with
    | NamedDecl.LocalDef (id, b, t) ->
      let b = Vars.subst_vars subst b in
      let t = Vars.subst_vars subst t in
      id, RelDecl.LocalDef (map_annot Name.mk_name id, b, t)
    | NamedDecl.LocalAssum (id, t) ->
      let t = Vars.subst_vars subst t in
      id, RelDecl.LocalAssum (map_annot Name.mk_name id, t)
    in
    (decl :: ctx, id.binder_name :: subst)
  in
  Context.Named.fold_outside fold hyps ~init:([], [])

let abstract_constant_type t (hyps, subst) =
  let t = Vars.subst_vars subst t in
  List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps

let abstract_constant_body c (hyps, subst) =
  let c = Vars.subst_vars subst c in
  it_mkLambda_or_LetIn c hyps

type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool

type result = {
  cook_body : constr Mod_subst.substituted constant_def;
  cook_type : types;
  cook_universes : universes;
  cook_private_univs : Univ.ContextSet.t option;
  cook_relevance : Sorts.relevance;
  cook_inline : inline;
  cook_context : Constr.named_context option;
}

let expmod_constr_subst cache modlist subst c =
  let subst = Univ.make_instance_subst subst in
  let c = expmod_constr cache modlist c in
    Vars.subst_univs_level_constr subst c

let lift_univs cb subst auctx0 =
  match cb.const_universes with
  | Monomorphic ctx ->
    assert (AUContext.is_empty auctx0);
    subst, (Monomorphic ctx)
  | Polymorphic auctx ->
    (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
        context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
        and another abstract context relative to the former context
        [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
        construct the lifted abstract universe context
        [0 ... n - 1 n ... n + m - 1 |=
          C{0, ... n - 1} ∪
          C'{0, ..., n - 1, n, ..., n + m - 1} ]
        together with the instance
        [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
    *)
    if (Univ.Instance.is_empty subst) then
      (** Still need to take the union for the constraints between globals *)
      subst, (Polymorphic (AUContext.union auctx0 auctx))
    else
      let ainst = Univ.make_abstract_instance auctx in
      let subst = Instance.append subst ainst in
      let substf = Univ.make_instance_subst subst in
      let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
      subst, (Polymorphic (AUContext.union auctx0 auctx'))

let cook_constr { Opaqueproof.modlist ; abstract } c =
  let cache = RefTable.create 13 in
  let abstract, usubst, abs_ctx = abstract in
  (* For now the STM only handles deferred computation of monomorphic
    constants. The API will need to be adapted when it's not the case
    anymore. *)
  let () = assert (AUContext.is_empty abs_ctx) in
  let expmod = expmod_constr_subst cache modlist usubst in
  let hyps = Context.Named.map expmod abstract in
  let hyps = abstract_context hyps in
  abstract_constant_body (expmod c) hyps

let cook_constant { from = cb; info } =
  let { Opaqueproof.modlist; abstract } = info in
  let cache = RefTable.create 13 in
  let abstract, usubst, abs_ctx = abstract in
  let usubst, univs = lift_univs cb usubst abs_ctx in
  let expmod = expmod_constr_subst cache modlist usubst in
  let hyps0 = Context.Named.map expmod abstract in
  let hyps = abstract_context hyps0 in
  let map c = abstract_constant_body (expmod c) hyps in
  let body = match cb.const_body with
  | Undef _ as x -> x
  | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
  | OpaqueDef o ->
    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
  | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
  in
  let const_hyps =
    Context.Named.fold_outside (fun decl hyps ->
      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
    hyps)
      hyps0 ~init:cb.const_hyps in
  let typ = abstract_constant_type (expmod cb.const_type) hyps in
  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
                                            (Univ.make_instance_subst usubst)))
      cb.const_private_poly_univs
  in
  {
    cook_body = body;
    cook_type = typ;
    cook_universes = univs;
    cook_private_univs = private_univs;
    cook_relevance = cb.const_relevance;
    cook_inline = cb.const_inline_code;
    cook_context = Some const_hyps;
  }

(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)

let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c

¤ Dauer der Verarbeitung: 0.4 Sekunden  (vorverarbeitet)  ¤



aufgebrochen in jeweils 16 Zeichen
Drucken
aufgebrochen in jeweils 16 Zeichen
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff