src/basic_rg/brgValidity.cmi : src/common/layer.cmi \
src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
src/basic_rg/brgValidity.cmo : src/common/options.cmx src/lib/log.cmi \
- src/common/entity.cmx src/basic_rg/brgReduction.cmi \
+ src/common/layer.cmi src/common/entity.cmx src/basic_rg/brgReduction.cmi \
src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
src/basic_rg/brgValidity.cmi
src/basic_rg/brgValidity.cmx : src/common/options.cmx src/lib/log.cmx \
- src/common/entity.cmx src/basic_rg/brgReduction.cmx \
+ src/common/layer.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \
src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgValidity.cmi
src/basic_rg/brgType.cmi : src/common/layer.cmi \
(* Internal functions *******************************************************)
-let level = 4
+let level = 5
let term_of_whdr = function
| Sort_ h -> Z.Sort h
let log1 st s c t =
let s1, s2 = s ^ " in the environment", "the term" in
- L.log st ZO.specs level (L.et_items1 s1 c s2 t)
+ L.log st ZO.specs (pred level) (L.et_items1 s1 c s2 t)
let log2 st s cu u ct t =
let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
- L.log st ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ L.log st ZO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let empty_machine = {i = 0; c = Z.empty_lenv; s = []}
(* Internal functions *******************************************************)
-let level = 3
+let level = 4
let log1 st s c t =
let s1, s2 = s ^ " in the envireonment", "the term" in
- L.log st ZO.specs level (L.et_items1 s1 c s2 t)
+ L.log st ZO.specs (pred level) (L.et_items1 s1 c s2 t)
let error1 err st c t =
let sc = "In the envireonment" in
| Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->
- if !G.trace > level then L.log st ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
+ if !G.trace > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
(* Internal functions *******************************************************)
-let level = 4
+let level = 5
let sublevel = succ level
let log1 st s c t =
let s1, s2 = s ^ " in the environment", "the term" in
- L.log st BO.specs level (L.et_items1 s1 c s2 t)
+ L.log st BO.specs (pred level) (L.et_items1 s1 c s2 t)
let log2 st s cu u ct t =
let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
- L.log st BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let rec list_and map = function
| hd1 :: tl1, hd2 :: tl2 ->
(* Internal functions *******************************************************)
-let level = 3
+let level = 4
let message1 st1 m t1 =
L.et_items1 "In the environment" m st1 t1
let log1 st s m t =
let s = s ^ " the term" in
- L.log st BR.specs level (message1 s m t)
+ L.log st BR.specs (pred level) (message1 s m t)
let error1 err s m t =
err (message1 s m t)
match BR.xwhd st m None u with
| _, B.Sort _ ->
error1 err "not a function type" m u
- | mu, B.Bind (_, B.Abst (_, u), _) ->
+ | mu, B.Bind (_, B.Abst (n, u), _) ->
+ if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function type" m u else
if BR.are_convertible st mu zero u m zero w then f () else
error3 err m v w ~mu u
| _ -> assert false (**)
module L = Log
module G = Options
+module N = Layer
module E = Entity
module B = Brg
module BE = BrgEnvironment
(* Internal functions *******************************************************)
-let level = 3
+let level = 4
-let warn s = L.warn level s
+let warn s = L.warn (pred level) s
let message1 st1 m t1 =
L.et_items1 "In the environment" m st1 t1
let log1 st s m t =
let s = s ^ " the term" in
- L.log st BR.specs level (message1 s m t)
+ L.log st BR.specs (pred level) (message1 s m t)
let error1 err s m t =
err (message1 s m t)
match BR.xwhd st m None t with
| _, B.Sort _ ->
error1 err "not a function" m t
- | mw, B.Bind (_, B.Abst (_, w), _) ->
- if !G.trace >= level then warn "Asserting convertibility for application";
- if BR.are_convertible st mw zero w m one v then f () else
- error2 err mw w m v
+ | mw, B.Bind (_, B.Abst (n, w), _) ->
+ if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
+ else begin
+ if !G.trace >= level then warn "Asserting convertibility for application";
+ if BR.are_convertible st mw zero w m one v then f () else
+ error2 err mw w m v
+ end
| _ -> assert false (**)
let rec b_validate err f st m x =
(* Internal functions *******************************************************)
-let level = 6
+let level = 7
let env_size = 1300
-let warn s = L.warn level s
+let warn s = L.warn (pred level) s
let zero = Fin 0
let pp_progress e =
let f _ na u =
let s = U.string_of_uri u in
- L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s)
+ L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s);
in
+ Y.utime_stamp "intermediate";
match e with
| CrgEntity e -> E.common f e
| BrgEntity e -> E.common f e
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
let st = process st lexbuf input in
- close_in ich;
-(* if !G.cc then XL.export_csys st.kst.S.cc; *)
+ close_in ich;
st, input
let main =
in
let help =
"Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -m <file> | -ahkr <string> ]* [ <file> ]*\n\n" ^
- "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 typing information,\n" ^
- " 4 conversion information, 5 reduction information, 6 level disambiguation\n\n" ^
+ "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
+ " 4 typing information, 5 conversion information, 6 reduction information,\n" ^
+ " 7 level disambiguation\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
in
let help_L = " show lexer debug information" in
("-t", Arg.Clear version, help_t);
("-x", Arg.Set export, help_x);
("-1", Arg.Set streaming, help_1);
- ] process_file help;
+ ] process_file help
projects / helm.git / commitdiff