common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi
common/output.cmo: lib/log.cmi common/output.cmi
common/output.cmx: lib/log.cmx common/output.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/entity.cmo: lib/nUri.cmi automath/aut.cmx
+common/entity.cmx: lib/nUri.cmx automath/aut.cmx
+common/library.cmi: common/hierarchy.cmi common/entity.cmx
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/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/brg.cmo: common/entity.cmx
+basic_rg/brg.cmx: common/entity.cmx
+basic_rg/brgOutput.cmi: lib/log.cmi common/entity.cmx 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 \
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: common/unit.cmx lib/log.cmi lib/cps.cmx
-basic_ag/bag.cmx: common/unit.cmx lib/log.cmx lib/cps.cmx
+basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx
+basic_ag/bag.cmx: lib/log.cmx common/entity.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/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/unit.cmx
-toplevel/meta.cmx: common/unit.cmx
+toplevel/meta.cmo: common/entity.cmx
+toplevel/meta.cmx: common/entity.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
# This book is not accepted in AUT-QE because [y:'type'] is not allowed
# This book is accepted in lambda-delta with sort inclusion but Omega is not
# valid if sort inclusion is allowed on the term backbone only
-# This book is valid in lambda-delta with sort inclusion allowed everywhere
+# This book is valid in lambda-delta with unrestricted sort inclusion
+l
@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
| GRef of qid * term list (* reference: name, arguments *)
| Appl of term * term (* application: argument, function *)
- | Abst of id * term * term (* abstraction: name, type, body *)
+ | Abst of id * term * term (* abstraction: name, domain, scope *)
-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 *)
- | Def of id * term * bool * term (* definition: name, type, transparent?, body *)
+type entity = 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, domain *)
+ | Decl of id * term (* declaration: name, domain *)
+ | Def of id * term * bool * term (* definition: name, domain, transparent?, body *)
let f c = count_term f c t in
count_term f c w
-let count_unit f c = function
+let count_entity 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 units = c.sections + c.contexts + c.blocks + c.decls + c.defs in
+ let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in
L.warn (P.sprintf " Automath representation summary");
- 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 book entities: %7u" entities);
+ L.warn (P.sprintf " Section entities: %7u" c.sections);
+ L.warn (P.sprintf " Context entities: %7u" c.contexts);
+ L.warn (P.sprintf " Block entities: %7u" c.blocks);
+ L.warn (P.sprintf " Declaration entities: %7u" c.decls);
+ L.warn (P.sprintf " Definition entities: %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_unit: (counters -> 'a) -> counters -> Aut.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Aut.entity -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
%token TYPE PROP DEF EB E PN EXIT
%start book
- %type <Aut.unit list> book
+ %type <Aut.entity list> book
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
| term { [$1] }
| term CM terms { $1 :: $3 }
;
- unit:
+ entity:
| 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) }
;
- units:
- | { [] }
- | unit units { $1 :: $2 }
+ entities:
+ | { [] }
+ | entity entities { $1 :: $2 }
;
book:
- | units eof { $1 }
+ | entities eof { $1 }
;
in
exp_count f st
-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
+let proc_entity f st entity = match entity with
+ | A.Section section -> proc_section f st section entity
+ | A.Context _ -> proc_context f st entity
+ | A.Block _ -> proc_block f st entity
+ | A.Decl _ -> proc_global f st entity
+ | A.Def _ -> proc_global f st entity
(* interface functions ******************************************************)
iao = 0; iar = 0; iac = 0; iag = 0
}
-let process_unit = proc_unit
+let process_entity = proc_entity
let get_counters f st = f st.iao st.iar st.iac st.iag
val initial_status: status
-val process_unit: (status -> Aut.unit -> 'a) -> status -> Aut.unit -> 'a
+val process_entity: (status -> Aut.entity -> 'a) -> status -> Aut.entity -> 'a
val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a
(* kernel version: basic, absolute, global *)
(* note : experimental *)
-type uri = Unit.uri
-type id = Unit.id
+type uri = Entity.uri
+type id = Entity.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
and term = Sort of int (* hierarchy index *)
| LRef of int (* location *)
| GRef of uri (* reference *)
- | Cast of term * term (* type, term *)
+ | Cast of term * term (* domain, element *)
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type entry = bind Unit.entry (* age, uri, binder *)
+type entry = bind Entity.entry (* age, uri, binder *)
-type unit = bind Unit.unit
+type entity = bind Entity.entity
type lenv = (int * id * bind) list (* location, name, binder *)
let count_entry f c (_, _, b) =
count_entry_binder f c b
-let count_unit f c = function
+let count_entity f c = function
| Some entry -> count_entry f c entry
| None -> f c
val initial_counters: counters
-val count_unit: (counters -> 'a) -> counters -> Bag.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
V_______________________________________________________________ *)
val type_check:
- (Bag.term option -> Bag.unit -> 'a) -> ?si:bool ->
- Hierarchy.graph -> Bag.unit -> 'a
+ (Bag.term option -> Bag.entity -> 'a) -> ?si:bool ->
+ Hierarchy.graph -> Bag.entity -> 'a
(* kernel version: basic, relative, global *)
(* note : ufficial basic lambda-delta *)
-type uri = Unit.uri
-type id = Unit.id
+type uri = Entity.uri
+type id = Entity.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 entry = bind Unit.entry (* age, uri, binder *)
+type entry = bind Entity.entry (* age, uri, binder *)
-type unit = bind Unit.unit
+type entity = bind Entity.entity
type lenv = Null
(* Cons: tail, relative local environment, binder *)
} in
f c
-let count_unit f c = function
+let count_entity f c = function
| Some entry -> count_entry f c entry
| None -> f c
val initial_counters: counters
-val count_unit: (counters -> 'a) -> counters -> Brg.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
val specs: (Brg.lenv, Brg.term) Log.specs
-val export_entry: Format.formatter -> Brg.bind Unit.entry -> unit
+val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit
V_______________________________________________________________ *)
val type_check:
- (BrgType.message -> 'a) -> (Brg.term option -> Brg.unit -> 'a) ->
- ?si:bool -> Hierarchy.graph -> Brg.unit -> 'a
+ (BrgType.message -> 'a) -> (Brg.term option -> Brg.entity -> 'a) ->
+ ?si:bool -> Hierarchy.graph -> Brg.entity -> 'a
-hierarchy output unit library
+hierarchy output entity library
--- /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 entity = 'bind entry option
(* interface functions ******************************************************)
-let export_unit export_entry si g = function
+let export_entity export_entry si g = function
| Some entry ->
let _, uri, bind = entry in
let path = path_of_uri uri in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val export_unit:
- (Format.formatter -> 'bind Unit.entry -> unit) ->
- bool -> Hierarchy.graph -> 'bind Unit.unit -> unit
+val export_entity:
+ (Format.formatter -> 'bind Entity.entry -> unit) ->
+ bool -> Hierarchy.graph -> 'bind Entity.entity -> 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 = Unit.uri
+type uri = Entity.uri
-type id = Unit.id
+type id = Entity.id
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
| LRef of int * int (* local reference: local environment length, de bruijn index *)
| GRef of int * uri * term list (* global reference: local environment length, name, arguments *)
| Appl of term * term (* application: argument, function *)
- | Abst of id * term * term (* abstraction: name, type, scope *)
+ | Abst of id * term * term (* abstraction: name, domain, scope *)
type pars = (id * term) list (* parameter declarations: name, type *)
-(* entry: line number, parameters, name, type, (transparent?, body) *)
+(* entry: line number, parameters, name, domain, (transparent?, body) *)
type entry = int * pars * uri * term * (bool * term) option
-type unit = entry option
+type entity = entry option
in
resolve_lref f st l lenv (id_of_name name)
-let xlate_unit f st = function
+let xlate_entity 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_unit
+let meta_of_aut = xlate_entity
val initial_status: ?cover:string -> unit -> status
-val meta_of_aut: (status -> Meta.unit -> 'a) -> status -> Aut.unit -> 'a
+val meta_of_aut: (status -> Meta.entity -> 'a) -> status -> Aut.entity -> 'a
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-let xlate_unit f = function
+let xlate_entity 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_unit
+let bag_of_meta = xlate_entity
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val bag_of_meta: (Bag.unit -> 'a) -> Meta.unit -> 'a
+val bag_of_meta: (Bag.entity -> 'a) -> Meta.entity -> 'a
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-let xlate_unit f = function
+let xlate_entity 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_unit
+let brg_of_meta = xlate_entity
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val brg_of_meta: (Brg.unit -> 'a) -> Meta.unit -> 'a
+val brg_of_meta: (Brg.entity -> 'a) -> Meta.entity -> 'a
F.pp_set_margin frm max_int;
f (och, frm)
-let write_unit f (_, frm) unit =
- O.pp_unit f frm unit
+let write_entity f (_, frm) entity =
+ O.pp_entity f frm entity
let close_out f (och, _) =
close_out och; f ()
val open_out: (out_channel -> 'a) -> string -> 'a
-val write_unit: (unit -> 'a) -> out_channel -> Meta.unit -> 'a
+val write_entity: (unit -> 'a) -> out_channel -> Meta.entity -> '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_unit f c = function
+let count_entity f c = function
| Some e -> count_entry f c e
| None -> f c
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_unit f frm = function
+let pp_entity f frm = function
| Some entry -> pp_entry frm entry; f ()
| None -> f ()
val initial_counters: counters
-val count_unit: (counters -> 'a) -> counters -> Meta.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
-val pp_unit: (unit -> 'a) -> Format.formatter -> Meta.unit -> 'a
+val pp_entity: (unit -> 'a) -> Format.formatter -> Meta.entity -> 'a
ast = AP.initial_status
}
-let count count_fun c unit =
- if !L.level > 2 then count_fun C.start c unit else c
+let count count_fun c entity =
+ if !L.level > 2 then count_fun C.start c entity 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_unit f st =
+let process_entity f st =
let f ast = f {st with ast = ast} in
- AP.process_unit f st.ast
+ AP.process_entity f st.ast
(* kernel related ***********************************************************)
type kernel = Brg | Bag
-type kernel_unit = Brgunit of Brg.unit
- | Bagunit of Bag.unit
+type kernel_entity = BrgEntity of Brg.entity
+ | BagEntity of Bag.entity
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 unit = match !kernel with
+let kernel_of_meta f st entity = match !kernel with
| Brg ->
- let f unit = f st (Brgunit unit) in
- MBrg.brg_of_meta f unit
+ let f entity = f st (BrgEntity entity) in
+ MBrg.brg_of_meta f entity
| Bag ->
- let f unit = f st (Bagunit unit) in
- MBag.bag_of_meta f unit
+ let f entity = f st (BagEntity entity) in
+ MBag.bag_of_meta f entity
-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 count_entity st = function
+ | BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity}
+ | BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity}
-let export_unit si g = function
- | Brgunit unit -> G.export_unit BrgO.export_entry si g unit
- | Bagunit _ -> ()
+let export_entity si g = function
+ | BrgEntity entity -> G.export_entity BrgO.export_entry si g entity
+ | BagEntity _ -> ()
let type_check f st si g k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
| Some (i, u, _) -> f st (Some (i, u))
in
match k with
- | Brgunit unit -> BrgU.type_check brg_err f ~si g unit
- | Bagunit unit -> BagU.type_check f ~si g unit
+ | BrgEntity entity -> BrgU.type_check brg_err f ~si g entity
+ | BagEntity entity -> BagU.type_check f ~si g entity
(****************************************************************************)
if !L.level > 0 then T.utime_stamp "parsed";
let rec aux st = function
| [] -> st
- | unit :: tl ->
+ | entity :: tl ->
(* stage 3 *)
let f st = function
| None -> st
st
in
(* stage 2 *)
- 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
+ let f st entity =
+ let st = count_entity st entity in
+ if !export then export_entity !si !graph entity;
+ if !stage > 2 then type_check f st !si !graph entity else st
in
(* stage 1 *)
- let f st mst unit =
+ let f st mst entity =
let st = {st with
- mst = mst; mc = count MO.count_unit st.mc unit
+ mst = mst; mc = count MO.count_entity st.mc entity
} in
begin match !moch with
| None -> ()
- | Some och -> ML.write_unit C.start och unit
+ | Some och -> ML.write_entity C.start och entity
end;
- if !stage > 1 then kernel_of_meta f st unit else st
+ if !stage > 1 then kernel_of_meta f st entity else st
in
(* stage 0 *)
- let st = {st with ac = count AO.count_unit st.ac unit} in
- let f st unit =
+ let st = {st with ac = count AO.count_entity st.ac entity} in
+ let f st entity =
let st =
- if !stage > 0 then MA.meta_of_aut (f st) st.mst unit else st
+ if !stage > 0 then MA.meta_of_aut (f st) st.mst entity else st
in
aux st tl
in
- if !process then process_unit f st unit else f st unit
+ if !process then process_entity f st entity else f st entity
in
O.clear_reductions ();
let cover = if !use_cover then base_name else "" in
projects / helm.git / commitdiff