-
Notifications
You must be signed in to change notification settings - Fork 78
/
g_metacoq_safechecker.mlg
105 lines (96 loc) · 3.5 KB
/
g_metacoq_safechecker.mlg
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
DECLARE PLUGIN "coq-metacoq-safechecker.plugin"
{
open Attributes
open Stdarg
open Pp
open PeanoNat.Nat
open Datatypes
open Extraction
open Tm_util
open Caml_bytestring
let pr_string l =
(* We allow utf8 encoding *)
str (caml_string_of_bytestring l)
let check env evm poly (c, ustate) =
debug (fun () -> str"Quoting");
let uctx = Evd.universe_context_set evm in
let env = if poly then env else Environ.push_context_set ~strict:true uctx env in
let prog = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass:true ~with_universes:true env evm) (EConstr.to_constr evm c) in
let uctx =
if poly then
let uctx = Evd.to_universe_context evm in
let inst, auctx = UVars.abstract_universes uctx in
Ast_quoter.mkPolymorphic_ctx (Ast_quoter.quote_abstract_univ_context auctx)
else Ast_quoter.mkMonomorphic_ctx ()
in
let check =
time (str"Checking")
(Extraction.infer_and_print_template_program_with_guard
Config0.default_checker_flags
(* Config0.type_in_type *)
prog)
uctx
in
match check with
| Coq_inl s -> Feedback.msg_info (pr_string s)
| Coq_inr s -> CErrors.user_err (pr_string s)
}
VERNAC COMMAND EXTEND MetaCoqSafeCheck CLASSIFIED AS QUERY
| #[ poly = polymorphic ] [ "MetaCoq" "SafeCheck" constr(c) ] -> {
let env = Global.env () in
let evm = Evd.from_env env in
let c = Constrintern.interp_constr env evm c in
check env evm poly c
}
END
{
let retypecheck_term_dependencies env gr =
let typecheck env c = ignore (Typeops.infer env c) in
let typecheck_constant c =
let auctx = Environ.constant_context env c in
let qnames, unames as names = UVars.AbstractContext.names auctx in
let dp = Names.DirPath.make [Names.Id.of_string "MetaCoq"; Names.Id.of_string "Retypecheck"] in
let fake_quality i _ =
Sorts.Quality.QVar (Sorts.QVar.make_unif "" i)
in
let fake_level i _ =
Univ.Level.make (Univ.UGlobal.make dp "" i)
in
let fake_inst = UVars.Instance.of_array (Array.mapi fake_quality qnames, Array.mapi fake_level unames) in
let cu = (c, fake_inst) in
let cbody, ctype, cstrs = Environ.constant_value_and_type env cu in
let env' = Environ.push_context (UVars.UContext.make names (fake_inst, cstrs)) env in
typecheck env' ctype;
Option.iter (typecheck env') cbody
in
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
let deps = Assumptions.assumptions ~add_opaque:true ~add_transparent:true
st gr (fst (UnivGen.fresh_global_instance env gr)) in
let process_object k _ty =
let open Printer in
match k with
| Variable id -> debug (fun () -> str "Ignoring variable " ++ Names.Id.print id)
| Axiom (ax, _) ->
begin match ax with
| Constant c -> typecheck_constant c
| Positive mi -> () (* typecheck_inductive mi *)
| Guarded (Names.GlobRef.ConstRef c) -> typecheck_constant c
| Guarded _ -> ()
| TypeInType c -> ()
| UIP _ -> ()
end
| Opaque c | Transparent c -> typecheck_constant c
in Printer.ContextObjectMap.iter process_object deps
let kern_check env evm gr =
try
let () = time (str"Coq kernel checking") (retypecheck_term_dependencies env) gr in
Feedback.msg_info (Printer.pr_global gr ++ str " and all its dependencies are well-typed.")
with e -> raise e
}
VERNAC COMMAND EXTEND MetaCoqCoqCheck CLASSIFIED AS QUERY
| [ "MetaCoq" "CoqCheck" global(c) ] -> {
let env = Global.env () in
let evm = Evd.from_env env in
kern_check env evm (Nametab.global c)
}
END