+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
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
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
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
-lib automath basic_ag toplevel
+lib automath basic_rg basic_ag toplevel
@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)"
include .depend.opt
endif
-ifeq ($(MAKECMDGOALS), test-nsi)
+ifeq ($(MAKECMDGOALS), test-si)
include .depend.opt
endif
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+(* kernel version: basic, absolute, global *)
+(* note : experimental *)
+
type uri = NUri.uri
type id = Aut.id
type ho_whd_result =
| Sort of int
- | GRef of U.uri * B.term list
| Abst of B.term
(* Internal functions *******************************************************)
type ho_whd_result =
| Sort of int
- | GRef of NUri.uri * Bag.term list
| Abst of Bag.term
val ho_whd:
--- /dev/null
+brg brgOutput
+brgEnvironment brgSubstitution brgReduction brgType brgUntrusted
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
+}
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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)
--- /dev/null
+(*
+ ||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
-meta metaOutput metaAut metaBag top
+meta metaOutput metaAut metaBag metaBrg top
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
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
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
}
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
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
| [] -> 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 =
| 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
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 <number> | -m <file> | -h <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Viu | -Ss <number> | -m <file> | -hk <string> ] <file> ...\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"
let help_V = " show version information" in
let help_h = "<string> set type hierarchy" in
let help_i = " show local references by index" in
+ let help_k = "<string> set kernel version" in
let help_m = "<file> output intermediate representation" in
- let help_n = " activate naive sort inclusion" in
+ let help_u = " activate sort inclusion" in
let help_s = "<number> Set translation stage" in
L.box 0; L.box_err ();
H.set_new_sorts ignore ["Set"; "Prop"];
("-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
projects / helm.git / commitdiff