Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192(* -*-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 relevant 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";;
#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.quiet := 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);;
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"];;*)