diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 13:43:26 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 19:23:51 +0200 |
commit | f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 (patch) | |
tree | eadad13bfd7e178d782bb46a9bd3e0daff84264b /checker/mod_checking.ml | |
parent | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (diff) |
Adapt the checker to polymorphic universes and projections (untested).
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 53316a2cb..12a97bf68 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -14,30 +14,31 @@ 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 u' = Univ.fresh_local_univ() in *) -(* mkArity (ctxt,Type u'), *) -(* Univ.enforce_leq u u' Univ.empty_constraint *) -(* | _ -> ar, Univ.empty_constraint *) +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 u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in + mkArity (ctxt,Prop Null), + Univ.enforce_leq u u' Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); -(* let env = add_constraints cb.const_constraints env in*) + let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in (match cb.const_type with - ty -> - let env' = add_constraints cb.const_constraints env in (*MS: FIXME*) - let _ = infer_type env' ty in - (match body_of_constant cb with + RegularArity ty -> + let ty, cu = refresh_arity ty in + let envty = add_constraints cu env in + let _ = infer_type envty ty in + (match body_of_constant cb with | Some bd -> - let j = infer env' bd in - conv_leq env' j ty + let j = infer envty bd in + conv_leq envty j ty | None -> ()) - (* | PolymorphicArity(ctxt,par) -> *) - (* let _ = check_ctxt env ctxt in *) - (* check_polymorphic_arity env ctxt par *)); + | TemplateArity(ctxt,par) -> + let _ = check_ctxt env ctxt in + check_polymorphic_arity env ctxt par); add_constant kn cb env |