From dcdee4ca839dac671924a95f0ada71faf06a8be4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 28 Jun 2009 17:59:13 +0000 Subject: [PATCH] new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes --- helm/software/lambda-delta/.depend.opt | 68 +++++- helm/software/lambda-delta/Make | 2 +- helm/software/lambda-delta/Makefile | 8 +- helm/software/lambda-delta/basic_ag/bag.ml | 3 + .../lambda-delta/basic_ag/bagReduction.ml | 1 - .../lambda-delta/basic_ag/bagReduction.mli | 1 - helm/software/lambda-delta/basic_rg/Make | 2 + helm/software/lambda-delta/basic_rg/brg.ml | 88 ++++++++ .../lambda-delta/basic_rg/brgEnvironment.ml | 35 +++ .../lambda-delta/basic_rg/brgEnvironment.mli | 16 ++ .../lambda-delta/basic_rg/brgOutput.ml | 184 ++++++++++++++++ .../lambda-delta/basic_rg/brgOutput.mli | 30 +++ .../lambda-delta/basic_rg/brgReduction.ml | 204 ++++++++++++++++++ .../lambda-delta/basic_rg/brgReduction.mli | 21 ++ .../lambda-delta/basic_rg/brgSubstitution.ml | 38 ++++ .../lambda-delta/basic_rg/brgSubstitution.mli | 14 ++ .../software/lambda-delta/basic_rg/brgType.ml | 125 +++++++++++ .../lambda-delta/basic_rg/brgType.mli | 18 ++ .../lambda-delta/basic_rg/brgUntrusted.ml | 32 +++ .../lambda-delta/basic_rg/brgUntrusted.mli | 13 ++ helm/software/lambda-delta/toplevel/Make | 2 +- .../software/lambda-delta/toplevel/metaBrg.ml | 71 ++++++ .../lambda-delta/toplevel/metaBrg.mli | 12 ++ helm/software/lambda-delta/toplevel/top.ml | 88 +++++++- 24 files changed, 1050 insertions(+), 26 deletions(-) create mode 100644 helm/software/lambda-delta/basic_rg/Make create mode 100644 helm/software/lambda-delta/basic_rg/brg.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgEnvironment.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgEnvironment.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgOutput.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgOutput.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgReduction.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgReduction.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgSubstitution.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgSubstitution.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgType.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgType.mli create mode 100644 helm/software/lambda-delta/basic_rg/brgUntrusted.ml create mode 100644 helm/software/lambda-delta/basic_rg/brgUntrusted.mli create mode 100644 helm/software/lambda-delta/toplevel/metaBrg.ml create mode 100644 helm/software/lambda-delta/toplevel/metaBrg.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index d2b1d720f..90909683b 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,11 +1,20 @@ +lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi +lib/cps.cmo: +lib/cps.cmx: +lib/share.cmo: +lib/share.cmx: +lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +lib/hierarchy.cmi: lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi +automath/aut.cmo: +automath/aut.cmx: automath/autOutput.cmi: automath/aut.cmx automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \ automath/autOutput.cmi @@ -16,6 +25,42 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.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/brgSubstitution.cmi: basic_rg/brg.cmx +basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi +basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi +basic_rg/brgReduction.cmi: basic_rg/brgOutput.cmi basic_rg/brg.cmx +basic_rg/brgReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ + basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ + basic_rg/brgSubstitution.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 lib/cps.cmx basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ + basic_rg/brgType.cmi +basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ + lib/hierarchy.cmx lib/cps.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ + basic_rg/brgType.cmi +basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx +basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi +basic_rg/brgUntrusted.cmx: lib/log.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 @@ -33,7 +78,7 @@ 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: lib/nUri.cmi basic_ag/bag.cmx +basic_ag/bagReduction.cmi: basic_ag/bag.cmx basic_ag/bagReduction.cmo: lib/nUri.cmi 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 @@ -71,13 +116,22 @@ 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/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/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.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/bagReduction.cmi basic_ag/bagOutput.cmi automath/autParser.cmi \ + toplevel/metaBrg.cmi toplevel/metaBag.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 basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagReduction.cmi \ + basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autParser.cmi \ automath/autOutput.cmi automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.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/bagReduction.cmx basic_ag/bagOutput.cmx automath/autParser.cmx \ + toplevel/metaBrg.cmx toplevel/metaBag.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 basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagReduction.cmx \ + basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autParser.cmx \ automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make index 5c7f64d02..af2aa18aa 100644 --- a/helm/software/lambda-delta/Make +++ b/helm/software/lambda-delta/Make @@ -1 +1 @@ -lib automath basic_ag toplevel +lib automath basic_rg basic_ag toplevel diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 30cdd2e51..4982986a3 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -16,9 +16,9 @@ test: $(MAIN).opt @echo " HELENA $(INPUT)" $(H)./$(MAIN).opt -S 3 $(O) $(INPUT) > log.txt -test-nsi: $(MAIN).opt - @echo " HELENA -n $(INPUT-ORIG)" - $(H)./$(MAIN).opt -n -S 3 $(O) $(INPUT-ORIG) > log.txt +test-si: $(MAIN).opt + @echo " HELENA -u $(INPUT-ORIG)" + $(H)./$(MAIN).opt -k bag -u -S 3 $(O) $(INPUT-ORIG) > log.txt meta: $(MAIN).opt @echo " HELENA -m meta.txt $(INPUT)" @@ -29,7 +29,7 @@ ifeq ($(MAKECMDGOALS), test) include .depend.opt endif -ifeq ($(MAKECMDGOALS), test-nsi) +ifeq ($(MAKECMDGOALS), test-si) include .depend.opt endif diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 624b47cbb..b04fc5ab6 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -9,6 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +(* kernel version: basic, absolute, global *) +(* note : experimental *) + type uri = NUri.uri type id = Aut.id diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index 518f7061b..fc1efcd77 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -33,7 +33,6 @@ type whd_result = type ho_whd_result = | Sort of int - | GRef of U.uri * B.term list | Abst of B.term (* Internal functions *******************************************************) diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index a07e65cb0..ead9d5118 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -14,7 +14,6 @@ exception LRefNotFound of Bag.message type ho_whd_result = | Sort of int - | GRef of NUri.uri * Bag.term list | Abst of Bag.term val ho_whd: diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make new file mode 100644 index 000000000..ee53ca212 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/Make @@ -0,0 +1,2 @@ +brg brgOutput +brgEnvironment brgSubstitution brgReduction brgType brgUntrusted diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml new file mode 100644 index 000000000..e42db3319 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -0,0 +1,88 @@ +(* + ||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_______________________________________________________________ *) + +(* kernel version: basic, relative, global *) +(* note : ufficial basic lambda-delta *) + +type uri = NUri.uri +type id = Aut.id + +type bind = Void (* exclusion *) + | Abst of term (* abstraction *) + | Abbr of term (* abbreviation *) + +and term = Sort of attrs * int (* attrs, hierarchy index *) + | LRef of attrs * int (* attrs, position index *) + | GRef of attrs * uri (* attrs, reference *) + | Cast of attrs * term * term (* attrs, type, term *) + | Appl of attrs * term * term (* attrs, argument, function *) + | Bind of attrs * bind * term (* attrs, binder, scope *) + +and attr = Name of bool * id (* real?, name *) + | Entry of int * bind (* age, binder *) + +and attrs = attr list + +type obj = int * uri * bind (* age, uri, binder, contents *) + +type item = obj option + +type context = (attrs * bind) list (* attrs, binder *) + +type message = (context, term) Log.item list + +(* Currified constructors ***************************************************) + +let abst w = Abst w + +let abbr v = Abbr v + +let lref a i = LRef (a, i) + +let cast a u t = Cast (a, u, t) + +let appl a u t = Appl (a, u, t) + +let bind a b t = Bind (a, b, t) + +let bind_abst a u t = Bind (a, Abst u, t) + +let bind_abbr a v t = Bind (a, Abbr v, t) + +(* context handling functions ***********************************************) + +let empty_context = [] + +let push f es a b = + let c = (a, 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 e i = function + | [] -> f e None + | hd :: tl -> + if i = 0 then f e (Some hd) else + let e = match hd with _, Abst _ -> succ e | _ -> e in + aux e (pred i) tl + in + aux 0 i es + +let rec name f = function + | [] -> f None + | Name (r, n) :: _ -> f (Some (r, n)) + | _ :: tl -> name f tl diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml new file mode 100644 index 000000000..902eeb45a --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/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 1 + +(* 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 new file mode 100644 index 000000000..8f9f8b1b0 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/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_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml new file mode 100644 index 000000000..b8fc2d0c2 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -0,0 +1,184 @@ +(* + ||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 + +(* nodes count **************************************************************) + +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_rg)"); + L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.tsorts); + L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn (P.sprintf " Application items: %7u" c.tappls); + L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); + f () + +(* reductions count *********************************************************) + +type reductions = { + beta : int; + upsilon: int; + tau : int; + ldelta : int; + gdelta : int +} + +let initial_reductions = { + beta = 0; upsilon = 0; tau = 0; ldelta = 0; gdelta = 0 +} + +let add ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) r = { + beta = r.beta + beta; + upsilon = r.upsilon + upsilon; + tau = r.tau + tau; + ldelta = r.ldelta + ldelta; + gdelta = r.gdelta + gdelta +} + +(* context/term pretty printing *********************************************) + +let indexes = ref false + +let id frm a = + let f = function + | None -> assert false + | Some (true, n) -> F.fprintf frm "%s" n + | Some (false, n) -> F.fprintf frm "^%s" n + in + B.name f a + +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 (a, _) -> F.fprintf frm "@[%a@]" id a + | None -> F.fprintf frm "@[#%u@]" i + in + if !indexes then f 0 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 (a, B.Abst w, t) -> + let f cc = + F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t + in + B.push f c a (B.Abst w) + | B.Bind (a, B.Abbr v, t) -> + let f cc = + F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t + in + B.push f c a (B.Abbr v) + | B.Bind (a, B.Void, t) -> + let f cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in + B.push f c a B.Void + +let pp_context frm c = + let pp_entry frm = function + | a, B.Abst w -> + F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w + | a, B.Abbr v -> + F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v + | a, B.Void -> + F.fprintf frm "@,%a" id a + 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 new file mode 100644 index 000000000..6e578d80a --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -0,0 +1,30 @@ +(* + ||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 + +type reductions + +val initial_reductions: reductions + +val add: + ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> + reductions -> reductions diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml new file mode 100644 index 000000000..8ad752bad --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -0,0 +1,204 @@ +(* + ||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 C = Cps +module L = Log +module B = Brg +module O = BrgOutput +module E = BrgEnvironment +module S = BrgSubstitution + +exception LRefNotFound of B.message + +type machine = { + c: B.context; + s: (B.term * int) list +} + +(* Internal functions *******************************************************) + +let reductions = ref O.initial_reductions + +let level = 5 + +let error i = raise (LRefNotFound (L.items1 (string_of_int i))) + +let log1 s c t = + let sc, st = s ^ " in the context", "the term" in + L.log O.specs level (L.ct_items1 sc c st t) + +let log2 s c u t = + let sc, su, st = s ^ " in the context", "the term", "and the term" in + L.log O.specs level (L.ct_items2 sc c su u st t) + +let empty_machine = { + c = B.empty_context; s = [] +} + +let get f c m i = + let f e = function + | Some (_, b) -> f e b + | None -> error i + in + let f c = B.get f c i in + B.append f c m.c + +let lift_stack f s = + let map f (v, i) = f (v, succ i) in + Cps.list_map f map s + +let unwind_to_term f m t = + let map f t (a, b) = f (B.Bind (a, b, t)) in + let f mc = C.list_fold_left f map t mc in + assert (m.s = []); + B.contents f m.c + +let push f m a b = + assert (m.s = []); + f {m with c = (a, b) :: m.c} + +(* to share *) +let rec step f ?(delta=false) ?(sty=false) c m x = +(* L.warn "entering R.step"; *) + match x with + | B.Sort _ -> f m x + | B.GRef (a, uri) -> + let f = function + | _, _, B.Abbr v when delta -> + reductions := O.add ~gdelta:1 !reductions; + step f ~delta ~sty c m v + | _, _, B.Abst w when sty -> + step f ~delta ~sty c m w + | e, _, b -> + f m (B.GRef (B.Entry (e, b) :: a, uri)) + in + E.get_obj f uri + | B.LRef (a, i) -> + let f e = function + | B.Abbr v -> + reductions := O.add ~ldelta:1 !reductions; + step f ~delta ~sty c m v + | B.Abst w when sty -> + step f ~delta ~sty c m w + | b -> + f m (B.LRef (B.Entry (e, b) :: a, i)) + in + let f e = S.lift_bind (f e) (succ i) (0) in + get f c m i + | B.Cast (_, _, t) -> + reductions := O.add ~tau:1 !reductions; + step f ~delta ~sty c m t + | B.Appl (_, v, t) -> + step f ~delta ~sty c {m with s = (v, 0) :: m.s} t + | B.Bind (a, B.Abst w, t) -> + begin match m.s with + | [] -> f m x + | (v, h) :: tl -> + reductions := O.add ~beta:1 !reductions; + let f mc = step f ~delta ~sty c {c = mc; s = tl} t in + let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in + S.lift f h (0) v + end + | B.Bind (a, b, t) -> + reductions := O.add ~upsilon:(List.length m.s) !reductions; + let f sc mc = step f ~delta ~sty c {c = mc; s = sc} t in + let f sc = B.push (f sc) m.c a b in + lift_stack f m.s + +(* Interface functions ******************************************************) + +let domain f c t = + let f r = L.unbox level; f r in + let f m = function + | B.Bind (_, B.Abst w, _) -> + let f w = f (Some w) in unwind_to_term f m w + | x -> f None + in + L.box level; log1 "Now scanning" c t; + step f ~delta:true ~sty:true c empty_machine t + +let rec ac_nfs f ~si r c m1 u m2 t = +(* L.warn "entering R.are_convertible_aux"; *) + log2 "Now converting nfs" c u t; + match u, t with + | B.Sort (_, h1), B.Sort (_, h2) -> + if h1 = h2 then f r else f false + | B.LRef (B.Entry (e1, B.Abst _) :: _, _), + B.LRef (B.Entry (e2, B.Abst _) :: _, _) -> + if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + | B.GRef (B.Entry (e1, B.Abst _) :: _, _), + B.GRef (B.Entry (e2, B.Abst _) :: _, _) -> + if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _), + B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) -> + if e1 = e2 then + let f r = + if r then f r + else begin + reductions := O.add ~gdelta:2 !reductions; + ac f ~si true c m1 v1 m2 v2 + end + in + ac_stacks f ~si r c m1 m2 + else if e1 < e2 then begin + reductions := O.add ~gdelta:1 !reductions; + step (ac_nfs f ~si r c m1 u) c m2 v2 + end else begin + reductions := O.add ~gdelta:1 !reductions; + step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + end + | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) -> + reductions := O.add ~gdelta:1 !reductions; + step (ac_nfs f ~si r c m1 u) c m2 v2 + | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ -> + reductions := O.add ~gdelta:1 !reductions; + step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + | B.Bind (a1, (B.Abst w1 as b1), t1), + B.Bind (a2, (B.Abst w2 as b2), t2) -> + let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in + let g m1 = push (g m1) m2 a2 b2 in + let f r = if r then push g m1 a1 b1 else f false in + ac f ~si r c m1 w1 m2 w2 + | B.Sort _, B.Bind (a, b, t) when si -> + let f m1 m2 = ac f ~si r c m1 u m2 t in + let f m1 = push (f m1) m2 a b in + push f m1 a b + | _ -> f false + +and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t + +and ac f ~si r c m1 t1 m2 t2 = +(* L.warn "entering R.are_convertible"; *) + let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in + if r = false then f false else step g c m1 t1 + +and ac_stacks f ~si r c m1 m2 = +(* L.warn "entering R.are_convertible_stacks"; *) + let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in + let map f r (v1, h1) (v2, h2) = + let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in + S.lift f h1 (0) v1 + in + if List.length m1.s <> List.length m2.s then + begin +(* L.warn (Printf.sprintf "Different lengths: %u %u" + (List.length m1.s) (List.length m2.s) + ); *) + f false + end + else + C.list_fold_left2 f map r m1.s m2.s + +let are_convertible f ?(si=false) c u t = + let f b = L.unbox level; f b in + L.box level; log2 "Now converting" c u t; + ac f ~si true c empty_machine u empty_machine t diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli new file mode 100644 index 000000000..a384548b3 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -0,0 +1,21 @@ +(* + ||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 + +val domain: + (Brg.term option -> 'a) -> Brg.context -> Brg.term -> 'a + +val are_convertible: + (bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a + +val reductions: BrgOutput.reductions ref diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml new file mode 100644 index 000000000..5adc12631 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml @@ -0,0 +1,38 @@ +(* + ||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 + +let iter map d = + let rec iter_bind d = function + | B.Void as b -> b + | B.Abst w -> B.Abst (iter_term d w) + | B.Abbr v -> B.Abbr (iter_term d v) + and iter_term d = function + | B.Sort _ as t -> t + | B.GRef _ as t -> t + | B.LRef (a, i) as t -> if i < d then t else map d a i + | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v) + | B.Appl (a, w, u) -> B.Appl (a, iter_term d w, iter_term d u) + | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u) + in + iter_term d + +let lift_map h _ a i = + if i + h >= 0 then B.LRef (a, i + h) else assert false + +let lift g h d t = + if h = 0 then g t else g (iter (lift_map h) d t) + +let lift_bind g h d = function + | B.Void -> g B.Void + | B.Abst w -> let g w = g (B.Abst w) in lift g h d w + | B.Abbr v -> let g v = g (B.Abbr v) in lift g h d v diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.mli b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli new file mode 100644 index 000000000..4c5c9c8a7 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val lift: (Brg.term -> 'a) -> int -> int -> Brg.term -> 'a + +val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml new file mode 100644 index 000000000..8c9996c22 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -0,0 +1,125 @@ +(* + ||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 C = Cps +module S = Share +module L = Log +module H = Hierarchy +module B = Brg +module O = BrgOutput +module E = BrgEnvironment +module R = BrgReduction + +exception TypeError of B.message + +(* Internal functions *******************************************************) + +let level = 4 + +let log1 s c t = + let sc, st = s ^ " in the context", "the term" in + L.log O.specs level (L.ct_items1 sc c st t) + +let error1 st c t = + let sc = "In the context" in + raise (TypeError (L.ct_items1 sc c st t)) + +let error3 c t1 t2 t3 = + let sc, st1, st2, st3 = + "In the context", "the term", "is of type", "but must be of type" + in + raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + +(* Interface functions ******************************************************) + +let si = ref false + +let rec b_type_of f g c x = +(* L.warn "Entering T.b_type_of"; *) + log1 "Now checking" c x; + match x with + | B.Sort (a, h) -> + let f h = f x (B.Sort (a, 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, _))) -> 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, _)) -> f x w + | _, _, B.Abbr _ -> assert false + | _, _, B.Void -> + error1 "reference to excluded object" c x + in + E.get_obj f uri + | B.Bind (a, B.Abbr v, t) -> + let f xv xt tt = + f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) + in + let f xv cc = b_type_of (f xv) g cc t in + let f xv = B.push (f xv) c a (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 (a, B.Abst u, t) -> + let f xu xt tt = + f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) + in + let f xu cc = b_type_of (f xu) g cc t in + let f xu _ = B.push (f xu) c a (B.Abst xu) in + type_of f g c u + | B.Bind (a, B.Void, t) -> + let f xt tt = + f (S.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt) + in + let f cc = b_type_of f g cc t in + B.push f c a B.Void + | B.Appl (a, v, t) -> + let f xv vv xt tt = function + | Some w -> + L.box (succ level); + L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); + L.unbox (succ level); + let f r = +(* L.warn (Printf.sprintf "Convertible: %b" a); *) + if r then f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) + else error3 c xv vv w + in + R.are_convertible f ~si:!si c w vv + | None -> + error1 "not a function" c xt + in + let f xv vv xt tt = R.domain (f 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 (a, u, t) -> + let f xu xt tt r = + (* L.warn (Printf.sprintf "Convertible: %b" a); *) + if r then f (S.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu + in + let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) 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 level; f t u in + L.box level; 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 new file mode 100644 index 000000000..26a33509c --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -0,0 +1,18 @@ +(* + ||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 + +val si: bool ref diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml new file mode 100644 index 000000000..c57b6eb16 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -0,0 +1,32 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = Log +module B = Brg +module E = BrgEnvironment +module T = BrgType + +(* Interface functions ******************************************************) + +(* to share *) +let type_check f g = function + | None -> f None None + | Some (e, uri, B.Abst t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (e, uri, B.Abst xt) in + L.loc := e; T.type_of f g B.empty_context t + | Some (e, uri, B.Abbr t) -> + let f tt obj = f (Some tt) (Some obj) in + let f xt tt = E.set_obj (f tt) (e, uri, B.Abbr xt) in + L.loc := e; T.type_of f g B.empty_context t + | Some (e, uri, B.Void) -> + let f obj = f None (Some obj) in + L.loc := e; E.set_obj f (e, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli new file mode 100644 index 000000000..92e401e7d --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -0,0 +1,13 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val type_check: + (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index b185d6004..c32bec6c7 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaAut metaBag top +meta metaOutput metaAut metaBag metaBrg top diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml new file mode 100644 index 000000000..b82e51a3e --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBrg.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_______________________________________________________________ *) + +module C = Cps +module B = Brg +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) -> + f (B.LRef ([], i)) + | 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 a = [B.Name (true, id)] in + let f t = f (B.Bind (a, B.Abst w, t)) in + let f c = xlate_term c f t in + B.push f c a (B.Abst w) + in + xlate_term c f w + +let xlate_pars f pars = + let map f (id, w) c = + let a = [B.Name (true, id)] in + let f w = B.push f c a (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 (a, b) = f (B.bind a 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 brg_of_meta = xlate_item diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli new file mode 100644 index 000000000..cb47bc9c1 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaBrg.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 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 1774cc991..6cbac04a4 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -17,6 +17,10 @@ module H = Hierarchy module AO = AutOutput module MA = MetaAut module MO = MetaOutput +module MBrg = MetaBrg +module BrgO = BrgOutput +module BrgT = BrgType +module BrgU = BrgUntrusted module MBag = MetaBag module BagO = BagOutput module BagR = BagReduction @@ -26,12 +30,14 @@ 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; bagc = BagO.initial_counters; mst = MA.initial_status } @@ -44,6 +50,58 @@ let flush () = L.flush 0; L.flush_err () let bag_error s msg = L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () +let brg_error s msg = + L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush () + +(* kernel related ***********************************************************) + +type kernel = Brg | Bag + +type kernel_item = BrgItem of Brg.item + | BagItem of Bag.item + +let kernel = ref Brg + +let print_counters st = match !kernel with + | Brg -> BrgO.print_counters C.start st.brgc + | Bag -> BagO.print_counters C.start st.bagc + +let kernel_of_meta f st item = match !kernel with + | Brg -> + let f item = f st (BrgItem item) in + MBrg.brg_of_meta f item + | Bag -> + let f item = f st (BagItem item) in + MBag.bag_of_meta f item + +let count_item st = function + | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item} + | BagItem item -> {st with bagc = count BagO.count_item st.bagc item} + +let type_check f st g = function + | BrgItem item -> + let f _ = function + | None -> f st None + | Some (i, u, _) -> f st (Some (i, u)) + in + BrgU.type_check f g item + | BagItem item -> + let f _ = function + | None -> f st None + | Some (i, u, _) -> f st (Some (i, u)) + in + BagU.type_check f g item + +let indexes () = match !kernel with + | Brg -> BrgO.indexes := true + | Bag -> BagO.indexes := true + +let si () = match !kernel with + | Brg -> BrgT.si := true + | Bag -> BagR.nsi := true + +(****************************************************************************) + let main = try let version_string = "Helena 0.8.0 M - June 2009" in @@ -56,6 +114,11 @@ try in H.graph_of_string f s in + let set_kernel = function + | "brg" -> kernel := Brg + | "bag" -> kernel := Bag + | s -> L.warn (P.sprintf "Unknown kernel version: %s" s) + in let set_summary i = L.level := i in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_stage i = stage := i in @@ -84,16 +147,16 @@ try | [] -> st | item :: tl -> (* stage 3 *) - let f st _ = function - | None -> st - | Some (i, u, _) -> + let f st = function + | None -> st + | Some (i, u) -> Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st in (* stage 2 *) let f st item = - 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 + let st = count_item st item in + if !stage > 2 then type_check f st !H.graph item else st in (* stage 1 *) let f st mst item = @@ -104,7 +167,7 @@ try | None -> () | Some (_, frm) -> MO.pp_item C.start frm item end; - if !stage > 1 then MBag.bag_of_meta (f st) item else st + if !stage > 1 then kernel_of_meta f st item else st in (* stage 0 *) let st = {st with ac = count AO.count_item st.ac item} in @@ -117,10 +180,10 @@ 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 BagO.print_counters C.start st.bagc; + if !L.level > 2 && !stage > 1 then print_counters st in let help = - "Usage: helena [ -Vin | -Ss | -m | -h ] ...\n\n" ^ + "Usage: helena [ -Viu | -Ss | -m | -hk ] ...\n\n" ^ "Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n" @@ -129,8 +192,9 @@ try let help_V = " show version information" in let help_h = " set type hierarchy" in let help_i = " show local references by index" in + let help_k = " set kernel version" in let help_m = " output intermediate representation" in - let help_n = " activate naive sort inclusion" in + let help_u = " activate sort inclusion" in let help_s = " Set translation stage" in L.box 0; L.box_err (); H.set_new_sorts ignore ["Set"; "Prop"]; @@ -138,11 +202,13 @@ 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 BagO.indexes, help_i); + ("-i", Arg.Unit indexes, help_i); + ("-k", Arg.String set_kernel, help_k); ("-m", Arg.String set_meta_file, help_m); - ("-n", Arg.Set BagR.nsi, help_n); + ("-u", Arg.Unit si, help_u); ("-s", Arg.Int set_stage, help_s) ] read_file help; if !L.level > 0 then Time.utime_stamp "at exit"; flush () with BagType.TypeError msg -> bag_error "Type Error" msg + | BrgT.TypeError msg -> brg_error "Type Error" msg -- 2.39.2