From: Ferruccio Guidi Date: Sun, 14 Dec 2008 19:34:19 +0000 (+0000) Subject: new kernel basic_ag (with absolute local references) X-Git-Tag: make_still_working~4399 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=338e3e5c639fbcfeeb347a0121cacc6c0f1fc42a;p=helm.git new kernel basic_ag (with absolute local references) --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index ae6e441cc..88f23f93e 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -18,39 +18,44 @@ automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx automath/autItem.cmo: lib/nUri.cmi automath/autItem.cmx: lib/nUri.cmx -basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx -basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx -basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx -basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \ - lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \ - lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx -basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \ - basic_rg/brgEnvironment.cmi -basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \ - basic_rg/brgEnvironment.cmi -basic_rg/brgReduction.cmi: basic_rg/brg.cmx -basic_rg/brgReduction.cmo: lib/share.cmx lib/log.cmi lib/cps.cmx \ - basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ - basic_rg/brgReduction.cmi -basic_rg/brgReduction.cmx: lib/share.cmx lib/log.cmx lib/cps.cmx \ - basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ - basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx -basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ - basic_rg/brgEnvironment.cmi basic_rg/brg.cmx automath/autItem.cmx \ - basic_rg/brgType.cmi -basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ - basic_rg/brgEnvironment.cmx basic_rg/brg.cmx automath/autItem.cmx \ - basic_rg/brgType.cmi -basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx -basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \ - basic_rg/brg.cmx basic_rg/brgUntrusted.cmi -basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgEnvironment.cmx \ - basic_rg/brg.cmx basic_rg/brgUntrusted.cmi +basic_ag/bag.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx +basic_ag/bag.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx +basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx +basic_ag/bagOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \ + lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \ + lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi +basic_ag/bagEnvironment.cmi: lib/nUri.cmi basic_ag/bag.cmx +basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \ + basic_ag/bagEnvironment.cmi +basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \ + basic_ag/bagEnvironment.cmi +basic_ag/bagSubstitution.cmi: basic_ag/bag.cmx +basic_ag/bagSubstitution.cmo: lib/share.cmx basic_ag/bag.cmx \ + basic_ag/bagSubstitution.cmi +basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \ + basic_ag/bagSubstitution.cmi +basic_ag/bagReduction.cmi: basic_ag/bag.cmx +basic_ag/bagReduction.cmo: lib/log.cmi lib/cps.cmx \ + basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \ + basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagReduction.cmi +basic_ag/bagReduction.cmx: lib/log.cmx lib/cps.cmx \ + basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ + basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi +basic_ag/bagType.cmi: lib/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ + lib/hierarchy.cmi basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi \ + basic_ag/bagEnvironment.cmi basic_ag/bag.cmx automath/autItem.cmx \ + basic_ag/bagType.cmi +basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ + lib/hierarchy.cmx basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx \ + basic_ag/bagEnvironment.cmx basic_ag/bag.cmx automath/autItem.cmx \ + basic_ag/bagType.cmi +basic_ag/bagUntrusted.cmi: lib/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagUntrusted.cmo: basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi \ + basic_ag/bag.cmx basic_ag/bagUntrusted.cmi +basic_ag/bagUntrusted.cmx: basic_ag/bagType.cmx basic_ag/bagEnvironment.cmx \ + basic_ag/bag.cmx basic_ag/bagUntrusted.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 @@ -63,18 +68,18 @@ toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi -toplevel/metaBrg.cmi: toplevel/meta.cmx basic_rg/brg.cmx -toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ - toplevel/metaBrg.cmi -toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ - toplevel/metaBrg.cmi +toplevel/metaBag.cmi: toplevel/meta.cmx basic_ag/bag.cmx +toplevel/metaBag.cmo: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \ + toplevel/metaBag.cmi +toplevel/metaBag.cmx: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \ + toplevel/metaBag.cmi toplevel/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \ - toplevel/metaBrg.cmi toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi \ - lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi \ - basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \ + toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi \ + lib/cps.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \ + basic_ag/bagOutput.cmi automath/autParser.cmi automath/autOutput.cmi \ automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.cmx \ - toplevel/metaBrg.cmx toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx \ - lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx \ - basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \ + toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx \ + lib/cps.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \ + basic_ag/bagOutput.cmx automath/autParser.cmx automath/autOutput.cmx \ automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make new file mode 100644 index 000000000..5c7f64d02 --- /dev/null +++ b/helm/software/lambda-delta/Make @@ -0,0 +1 @@ +lib automath basic_ag toplevel diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 2be69cba3..3b212fa94 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -1,7 +1,5 @@ MAIN = helena -DIRECTORIES = lib automath basic_rg toplevel - REQUIRES = unix KEEP = README automath/*.aut diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index e4489040d..cf15ef85d 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -1,5 +1,7 @@ H=@ +DIRECTORIES = $(shell cat Make) + INCLUDES = $(DIRECTORIES:%=-I %) OCAMLDEP = ocamlfind ocamldep -native $(INCLUDES) diff --git a/helm/software/lambda-delta/basic_ag/Make b/helm/software/lambda-delta/basic_ag/Make index eb1c64a66..1d2286b52 100644 --- a/helm/software/lambda-delta/basic_ag/Make +++ b/helm/software/lambda-delta/basic_ag/Make @@ -1 +1,2 @@ -brg brgOutput brgEnvironment brgReduction brgType brgUntrusted +bag bagOutput +bagEnvironment bagSubstitution bagReduction bagType bagUntrusted diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml new file mode 100644 index 000000000..d0c193a2a --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -0,0 +1,78 @@ +(* + ||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 (* location *) + | GRef of uri (* reference *) + | Cast of term * term (* type, term *) + | Appl of term * term (* argument, function *) + | Bind of int * id * bind * term (* location, name, binder, scope *) + +type obj = int * uri * bind (* age, uri, binder, contents *) + +type item = obj option + +type context = (int * id * bind) list (* location, name, binder *) + +type message = (context, term) Log.item list + +(* Currified constructors ***************************************************) + +let abst w = Abst w + +let abbr v = Abbr v + +let lref i = LRef i + +let cast u t = Cast (u, t) + +let appl u t = Appl (u, t) + +let bind l id b t = Bind (l, id, b, t) + +let bind_abst l id u t = Bind (l, id, Abst u, t) + +let bind_abbr l id v t = Bind (l, id, Abbr v, t) + +(* location handling functions **********************************************) + +let location = ref 0 + +let new_location () = let loc = !location in incr location; loc + +(* context handling functions ***********************************************) + +let empty_context = [] + +let push f es l id b = + let c = (l, id, b) :: es in f c + +let append f es1 es2 = + f (List.append es2 es1) + +let map f map es = + Cps.list_map f map es + +let contents f es = f es + +let get f es i = + let rec aux = function + | [] -> f None + | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl + in + aux es diff --git a/helm/software/lambda-delta/basic_ag/bagEnvironment.ml b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml new file mode 100644 index 000000000..5e6c9f1a0 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.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 = Bag + +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/bagEnvironment.mli b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli new file mode 100644 index 000000000..6dc2330c1 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.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 Bag.message + +val set_obj: (Bag.obj -> 'a) -> Bag.obj -> 'a + +val get_obj: (Bag.obj -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml new file mode 100644 index 000000000..589ce60f0 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -0,0 +1,153 @@ +(* + ||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 = Bag + +type counters = { + eabsts: int; + eabbrs: int; + tsorts: int; + tlrefs: int; + tgrefs: int; + tcasts: int; + tappls: int; + tabsts: int; + tabbrs: int +} + +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_ag)"); + 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 indexes = ref false + +let res l id = + if !indexes then P.sprintf "#%u" l else id + +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 (l, id, B.Abst w, t) -> + let f cc = + F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t + in + B.push f c l id (B.Abst w) + | B.Bind (l, id, B.Abbr v, t) -> + let f cc = + F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t + in + B.push f c l id (B.Abbr v) + | B.Bind (l, id, B.Void, t) -> + let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in + B.push f c l id B.Void + +let pp_context frm c = + let pp_entry frm = function + | l, id, B.Abst w -> + F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w + | l, id, B.Abbr v -> + F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v + | l, id, B.Void -> + F.fprintf frm "@,%s" (res l 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/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli new file mode 100644 index 000000000..fe4d9f344 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagOutput.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 -> Bag.item -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a + +val specs: (Bag.context, Bag.term) Log.specs + +val indexes: bool ref diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml new file mode 100644 index 000000000..0310e8d28 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -0,0 +1,154 @@ +(* + ||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 L = Log +module B = Bag +module O = BagOutput +module E = BagEnvironment +module S = BagSubstitution + +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 int * 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 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 (l, id, b) = f (B.Bind (l, id, b, t)) in + let f mc = C.list_fold_left f map t mc in + B.contents f m.c + +let get f c m i = + let f = function + | Some (_, b) -> f b + | None -> error i + in + let f c = B.get f c i in + unwind_to_context f c m + +let push f c m l id w = + assert (m.s = []); + let f w = B.push f c l 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 (l, id, B.Abst w, t) -> + begin match m.s with + | [] -> f m (Bind_ (l, id, w, t)) + | v :: tl -> + let f mc = whd f c {c = mc; s = tl} t in + B.push f m.c l id (B.Abbr (B.Cast (w, v))) + end + | B.Bind (l, id, b, t) -> + let f mc = whd f c {m with c = mc} t in + B.push f m.c l 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 = + let f c r = L.unbox (); f c r in + L.box (); L.log O.specs level (L.ct_items1 "Now scanning" c t); + ho_whd f c empty_machine t + +let rec are_convertible f c m1 t1 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 c m1 m2 else f false + | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) -> + if a1 = a2 then are_convertible_stacks f c m1 m2 else f false + | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) -> + if a1 = a2 then are_convertible_stacks f c m1 m2 else + if a1 < a2 then whd (aux m1 r1) c m2 v2 else + whd (aux_rev m2 r2) c m1 v1 + | _, GRef_ (_, B.Abbr v2) -> + whd (aux m1 r1) c m2 v2 + | GRef_ (_, B.Abbr v1), _ -> + whd (aux_rev m2 r2) c m1 v1 + | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) -> + let f b = + if b then + let f c = + S.subst (are_convertible f c m1 t1 m2) l1 l2 t2 + in + push f c m1 l1 id1 w1 + else f false + in + are_convertible f c m1 w1 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) c m2 t2 in + whd f c m1 t1 + +and are_convertible_stacks f c m1 m2 = + let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in + let map f v1 v2 = are_convertible f c mm1 v1 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 = + let f b = L.unbox (); f b in + L.box (); + L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2); + are_convertible f c empty_machine t1 empty_machine t2 diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli new file mode 100644 index 000000000..2b5f02e71 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagReduction.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 Bag.message + +type ho_whd_result = + | Sort of int + | Abst of Bag.term + +val ho_whd: + (Bag.context -> ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a + +val are_convertible: + (bool -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml new file mode 100644 index 000000000..25725520d --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml @@ -0,0 +1,48 @@ +(* + ||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 S = Share +module B = Bag + +(* Internal functions *******************************************************) + +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 -> + let ii = map i in f (S.sh1 i ii t B.lref) + | 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 (l, id, b, u) -> + let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in + let f b' = lref_map (f b') map u in + lref_map_bind f map b + +(* Interface functions ******************************************************) + +let subst f new_l old_l t = + let map i = if i = old_l then new_l else i in + lref_map f map t diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.mli b/helm/software/lambda-delta/basic_ag/bagSubstitution.mli new file mode 100644 index 000000000..b48c056df --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.mli @@ -0,0 +1,12 @@ +(* + ||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 subst: (Bag.term -> 'a) -> int -> int -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml new file mode 100644 index 000000000..a651c6e33 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -0,0 +1,121 @@ +(* + ||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 = Bag +module O = BagOutput +module E = BagEnvironment +module R = BagReduction + +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 (l, id, B.Abbr v, t) -> + let f xv xt tt = + f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l 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 l 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 (l, id, B.Abst u, t) -> + let f xu xt tt = + f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l 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 l id (B.Abst xu) in + type_of f g c u + | B.Bind (l, id, B.Void, t) -> + let f xt tt = + f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) + in + let f cc = b_type_of f g cc t in + B.push f c l 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.box (); + L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w); + L.unbox (); + 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/bagType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli new file mode 100644 index 000000000..24d1f57a2 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagType.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 Bag.message + +val type_of: + (Bag.term -> Bag.term -> 'a) -> + Hierarchy.graph -> Bag.context -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml new file mode 100644 index 000000000..e80a06125 --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.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 = Bag +module E = BagEnvironment +module T = BagType + +(* 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/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli new file mode 100644 index 000000000..54ae7717c --- /dev/null +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.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: + (Bag.term option -> Bag.item -> 'a) -> Hierarchy.graph -> Bag.item -> 'a diff --git a/helm/software/lambda-delta/basic_ag/brg.ml b/helm/software/lambda-delta/basic_ag/brg.ml deleted file mode 100644 index 73da25b2d..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgEnvironment.ml b/helm/software/lambda-delta/basic_ag/brgEnvironment.ml deleted file mode 100644 index fb4243c74..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgEnvironment.mli b/helm/software/lambda-delta/basic_ag/brgEnvironment.mli deleted file mode 100644 index 8f9f8b1b0..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgOutput.ml b/helm/software/lambda-delta/basic_ag/brgOutput.ml deleted file mode 100644 index 66c7ed3d8..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgOutput.mli b/helm/software/lambda-delta/basic_ag/brgOutput.mli deleted file mode 100644 index 566dfe8f3..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgReduction.ml b/helm/software/lambda-delta/basic_ag/brgReduction.ml deleted file mode 100644 index 4cfd5260d..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgReduction.mli b/helm/software/lambda-delta/basic_ag/brgReduction.mli deleted file mode 100644 index 91a0289bb..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgType.ml b/helm/software/lambda-delta/basic_ag/brgType.ml deleted file mode 100644 index fb7862c24..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgType.mli b/helm/software/lambda-delta/basic_ag/brgType.mli deleted file mode 100644 index e7e2d7ed7..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgUntrusted.ml b/helm/software/lambda-delta/basic_ag/brgUntrusted.ml deleted file mode 100644 index 96be16217..000000000 --- a/helm/software/lambda-delta/basic_ag/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_ag/brgUntrusted.mli b/helm/software/lambda-delta/basic_ag/brgUntrusted.mli deleted file mode 100644 index 92e401e7d..000000000 --- a/helm/software/lambda-delta/basic_ag/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 diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index 2e8b2c715..9fc5dc9b2 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -46,6 +46,10 @@ let list_rev_map = let list_rev = list_rev_append ~tail:[] +let list_fold_right f map l a = + let map f a m = map f m a in + list_rev (list_fold_left f map a) l + let list_map f = list_rev_map (list_rev f) diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index 7b8610821..b185d6004 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaAut metaBrg top +meta metaOutput metaAut metaBag top diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml new file mode 100644 index 000000000..cf2c009f4 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBag.ml @@ -0,0 +1,72 @@ +(* + ||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 B = Bag +module M = Meta + +(* Internal functions *******************************************************) + +let rec xlate_term c f = function + | M.Sort s -> + let f h = f (B.Sort h) in + if s then f 0 else f 1 + | M.LRef (_, i) -> + let l, _, _ = List.nth c i in + f (B.LRef l) + | M.GRef (_, uri, vs) -> + let map f t v = f (B.appl v t) in + let f vs = C.list_fold_left f map (B.GRef uri) vs in + C.list_map f (xlate_term c) vs + | M.Appl (v, t) -> + let f v t = f (B.Appl (v, t)) in + let f v = xlate_term c (f v) t in + xlate_term c f v + | M.Abst (id, w, t) -> + let f w = + let l = B.new_location () in + let f t = f (B.Bind (l, id, B.Abst w, t)) in + let f c = xlate_term c f t in + B.push f c l id (B.Abst w) + in + xlate_term c f w + +let xlate_pars f pars = + let map f (id, w) c = + let l = B.new_location () in + let f w = B.push f c l id (B.Abst w) in + xlate_term c f w + in + C.list_fold_right f map pars B.empty_context + +let unwind_to_xlate_term f c t = + let map f t (l, id, b) = f (B.bind l id b t) in + let f t = C.list_fold_left f map t c in + xlate_term c f t + +let xlate_entry f = function + | e, pars, uri, u, None -> + let f u = f (e, uri, B.Abst u) in + let f c = unwind_to_xlate_term f c u in + xlate_pars f pars + | e, pars, uri, u, Some (_, t) -> + let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in + let f c u = unwind_to_xlate_term (f u) c t in + let f c = unwind_to_xlate_term (f c) c u in + xlate_pars f pars + +let xlate_item f = function + | None -> f None + | Some e -> let f e = f (Some e) in xlate_entry f e + +(* Interface functions ******************************************************) + +let bag_of_meta = xlate_item diff --git a/helm/software/lambda-delta/toplevel/metaBag.mli b/helm/software/lambda-delta/toplevel/metaBag.mli new file mode 100644 index 000000000..87e341692 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBag.mli @@ -0,0 +1,12 @@ +(* + ||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 bag_of_meta: (Bag.item -> 'a) -> Meta.item -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml deleted file mode 100644 index dfc7e8b56..000000000 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ /dev/null @@ -1,65 +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 B = Brg -module M = Meta - -(* Internal functions *******************************************************) - -let map_fold_left f map1 map2 a l = - let f a = C.list_fold_left f map2 a l in - map1 f a - -let map_args f t v = f (B.Appl (v, t)) - -let map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t)) - -let rec xlate_term f = function - | M.Sort s -> - let f h = f (B.Sort h) in - if s then f 0 else f 1 - | M.LRef (l, i) -> - f (B.LRef (l - succ i)) - | M.GRef (_, uri, vs) -> - let f vs = map_fold_left f C.id map_args (B.GRef uri) vs in - C.list_map f xlate_term vs - | M.Appl (v, t) -> - let f v t = f (B.Appl (v, t)) in - let f v = xlate_term (f v) t in - xlate_term f v - | M.Abst (id, w, t) -> - let f w t = f (B.Bind (id, B.Abst w, t)) in - let f w = xlate_term (f w) t in - xlate_term f w - -let xlate_pars f (id, w) = - let f w = f (id, w) in - xlate_term f w - -let xlate_entry f = function - | e, pars, uri, u, None -> - let f u = f (e, uri, B.Abst u) in - let f pars = map_fold_left f xlate_term map_pars u pars in - C.list_map f xlate_pars pars - | e, pars, uri, u, Some (_, t) -> - let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in - let f pars u = map_fold_left (f u) xlate_term map_pars t pars in - let f pars = map_fold_left (f pars) xlate_term map_pars u pars in - C.list_map f xlate_pars pars - -let xlate_item f = function - | None -> f None - | Some e -> let f e = f (Some e) in xlate_entry f e - -(* Interface functions ******************************************************) - -let brg_of_meta = xlate_item diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli deleted file mode 100644 index cb47bc9c1..000000000 --- a/helm/software/lambda-delta/toplevel/metaBrg.mli +++ /dev/null @@ -1,12 +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 brg_of_meta: (Brg.item -> 'a) -> Meta.item -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 06df1ab03..1286db0bb 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -17,22 +17,22 @@ module H = Hierarchy module AO = AutOutput module MA = MetaAut module MO = MetaOutput -module MBrg = MetaBrg -module BrgO = BrgOutput -module BrgU = BrgUntrusted +module MBag = MetaBag +module BagO = BagOutput +module BagU = BagUntrusted type status = { mst : MA.status; ac : AO.counters; mc : MO.counters; - brgc: BrgO.counters + bagc: BagO.counters } let initial_status = { - ac = AO.initial_counters; - mc = MO.initial_counters; - brgc= BrgO.initial_counters; - mst = MA.initial_status + ac = AO.initial_counters; + mc = MO.initial_counters; + bagc = BagO.initial_counters; + mst = MA.initial_status } let count count_fun c item = @@ -40,8 +40,8 @@ let count count_fun c item = let flush () = L.flush (); L.flush_err () -let brg_error s msg = - L.error BrgO.specs (L.Warn s :: msg); flush () +let bag_error s msg = + L.error BagO.specs (L.Warn s :: msg); flush () let main = try @@ -90,8 +90,8 @@ try in (* stage 2 *) let f st item = - let st = {st with brgc = count BrgO.count_item st.brgc item} in - if !stage > 2 then BrgU.type_check (f st) !H.graph item else st + let st = {st with bagc = count BagO.count_item st.bagc item} in + if !stage > 2 then BagU.type_check (f st) !H.graph item else st in (* stage 1 *) let f mst item = @@ -102,7 +102,7 @@ try | None -> () | Some (_, frm) -> MO.pp_item C.start frm item end; - if !stage > 1 then MBrg.brg_of_meta (f st) item else st + if !stage > 1 then MBag.bag_of_meta (f st) item else st in (* stage 0 *) let st = {st with ac = count AO.count_item st.ac item} in @@ -115,7 +115,7 @@ try if !L.level > 0 then Time.utime_stamp "processed"; if !L.level > 2 then AO.print_counters C.start st.ac; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; - if !L.level > 2 && !stage > 1 then BrgO.print_counters C.start st.brgc; + if !L.level > 2 && !stage > 1 then BagO.print_counters C.start st.bagc; in let help = "Usage: helena [ -Vi | -Ss | -m | -h ] ...\n\n" ^ @@ -135,10 +135,10 @@ try ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set BrgO.indexes, help_i); + ("-i", Arg.Set BagO.indexes, help_i); ("-m", Arg.String set_meta_file, help_m); ("-s", Arg.Int set_stage, help_s); ] read_file help; if !L.level > 0 then Time.utime_stamp "at exit"; flush () -with BrgType.TypeError msg -> brg_error "Type Error" msg +with BagType.TypeError msg -> bag_error "Type Error" msg