blob: 6bea3c91a71d6086b916db3707f3162629a2e908 (
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
(* -*-tuareg-*- *)
(* Caml script to include for debugging the checker.
Usage: from the checker/ directory launch ocaml toplevel and then
type #use"include";;
This command loads the relevent modules, defines some pretty
printers, and provides functions to interactively check modules
(mainly run_l and norec).
*)
#cd "..";;
#directory "lib";;
#directory "kernel";;
#directory "checker";;
#directory "+threads";;
#directory "+camlp4";;
#directory "+camlp5";;
#load "unix.cma";;
#load"threads.cma";;
#load "str.cma";;
#load "gramlib.cma";;
(*#load "toplevellib.cma";;
#directory "/usr/lib/ocaml/compiler-libs/utils";;
let _ = Clflags.recursive_types:=true;;
*)
#load "check.cma";;
open Typeops;;
open Check;;
open Pp;;
open CErrors;;
open Util;;
open Names;;
open Term;;
open Environ;;
open Declarations;;
open Mod_checking;;
open Cic;;
let pr_id id = str(string_of_id id)
let pr_na = function Name id -> pr_id id | _ -> str"_";;
let prdp dp = pp(str(string_of_dirpath dp));;
(*
let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
let prcs cs = prc (Declarations.force cs);;
let pru u = pp(str(Univ.string_of_universe u));;*)
let pru u = pp(Univ.pr_uni u);;
let prlab l = pp(str(string_of_label l));;
let prid id = pp(pr_id id);;
let prcon c = pp(Indtypes.prcon c);;
let prkn kn = pp(Indtypes.prkn kn);;
let prus g = pp(Univ.pr_universes g);;
let prcstrs c =
let g = Univ.merge_constraints c Univ.initial_universes in
pp(Univ.pr_universes g);;
(*let prcstrs c = pp(Univ.pr_constraints c);; *)
(*
let prenvu e =
let u = universes e in
let pu =
str "UNIVERSES:"++fnl()++str" "++hov 0 (Univ.pr_universes u) ++fnl() in
pp pu;;
let prenv e =
let ctx1 = named_context e in
let ctx2 = rel_context e in
let pe =
hov 1 (str"[" ++
prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
str"]") ++ spc() ++
hov 1 (str"[" ++
prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
str"]") in
pp pe;;
*)
(*
let prsub s =
let string_of_mp mp =
let s = string_of_mp mp in
(match mp with MPbound _ -> "#bound."|_->"")^s in
pp (hv 0
(fold_subst
(fun msid mp strm ->
str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
str (string_of_mp mp) ++ fnl() ++ strm)
(fun mbid mp strm ->
str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
str (string_of_mp mp) ++ fnl() ++ strm)
(fun mp1 mp strm ->
str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
;;
*)
#install_printer prid;;
#install_printer prcon;;
#install_printer prlab;;
#install_printer prdp;;
#install_printer prkn;;
#install_printer pru;;
(*
#install_printer prc;;
#install_printer prcs;;
*)
#install_printer prcstrs;;
(*#install_printer prus;;*)
(*#install_printer prenv;;*)
(*#install_printer prenvu;;
#install_printer prsub;;*)
Checker.init_with_argv [|"";"-coqlib";"."|];;
Flags.make_silent false;;
Flags.debug := true;;
Sys.catch_break true;;
let module_of_file f =
let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
(mb:Cic.module_body)
;;
let deref_mod md s =
let l = match md.mod_expr with
Struct(NoFunctor l) -> l
| FullStruct ->
(match md.mod_type with
NoFunctor l -> l)
in
List.assoc (label_of_id(id_of_string s)) l
;;
(*
let mod_access m fld =
match m.mod_expr with
Some(SEBstruct l) -> List.assoc fld l
| _ -> failwith "bad structure type"
;;
*)
let parse_dp s =
make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s))
;;
let parse_sp s =
let l = List.rev (Str.split(Str.regexp"\\.") s) in
{dirpath=List.tl l; basename=List.hd l};;
let parse_kn s =
let l = List.rev (Str.split(Str.regexp"\\.") s) in
let dp = make_dirpath(List.map id_of_string(List.tl l)) in
make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
;;
let parse_con s =
let l = List.rev (Str.split(Str.regexp"\\.") s) in
let dp = make_dirpath(List.map id_of_string(List.tl l)) in
make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
;;
let get_mod dp =
lookup_module dp (Safe_typing.get_env())
;;
let get_mod_type dp =
lookup_modtype dp (Safe_typing.get_env())
;;
let get_cst kn =
lookup_constant kn (Safe_typing.get_env())
;;
let read_mod s f =
let lib = intern_from_file (parse_dp s,f) in
((Obj.magic lib.library_compiled):
dir_path *
module_body *
(dir_path * Digest.t) list *
engagement option);;
let expln f x =
try f x
with UserError(_,strm) as e ->
msgnl strm; raise e
let admit_l l =
let l = List.map parse_sp l in
Check.recheck_library ~admit:l ~check:l;;
let run_l l =
Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
let norec q =
Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;
(*
admit_l["Bool";"OrderedType";"DecidableType"];;
run_l["FSetInterface"];;
*)
|
