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_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/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: basic_ag/bag.cmx
+basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \
+ basic_ag/bagEnvironment.cmi
+basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \
+ basic_ag/bagEnvironment.cmi
+basic_ag/bagSubstitution.cmi: basic_ag/bag.cmx
+basic_ag/bagSubstitution.cmo: lib/share.cmx basic_ag/bag.cmx \
+ basic_ag/bagSubstitution.cmi
+basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \
+ basic_ag/bagSubstitution.cmi
+basic_ag/bagReduction.cmi: basic_ag/bag.cmx
+basic_ag/bagReduction.cmo: lib/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
+basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \
+ basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \
+ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi
+basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx
+basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
+ common/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \
+ basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \
+ basic_ag/bagType.cmi
+basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
+ common/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \
+ basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \
+ basic_ag/bagType.cmi
+basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx
+basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.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
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/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/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/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: basic_ag/bag.cmx
-basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \
- basic_ag/bagEnvironment.cmi
-basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \
- basic_ag/bagEnvironment.cmi
-basic_ag/bagSubstitution.cmi: basic_ag/bag.cmx
-basic_ag/bagSubstitution.cmo: lib/share.cmx basic_ag/bag.cmx \
- basic_ag/bagSubstitution.cmi
-basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \
- basic_ag/bagSubstitution.cmi
-basic_ag/bagReduction.cmi: basic_ag/bag.cmx
-basic_ag/bagReduction.cmo: lib/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
-basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \
- basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \
- basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi
-basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx
-basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
- common/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \
- basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \
- basic_ag/bagType.cmi
-basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
- common/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \
- basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \
- basic_ag/bagType.cmi
-basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx
-basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.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
+dual_rg/drg.cmo: common/entity.cmx
+dual_rg/drg.cmx: common/entity.cmx
+dual_rg/drgAut.cmi: common/entity.cmx dual_rg/drg.cmx automath/aut.cmx
+dual_rg/drgAut.cmo: lib/nUri.cmi common/entity.cmx dual_rg/drg.cmx \
+ lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi
+dual_rg/drgAut.cmx: lib/nUri.cmx common/entity.cmx dual_rg/drg.cmx \
+ lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi
toplevel/meta.cmo: common/entity.cmx
toplevel/meta.cmx: common/entity.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
-lib automath common basic_rg basic_ag toplevel
+lib automath common basic_ag basic_rg dual_rg toplevel
INPUT-ORIG = automath/grundlagen-orig.aut
test: $(MAIN).opt
- @echo " HELENA -a -c $(INPUT)"
- $(H)./$(MAIN).opt -a -c -S 3 $(O) $(INPUT) > log.txt
+ @echo " HELENA -a -r $(INPUT)"
+ $(H)./$(MAIN).opt -a -r -S 3 $(O) $(INPUT) > log.txt
test-si: $(MAIN).opt
- @echo " HELENA -a -c -u $(INPUT)"
- $(H)./$(MAIN).opt -a -c -u -S 3 $(O) $(INPUT) > log.txt
+ @echo " HELENA -a -r -u $(INPUT)"
+ $(H)./$(MAIN).opt -a -r -u -S 3 $(O) $(INPUT) > log.txt
test-si-fast: $(MAIN).opt
- @echo " HELENA -u $(INPUT)"
- $(H)./$(MAIN).opt -u -S 1 $(O) $(INPUT) > log.txt
+ @echo " HELENA -r -u $(INPUT)"
+ $(H)./$(MAIN).opt -r -u -S 1 $(O) $(INPUT) > log.txt
hal: $(MAIN).opt
@echo " HELENA -m $(INPUT)"
-Helena 0.8.0 M
+Helena 0.8.1 M
* type "make" or "make opt" to compile the native executable
type 'bind entry = int * uri * 'bind (* age, uri, binder *)
type 'bind entity = 'bind entry option
+
+type 'a uri_generator = (string -> 'a) -> string -> 'a
module U = NUri
module H = Hierarchy
+type 'a out = (unit -> 'a) -> string -> 'a
+
(* internal functions *******************************************************)
let base = "xml"
(* interface functions ******************************************************)
-let export_entity export_entry si g = function
+let old_export_entity export_entry si g = function
| Some entry ->
let _, uri, bind = entry in
let path = path_of_uri uri in
pp_head pp_doctype (open_entry si g) export_entry entry close_entry;
close_out och
| None -> ()
+
+(****************************************************************************)
+(*
+let export_entity export_entry si g = function
+ | Some entry ->
+ let _, uri, bind = entry in
+ let path = path_of_uri root uri in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
+ let och = open_out (path ^ obj_ext) in
+ let out f s = output_string och s; f () in
+ let f () = close_out och in
+
+ Format.fprintf frm "@[<v>%t%t%t%a%t@]@."
+ 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_______________________________________________________________ *)
+type 'a out = (unit -> 'a) -> string -> 'a
+(*
val export_entity:
+ ('a och -> string -> 'bind Entity.entry -> 'a) ->
+ string -> bool -> Hierarchy.graph -> 'bind Entity.entity -> 'a
+*)
+val old_export_entity:
(Format.formatter -> 'bind Entity.entry -> unit) ->
bool -> Hierarchy.graph -> 'bind Entity.entity -> unit
--- /dev/null
+drg drgAut
--- /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: dual, relative, global *)
+(* note : fragment of dual lambda-delta serving as abstract layer *)
+
+type uri = Entity.uri
+type id = Entity.id
+
+type attr = Name of id * bool (* name, real? *)
+ | Priv (* private global definition *)
+
+type attrs = attr list (* attributes *)
+
+type bind = Abst of attrs * term (* attrs, domain *)
+ | Abbr of attrs * term (* attrs, body *)
+ | Void of attrs (* attrs *)
+
+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, domain, element *)
+ | Proj of attrs * lenv * term (* attrs, closure, scope *)
+ | Appl of attrs * term list * term (* attrs, arguments, function *)
+ | Bind of bind * term (* binder, scope *)
+
+and lenv = bind list (* local environment *)
+
+type entry = bind Entity.entry (* age, uri, binder *)
+
+type entity = bind Entity.entity
+
+(* helpers ******************************************************************)
+
+let mk_uri root f s =
+ let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
+ f str
+
+let rec name_of err f = function
+ | Name (n, r) :: _ -> f n r
+ | _ :: tl -> name_of err f tl
+ | [] -> err ()
+
+let name_of_binder err f = function
+ | Abst (a, _) -> name_of err f a
+ | Abbr (a, _) -> name_of err f a
+ | Void a -> name_of err f a
+
+let resolve_lref err f id lenv =
+ let rec aux f i = function
+ | [] -> err ()
+ | b :: tl ->
+ let err () = aux f (succ i) tl in
+ let f name _ = if name = id then f i else err () in
+ name_of_binder err f b
+ in
+ aux f 0 lenv
--- /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 H = U.UriHash
+module C = Cps
+module E = Entity
+module A = Aut
+module D = Drg
+
+(* qualified identifier: uri, name, qualifiers *)
+type qid = D.uri * D.id * D.id list
+
+type environment = D.lenv H.t
+
+type context_node = qid option (* context node: None = root *)
+
+type 'b status = {
+ henv: environment; (* optimized global environment *)
+ path: D.id list; (* current section path *)
+ hcnt: environment; (* optimized context *)
+ node: context_node; (* current context node *)
+ nodes: context_node list; (* context node list *)
+ line: int; (* line number *)
+ mk_uri:'b E.uri_generator (* uri generator *)
+}
+
+type resolver = Local of int
+ | Global of D.lenv
+
+let hsize = 7000 (* hash tables initial size *)
+
+(* Internal functions *******************************************************)
+
+let initial_status size mk_uri = {
+ path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri;
+ henv = H.create size; hcnt = H.create size
+}
+
+let mk_lref f i = f (D.LRef ([], i))
+
+let mk_abst id w = D.Abst ([D.Name (id, true)], w)
+
+let id_of_name (id, _, _) = id
+
+let mk_qid f st id path =
+ let str = String.concat "/" path in
+ let str = Filename.concat str id in
+ let f str = f (U.uri_of_string str, id, path) in
+ st.mk_uri f str
+
+let uri_of_qid (uri, _, _) = uri
+
+let complete_qid f st (id, is_local, qs) =
+ let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
+ let rec skip f = function
+ | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
+ | _ :: ptl, _ :: _ -> skip f (ptl, qs)
+ | _ -> f []
+ in
+ if is_local then f st.path else skip f (st.path, qs)
+
+let relax_qid f st (_, id, path) =
+ let f = function
+ | _ :: tl -> C.list_rev (mk_qid f st id) tl
+ | [] -> assert false
+ in
+ C.list_rev f path
+
+let relax_opt_qid f st = function
+ | None -> f None
+ | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
+
+let resolve_gref err f st qid =
+ try let cnt = H.find st.henv (uri_of_qid qid) in f qid cnt
+ with Not_found -> err ()
+
+let resolve_gref_relaxed f st qid =
+ let rec err () = relax_qid (resolve_gref err f st) st qid in
+ resolve_gref err f st qid
+
+let get_cnt err f st = function
+ | None -> f []
+ | Some qid as node ->
+ try let cnt = H.find st.hcnt (uri_of_qid qid) in f cnt
+ with Not_found -> err node
+
+let get_cnt_relaxed f st =
+ let rec err node = relax_opt_qid (get_cnt err f st) st node in
+ get_cnt err f st st.node
+
+let rec xlate_term f st lenv = function
+ | A.Sort s ->
+ let f h = f (D.Sort ([], h)) in
+ if s then f 0 else f 1
+ | A.Appl (v, t) ->
+ let f vv tt = f (D.Appl ([], [vv], tt)) in
+ let f vv = xlate_term (f vv) st lenv t in
+ xlate_term f st lenv v
+ | A.Abst (name, w, t) ->
+ let f ww =
+ let b = mk_abst name ww in
+ let f tt = f (D.Bind (b, tt)) in
+ xlate_term f st (b :: lenv) t
+ in
+ xlate_term f st lenv w
+ | A.GRef (name, args) ->
+ let g qid cnt =
+ let map1 f = xlate_term f st lenv in
+ let map2 f b =
+ let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in
+ D.name_of_binder C.err f b
+ in
+ let f tail =
+ let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
+ let f cnt = C.list_rev_map_append f map2 cnt ~tail in
+ C.list_sub_strict f cnt args
+ in
+ C.list_map f map1 args
+ in
+ let g qid = resolve_gref_relaxed g st qid in
+ let err () = complete_qid g st name in
+ D.resolve_lref err (mk_lref f) (id_of_name name) lenv
+
+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 ->
+ begin match st.path, st.nodes with
+ | _ :: ptl, nhd :: ntl ->
+ f {st with path = ptl; node = nhd; nodes = ntl} None
+ | _ -> assert false
+ end
+ | A.Context None ->
+ f {st with node = None} None
+ | A.Context (Some name) ->
+ let f name = f {st with node = Some name} None in
+ complete_qid f st name
+ | A.Block (name, w) ->
+ let f qid =
+ let f cnt =
+ let f ww =
+ H.add st.hcnt (uri_of_qid qid) (mk_abst name ww :: cnt);
+ f {st with node = Some qid} None
+ in
+ xlate_term f st cnt w
+ in
+ get_cnt_relaxed f st
+ in
+ complete_qid f st (name, true, [])
+ | A.Decl (name, w) ->
+ let f cnt =
+ let f qid =
+ let f ww =
+ let b = D.Abst ([], D.Proj ([], cnt, ww)) in
+ let entry = st.line, uri_of_qid qid, b in
+ H.add st.henv (uri_of_qid qid) cnt;
+ f {st with line = succ st.line} (Some entry)
+ in
+ xlate_term f st cnt w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_cnt_relaxed f st
+ | A.Def (name, w, trans, v) ->
+ let f cnt =
+ let f qid =
+ let f ww vv =
+ let a = if trans then [] else [D.Priv] in
+ let b = D.Abbr (a, D.Proj ([], cnt, D.Cast ([], ww, vv))) in
+ let entry = st.line, uri_of_qid qid, b in
+ H.add st.henv (uri_of_qid qid) cnt;
+ f {st with line = succ st.line} (Some entry)
+ in
+ let f ww = xlate_term (f ww) st cnt v in
+ xlate_term f st cnt w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_cnt_relaxed f st
+
+(* Interface functions ******************************************************)
+
+let initial_status mk_uri =
+ initial_status hsize mk_uri
+
+let drg_of_aut = xlate_entity
--- /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 'a status
+
+val initial_status: 'a Entity.uri_generator -> 'a status
+
+val drg_of_aut: ('a status -> Drg.entity -> 'a) ->
+ 'a status -> Aut.entity -> 'a
+++ /dev/null
-parsed : 0.7
-intermediate: 1.6
-untrusted : 0.4
-trusted : 6.5 + 3 with upsilon relocations
-------------------
-total : 9.2
+++ /dev/null
-Type Error (line 366)
-In the context
-a : Prop
-b : [x:a1].Prop
-a1 : (a1).(b).$ld:/l/and
-not a function
-(a1).(b).(a).$ld:/l/ande2
-
| BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity}
let export_entity si g = function
- | BrgEntity entity -> G.export_entity BrgO.export_entry si g entity
+ | BrgEntity entity -> G.old_export_entity BrgO.export_entry si g entity
| BagEntity _ -> ()
let type_check f st si g k =
let main =
try
- let version_string = "Helena 0.8.0 M - September 2009" in
+ let version_string = "Helena 0.8.1 M - September 2009" in
let stage = ref 3 in
let moch = ref None in
let meta = ref false in
let process = ref false in
let use_cover = ref true in
let si = ref false in
+ let cc = ref false in
let export = ref false in
let graph = ref (H.graph_of_string C.err C.start "Z2") in
let set_hierarchy s =
let help_S = "<number> set summary level (see above)" in
let help_V = " show version information" in
- let help_c = " disable initial segment of URI hierarchy" in
+ let help_c = " output conversion constraints" in
let help_h = "<string> set type hierarchy (default: Z2)" in
let help_i = " show local references by index" in
let help_j = " show URI of processed kernel objects" in
let help_k = "<string> set kernel version (default: brg)" in
let help_m = " output intermediate representation (HAL)" in
let help_p = " preprocess Automath source" in
- let help_u = " activate sort inclusion" in
+ let help_r = " disable initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
+ let help_u = " activate sort inclusion" in
let help_x = " export kernel objects (XML)" in
L.box 0; L.box_err ();
H.set_sorts ignore ["Set"; "Prop"] 0;
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
- ("-c", Arg.Clear use_cover, help_c);
+ ("-c", Arg.Set cc, help_c);
("-h", Arg.String set_hierarchy, help_h);
("-i", Arg.Set O.indexes, help_i);
("-j", Arg.Set progress, help_j);
("-k", Arg.String set_kernel, help_k);
("-m", Arg.Set meta, help_m);
("-p", Arg.Set process, help_p);
- ("-u", Arg.Set si, help_u);
+ ("-r", Arg.Clear use_cover, help_r);
("-s", Arg.Int set_stage, help_s);
+ ("-u", Arg.Set si, help_u);
("-x", Arg.Set export, help_x)
] read_file help;
with BagT.TypeError msg -> bag_error "Type Error" msg
projects / helm.git / commitdiff