diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 60 |
1 files changed, 23 insertions, 37 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7f93e156..3ef2b340 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -1,9 +1,7 @@ - open Pp open Util open Names open Cic -open Term open Reduction open Typeops open Indtypes @@ -14,51 +12,39 @@ 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); + Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); + (** Locally set the oracle for further typechecking *) + let oracle = env.env_conv_oracle in + let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in + (** [env'] contains De Bruijn universe variables *) 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 + match cb.const_universes with + | Monomorphic_const ctx -> push_context_set ~strict:true ctx env + | Polymorphic_const auctx -> + let ctx = Univ.AUContext.repr auctx in + push_context ~strict:false ctx env in + let ty = cb.const_type in + let () = ignore(infer_type env' ty) 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 + | None -> let j = infer env' bd in + conv_leq env' j ty | Some pb -> let env' = add_constant kn cb env' in let j = infer env' bd in - conv_leq envty j ty) + conv_leq env' j ty) | None -> () in - if cb.const_polymorphic then add_constant kn cb env - else add_constant kn cb env' + let env = + if constant_is_polymorphic cb 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 } *) @@ -74,12 +60,12 @@ let lookup_module mp env = let mk_mtb mp sign delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; mod_delta = delta; - mod_retroknowledge = []; } + mod_retroknowledge = ModTypeRK; } let rec check_module env mp mb = let (_:module_signature) = |