From: Ferruccio Guidi Date: Mon, 10 Nov 2014 17:27:22 +0000 (+0000) Subject: the commit continues with the support for validation (inactive for now) X-Git-Tag: make_still_working~802 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d21e43252fea9aa0351824525014a2471b7bd232;p=helm.git the commit continues with the support for validation (inactive for now) --- diff --git a/helm/software/helena/src/basic_rg/Make b/helm/software/helena/src/basic_rg/Make index ccbbf5003..0116820c7 100644 --- a/helm/software/helena/src/basic_rg/Make +++ b/helm/software/helena/src/basic_rg/Make @@ -1,2 +1,2 @@ brg brgCrg brgOutput -brgEnvironment brgSubstitution brgReduction brgType brgUntrusted +brgEnvironment brgSubstitution brgReduction brgValidity brgType brgUntrusted diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 27f471f9a..373f94973 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -16,6 +16,7 @@ module B = Brg module BE = BrgEnvironment module BR = BrgReduction module BT = BrgType +module BV = BrgValidity (* Interface functions ******************************************************) @@ -36,3 +37,12 @@ let type_check err f st = function in L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t | _, _, E.Void -> assert false + +let validate err f st e = + let uri, t = match e with + | _, uri, E.Abst (_, t) -> uri, t + | _, uri, E.Abbr t -> uri, t + | _, _, E.Void -> assert false + in + let f () = let _ = BE.set_entity e in f () in + L.loc := U.string_of_uri uri; BV.validate err f st BR.empty_kam t diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.mli b/helm/software/helena/src/basic_rg/brgUntrusted.mli index eb3136da2..a93abd5b6 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.mli +++ b/helm/software/helena/src/basic_rg/brgUntrusted.mli @@ -10,5 +10,9 @@ V_______________________________________________________________ *) val type_check: - (BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> + (BrgReduction.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> + Status.status -> Brg.entity -> 'a + +val validate: + (BrgReduction.message -> 'a) -> (unit -> 'a) -> Status.status -> Brg.entity -> 'a diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml new file mode 100644 index 000000000..0fd2b8cba --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -0,0 +1,91 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = Log +module E = Entity +module B = Brg +module BE = BrgEnvironment +module BR = BrgReduction + +(* Internal functions *******************************************************) + +let level = 4 + +let message1 st1 m t1 = + L.et_items1 "In the environment" m st1 t1 + +let log1 s m t = + let s = s ^ " the term" in + L.log BR.specs level (message1 s m t) + +let error1 err s m t = + err (message1 s m t) + +let message2 m1 t1 m2 t2 = + let sm2, st2 = "In the environment", "the term" in + let sm1, st1 = "is valid, but in the environment", "it must be of type" in + L.et_items2 sm2 m2 st2 t2 ~sc2:sm1 ~c2:m1 st1 t1 + +let error2 err m1 t1 m2 t2 = + err (message2 m1 t1 m2 t2) + +let assert_convertibility err f st m u t = + if BR.are_convertible st m (Some 0) u m (Some 1) t then f () else + error2 err m u m t + +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 BR.are_convertible st mw (Some 0) w m (Some 1) v then f () else + error2 err mw w m v + | _ -> assert false (**) + +let rec b_validate err f st m x = + log1 "Now checking" m x; + match x with + | B.Sort _ -> f () + | B.LRef (_, i) -> + begin match BR.get m i with + | B.Abst _ + | B.Abbr _ -> f () + | B.Void -> + error1 err "reference to excluded variable" m x + end + | B.GRef (_, uri) -> + begin match BE.get_entity uri with + | _, _, E.Abst _ + | _, _, E.Abbr _ -> f () + | _, _, E.Void -> + error1 err "reference to unknown entry" m x + end + | B.Bind (a, b, t) -> + let f () = b_validate err f st (BR.push m a b) t in + begin match b with + | B.Abst (n, u) -> validate err f st m u + | B.Abbr v -> validate err f st m v + | B.Void -> f () + end + | B.Appl (_, v, t) -> + let f () = assert_applicability err f st m v t in + let f () = b_validate err f st m t in + validate err f st m v + | B.Cast (_, u, t) -> + let f () = assert_convertibility err f st m u t in + let f () = b_validate err f st m t in + validate err f st m u + +(* Interface functions ******************************************************) + +and validate err f st m x = + let f () = L.unbox level; f () in + L.box level; b_validate err f st m x diff --git a/helm/software/helena/src/basic_rg/brgValidity.mli b/helm/software/helena/src/basic_rg/brgValidity.mli new file mode 100644 index 000000000..8ee88457d --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgValidity.mli @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val validate: + (BrgReduction.message -> 'a) -> (unit -> 'a) -> + Status.status -> BrgReduction.kam -> Brg.term -> 'a diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 207fcccda..63cadfb75 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -44,7 +44,7 @@ module BE = brgEnvironment module BS = brgSubstitution module BR = brgReduction module BT = brgType -module BV = brgValid +module BV = brgValidity module BU = brgUntrusted module Z = bag diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index d0476f78a..52d2b0be2 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -95,7 +95,7 @@ let pp_progress e = let s = U.string_of_uri u in let err () = L.warn (P.sprintf "%s" s) in let f i = L.warn (P.sprintf "[%u] %s" i s) in - E.mark err f a + E.apix err f a in match e with | CrgEntity e -> E.common f e @@ -120,6 +120,14 @@ let type_check st k = | BagEntity entity -> ZU.type_check ok st.kst entity | CrgEntity _ -> st +let validate st k = + let brg_err msg = brg_error "Validation Error" msg; failwith "Interrupted" in + let ok _ = st in + match k with + | BrgEntity entity -> BU.validate brg_err ok st.kst entity + | BagEntity _ -> st + | CrgEntity _ -> st + (* extended lexer ***********************************************************) type 'token lexer = { @@ -192,6 +200,7 @@ let count_input st = function (****************************************************************************) +let version = ref true let stage = ref 3 let progress = ref false let preprocess = ref false @@ -203,7 +212,10 @@ let streaming = ref false (* parsing style (temporary) *) let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in if !export then export_entity entity; - if !stage > 2 then type_check st entity else st + if !stage > 2 then + let f = if !version then validate else type_check in + f st entity + else st let process_1 st entity = if !progress then pp_progress entity; @@ -261,7 +273,7 @@ let process st name = let main = try - let version_string = "Helena 0.8.2 M - January 2011" in + let version_string = "Helena 0.8.2 M - November 2014" in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else @@ -282,6 +294,7 @@ try st := initial_status (); L.clear (); G.clear (); H.clear (); O.clear_reductions (); streaming := false; + version := true in let process_file name = if !L.level > 0 then Y.gmtime version_string; @@ -308,7 +321,7 @@ try flush_all () in let help = - "Usage: helena [ -LPVXcgijopqx1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijopqtx1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -331,6 +344,7 @@ try let help_q = " disable quotation of identifiers" in let help_r = " set initial segment of URI hierarchy (default: empty)" in let help_s = " set translation stage (see above)" in + let help_t = " type check [version 1]" in let help_x = " export kernel entities (XML)" in let help_1 = " parse files with streaming policy" in @@ -354,6 +368,7 @@ try ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); + ("-t", Arg.Clear version, help_t); ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help;