From: Ferruccio Guidi Date: Tue, 16 Dec 2014 12:45:24 +0000 (+0000) Subject: - we add the missing layer constraint on applicability condition X-Git-Tag: make_still_working~781 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c86bc0cda903d7cac66e2d4cb81bca345b4b5bc;p=helm.git - we add the missing layer constraint on applicability condition - trace levels refactoring --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index b6d1f4d83..42463197a 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -153,11 +153,11 @@ src/basic_rg/brgReduction.cmx : src/lib/share.cmx src/common/output.cmx \ 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 \ diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index c9cc85e9b..6524dda86 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -38,7 +38,7 @@ type ho_whd_result = (* Internal functions *******************************************************) -let level = 4 +let level = 5 let term_of_whdr = function | Sort_ h -> Z.Sort h @@ -48,11 +48,11 @@ let term_of_whdr = function 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 = []} diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index e76399c5f..b6f3deb55 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -23,11 +23,11 @@ module ZR = BagReduction (* 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 @@ -93,7 +93,7 @@ let rec b_type_of err f st c x = | 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) diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 08f3a3407..e20737ec4 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -33,17 +33,17 @@ type message = (rtm, B.term) L.message (* 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 -> diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 2dfb2552d..fd06282fe 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -24,14 +24,14 @@ module BR = BrgReduction (* 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) @@ -59,7 +59,8 @@ let assert_applicability err f st m u w v = 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 (**) diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index 458962b1f..d028e0585 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -11,6 +11,7 @@ module L = Log module G = Options +module N = Layer module E = Entity module B = Brg module BE = BrgEnvironment @@ -18,16 +19,16 @@ module BR = BrgReduction (* 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) @@ -54,10 +55,13 @@ let assert_applicability err f st m v 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 = diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index d78100324..494b39159 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -30,11 +30,11 @@ type status = (J.mark, layer) H.t (* environment for layer variables *) (* 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 diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index bded35b3b..e7f9158b1 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -97,8 +97,9 @@ let xlate_entity st entity = match !G.kernel, entity with 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 @@ -275,8 +276,7 @@ let process st name = 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 = @@ -338,8 +338,9 @@ let main = in let help = "Usage: helena [ -LPVXdgilopqtx1 | -Ts | -MO | -m | -ahkr ]* [ ]*\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 @@ -392,4 +393,4 @@ let main = ("-t", Arg.Clear version, help_t); ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); - ] process_file help; + ] process_file help