-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
-automath/aut.cmo:
-automath/aut.cmx:
automath/autProcess.cmi: automath/aut.cmx
automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi
automath/autProcess.cmx: automath/aut.cmx automath/autProcess.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
-common/hierarchy.cmi:
common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi
common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi
-common/output.cmi:
common/output.cmo: lib/log.cmi common/output.cmi
common/output.cmx: lib/log.cmx common/output.cmi
-common/item.cmo: lib/nUri.cmi automath/aut.cmx
-common/item.cmx: lib/nUri.cmx automath/aut.cmx
-common/library.cmi: common/item.cmx common/hierarchy.cmi
+common/unit.cmo: lib/nUri.cmi automath/aut.cmx
+common/unit.cmx: lib/nUri.cmx automath/aut.cmx
+common/library.cmi: common/unit.cmx common/hierarchy.cmi
common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi
common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi
-basic_rg/brg.cmo: common/item.cmx
-basic_rg/brg.cmx: common/item.cmx
-basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx
+basic_rg/brg.cmo: common/unit.cmx
+basic_rg/brg.cmx: common/unit.cmx
+basic_rg/brgOutput.cmi: common/unit.cmx lib/log.cmi basic_rg/brg.cmx
basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
common/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.cmi: basic_rg/brg.cmx
basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \
common/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.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: common/hierarchy.cmi basic_rg/brg.cmx
+basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brgType.cmi \
+ basic_rg/brg.cmx
basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \
basic_rg/brgReduction.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/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
basic_rg/brgUntrusted.cmi
-basic_ag/bag.cmo: lib/log.cmi common/item.cmx lib/cps.cmx
-basic_ag/bag.cmx: lib/log.cmx common/item.cmx lib/cps.cmx
+basic_ag/bag.cmo: common/unit.cmx lib/log.cmi lib/cps.cmx
+basic_ag/bag.cmx: common/unit.cmx lib/log.cmx lib/cps.cmx
basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx
basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi
basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
common/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi
-basic_ag/bagEnvironment.cmi: lib/nUri.cmi basic_ag/bag.cmx
+basic_ag/bagEnvironment.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/bag.cmx basic_ag/bagUntrusted.cmi
basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \
basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi
-toplevel/meta.cmo: common/item.cmx
-toplevel/meta.cmx: common/item.cmx
+toplevel/meta.cmo: common/unit.cmx
+toplevel/meta.cmx: common/unit.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \
lib/cps.cmx toplevel/metaOutput.cmi
toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \
common/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
- basic_rg/brgType.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \
- basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \
- basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autProcess.cmi \
- automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
+ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \
+ basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \
+ basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \
+ automath/autOutput.cmi automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \
common/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
- basic_rg/brgType.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \
- basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \
- basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autProcess.cmx \
- automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
+ basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \
+ basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \
+ basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \
+ automath/autOutput.cmx automath/autLexer.cmx
| Appl of term * term (* application: argument, function *)
| Abst of id * term * term (* abstraction: name, type, body *)
-type item = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *)
+type unit = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *)
| Context of qid option (* context: Some = last node, None = root *)
| Block of id * term (* block opener: name, type *)
| Decl of id * term (* declaration: name, type *)
let f c = count_term f c t in
count_term f c w
-let count_item f c = function
+let count_unit f c = function
| A.Section _ ->
f {c with sections = succ c.sections}
| A.Context _ ->
let print_counters f c =
let terms = c.sorts + c.grefs + c.appls + c.absts in
- let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in
+ let units = c.sections + c.contexts + c.blocks + c.decls + c.defs in
L.warn (P.sprintf " Automath representation summary");
- L.warn (P.sprintf " Total book items: %7u" items);
- L.warn (P.sprintf " Section items: %7u" c.sections);
- L.warn (P.sprintf " Context items: %7u" c.contexts);
- L.warn (P.sprintf " Block items: %7u" c.blocks);
- L.warn (P.sprintf " Declaration items: %7u" c.decls);
- L.warn (P.sprintf " Definition items: %7u" c.defs);
+ L.warn (P.sprintf " Total book units: %7u" units);
+ L.warn (P.sprintf " Section units: %7u" c.sections);
+ L.warn (P.sprintf " Context units: %7u" c.contexts);
+ L.warn (P.sprintf " Block units: %7u" c.blocks);
+ L.warn (P.sprintf " Declaration units: %7u" c.decls);
+ L.warn (P.sprintf " Definition units: %7u" c.defs);
L.warn (P.sprintf " Total Parameter items: %7u" c.pars);
L.warn (P.sprintf " Application items: %7u" c.pars);
L.warn (P.sprintf " Total term items: %7u" terms);
val initial_counters: counters
-val count_item: (counters -> 'a) -> counters -> Aut.item -> 'a
+val count_unit: (counters -> 'a) -> counters -> Aut.unit -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
%token TYPE PROP DEF EB E PN EXIT
%start book
- %type <Aut.item list> book
+ %type <Aut.unit list> book
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
| term { [$1] }
| term CM terms { $1 :: $3 }
;
- item:
+ unit:
| PLUS IDENT { A.Section (Some (true, $2)) }
| PLUS TIMES IDENT { A.Section (Some (false, $3)) }
| MINUS IDENT { A.Section None }
| IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) }
| IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) }
;
- items:
+ units:
| { [] }
- | item items { $1 :: $2 }
+ | unit units { $1 :: $2 }
;
book:
- | items eof { $1 }
+ | units eof { $1 }
;
in
exp_count f st
-let proc_item f st item = match item with
- | A.Section section -> proc_section f st section item
- | A.Context _ -> proc_context f st item
- | A.Block _ -> proc_block f st item
- | A.Decl _ -> proc_global f st item
- | A.Def _ -> proc_global f st item
+let proc_unit f st unit = match unit with
+ | A.Section section -> proc_section f st section unit
+ | A.Context _ -> proc_context f st unit
+ | A.Block _ -> proc_block f st unit
+ | A.Decl _ -> proc_global f st unit
+ | A.Def _ -> proc_global f st unit
(* interface functions ******************************************************)
iao = 0; iar = 0; iac = 0; iag = 0
}
-let process_item = proc_item
+let process_unit = proc_unit
let get_counters f st = f st.iao st.iar st.iac st.iag
val initial_status: status
-val process_item: (status -> Aut.item -> 'a) -> status -> Aut.item -> 'a
+val process_unit: (status -> Aut.unit -> 'a) -> status -> Aut.unit -> 'a
val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a
(* kernel version: basic, absolute, global *)
(* note : experimental *)
-type uri = Item.uri
-type id = Item.id
+type uri = Unit.uri
+type id = Unit.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type obj = bind Item.obj (* age, uri, binder *)
+type entry = bind Unit.entry (* age, uri, binder *)
-type item = bind Item.item
+type unit = bind Unit.unit
type lenv = (int * id * bind) list (* location, name, binder *)
let hsize = 7000
let env = H.create hsize
-let entry = ref 1
+let age = ref 1
(* Internal functions *******************************************************)
(* 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 set_entry f entry =
+ let _, uri, b = entry in
+ let entry = !age, uri, b in
+ incr age; H.add env uri entry; f entry
-let get_obj f uri =
+let get_entry f uri =
try f (H.find env uri) with Not_found -> error uri
exception ObjectNotFound of Bag.message
-val set_obj: (Bag.obj -> 'a) -> Bag.obj -> 'a
+val set_entry: (Bag.entry -> 'a) -> Bag.entry -> 'a
-val get_obj: (Bag.obj -> 'a) -> NUri.uri -> 'a
+val get_entry: (Bag.entry -> 'a) -> Bag.uri -> 'a
let f c = count_term_binder f c b in
count_term f c t
-let count_obj_binder f c = function
+let count_entry_binder f c = function
| B.Abst w ->
let c = {c with eabsts = succ c.eabsts} in
count_term f c w
count_term f c v
| B.Void -> f c
-let count_obj f c (_, _, b) =
- count_obj_binder f c b
+let count_entry f c (_, _, b) =
+ count_entry_binder f c b
-let count_item f c = function
- | Some obj -> count_obj f c obj
+let count_unit f c = function
+ | Some entry -> count_entry f c entry
| None -> f c
let print_counters f c =
val initial_counters: counters
-val count_item: (counters -> 'a) -> counters -> Bag.item -> 'a
+val count_unit: (counters -> 'a) -> counters -> Bag.unit -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
type whd_result =
| Sort_ of int
| LRef_ of int * B.term option
- | GRef_ of B.obj
+ | GRef_ of B.entry
| Bind_ of int * B.id * B.term * B.term
type ho_whd_result =
match x with
| B.Sort h -> f m (Sort_ h)
| B.GRef uri ->
- let f obj = f m (GRef_ obj) in
- E.get_obj f uri
+ let f entry = f m (GRef_ entry) in
+ E.get_entry f uri
| B.LRef i ->
let f = function
| B.Void -> f m (LRef_ (i, None))
| _, _, B.Abbr (B.Cast (w, v)) -> f x w
| _, _, B.Abbr _ -> assert false
| _, _, B.Void ->
- error1 "reference to excluded object" c x
+ error1 "reference to excluded entry" c x
in
- E.get_obj f uri
+ E.get_entry 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)
let type_check f ?(si=false) 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
+ let f tt entry = f (Some tt) (Some entry) in
+ let f xt tt = E.set_entry (f tt) (a, uri, B.Abst xt) in
L.loc := a; T.type_of f ~si g B.empty_lenv 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
+ let f tt entry = f (Some tt) (Some entry) in
+ let f xt tt = E.set_entry (f tt) (a, uri, B.Abbr xt) in
L.loc := a; T.type_of f ~si g B.empty_lenv t
| Some (a, uri, B.Void) ->
- let f obj = f None (Some obj) in
- L.loc := a; E.set_obj f (a, uri, B.Void)
+ let f entry = f None (Some entry) in
+ L.loc := a; E.set_entry f (a, uri, B.Void)
V_______________________________________________________________ *)
val type_check:
- (Bag.term option -> Bag.item -> 'a) -> ?si:bool ->
- Hierarchy.graph -> Bag.item -> 'a
+ (Bag.term option -> Bag.unit -> 'a) -> ?si:bool ->
+ Hierarchy.graph -> Bag.unit -> 'a
(* kernel version: basic, relative, global *)
(* note : ufficial basic lambda-delta *)
-type uri = Item.uri
-type id = Item.id
+type uri = Unit.uri
+type id = Unit.id
type attr = Name of bool * id (* real?, name *)
| Apix of int (* additional position index *)
| Appl of attrs * term * term (* attrs, argument, function *)
| Bind of bind * term (* binder, scope *)
-type obj = bind Item.obj (* age, uri, binder *)
+type entry = bind Unit.entry (* age, uri, binder *)
-type item = bind Item.item
+type unit = bind Unit.unit
type lenv = Null
(* Cons: tail, relative local environment, binder *)
let hsize = 7000
let env = H.create hsize
-let entry = ref 1
+let age = ref 1
(* Internal functions *******************************************************)
(* 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 set_entry f entry =
+ let _, uri, b = entry in
+ let entry = !age, uri, b in
+ incr age; H.add env uri entry; f entry
-let get_obj err f uri =
+let get_entry err f uri =
try f (H.find env uri) with Not_found -> err ()
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a
+val set_entry: (Brg.entry -> 'a) -> Brg.entry -> 'a
-val get_obj: (unit -> 'a) -> (Brg.obj -> 'a) -> NUri.uri -> 'a
+val get_entry: (unit -> 'a) -> (Brg.entry -> 'a) -> Brg.uri -> 'a
let f c = B.push (f c) e b in
count_term_binder f c e b
-let count_obj f c = function
+let count_entry f c = function
| (_, u, B.Abst (_, w)) ->
let c = {c with
eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
} in
f c
-let count_item f c = function
- | Some obj -> count_obj f c obj
+let count_unit f c = function
+ | Some entry -> count_entry f c entry
| None -> f c
let print_counters f c =
| B.Void a ->
F.fprintf frm "<Void%a/>" id a
-let exp_obj c frm = function
+let exp_entry c frm = function
| _, u, B.Abst (a, w) ->
let str = U.string_of_uri u in
let a = B.Name (true, U.name_of_uri u) :: a in
let a = B.Name (true, U.name_of_uri u) :: a in
F.fprintf frm "<VOID uri=%S%a/>" str id a
-let export_obj frm obj =
- F.fprintf frm "@,@[<v3> %a@]@," (exp_obj B.empty_lenv) obj
+let export_entry frm entry =
+ F.fprintf frm "@,@[<v3> %a@]@," (exp_entry B.empty_lenv) entry
val initial_counters: counters
-val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a
+val count_unit: (counters -> 'a) -> counters -> Brg.unit -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
val specs: (Brg.lenv, Brg.term) Log.specs
-val export_obj: Format.formatter -> Brg.bind Item.obj -> unit
+val export_entry: Format.formatter -> Brg.bind Unit.entry -> unit
module O = BrgOutput
module E = BrgEnvironment
-type machine = {
+type kam = {
c: B.lenv;
s: (B.lenv * B.term) list;
i: int
| e, _, b ->
f m (Some (e, b)) x
in
- E.get_obj C.err f uri
+ E.get_entry C.err f uri
| B.LRef (_, i) ->
let f c = function
| B.Abbr (_, v) ->
(* Interface functions ******************************************************)
-let empty_machine = {
+let empty_kam = {
c = B.empty_lenv; s = []; i = 0
}
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type machine
+type kam
-val empty_machine: machine
+val empty_kam: kam
-val get: (unit -> 'a) -> (Brg.bind -> 'a) -> machine -> int -> 'a
+val get: (unit -> 'a) -> (Brg.bind -> 'a) -> kam -> int -> 'a
-val push: (machine -> 'a) -> machine -> Brg.bind -> 'a
+val push: (kam -> 'a) -> kam -> Brg.bind -> 'a
-val xwhd: (machine -> Brg.term -> 'a) -> machine -> Brg.term -> 'a
+val xwhd: (kam -> Brg.term -> 'a) -> kam -> Brg.term -> 'a
(* arguments: expected type, inferred type *)
val are_convertible:
(unit -> 'a) -> (unit -> 'a) ->
- ?si:bool -> machine -> Brg.term -> machine -> Brg.term -> 'a
+ ?si:bool -> kam -> Brg.term -> kam -> Brg.term -> 'a
-val specs: (machine, Brg.term) Log.specs
+val specs: (kam, Brg.term) Log.specs
V_______________________________________________________________ *)
val lift: (Brg.term -> 'a) -> int -> int -> Brg.term -> 'a
-
+(*
val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a
+*)
module S = BrgSubstitution
module R = BrgReduction
-type message = (R.machine, B.term) Log.item list
-
-exception TypeError of message
+type message = (R.kam, B.term) Log.message
(* Internal functions *******************************************************)
let s = s ^ " the term" in
L.log R.specs level (message1 s m t)
-let error1 s m t =
- raise (TypeError (message1 s m t))
+let error1 err s m t =
+ err (message1 s m t)
let message3 m t1 t2 ?mu t3 =
let sm, st1, st2 = "In the environment", "the term", "is of type" in
let st3 = "but it must be of type" in
L.et_items3 sm m st1 t1 st2 t2 st3 t3
-let error3 m t1 t2 ?mu t3 =
- raise (TypeError (message3 m t1 t2 ?mu t3))
+let error3 err m t1 t2 ?mu t3 =
+ err (message3 m t1 t2 ?mu t3)
-let assert_convertibility f ~si m u w v =
- let err _ = error3 m v w u in
+let assert_convertibility err f ~si m u w v =
+ let err _ = error3 err m v w u in
R.are_convertible err f ~si m u m w
-let assert_applicability f ~si m u w v =
+let assert_applicability err f ~si m u w v =
let f mu = function
+ | B.Sort _ -> error1 err "not a function type" m u
| B.Bind (B.Abst (_, u), _) ->
- let err _ = error3 m v w ~mu u in
+ let err _ = error3 err m v w ~mu u in
R.are_convertible err f ~si mu u m w
- | _ -> error1 "not a function type" m u
+ | _ -> assert false
in
R.xwhd f m u
-let rec b_type_of f ~si g m x =
+let rec b_type_of err f ~si g m x =
log1 "Now checking" m x;
match x with
| B.Sort (a, h) ->
S.lift (f x) (succ i) (0) w
| B.Abbr _ -> assert false
| B.Void _ ->
- error1 "reference to excluded variable" m x
+ error1 err "reference to excluded variable" m x
in
- let err _ = error1 "reference to unknown variable" m x in
+ let err _ = error1 err "reference to unknown variable" m x in
R.get err f m i
| B.GRef (_, uri) ->
let f = function
| _, _, B.Abbr (_, B.Cast (_, w, _)) -> f x w
| _, _, B.Abbr _ -> assert false
| _, _, B.Void _ ->
- error1 "reference to excluded object" m x
+ error1 err "reference to excluded entry" m x
in
- let err _ = error1 "reference to unknown object" m x in
- E.get_obj err f uri
+ let err _ = error1 err "reference to unknown entry" m x in
+ E.get_entry err f uri
| B.Bind (B.Abbr (a, v), t) ->
let f xv xt tt =
f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
in
- let f xv m = b_type_of (f xv) ~si g m t in
+ let f xv m = b_type_of err (f xv) ~si g m t in
let f xv = R.push (f xv) m (B.abbr a xv) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> f (B.Cast ([], vv, xv))
in
- type_of f ~si g m v
+ type_of err f ~si g m v
| B.Bind (B.Abst (a, u), t) ->
let f xu xt tt =
f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
in
- let f xu m = b_type_of (f xu) ~si g m t in
+ let f xu m = b_type_of err (f xu) ~si g m t in
let f xu _ = R.push (f xu) m (B.abst a xu) in
- type_of f ~si g m u
+ type_of err f ~si g m u
| B.Bind (B.Void a as b, t) ->
let f xt tt =
f (A.sh1 t xt x (B.bind b)) (B.bind b tt)
in
- let f m = b_type_of f ~si g m t in
+ let f m = b_type_of err f ~si g m t in
R.push f m b
| B.Appl (a, v, t) ->
let f xv vv xt tt =
let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
- assert_applicability f ~si m tt vv xv
+ assert_applicability err f ~si m tt vv xv
in
- let f xv vv = b_type_of (f xv vv) ~si g m t in
- type_of f ~si g m v
+ let f xv vv = b_type_of err (f xv vv) ~si g m t in
+ type_of err f ~si g m v
| B.Cast (a, u, t) ->
let f xu xt tt =
let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in
- assert_convertibility f ~si m xu tt xt
+ assert_convertibility err f ~si m xu tt xt
in
- let f xu _ = b_type_of (f xu) ~si g m t in
- type_of f ~si g m u
+ let f xu _ = b_type_of err (f xu) ~si g m t in
+ type_of err f ~si g m u
(* Interface functions ******************************************************)
-and type_of f ?(si=false) g m x =
+and type_of err f ?(si=false) g m x =
let f t u = L.unbox level; f t u in
- L.box level; b_type_of f ~si g m x
+ L.box level; b_type_of err f ~si g m x
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type message = (BrgReduction.machine, Brg.term) Log.item list
-
-exception TypeError of message
+type message = (BrgReduction.kam, Brg.term) Log.message
val type_of:
- (Brg.term -> Brg.term -> 'a) -> ?si:bool ->
- Hierarchy.graph -> BrgReduction.machine -> Brg.term -> 'a
+ (message -> 'a) -> (Brg.term -> Brg.term -> 'a) ->
+ ?si:bool -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a
(* Interface functions ******************************************************)
(* to share *)
-let type_check f ?(si=false) g = function
+let type_check err f ?(si=false) g = function
| None -> f None None
| Some (e, uri, B.Abst (a, t)) ->
- let f tt obj = f (Some tt) (Some obj) in
- let f xt tt = E.set_obj (f tt) (e, uri, B.abst a xt) in
- L.loc := e; T.type_of f ~si g R.empty_machine t
+ let f tt entry = f (Some tt) (Some entry) in
+ let f xt tt = E.set_entry (f tt) (e, uri, B.abst a xt) in
+ L.loc := e; T.type_of err f ~si g R.empty_kam t
| Some (e, uri, B.Abbr (a, t)) ->
- let f tt obj = f (Some tt) (Some obj) in
- let f xt tt = E.set_obj (f tt) (e, uri, B.abbr a xt) in
- L.loc := e; T.type_of f ~si g R.empty_machine t
+ let f tt entry = f (Some tt) (Some entry) in
+ let f xt tt = E.set_entry (f tt) (e, uri, B.abbr a xt) in
+ L.loc := e; T.type_of err f ~si g R.empty_kam t
| Some (e, uri, (B.Void _ as b)) ->
- let f obj = f None (Some obj) in
- L.loc := e; E.set_obj f (e, uri, b)
+ let f entry = f None (Some entry) in
+ L.loc := e; E.set_entry f (e, uri, b)
V_______________________________________________________________ *)
val type_check:
- (Brg.term option -> Brg.item -> 'a) -> ?si:bool ->
- Hierarchy.graph -> Brg.item -> 'a
+ (BrgType.message -> 'a) -> (Brg.term option -> Brg.unit -> 'a) ->
+ ?si:bool -> Hierarchy.graph -> Brg.unit -> 'a
-hierarchy output item library
+hierarchy output unit library
type graph = string * (int -> int)
let sorts = 2
-let sort = H.create sorts
-let index = ref 0
+let sort = H.create sorts
(* Internal functions *******************************************************)
(* Interface functions ******************************************************)
-let set_new_sorts f ss =
- let f i = index := i; f i in
- C.list_fold_left f set_sort !index ss
+let set_sorts f ss i =
+ C.list_fold_left f set_sort i ss
let get_sort err f h =
try f (H.find sort h) with Not_found -> err ()
type graph
-val set_new_sorts: (int -> 'a) -> string list -> 'a
+val set_sorts: (int -> 'a) -> string list -> int -> 'a
val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> '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_______________________________________________________________ *)
-
-type uri = NUri.uri
-type id = Aut.id
-
-type 'bind obj = int * uri * 'bind (* age, uri, binder *)
-
-type 'bind item = 'bind obj option
(* interface functions ******************************************************)
-let export_item export_obj si g = function
- | Some obj ->
- let _, uri, bind = obj in
+let export_unit export_entry si g = function
+ | Some entry ->
+ let _, uri, bind = entry in
let path = path_of_uri uri in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let och = open_out (path ^ obj_ext) in
let frm = Format.formatter_of_out_channel och in
Format.pp_set_margin frm max_int;
Format.fprintf frm "@[<v>%t%t%t%a%t@]@."
- pp_head pp_doctype (open_entry si g) export_obj obj close_entry;
+ pp_head pp_doctype (open_entry si g) export_entry entry close_entry;
close_out och
| None -> ()
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val export_item:
- (Format.formatter -> 'bind Item.obj -> unit) ->
- bool -> Hierarchy.graph -> 'bind Item.item -> unit
+val export_unit:
+ (Format.formatter -> 'bind Unit.entry -> unit) ->
+ bool -> Hierarchy.graph -> 'bind Unit.unit -> unit
--- /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 uri = NUri.uri
+type id = Aut.id
+
+type 'bind entry = int * uri * 'bind (* age, uri, binder *)
+
+type 'bind unit = 'bind entry option
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type uri = Item.uri
+type uri = Unit.uri
-type id = Item.id
+type id = Unit.id
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
| LRef of int * int (* local reference: local environment length, de bruijn index *)
(* entry: line number, parameters, name, type, (transparent?, body) *)
type entry = int * pars * uri * term * (bool * term) option
-type item = entry option
+type unit = entry option
in
resolve_lref f st l lenv (id_of_name name)
-let xlate_item f st = function
+let xlate_unit f st = function
| A.Section (Some (_, name)) ->
f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
| A.Section None ->
let initial_status ?(cover="") () =
initial_status hsize cover
-let meta_of_aut = xlate_item
+let meta_of_aut = xlate_unit
val initial_status: ?cover:string -> unit -> status
-val meta_of_aut: (status -> Meta.item -> 'a) -> status -> Aut.item -> 'a
+val meta_of_aut: (status -> Meta.unit -> 'a) -> status -> Aut.unit -> 'a
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-let xlate_item f = function
+let xlate_unit 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
+let bag_of_meta = xlate_unit
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val bag_of_meta: (Bag.item -> 'a) -> Meta.item -> 'a
+val bag_of_meta: (Bag.unit -> 'a) -> Meta.unit -> 'a
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-let xlate_item f = function
+let xlate_unit 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
+let brg_of_meta = xlate_unit
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val brg_of_meta: (Brg.item -> 'a) -> Meta.item -> 'a
+val brg_of_meta: (Brg.unit -> 'a) -> Meta.unit -> 'a
F.pp_set_margin frm max_int;
f (och, frm)
-let write_item f (_, frm) item =
- O.pp_item f frm item
+let write_unit f (_, frm) unit =
+ O.pp_unit f frm unit
let close_out f (och, _) =
close_out och; f ()
val open_out: (out_channel -> 'a) -> string -> 'a
-val write_item: (unit -> 'a) -> out_channel -> Meta.item -> 'a
+val write_unit: (unit -> 'a) -> out_channel -> Meta.unit -> 'a
val close_out: (unit -> 'a) -> out_channel -> 'a
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
-let count_item f c = function
+let count_unit f c = function
| Some e -> count_entry f c e
| None -> f c
let print_counters f c =
let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
let pars = c.pabsts + c.pappls in
- let items = c.eabsts + c.eabbrs in
+ let entries = c.eabsts + c.eabbrs in
let nodes = c.nodes + c.xnodes in
L.warn (P.sprintf " Intermediate representation summary");
- L.warn (P.sprintf " Total entry items: %7u" items);
+ L.warn (P.sprintf " Total entries: %7u" entries);
L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
L.warn (P.sprintf " Definition items: %7u" c.eabbrs);
L.warn (P.sprintf " Total parameter items: %7u" pars);
F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
-let pp_item f frm = function
+let pp_unit f frm = function
| Some entry -> pp_entry frm entry; f ()
| None -> f ()
val initial_counters: counters
-val count_item: (counters -> 'a) -> counters -> Meta.item -> 'a
+val count_unit: (counters -> 'a) -> counters -> Meta.unit -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
-val pp_item: (unit -> 'a) -> Format.formatter -> Meta.item -> 'a
+val pp_unit: (unit -> 'a) -> Format.formatter -> Meta.unit -> 'a
module G = Library
module BrgO = BrgOutput
module BrgR = BrgReduction
-module BrgT = BrgType
module BrgU = BrgUntrusted
module MBag = MetaBag
module BagO = BagOutput
ast = AP.initial_status
}
-let count count_fun c item =
- if !L.level > 2 then count_fun C.start c item else c
+let count count_fun c unit =
+ if !L.level > 2 then count_fun C.start c unit else c
let flush () = L.flush 0; L.flush_err ()
let brg_error s msg =
L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush ()
-let process_item f st =
+let process_unit f st =
let f ast = f {st with ast = ast} in
- AP.process_item f st.ast
+ AP.process_unit f st.ast
(* kernel related ***********************************************************)
type kernel = Brg | Bag
-type kernel_item = BrgItem of Brg.item
- | BagItem of Bag.item
+type kernel_unit = Brgunit of Brg.unit
+ | Bagunit of Bag.unit
let kernel = ref Brg
| 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
+let kernel_of_meta f st unit = match !kernel with
| Brg ->
- let f item = f st (BrgItem item) in
- MBrg.brg_of_meta f item
+ let f unit = f st (Brgunit unit) in
+ MBrg.brg_of_meta f unit
| Bag ->
- let f item = f st (BagItem item) in
- MBag.bag_of_meta f item
+ let f unit = f st (Bagunit unit) in
+ MBag.bag_of_meta f unit
-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 count_unit st = function
+ | Brgunit unit -> {st with brgc = count BrgO.count_unit st.brgc unit}
+ | Bagunit unit -> {st with bagc = count BagO.count_unit st.bagc unit}
-let export_item si g = function
- | BrgItem item -> G.export_item BrgO.export_obj si g item
- | BagItem _ -> ()
+let export_unit si g = function
+ | Brgunit unit -> G.export_unit BrgO.export_entry si g unit
+ | Bagunit _ -> ()
let type_check f st si g k =
+ let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
let f _ = function
- | None -> f st None
+ | None -> f st None
| Some (i, u, _) -> f st (Some (i, u))
in
match k with
- | BrgItem item -> BrgU.type_check f ~si g item
- | BagItem item -> BagU.type_check f ~si g item
+ | Brgunit unit -> BrgU.type_check brg_err f ~si g unit
+ | Bagunit unit -> BagU.type_check f ~si g unit
(****************************************************************************)
if !L.level > 0 then T.utime_stamp "parsed";
let rec aux st = function
| [] -> st
- | item :: tl ->
+ | unit :: tl ->
(* stage 3 *)
let f st = function
| None -> st
st
in
(* stage 2 *)
- let f st item =
- let st = count_item st item in
- if !export then export_item !si !graph item;
- if !stage > 2 then type_check f st !si !graph item else st
+ let f st unit =
+ let st = count_unit st unit in
+ if !export then export_unit !si !graph unit;
+ if !stage > 2 then type_check f st !si !graph unit else st
in
(* stage 1 *)
- let f st mst item =
+ let f st mst unit =
let st = {st with
- mst = mst; mc = count MO.count_item st.mc item
+ mst = mst; mc = count MO.count_unit st.mc unit
} in
begin match !moch with
| None -> ()
- | Some och -> ML.write_item C.start och item
+ | Some och -> ML.write_unit C.start och unit
end;
- if !stage > 1 then kernel_of_meta f st item else st
+ if !stage > 1 then kernel_of_meta f st unit else st
in
(* stage 0 *)
- let st = {st with ac = count AO.count_item st.ac item} in
- let f st item =
+ let st = {st with ac = count AO.count_unit st.ac unit} in
+ let f st unit =
let st =
- if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st
+ if !stage > 0 then MA.meta_of_aut (f st) st.mst unit else st
in
aux st tl
in
- if !process then process_item f st item else f st item
+ if !process then process_unit f st unit else f st unit
in
O.clear_reductions ();
let cover = if !use_cover then base_name else "" in
let help_s = "<number> set translation stage (see above)" in
let help_x = " export kernel objects (XML)" in
L.box 0; L.box_err ();
- H.set_new_sorts ignore ["Set"; "Prop"];
+ H.set_sorts ignore ["Set"; "Prop"] 0;
at_exit exit;
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-x", Arg.Set export, help_x)
] read_file help;
with BagT.TypeError msg -> bag_error "Type Error" msg
- | BrgT.TypeError msg -> brg_error "Type Error" msg
projects / helm.git / commitdiff