Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: mod_checking.ml Sprache: SML

Original von: Coq^©

open Pp
open Util
open Names
open Reduction
open Typeops
open Declarations
open Environ

(** {6 Checking constants } *)

let check_constant_declaration env kn cb =
  Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
  (* Locally set the oracle for further typechecking *)
  let oracle = env.env_typing_flags.conv_oracle in
  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
  (* [env'] contains De Bruijn universe variables *)
  let poly, env' =
    match cb.const_universes with
    | Monomorphic ctx -> false, env
    | Polymorphic auctx ->
      let ctx = Univ.AUContext.repr auctx in
      let env = push_context ~strict:false ctx env in
      true, env
  in
  let ty = cb.const_type in
  let _ = infer_type env' ty in
  let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
    | None, _ -> env'
    | Some local, (OpaqueDef _, true) -> push_subgraph local env'
    | Some _, _ -> assert false
  in
  let () =
    match Environ.body_of_constant_body env cb with
    | Some bd ->
      let j = infer env' (fst bd) in
      (try conv_leq env' j.uj_type ty
       with NotConvertible -> Type_errors.error_actual_type env j ty)
    | None -> ()
  in
  let env =
    if poly then add_constant kn cb env
    else add_constant kn cb env'
  in
  (* Reset the value of the oracle *)
  Environ.set_oracle env oracle

(** {6 Checking modules } *)

(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields.
    The only delicate part is when [mod_expr] is an algebraic expression :
    we need to expand it before checking it is indeed a subtype of [mod_type].
    Fortunately, [mod_expr] cannot contain any [MEwith]. *)

let lookup_module mp env =
  try Environ.lookup_module mp env
  with Not_found ->
    failwith ("Unknown module: "^ModPath.to_string mp)

let mk_mtb mp sign delta =
  { mod_mp = mp;
    mod_expr = ();
    mod_type = sign;
    mod_type_alg = None;
    mod_constraints = Univ.ContextSet.empty;
    mod_delta = delta;
    mod_retroknowledge = ModTypeRK; }

let rec check_module env mp mb =
  Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp));
  let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
  let (_:module_signature) =
    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
  in
  let optsign = match mb.mod_expr with
    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta)
    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
    |Abstract|FullStruct -> None
  in
  match optsign with
  |None -> ()
  |Some (sign,delta) ->
    let mtb1 = mk_mtb mp sign delta
    and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in
    let env = Modops.add_module_type mp mtb1 env in
    let cu = Subtyping.check_subtypes env mtb1 mtb2 in
    if not (Environ.check_constraints cu env) then
      CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");

and check_module_type env mty =
  Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string mty.mod_mp));
  let (_:module_signature) =
    check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
  ()

and check_structure_field env mp lab res = function
  | SFBconst cb ->
      let c = Constant.make2 mp lab in
      check_constant_declaration env c cb
  | SFBmind mib ->
      let kn = KerName.make mp lab in
      let kn = Mod_subst.mind_of_delta_kn res kn in
      CheckInductive.check_inductive env kn mib
  | SFBmodule msb ->
      let () = check_module env (MPdot(mp,lab)) msb in
      Modops.add_module msb env
  | SFBmodtype mty ->
      check_module_type env mty;
      add_modtype mty env

and check_mexpr env mse mp_mse res = match mse with
  | MEident mp ->
      let mb = lookup_module mp env in
      let mb = Modops.strengthen_and_subst_mb mb mp_mse false in
      mb.mod_type, mb.mod_delta
  | MEapply (f,mp) ->
      let sign, delta = check_mexpr env f mp_mse res in
      let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
      let mtb = Modops.module_type_of_module (lookup_module mp env) in
      let cu = Subtyping.check_subtypes env mtb farg_b in
      if not (Environ.check_constraints cu env) then
        CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");
      let subst = Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver in
      Modops.subst_signature subst fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
  | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")

and check_mexpression env sign mp_mse res = match sign with
  | MoreFunctor (arg_id, mtb, body) ->
      check_module_type env mtb;
      let env' = Modops.add_module_type (MPbound arg_id) mtb env in
      let body, delta = check_mexpression env' body mp_mse res in
      MoreFunctor(arg_id,mtb,body), delta
  | NoFunctor me -> check_mexpr env me mp_mse res

and check_signature env sign mp_mse res = match sign with
  | MoreFunctor (arg_id, mtb, body) ->
      check_module_type env mtb;
      let env' = Modops.add_module_type (MPbound arg_id) mtb env in
      let body = check_signature env' body mp_mse res in
      MoreFunctor(arg_id,mtb,body)
  | NoFunctor struc ->
      let (_:env) = List.fold_left (fun env (lab,mb) ->
check_structure_field env mp_mse lab res mb) env struc
      in
      NoFunctor struc

¤ Dauer der Verarbeitung: 0.2 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.