aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
blob: 7f93e15609e91935c7e6ab3a0762f9f918bcbeef (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

open Pp
open Util
open Names
open Cic
open Term
open Reduction
open Typeops
open Indtypes
open Modops
open Subtyping
open Declarations
open Environ

(** {6 Checking constants } *)

let refresh_arity ar =
  let ctxt, hd = decompose_prod_assum ar in
  match hd with
      Sort (Type u) when not (Univ.is_univ_variable u) ->
      let ul = Univ.Level.make DirPath.empty 1 in
      let u' = Univ.Universe.make ul in
      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
        mkArity (ctxt,Prop Null), ctx
    | _ -> ar, Univ.ContextSet.empty

let check_constant_declaration env kn cb =
  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
  let env' =
    if cb.const_polymorphic then
      let inst = Univ.make_abstract_instance cb.const_universes in
      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
        push_context ~strict:false ctx env
    else push_context ~strict:true cb.const_universes env
  in
  let envty, ty = 
    match cb.const_type with
      RegularArity ty ->
        let ty', cu = refresh_arity ty in
        let envty = push_context_set cu env' in
        let _ = infer_type envty ty' in envty, ty
    | TemplateArity(ctxt,par) ->
        let _ = check_ctxt env' ctxt in
        check_polymorphic_arity env' ctxt par;
	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
  in
  let () = 
    match body_of_constant cb with
    | Some bd ->
      (match cb.const_proj with 
      | None -> let j = infer envty bd in
		  conv_leq envty j ty
      | Some pb -> 
	let env' = add_constant kn cb env' in
	let j = infer env' bd in
	  conv_leq envty j ty)
    | None -> ()
  in
  if cb.const_polymorphic then add_constant kn cb env
  else add_constant kn cb env'

(** {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 = Abstract;
    mod_type = sign;
    mod_type_alg = None;
    mod_constraints = Univ.ContextSet.empty;
    mod_delta = delta;
    mod_retroknowledge = []; }

let rec check_module env mp mb =
  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)
    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
    |Abstract|FullStruct -> None
  in
  match optsign with
  |None -> ()
  |Some sign ->
    let mtb1 = mk_mtb mp sign mb.mod_delta
    and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in
    let env = add_module_type mp mtb1 env in
    Subtyping.check_subtypes env mtb1 mtb2

and check_module_type env mty =
  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 = MutInd.make2 mp lab in
      let kn = mind_of_delta res kn in
      Indtypes.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 (MPdot(mp,lab)) mty env

and check_mexpr env mse mp_mse res = match mse with
  | MEident mp ->
      let mb = lookup_module mp env in
      (subst_and_strengthen mb mp_mse).mod_type
  | MEapply (f,mp) ->
      let sign = check_mexpr env f mp_mse res in
      let farg_id, farg_b, fbody_b = destr_functor sign in
      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
      check_subtypes env mtb farg_b;
      subst_signature (map_mbid farg_id mp) fbody_b
  | MEwith _ -> error_with_module ()

and check_mexpression env sign mp_mse res = match sign with
  | MoreFunctor (arg_id, mtb, body) ->
      check_module_type env mtb;
      let env' = add_module_type (MPbound arg_id) mtb env in
      let body = check_mexpression env' body mp_mse res in
      MoreFunctor(arg_id,mtb,body)
  | 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' = 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