From f3b4d265268a43ca98e6843b733109fdfe3f6b0b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 9 Dec 2008 19:26:31 +0000 Subject: [PATCH] first version of kernel "basic_rg" the grundlagen does not typecheck because some of its lambdas are actually pis (this is known) --- helm/software/lambda-delta/.depend.opt | 29 +++- helm/software/lambda-delta/basic_rg/Make | 2 +- helm/software/lambda-delta/basic_rg/brg.ml | 10 ++ .../lambda-delta/basic_rg/brgReduction.ml | 159 +++++++++++++++--- .../lambda-delta/basic_rg/brgReduction.mli | 14 ++ .../software/lambda-delta/basic_rg/brgType.ml | 61 +++++++ .../lambda-delta/basic_rg/brgType.mli | 15 ++ .../lambda-delta/basic_rg/brgUntrusted.ml | 23 +++ .../lambda-delta/basic_rg/brgUntrusted.mli | 13 ++ helm/software/lambda-delta/lib/Make | 2 +- helm/software/lambda-delta/lib/cps.ml | 7 + helm/software/lambda-delta/lib/share.ml | 16 ++ helm/software/lambda-delta/toplevel/top.ml | 18 +- 13 files changed, 335 insertions(+), 34 deletions(-) create mode 100644 helm/software/lambda-delta/basic_rg/brgType.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgType.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgUntrusted.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgUntrusted.mli create mode 100644 helm/software/lambda-delta/lib/share.ml diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index a00ee1636..418d35ef0 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -24,10 +24,21 @@ basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi -basic_rg/brgReduction.cmo: lib/nUri.cmi basic_rg/brgEnvironment.cmi \ - basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgReduction.cmx: lib/nUri.cmx basic_rg/brgEnvironment.cmx \ - basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgReduction.cmi: basic_rg/brg.cmx +basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/cps.cmx \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/cps.cmx \ + basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgType.cmi: basic_rg/brgReduction.cmi basic_rg/brg.cmx +basic_rg/brgType.cmo: basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi \ + basic_rg/brg.cmx basic_rg/brgType.cmi +basic_rg/brgType.cmx: basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx \ + basic_rg/brg.cmx basic_rg/brgType.cmi +basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx +basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brgUntrusted.cmi +basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgEnvironment.cmx basic_rg/brgUntrusted.cmi toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx @@ -46,8 +57,10 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \ - toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \ - automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx + toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \ + basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \ + automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \ - toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ - automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx + toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ + basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \ + automath/autLexer.cmx diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make index c40f0cc46..eb1c64a66 100644 --- a/helm/software/lambda-delta/basic_rg/Make +++ b/helm/software/lambda-delta/basic_rg/Make @@ -1 +1 @@ -brg brgOutput brgEnvironment brgReduction +brg brgOutput brgEnvironment brgReduction brgType brgUntrusted diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 45777ead4..36e4fefe8 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -24,3 +24,13 @@ type term = Sort of int (* hierarchy index *) type obj = int * uri * bind * term (* age, uri, binder, contents *) type item = obj option + +type hierarchy = int -> int + +(* Currified constructors ***************************************************) + +let cast u t = Cast (u, t) + +let appl u t = Appl (u, t) + +let bind id b u t = Bind (id, b, u, t) diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index b194b00bf..aced1a22e 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -10,12 +10,18 @@ V_______________________________________________________________ *) module U = NUri +module C = Cps +module S = Share module B = Brg module E = BrgEnvironment exception LRefNotFound of string Lazy.t -type environment = int * (B.bind * B.term) list +type bind = Void_ + | Abst_ of B.term + | Abbr_ of B.term + +type environment = int * bind list type stack = B.term list @@ -27,51 +33,162 @@ type context = { type whd_result = | Sort_ of int - | LRef_ of int - | GRef_ of int * U.uri * B.bind - | Abst_ of B.term + | LRef_ of int * B.term option + | GRef_ of int * B.bind * B.term + | Bind_ of B.term * B.term + +type ho_whd_result = + | Sort of int + | Abst of B.term (* Internal functions *******************************************************) -let push_e f b t (l, e) = - f (succ l, (b, t) :: e) +let empty_e = 0, [] + +let push_e f b (l, e) = + f (succ l, b :: e) -let rec find_e f c i = +let get_e f c i = let (gl, ge), (ll, le) = c.g, c.l in if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i))); - let b, t = + let b = if i < gl then List.nth ge (gl - (succ i)) else List.nth le (gl + ll - (succ i)) in - f t b - + f b + +let rec lref_map f map t = match t with + | B.LRef i -> f (B.LRef (map i)) + | B.GRef _ -> f t + | B.Sort _ -> f t + | B.Cast (w, u) -> + let f w' u' = f (S.sh2 w w' u u' t B.cast) in + let f w' = lref_map (f w') map u in + lref_map f map w + | B.Appl (w, u) -> + let f w' u' = f (S.sh2 w w' u u' t B.appl) in + let f w' = lref_map (f w') map u in + lref_map f map w + | B.Bind (id, b, w, u) -> + let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in + let f w' = lref_map (f w') map u in + lref_map f map w + +(* to share *) +let lift f c = + let (gl, _), (ll, le) = c.g, c.l in + let map i = if i >= gl then succ i else i in + let map f = function + | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t + | _ -> assert false + in + let f le' = f {c with l = (ll, le')} in + C.list_map f map le + +let xchg f c t = + let (gl, _), (ll, _) = c.g, c.l in + let map i = + if i < gl || i > gl + ll then i else + if i >= gl && i < gl + ll then succ i else gl + in + lref_map (f c) map t + +(* to share *) let rec whd f c t = match t with - | B.Sort h -> f c t (Sort_ h) + | B.Sort h -> f c (Sort_ h) | B.GRef uri -> - let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in + let f (i, _, b, t) = f c (GRef_ (i, b, t)) in E.get_obj f uri | B.LRef i -> - let f t = function - | B.Abst -> f c t (LRef_ i) - | B.Abbr -> whd f c t + let f = function + | Void_ -> f c (LRef_ (i, None)) + | Abst_ t -> f c (LRef_ (i, Some t)) + | Abbr_ t -> whd f c t in - find_e f c i + get_e f c i | B.Appl (v, t) -> whd f {c with s = v :: c.s} t | B.Bind (_, B.Abbr, v, t) -> let f l = whd f {c with l = l} t in - push_e f B.Abbr v c.l + push_e f (Abbr_ v) c.l | B.Bind (_, B.Abst, w, t) -> begin match c.s with - | [] -> f c t (Abst_ w) + | [] -> f c (Bind_ (w, t)) | v :: tl -> let f tl l = whd f {c with l = l; s = tl} t in - push_e (f tl) B.Abbr v c.l + push_e (f tl) (Abbr_ v) c.l end | B.Cast (_, t) -> whd f c t +let push f c t = + assert (c.s = []); + let f c g = xchg f {c with g = g} t in + let f c = push_e (f c) Void_ c.g in + lift f c + (* Interface functions ******************************************************) +let rec are_convertible f c1 t1 c2 t2 = + let rec aux c1' r1 c2' r2 = match r1, r2 with + | Sort_ h1, Sort_ h2 -> f (h1 = h2) + | LRef_ (i1, _), LRef_ (i2, _) -> + if i1 = i2 then are_convertible_stacks f c1' c2' else f false + | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _) -> + if a1 = a2 then are_convertible_stacks f c1' c2' else f false + | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) -> + if a1 = a2 then are_convertible_stacks f c1' c2' else + if a1 < a2 then whd (aux c1' r1) c2' v2 else + whd (aux_rev c2' r2) c1' v1 + | _, GRef_ (_, B.Abbr, v2) -> + whd (aux c1' r1) c2' v2 + | GRef_ (_, B.Abbr, v1), _ -> + whd (aux_rev c2' r2) c1' v1 + | Bind_ (w1, t1), Bind_ (w2, t2) -> + let f b = + if b then + let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in + push f c1' t1 + else f false + in + are_convertible f c1' w1 c2' w2 + | _ -> f false + and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in + let f c1' r1 = whd (aux c1' r1) c2 t2 in + whd f c1 t1 + +and are_convertible_stacks f c1 c2 = + let map f v1 v2 = are_convertible f c1 v1 c2 v2 in + if List.length c1.s <> List.length c2.s then f false else + C.forall2 f map c1.s c2.s + +let are_convertible f c t1 t2 = are_convertible f c t1 c t2 + +let rec ho_whd f c t = + let aux c' = function + | Sort_ h -> f c' (Sort h) + | Bind_ (w, t) -> f c' (Abst w) + | LRef_ (_, Some w) -> ho_whd f c w + | GRef_ (_, _, u) -> ho_whd f c u + | LRef_ (_, None) -> assert false + in + whd aux c t + let push f c b t = - assert (fst c.l = 0 && c.s = []); + assert (c.l = empty_e && c.s = []); let f g = f {c with g = g} in - push_e f b t c.g + let b = match b with + | B.Abbr -> Abbr_ t + | B.Abst -> Abst_ t + in + push_e f b c.g + +let get f c i = + let gl, ge = c.g in + if i >= gl then raise (LRefNotFound (lazy (string_of_int i))); + match List.nth ge (gl - (succ i)) with + | Abbr_ v -> f (B.Abbr, v) + | Abst_ w -> f (B.Abst, w) + | Void_ -> assert false + +let empty_context = { + g = empty_e; l = empty_e; s = [] +} diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index fecf29b83..a8320ed55 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -12,3 +12,17 @@ exception LRefNotFound of string Lazy.t type context + +type ho_whd_result = + | Sort of int + | Abst of Brg.term + +val empty_context: context + +val push: (context -> 'a) -> context -> Brg.bind -> Brg.term -> 'a + +val get: (Brg.bind * Brg.term -> 'a) -> context -> int -> 'a + +val are_convertible: (bool -> 'a) -> context -> Brg.term -> Brg.term -> 'a + +val ho_whd: (context -> ho_whd_result -> 'a) -> context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml new file mode 100644 index 000000000..d10ddefaa --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -0,0 +1,61 @@ +(* + ||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 B = Brg +module E = BrgEnvironment +module R = BrgReduction + +exception TypeError of string Lazy.t + +(* Internal functions *******************************************************) + +let error msg = raise (TypeError (lazy msg)) + +(* Interface functions ******************************************************) + +let rec type_of f g c = function + | B.Sort h -> f (B.Sort (g h)) + | B.LRef i -> + let f = function + | B.Abst, w -> f w + | B.Abbr, B.Cast (w, v) -> f w + | B.Abbr, _ -> error "lref" + in + R.get f c i + | B.GRef uri -> + let f = function + | _, _, B.Abst, w -> f w + | _, _, B.Abbr, B.Cast (w, v) -> f w + | _, _, B.Abbr, _ -> error "gref" + in + E.get_obj f uri + | B.Bind (id, b, u, t) -> + let f uu tt = match b, t with + | B.Abst, _ + | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt)) + | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt)) + in + let f uu cc = type_of (f uu) g cc t in + let f uu = R.push (f uu) c b u in + type_of f g c u + | B.Appl (v, t) -> + let f tt cc = function + | R.Sort _ -> error "appl" + | R.Abst w -> + let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in + type_of (R.are_convertible f cc w) g c v + in + let f tt = R.ho_whd (f tt) c t in + type_of f g c t + | B.Cast (u, t) -> + let f b = if b then f u else error "cast" in + let f _ = type_of (R.are_convertible f c u) g c t in + type_of f g c u diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli new file mode 100644 index 000000000..5b351cca4 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -0,0 +1,15 @@ +(* + ||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_______________________________________________________________ *) + +exception TypeError of string Lazy.t + +val type_of: (Brg.term -> 'a) -> + Brg.hierarchy -> BrgReduction.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml new file mode 100644 index 000000000..c9f425f88 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -0,0 +1,23 @@ +(* + ||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 E = BrgEnvironment +module R = BrgReduction +module T = BrgType + +(* Interface functions ******************************************************) + +let type_check f g = function + | None -> f None + | Some ((_, _, _, t) as obj) -> + let f tt obj = f (Some (tt, obj)) in + let f tt = E.set_obj (f tt) obj in + T.type_of f g R.empty_context t diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli new file mode 100644 index 000000000..7bf3c8793 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -0,0 +1,13 @@ +(* + ||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 type_check: ((Brg.term * Brg.obj) option -> 'a) -> + Brg.hierarchy -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/lib/Make b/helm/software/lambda-delta/lib/Make index 9a90150e8..5b884ad1b 100644 --- a/helm/software/lambda-delta/lib/Make +++ b/helm/software/lambda-delta/lib/Make @@ -1 +1 @@ -nUri cps log time +nUri cps share log time diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index 14b9d4a2c..c235197d9 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -30,6 +30,13 @@ let rec list_rev_map_append f map ~tail = function let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in map f hd +let rec forall2 f map l1 l2 = match l1, l2 with + | [], [] -> f true + | hd1 :: tl1, hd2 :: tl2 -> + let f b = if b then forall2 f map tl1 tl2 else f false in + map f hd1 hd2 + | _ -> f false + let list_rev_append f = list_rev_map_append f (fun f t -> f t) diff --git a/helm/software/lambda-delta/lib/share.ml b/helm/software/lambda-delta/lib/share.ml new file mode 100644 index 000000000..019cca982 --- /dev/null +++ b/helm/software/lambda-delta/lib/share.ml @@ -0,0 +1,16 @@ +(* + ||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_______________________________________________________________ *) + +let sh a b = + if a == b then a else b + +let sh2 a1 b1 a2 b2 c1 c2 = + if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2) diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 1442d7521..92840d54a 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -16,6 +16,7 @@ module MA = MetaAut module MO = MetaOutput module MBrg = MetaBrg module BrgO = BrgOutput +module BrgU = BrgUntrusted type status = { summary: int; @@ -39,8 +40,9 @@ let count st count_fun c item = let main = let version_string = "Helena Checker 0.8.0 M - December 2008" in let summary = ref 0 in - let stage = ref 2 in + let stage = ref 3 in let meta_file = ref None in + let hierarchy = ref (fun h -> h + 2) in let set_summary i = summary := i in let print_version () = L.warn version_string; exit 0 in let set_stage i = stage := i in @@ -68,10 +70,18 @@ let main = let rec aux st = function | [] -> st | item :: tl -> - let st = {st with ac = count st AO.count_item st.ac item} in +(* stage 3 *) + let f st = function + | None -> st + | Some (_, (i, _, _, _)) -> + Log.warn (string_of_int i); st + in +(* stage 2 *) let f st item = - {st with brgc = count st BrgO.count_item st.brgc item} + let st = {st with brgc = count st BrgO.count_item st.brgc item} in + if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st in +(* stage 1 *) let f mst item = let st = {st with mst = mst; mc = count st MO.count_item st.mc item @@ -82,6 +92,8 @@ let main = end; if !stage > 1 then MBrg.brg_of_meta (f st) item else st in +(* stage 0 *) + let st = {st with ac = count st AO.count_item st.ac item} in let st = if !stage > 0 then MA.meta_of_aut f st.mst item else st in -- 2.39.2