From: Ferruccio Guidi Date: Sun, 14 Dec 2008 15:32:38 +0000 (+0000) Subject: we are changing the kernel version from basic_rg to basic_ag X-Git-Tag: make_still_working~4400 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c87a73806365feadc23300194a42ab8edb0f8b1b;p=helm.git we are changing the kernel version from basic_rg to basic_ag --- diff --git a/helm/software/lambda-delta/basic_ag/Make b/helm/software/lambda-delta/basic_ag/Make new file mode 100644 index 000000000..eb1c64a66 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/Make @@ -0,0 +1 @@ +brg brgOutput brgEnvironment brgReduction brgType brgUntrusted diff --git a/helm/software/lambda-delta/basic_ag/brg.ml b/helm/software/lambda-delta/basic_ag/brg.ml new file mode 100644 index 000000000..73da25b2d --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brg.ml @@ -0,0 +1,71 @@ +(* + ||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_______________________________________________________________ *) + +type uri = NUri.uri +type id = Aut.id + +type bind = Void (* exclusion *) + | Abst of term (* abstraction *) + | Abbr of term (* abbreviation *) + +and term = Sort of int (* hierarchy index *) + | LRef of int (* reverse de Bruijn index *) + | GRef of uri (* reference *) + | Cast of term * term (* type, term *) + | Appl of term * term (* argument, function *) + | Bind of id * bind * term (* name, binder, scope *) + +type obj = int * uri * bind (* age, uri, binder, contents *) + +type item = obj option + +type context = int * (id * bind) list + +type message = (context, term) Log.item list + +(* Currified constructors ***************************************************) + +let abst w = Abst w + +let abbr v = Abbr v + +let cast u t = Cast (u, t) + +let appl u t = Appl (u, t) + +let bind id b t = Bind (id, b, t) + +let bind_abst id u t = Bind (id, Abst u, t) + +let bind_abbr id v t = Bind (id, Abbr v, t) + +(* context handling functions ***********************************************) + +let empty_context = 0, [] + +let push f (l, es) id b = + let c = succ l, (id, b) :: es in + f c + +let append f (l1, es1) (l2, es2) = + f (l2 + l1, List.append es2 es1) + +let map f map (l, es) = + let f es = f (l, es) in + Cps.list_map f map es + +let contents f (l, es) = f l es + +let get f (l, es) i = + if i < 0 || i >= l then f None else + let result = List.nth es (l - succ i) in + f (Some result) + diff --git a/helm/software/lambda-delta/basic_ag/brgEnvironment.ml b/helm/software/lambda-delta/basic_ag/brgEnvironment.ml new file mode 100644 index 000000000..fb4243c74 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgEnvironment.ml @@ -0,0 +1,35 @@ +(* + ||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 U = NUri +module L = Log +module H = U.UriHash +module B = Brg + +exception ObjectNotFound of B.message + +let hsize = 7000 +let env = H.create hsize +let entry = ref 0 + +(* Internal functions *******************************************************) + +let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) + +(* Interface functions ******************************************************) + +let set_obj f obj = + let _, uri, b = obj in + let obj = !entry, uri, b in + incr entry; H.add env uri obj; f obj + +let get_obj f uri = + try f (H.find env uri) with Not_found -> error uri diff --git a/helm/software/lambda-delta/basic_ag/brgEnvironment.mli b/helm/software/lambda-delta/basic_ag/brgEnvironment.mli new file mode 100644 index 000000000..8f9f8b1b0 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgEnvironment.mli @@ -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_______________________________________________________________ *) + +exception ObjectNotFound of Brg.message + +val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a + +val get_obj: (Brg.obj -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_ag/brgOutput.ml b/helm/software/lambda-delta/basic_ag/brgOutput.ml new file mode 100644 index 000000000..66c7ed3d8 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgOutput.ml @@ -0,0 +1,150 @@ +(* + ||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 P = Printf +module F = Format +module U = NUri +module C = Cps +module L = Log +module H = Hierarchy +module B = Brg + +type counters = { + eabsts: int; + eabbrs: int; + tsorts: int; + tlrefs: int; + tgrefs: int; + tcasts: int; + tappls: int; + tabsts: int; + tabbrs: int +} + +let indexes = ref false + +let initial_counters = { + eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; + tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 +} + +let rec count_term_binder f c = function + | B.Abst w -> + let c = {c with tabsts = succ c.tabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with tabbrs = succ c.tabbrs} in + count_term f c v + | B.Void -> f c + +and count_term f c = function + | B.Sort _ -> + f {c with tsorts = succ c.tsorts} + | B.LRef _ -> + f {c with tlrefs = succ c.tlrefs} + | B.GRef _ -> + f {c with tgrefs = succ c.tgrefs} + | B.Cast (v, t) -> + let c = {c with tcasts = succ c.tcasts} in + let f c = count_term f c t in + count_term f c v + | B.Appl (v, t) -> + let c = {c with tappls = succ c.tappls} in + let f c = count_term f c t in + count_term f c v + | B.Bind (_, b, t) -> + let f c = count_term_binder f c b in + count_term f c t + +let count_obj_binder f c = function + | B.Abst w -> + let c = {c with eabsts = succ c.eabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with eabbrs = succ c.eabbrs} in + count_term f c v + | B.Void -> f c + +let count_obj f c (_, _, b) = + count_obj_binder f c b + +let count_item f c = function + | Some obj -> count_obj f c obj + | None -> f c + +let print_counters f c = + let terms = + c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + + c.tabbrs + in + let items = c.eabsts + c.eabbrs in + L.warn (P.sprintf " Kernel representation summary (basic_rg)"); + L.warn (P.sprintf " Total entry items: %6u" items); + L.warn (P.sprintf " Declaration items: %6u" c.eabsts); + L.warn (P.sprintf " Definition items: %6u" c.eabbrs); + L.warn (P.sprintf " Total term items: %6u" terms); + L.warn (P.sprintf " Sort items: %6u" c.tsorts); + L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); + L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts); + L.warn (P.sprintf " Application items: %6u" c.tappls); + L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); + L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs); + f () + +let rec pp_term c frm = function + | B.Sort h -> + let f = function + | Some s -> F.fprintf frm "@[%s@]" s + | None -> F.fprintf frm "@[*%u@]" h + in + H.get_sort f h + | B.LRef i -> + let f = function + | Some (id, _) -> F.fprintf frm "@[%s@]" id + | None -> F.fprintf frm "@[#%u@]" i + in + if !indexes then f None else B.get f c i + | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) + | B.Cast (u, t) -> + F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t + | B.Appl (v, t) -> + F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t + | B.Bind (id, B.Abst w, t) -> + let f cc = + F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term cc) t + in + B.push f c id (B.Abst w) + | B.Bind (id, B.Abbr v, t) -> + let f cc = + F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term cc) t + in + B.push f c id (B.Abbr v) + | B.Bind (id, B.Void, t) -> + let f cc = F.fprintf frm "@[[%s].%a@]" id (pp_term cc) t in + B.push f c id B.Void + +let pp_context frm c = + let pp_entry frm = function + | id, B.Abst w -> + F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w + | id, B.Abbr v -> + F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v + | id, B.Void -> + F.fprintf frm "@,%s" id + in + let iter map frm l = List.iter (map frm) l in + let f _ es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in + B.contents f c + +let specs = { + L.pp_term = pp_term; L.pp_context = pp_context +} diff --git a/helm/software/lambda-delta/basic_ag/brgOutput.mli b/helm/software/lambda-delta/basic_ag/brgOutput.mli new file mode 100644 index 000000000..566dfe8f3 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgOutput.mli @@ -0,0 +1,22 @@ +(* + ||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_______________________________________________________________ *) + +type counters + +val initial_counters: counters + +val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a + +val specs: (Brg.context, Brg.term) Log.specs + +val indexes: bool ref diff --git a/helm/software/lambda-delta/basic_ag/brgReduction.ml b/helm/software/lambda-delta/basic_ag/brgReduction.ml new file mode 100644 index 000000000..4cfd5260d --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgReduction.ml @@ -0,0 +1,203 @@ +(* + ||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 C = Cps +module S = Share +module L = Log +module B = Brg +module O = BrgOutput +module E = BrgEnvironment + +exception LRefNotFound of B.message + +type machine = { + c: B.context; + s: B.term list +} + +type whd_result = + | Sort_ of int + | LRef_ of int * B.term option + | GRef_ of int * B.bind + | Bind_ of B.id * B.term * B.term + +type ho_whd_result = + | Sort of int + | Abst of B.term + +(* Internal functions *******************************************************) + +let level = 5 + +let error i = raise (LRefNotFound (L.items1 (string_of_int i))) + +let empty_machine = {c = B.empty_context; s = []} + +let get f c m i = + let f = function + | Some (_, b) -> f b + | None -> error i + in + let f gl _ = if i < gl then B.get f c i else B.get f m.c (i - gl) in + B.contents f c + +let contents f c m = + let f gl ges = B.contents (f gl ges) m.c in + B.contents f c + +let unwind_to_context f c m = B.append f c m.c + +let unwind_to_term f m t = + let map f t (id, b) = f (B.Bind (id, b, t)) in + let f _ mc = C.list_fold_left f map t mc in + B.contents f m.c + +let rec lref_map_bind f map b = match b with + | B.Abbr v -> + let f v' = f (S.sh1 v v' b B.abbr) in + lref_map f map v + | B.Abst w -> + let f w' = f (S.sh1 w w' b B.abst) in + lref_map f map w + | B.Void -> f b + +and 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, u) -> + let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in + let f b' = lref_map (f b') map u in + lref_map_bind f map b + +(* to share *) +let lift f c m = + let f gl _ = + let map i = if i >= gl then succ i else i in + let map f = function + | id, B.Abbr t -> let f t = f (id, B.Abbr t) in lref_map f map t + | _ -> assert false + in + let f mc = f {m with c = mc} in + B.map f map m.c + in + B.contents f c + +(* to share *) +let xchg f c m t = + let f gl _ ll _ = + 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 map t + in + contents f c m + +let push f c m id w t = + assert (m.s = []); + let f c m = xchg (f c m) c m t in + let f c = lift (f c) c m in + let f w = B.push f c id (B.Abst w) in + unwind_to_term f m w + +(* to share *) +let rec whd f c m x = match x with + | B.Sort h -> f m (Sort_ h) + | B.GRef uri -> + let f (i, _, b) = f m (GRef_ (i, b)) in + E.get_obj f uri + | B.LRef i -> + let f = function + | B.Void -> f m (LRef_ (i, None)) + | B.Abst t -> f m (LRef_ (i, Some t)) + | B.Abbr t -> whd f c m t + in + get f c m i + | B.Cast (_, t) -> whd f c m t + | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t + | B.Bind (id, B.Abst w, t) -> + begin match m.s with + | [] -> f m (Bind_ (id, w, t)) + | v :: tl -> + let f mc = whd f c {c = mc; s = tl} t in + B.push f m.c id (B.Abbr (B.Cast (w, v))) + end + | B.Bind (id, b, t) -> + let f mc = whd f c {m with c = mc} t in + B.push f m.c id b + +(* Interface functions ******************************************************) + +let rec ho_whd f c m x = + let aux m = function + | Sort_ h -> f c (Sort h) + | Bind_ (_, w, _) -> + let f c = f c (Abst w) in unwind_to_context f c m + | LRef_ (_, Some w) -> ho_whd f c m w + | GRef_ (_, B.Abst u) -> ho_whd f c m u + | GRef_ (_, B.Abbr t) -> ho_whd f c m t + | LRef_ (_, None) -> assert false + | GRef_ (_, B.Void) -> assert false + in + whd aux c m x + +let ho_whd f c t = + L.log O.specs level (L.ct_items1 "Now scanning" c t); + ho_whd f c empty_machine t + +let rec are_convertible f c1 m1 t1 c2 m2 t2 = + let rec aux m1 r1 m2 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 m1 c2 m2 else f false + | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) -> + if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else f false + | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) -> + if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else + if a1 < a2 then whd (aux m1 r1) c2 m2 v2 else + whd (aux_rev m2 r2) c1 m1 v1 + | _, GRef_ (_, B.Abbr v2) -> + whd (aux m1 r1) c2 m2 v2 + | GRef_ (_, B.Abbr v1), _ -> + whd (aux_rev m2 r2) c1 m1 v1 + | Bind_ (id1, w1, t1), Bind_ (id2, w2, t2) -> + let f b = + if b then + let f c1 m1 t1 = + push (are_convertible f c1 m1 t1) c2 m2 id2 w2 t2 + in + push f c1 m1 id1 w1 t1 + else f false + in + are_convertible f c1 m1 w1 c2 m2 w2 + | _ -> f false + and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in + let f m1 r1 = whd (aux m1 r1) c2 m2 t2 in + whd f c1 m1 t1 + +and are_convertible_stacks f c1 m1 c2 m2 = + let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in + let map f v1 v2 = are_convertible f c1 mm1 v1 c2 mm2 v2 in + if List.length m1.s <> List.length m2.s then f false else + C.forall2 f map m1.s m2.s + +let are_convertible f c t1 t2 = + L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2); + are_convertible f c empty_machine t1 c empty_machine t2 diff --git a/helm/software/lambda-delta/basic_ag/brgReduction.mli b/helm/software/lambda-delta/basic_ag/brgReduction.mli new file mode 100644 index 000000000..91a0289bb --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgReduction.mli @@ -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_______________________________________________________________ *) + + +exception LRefNotFound of Brg.message + +type ho_whd_result = + | Sort of int + | Abst of Brg.term + +val ho_whd: + (Brg.context -> ho_whd_result -> 'a) -> Brg.context -> Brg.term -> 'a + +val are_convertible: + (bool -> 'a) -> Brg.context -> Brg.term -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/brgType.ml b/helm/software/lambda-delta/basic_ag/brgType.ml new file mode 100644 index 000000000..fb7862c24 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgType.ml @@ -0,0 +1,119 @@ +(* + ||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 U = NUri +module S = Share +module L = Log +module H = Hierarchy +module I = AutItem +module B = Brg +module O = BrgOutput +module E = BrgEnvironment +module R = BrgReduction + +exception TypeError of B.message + +(* Internal functions *******************************************************) + +let level = 4 + +let error1 s c t = + raise (TypeError (L.ct_items1 s c t)) + +let error2 s1 c1 t1 s2 c2 t2 = + raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) + +let mk_gref u l = + let map t v = B.Appl (v, t) in + List.fold_left map (B.GRef u) l + +(* Interface functions ******************************************************) + +let rec b_type_of f g c x = + L.log O.specs level (L.ct_items1 "Now checking" c x); + match x with + | B.Sort h -> + let f h = f x (B.Sort h) in H.apply f g h + | B.LRef i -> + let f = function + | Some (_, B.Abst w) -> f x w + | Some (_, B.Abbr (B.Cast (w, v))) -> f x w + | Some (_, B.Abbr _) -> assert false + | Some (_, B.Void) -> + error1 "reference to excluded variable" c x + | None -> + error1 "variable not found" c x + in + B.get f c i + | B.GRef uri -> + let f = function + | _, _, B.Abst w -> f x w + | _, _, B.Abbr (B.Cast (w, v)) -> f x w + | _, _, B.Abbr _ -> assert false + | _, _, B.Void -> + error1 "reference to excluded object" c x + in + E.get_obj f uri + | B.Bind (id, B.Abbr v, t) -> + let f xv xt tt = + f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv tt) + in + let f xv cc = b_type_of (f xv) g cc t in + let f xv = B.push (f xv) c id (B.Abbr xv) in + let f xv vv = match xv with + | B.Cast _ -> f xv + | _ -> f (B.Cast (vv, xv)) + in + type_of f g c v + | B.Bind (id, B.Abst u, t) -> + let f xu xt tt = + f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu tt) + in + let f xu cc = b_type_of (f xu) g cc t in + let f xu _ = B.push (f xu) c id (B.Abst xu) in + type_of f g c u + | B.Bind (id, B.Void, t) -> + let f xt tt = + f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void tt) + in + let f cc = b_type_of f g cc t in + B.push f c id B.Void + | B.Appl (v, t) -> + let h xv vv xt tt cc = function + | R.Sort _ -> error1 "not a function" c xt + | R.Abst w -> + L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); + let f b = + if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else + error2 "the term" cc xv "must be of type" cc w + in + R.are_convertible f cc w vv + in + let f xv vv xt = function +(* inserting a missing "modus ponens" *) + | B.Appl (y2, B.Appl (y1, B.GRef u)) when U.eq u I.imp -> + b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt]) + | tt -> R.ho_whd (h xv vv xt tt) c tt + in + let f xv vv = b_type_of (f xv vv) g c t in + type_of f g c v + | B.Cast (u, t) -> + let f xu xt b = + if b then f (S.sh2 u xu t xt x B.cast) xu else + error2 "the term" c xt "must be of type" c xu + in + let f xu xt tt = R.are_convertible (f xu xt) c xu tt in + let f xu _ = b_type_of (f xu) g c t in + type_of f g c u + +and type_of f g c x = + let f t u = L.unbox (); f t u in + L.box (); b_type_of f g c x diff --git a/helm/software/lambda-delta/basic_ag/brgType.mli b/helm/software/lambda-delta/basic_ag/brgType.mli new file mode 100644 index 000000000..e7e2d7ed7 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgType.mli @@ -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_______________________________________________________________ *) + +exception TypeError of Brg.message + +val type_of: + (Brg.term -> Brg.term -> 'a) -> + Hierarchy.graph -> Brg.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/brgUntrusted.ml b/helm/software/lambda-delta/basic_ag/brgUntrusted.ml new file mode 100644 index 000000000..96be16217 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/brgUntrusted.ml @@ -0,0 +1,31 @@ +(* + ||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 T = BrgType + +(* Interface functions ******************************************************) + +(* to share *) +let type_check f g = function + | None -> f None None + | Some (a, uri, B.Abst t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in + T.type_of f g B.empty_context t + | Some (a, uri, B.Abbr t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in + T.type_of f g B.empty_context t + | Some (a, uri, B.Void) -> + let f obj = f None (Some obj) in + E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_ag/brgUntrusted.mli b/helm/software/lambda-delta/basic_ag/brgUntrusted.mli new file mode 100644 index 000000000..92e401e7d --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/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 option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make deleted file mode 100644 index eb1c64a66..000000000 --- a/helm/software/lambda-delta/basic_rg/Make +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 73da25b2d..000000000 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ /dev/null @@ -1,71 +0,0 @@ -(* - ||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_______________________________________________________________ *) - -type uri = NUri.uri -type id = Aut.id - -type bind = Void (* exclusion *) - | Abst of term (* abstraction *) - | Abbr of term (* abbreviation *) - -and term = Sort of int (* hierarchy index *) - | LRef of int (* reverse de Bruijn index *) - | GRef of uri (* reference *) - | Cast of term * term (* type, term *) - | Appl of term * term (* argument, function *) - | Bind of id * bind * term (* name, binder, scope *) - -type obj = int * uri * bind (* age, uri, binder, contents *) - -type item = obj option - -type context = int * (id * bind) list - -type message = (context, term) Log.item list - -(* Currified constructors ***************************************************) - -let abst w = Abst w - -let abbr v = Abbr v - -let cast u t = Cast (u, t) - -let appl u t = Appl (u, t) - -let bind id b t = Bind (id, b, t) - -let bind_abst id u t = Bind (id, Abst u, t) - -let bind_abbr id v t = Bind (id, Abbr v, t) - -(* context handling functions ***********************************************) - -let empty_context = 0, [] - -let push f (l, es) id b = - let c = succ l, (id, b) :: es in - f c - -let append f (l1, es1) (l2, es2) = - f (l2 + l1, List.append es2 es1) - -let map f map (l, es) = - let f es = f (l, es) in - Cps.list_map f map es - -let contents f (l, es) = f l es - -let get f (l, es) i = - if i < 0 || i >= l then f None else - let result = List.nth es (l - succ i) in - f (Some result) - diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml deleted file mode 100644 index fb4243c74..000000000 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ /dev/null @@ -1,35 +0,0 @@ -(* - ||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 U = NUri -module L = Log -module H = U.UriHash -module B = Brg - -exception ObjectNotFound of B.message - -let hsize = 7000 -let env = H.create hsize -let entry = ref 0 - -(* Internal functions *******************************************************) - -let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) - -(* Interface functions ******************************************************) - -let set_obj f obj = - let _, uri, b = obj in - let obj = !entry, uri, b in - incr entry; H.add env uri obj; f obj - -let get_obj f uri = - try f (H.find env uri) with Not_found -> error uri diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli deleted file mode 100644 index 8f9f8b1b0..000000000 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* - ||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 ObjectNotFound of Brg.message - -val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a - -val get_obj: (Brg.obj -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml deleted file mode 100644 index 66c7ed3d8..000000000 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ /dev/null @@ -1,150 +0,0 @@ -(* - ||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 P = Printf -module F = Format -module U = NUri -module C = Cps -module L = Log -module H = Hierarchy -module B = Brg - -type counters = { - eabsts: int; - eabbrs: int; - tsorts: int; - tlrefs: int; - tgrefs: int; - tcasts: int; - tappls: int; - tabsts: int; - tabbrs: int -} - -let indexes = ref false - -let initial_counters = { - eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; - tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 -} - -let rec count_term_binder f c = function - | B.Abst w -> - let c = {c with tabsts = succ c.tabsts} in - count_term f c w - | B.Abbr v -> - let c = {c with tabbrs = succ c.tabbrs} in - count_term f c v - | B.Void -> f c - -and count_term f c = function - | B.Sort _ -> - f {c with tsorts = succ c.tsorts} - | B.LRef _ -> - f {c with tlrefs = succ c.tlrefs} - | B.GRef _ -> - f {c with tgrefs = succ c.tgrefs} - | B.Cast (v, t) -> - let c = {c with tcasts = succ c.tcasts} in - let f c = count_term f c t in - count_term f c v - | B.Appl (v, t) -> - let c = {c with tappls = succ c.tappls} in - let f c = count_term f c t in - count_term f c v - | B.Bind (_, b, t) -> - let f c = count_term_binder f c b in - count_term f c t - -let count_obj_binder f c = function - | B.Abst w -> - let c = {c with eabsts = succ c.eabsts} in - count_term f c w - | B.Abbr v -> - let c = {c with eabbrs = succ c.eabbrs} in - count_term f c v - | B.Void -> f c - -let count_obj f c (_, _, b) = - count_obj_binder f c b - -let count_item f c = function - | Some obj -> count_obj f c obj - | None -> f c - -let print_counters f c = - let terms = - c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + - c.tabbrs - in - let items = c.eabsts + c.eabbrs in - L.warn (P.sprintf " Kernel representation summary (basic_rg)"); - L.warn (P.sprintf " Total entry items: %6u" items); - L.warn (P.sprintf " Declaration items: %6u" c.eabsts); - L.warn (P.sprintf " Definition items: %6u" c.eabbrs); - L.warn (P.sprintf " Total term items: %6u" terms); - L.warn (P.sprintf " Sort items: %6u" c.tsorts); - L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts); - L.warn (P.sprintf " Application items: %6u" c.tappls); - L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs); - f () - -let rec pp_term c frm = function - | B.Sort h -> - let f = function - | Some s -> F.fprintf frm "@[%s@]" s - | None -> F.fprintf frm "@[*%u@]" h - in - H.get_sort f h - | B.LRef i -> - let f = function - | Some (id, _) -> F.fprintf frm "@[%s@]" id - | None -> F.fprintf frm "@[#%u@]" i - in - if !indexes then f None else B.get f c i - | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) - | B.Cast (u, t) -> - F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t - | B.Appl (v, t) -> - F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t - | B.Bind (id, B.Abst w, t) -> - let f cc = - F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term cc) t - in - B.push f c id (B.Abst w) - | B.Bind (id, B.Abbr v, t) -> - let f cc = - F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term cc) t - in - B.push f c id (B.Abbr v) - | B.Bind (id, B.Void, t) -> - let f cc = F.fprintf frm "@[[%s].%a@]" id (pp_term cc) t in - B.push f c id B.Void - -let pp_context frm c = - let pp_entry frm = function - | id, B.Abst w -> - F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w - | id, B.Abbr v -> - F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v - | id, B.Void -> - F.fprintf frm "@,%s" id - in - let iter map frm l = List.iter (map frm) l in - let f _ es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in - B.contents f c - -let specs = { - L.pp_term = pp_term; L.pp_context = pp_context -} diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli deleted file mode 100644 index 566dfe8f3..000000000 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ /dev/null @@ -1,22 +0,0 @@ -(* - ||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_______________________________________________________________ *) - -type counters - -val initial_counters: counters - -val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a - -val print_counters: (unit -> 'a) -> counters -> 'a - -val specs: (Brg.context, Brg.term) Log.specs - -val indexes: bool ref diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml deleted file mode 100644 index 4cfd5260d..000000000 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ /dev/null @@ -1,203 +0,0 @@ -(* - ||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 C = Cps -module S = Share -module L = Log -module B = Brg -module O = BrgOutput -module E = BrgEnvironment - -exception LRefNotFound of B.message - -type machine = { - c: B.context; - s: B.term list -} - -type whd_result = - | Sort_ of int - | LRef_ of int * B.term option - | GRef_ of int * B.bind - | Bind_ of B.id * B.term * B.term - -type ho_whd_result = - | Sort of int - | Abst of B.term - -(* Internal functions *******************************************************) - -let level = 5 - -let error i = raise (LRefNotFound (L.items1 (string_of_int i))) - -let empty_machine = {c = B.empty_context; s = []} - -let get f c m i = - let f = function - | Some (_, b) -> f b - | None -> error i - in - let f gl _ = if i < gl then B.get f c i else B.get f m.c (i - gl) in - B.contents f c - -let contents f c m = - let f gl ges = B.contents (f gl ges) m.c in - B.contents f c - -let unwind_to_context f c m = B.append f c m.c - -let unwind_to_term f m t = - let map f t (id, b) = f (B.Bind (id, b, t)) in - let f _ mc = C.list_fold_left f map t mc in - B.contents f m.c - -let rec lref_map_bind f map b = match b with - | B.Abbr v -> - let f v' = f (S.sh1 v v' b B.abbr) in - lref_map f map v - | B.Abst w -> - let f w' = f (S.sh1 w w' b B.abst) in - lref_map f map w - | B.Void -> f b - -and 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, u) -> - let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in - let f b' = lref_map (f b') map u in - lref_map_bind f map b - -(* to share *) -let lift f c m = - let f gl _ = - let map i = if i >= gl then succ i else i in - let map f = function - | id, B.Abbr t -> let f t = f (id, B.Abbr t) in lref_map f map t - | _ -> assert false - in - let f mc = f {m with c = mc} in - B.map f map m.c - in - B.contents f c - -(* to share *) -let xchg f c m t = - let f gl _ ll _ = - 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 map t - in - contents f c m - -let push f c m id w t = - assert (m.s = []); - let f c m = xchg (f c m) c m t in - let f c = lift (f c) c m in - let f w = B.push f c id (B.Abst w) in - unwind_to_term f m w - -(* to share *) -let rec whd f c m x = match x with - | B.Sort h -> f m (Sort_ h) - | B.GRef uri -> - let f (i, _, b) = f m (GRef_ (i, b)) in - E.get_obj f uri - | B.LRef i -> - let f = function - | B.Void -> f m (LRef_ (i, None)) - | B.Abst t -> f m (LRef_ (i, Some t)) - | B.Abbr t -> whd f c m t - in - get f c m i - | B.Cast (_, t) -> whd f c m t - | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t - | B.Bind (id, B.Abst w, t) -> - begin match m.s with - | [] -> f m (Bind_ (id, w, t)) - | v :: tl -> - let f mc = whd f c {c = mc; s = tl} t in - B.push f m.c id (B.Abbr (B.Cast (w, v))) - end - | B.Bind (id, b, t) -> - let f mc = whd f c {m with c = mc} t in - B.push f m.c id b - -(* Interface functions ******************************************************) - -let rec ho_whd f c m x = - let aux m = function - | Sort_ h -> f c (Sort h) - | Bind_ (_, w, _) -> - let f c = f c (Abst w) in unwind_to_context f c m - | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, B.Abst u) -> ho_whd f c m u - | GRef_ (_, B.Abbr t) -> ho_whd f c m t - | LRef_ (_, None) -> assert false - | GRef_ (_, B.Void) -> assert false - in - whd aux c m x - -let ho_whd f c t = - L.log O.specs level (L.ct_items1 "Now scanning" c t); - ho_whd f c empty_machine t - -let rec are_convertible f c1 m1 t1 c2 m2 t2 = - let rec aux m1 r1 m2 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 m1 c2 m2 else f false - | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) -> - if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else f false - | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) -> - if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else - if a1 < a2 then whd (aux m1 r1) c2 m2 v2 else - whd (aux_rev m2 r2) c1 m1 v1 - | _, GRef_ (_, B.Abbr v2) -> - whd (aux m1 r1) c2 m2 v2 - | GRef_ (_, B.Abbr v1), _ -> - whd (aux_rev m2 r2) c1 m1 v1 - | Bind_ (id1, w1, t1), Bind_ (id2, w2, t2) -> - let f b = - if b then - let f c1 m1 t1 = - push (are_convertible f c1 m1 t1) c2 m2 id2 w2 t2 - in - push f c1 m1 id1 w1 t1 - else f false - in - are_convertible f c1 m1 w1 c2 m2 w2 - | _ -> f false - and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in - let f m1 r1 = whd (aux m1 r1) c2 m2 t2 in - whd f c1 m1 t1 - -and are_convertible_stacks f c1 m1 c2 m2 = - let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in - let map f v1 v2 = are_convertible f c1 mm1 v1 c2 mm2 v2 in - if List.length m1.s <> List.length m2.s then f false else - C.forall2 f map m1.s m2.s - -let are_convertible f c t1 t2 = - L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2); - are_convertible f c empty_machine t1 c empty_machine t2 diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli deleted file mode 100644 index 91a0289bb..000000000 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ /dev/null @@ -1,23 +0,0 @@ -(* - ||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 LRefNotFound of Brg.message - -type ho_whd_result = - | Sort of int - | Abst of Brg.term - -val ho_whd: - (Brg.context -> ho_whd_result -> 'a) -> Brg.context -> Brg.term -> 'a - -val are_convertible: - (bool -> 'a) -> Brg.context -> Brg.term -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml deleted file mode 100644 index fb7862c24..000000000 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ /dev/null @@ -1,119 +0,0 @@ -(* - ||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 U = NUri -module S = Share -module L = Log -module H = Hierarchy -module I = AutItem -module B = Brg -module O = BrgOutput -module E = BrgEnvironment -module R = BrgReduction - -exception TypeError of B.message - -(* Internal functions *******************************************************) - -let level = 4 - -let error1 s c t = - raise (TypeError (L.ct_items1 s c t)) - -let error2 s1 c1 t1 s2 c2 t2 = - raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) - -let mk_gref u l = - let map t v = B.Appl (v, t) in - List.fold_left map (B.GRef u) l - -(* Interface functions ******************************************************) - -let rec b_type_of f g c x = - L.log O.specs level (L.ct_items1 "Now checking" c x); - match x with - | B.Sort h -> - let f h = f x (B.Sort h) in H.apply f g h - | B.LRef i -> - let f = function - | Some (_, B.Abst w) -> f x w - | Some (_, B.Abbr (B.Cast (w, v))) -> f x w - | Some (_, B.Abbr _) -> assert false - | Some (_, B.Void) -> - error1 "reference to excluded variable" c x - | None -> - error1 "variable not found" c x - in - B.get f c i - | B.GRef uri -> - let f = function - | _, _, B.Abst w -> f x w - | _, _, B.Abbr (B.Cast (w, v)) -> f x w - | _, _, B.Abbr _ -> assert false - | _, _, B.Void -> - error1 "reference to excluded object" c x - in - E.get_obj f uri - | B.Bind (id, B.Abbr v, t) -> - let f xv xt tt = - f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv tt) - in - let f xv cc = b_type_of (f xv) g cc t in - let f xv = B.push (f xv) c id (B.Abbr xv) in - let f xv vv = match xv with - | B.Cast _ -> f xv - | _ -> f (B.Cast (vv, xv)) - in - type_of f g c v - | B.Bind (id, B.Abst u, t) -> - let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu tt) - in - let f xu cc = b_type_of (f xu) g cc t in - let f xu _ = B.push (f xu) c id (B.Abst xu) in - type_of f g c u - | B.Bind (id, B.Void, t) -> - let f xt tt = - f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void tt) - in - let f cc = b_type_of f g cc t in - B.push f c id B.Void - | B.Appl (v, t) -> - let h xv vv xt tt cc = function - | R.Sort _ -> error1 "not a function" c xt - | R.Abst w -> - L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); - let f b = - if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else - error2 "the term" cc xv "must be of type" cc w - in - R.are_convertible f cc w vv - in - let f xv vv xt = function -(* inserting a missing "modus ponens" *) - | B.Appl (y2, B.Appl (y1, B.GRef u)) when U.eq u I.imp -> - b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt]) - | tt -> R.ho_whd (h xv vv xt tt) c tt - in - let f xv vv = b_type_of (f xv vv) g c t in - type_of f g c v - | B.Cast (u, t) -> - let f xu xt b = - if b then f (S.sh2 u xu t xt x B.cast) xu else - error2 "the term" c xt "must be of type" c xu - in - let f xu xt tt = R.are_convertible (f xu xt) c xu tt in - let f xu _ = b_type_of (f xu) g c t in - type_of f g c u - -and type_of f g c x = - let f t u = L.unbox (); f t u in - L.box (); b_type_of f g c x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli deleted file mode 100644 index e7e2d7ed7..000000000 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* - ||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 Brg.message - -val type_of: - (Brg.term -> Brg.term -> 'a) -> - Hierarchy.graph -> Brg.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml deleted file mode 100644 index 96be16217..000000000 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ /dev/null @@ -1,31 +0,0 @@ -(* - ||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 T = BrgType - -(* Interface functions ******************************************************) - -(* to share *) -let type_check f g = function - | None -> f None None - | Some (a, uri, B.Abst t) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in - T.type_of f g B.empty_context t - | Some (a, uri, B.Abbr t) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in - T.type_of f g B.empty_context t - | Some (a, uri, B.Void) -> - let f obj = f None (Some obj) in - E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli deleted file mode 100644 index 92e401e7d..000000000 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* - ||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 option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a