diff options
| author |  Bruno Barras <bruno.barras@inria.fr> | 2014-12-23 13:43:48 +0100 |
|---|---|---|
| committer | Bruno Barras <bruno.barras@inria.fr> | 2015-01-06 15:32:12 +0100 |
| commit | fb6bee00a1b52aecbdccc76bf3aa6edf6ed3df08 (patch) | |
| tree | 7032b1a3b3edf9a28552775387d67e438536deaf /checker/include | |
| parent | ed93de78345ecd93c4fd8cac0917f1fd34f51d44 (diff) | |
updated include file for debugging
Diffstat (limited to 'checker/include')
| -rw-r--r-- | checker/include | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/checker/include b/checker/include index 0b68da4b7..f5bd2984e 100644 --- a/checker/include +++ b/checker/include @@ -12,10 +12,12 @@ #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";; @@ -29,12 +31,14 @@ open Typeops;; open Check;; open Pp;; +open Errors;; 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"_";; @@ -111,21 +115,31 @@ let prsub s = (*#install_printer prenvu;; #install_printer prsub;;*) -Checker.init_with_argv [|""|];; +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:module_body) + (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)) ;; @@ -160,10 +174,6 @@ let read_mod s f = (dir_path * Digest.t) list * engagement option);; -let deref_mod md s = - let (Some (SEBstruct l)) = md.mod_expr in - List.assoc (label_of_id(id_of_string s)) l -;; let expln f x = try f x |