From: Ferruccio Guidi Date: Thu, 17 Sep 2009 20:40:11 +0000 (+0000) Subject: we start version 0.8.1 by replacing the abstract layer AST with a fragment of dual... X-Git-Tag: make_still_working~3457 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9f15ca61aac8089fb4b599af72533c4a432ba7b;p=helm.git we start version 0.8.1 by replacing the abstract layer AST with a fragment of dual lambda-delta. To this aim we begin the dual_rg kernel --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 8ee2db5d8..e235d685e 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -26,6 +26,44 @@ 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_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 @@ -66,44 +104,13 @@ basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.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/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 diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make index c9c8ff41a..5179d30aa 100644 --- a/helm/software/lambda-delta/Make +++ b/helm/software/lambda-delta/Make @@ -1 +1 @@ -lib automath common basic_rg basic_ag toplevel +lib automath common basic_ag basic_rg dual_rg toplevel diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 31b7b13b3..665972224 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -17,16 +17,16 @@ INPUT = automath/grundlagen.aut 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)" diff --git a/helm/software/lambda-delta/README b/helm/software/lambda-delta/README index 2f2f894fc..8a0f0d674 100644 --- a/helm/software/lambda-delta/README +++ b/helm/software/lambda-delta/README @@ -1,4 +1,4 @@ -Helena 0.8.0 M +Helena 0.8.1 M * type "make" or "make opt" to compile the native executable diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 78d7c3ace..cd780601a 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -15,3 +15,5 @@ type id = Aut.id type 'bind entry = int * uri * 'bind (* age, uri, binder *) type 'bind entity = 'bind entry option + +type 'a uri_generator = (string -> 'a) -> string -> 'a diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 8ef875ce7..1238c2739 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -13,6 +13,8 @@ module F = Filename module U = NUri module H = Hierarchy +type 'a out = (unit -> 'a) -> string -> 'a + (* internal functions *******************************************************) let base = "xml" @@ -42,7 +44,7 @@ let close_entry frm = (* 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 @@ -54,3 +56,20 @@ let export_entity export_entry si g = function 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 "@[%t%t%t%a%t@]@." + pp_head pp_doctype (open_entry si g) export_entry entry close_entry; + close_out och + | None -> () +*) diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 68325f3d9..bda10346d 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -9,6 +9,12 @@ \ / 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 diff --git a/helm/software/lambda-delta/dual_rg/Make b/helm/software/lambda-delta/dual_rg/Make new file mode 100644 index 000000000..5020307c3 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/Make @@ -0,0 +1 @@ +drg drgAut diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml new file mode 100644 index 000000000..1d94a2643 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -0,0 +1,65 @@ +(* + ||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 diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml new file mode 100644 index 000000000..c978c4a63 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -0,0 +1,195 @@ +(* + ||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 diff --git a/helm/software/lambda-delta/dual_rg/drgAut.mli b/helm/software/lambda-delta/dual_rg/drgAut.mli new file mode 100644 index 000000000..ea4e4b021 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/drgAut.mli @@ -0,0 +1,17 @@ +(* + ||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 diff --git a/helm/software/lambda-delta/performance.txt b/helm/software/lambda-delta/performance.txt deleted file mode 100644 index 5d674bd66..000000000 --- a/helm/software/lambda-delta/performance.txt +++ /dev/null @@ -1,6 +0,0 @@ -parsed : 0.7 -intermediate: 1.6 -untrusted : 0.4 -trusted : 6.5 + 3 with upsilon relocations ------------------- -total : 9.2 diff --git a/helm/software/lambda-delta/rt.txt b/helm/software/lambda-delta/rt.txt deleted file mode 100644 index a24b968e6..000000000 --- a/helm/software/lambda-delta/rt.txt +++ /dev/null @@ -1,8 +0,0 @@ -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 - diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index c3923b387..869b1386a 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -90,7 +90,7 @@ let count_entity st = function | 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 = @@ -107,7 +107,7 @@ 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 @@ -115,6 +115,7 @@ try 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 = @@ -212,15 +213,16 @@ try let help_S = " 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 = " 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 = " 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 = " 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; @@ -228,15 +230,16 @@ try 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