From f7bb626faf6b9d89c0ee5ac48b1d97c69d189f8a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Oct 2009 20:05:02 +0000 Subject: [PATCH] we enabled the new style xml exportation, in particular for dual_rg --- helm/software/lambda-delta/.depend.opt | 30 ++--- helm/software/lambda-delta/Makefile | 15 ++- helm/software/lambda-delta/basic_ag/bag.ml | 5 + helm/software/lambda-delta/basic_rg/brg.ml | 5 + helm/software/lambda-delta/common/entity.ml | 21 ++++ helm/software/lambda-delta/common/library.ml | 40 +++---- helm/software/lambda-delta/common/library.mli | 8 +- helm/software/lambda-delta/dual_rg/drg.ml | 21 +++- helm/software/lambda-delta/dual_rg/drgAut.ml | 10 +- .../lambda-delta/dual_rg/drgOutput.ml | 110 ++++++++++++------ .../lambda-delta/dual_rg/drgOutput.mli | 2 +- helm/software/lambda-delta/lib/cps.ml | 4 +- helm/software/lambda-delta/lib/time.ml | 4 +- helm/software/lambda-delta/toplevel/top.ml | 14 ++- 14 files changed, 197 insertions(+), 92 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index a7c69ab8d..eb479838e 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -117,10 +117,10 @@ basic_rg/brgUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ dual_rg/drg.cmo: common/entity.cmx dual_rg/drg.cmx: common/entity.cmx dual_rg/drgOutput.cmi: common/library.cmi dual_rg/drg.cmx -dual_rg/drgOutput.cmo: common/library.cmi dual_rg/drg.cmx \ - dual_rg/drgOutput.cmi -dual_rg/drgOutput.cmx: common/library.cmx dual_rg/drg.cmx \ - dual_rg/drgOutput.cmi +dual_rg/drgOutput.cmo: lib/nUri.cmi common/library.cmi common/hierarchy.cmi \ + common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi +dual_rg/drgOutput.cmx: lib/nUri.cmx common/library.cmx common/hierarchy.cmx \ + common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi 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 @@ -155,17 +155,19 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \ common/library.cmi common/hierarchy.cmi common/entity.cmx \ - dual_rg/drgAut.cmi dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.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 + dual_rg/drgOutput.cmi dual_rg/drgAut.cmi dual_rg/drg.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.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 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 toplevel/meta.cmx lib/log.cmx \ common/library.cmx common/hierarchy.cmx common/entity.cmx \ - dual_rg/drgAut.cmx dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.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 + dual_rg/drgOutput.cmx dual_rg/drgAut.cmx dual_rg/drg.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.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 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 653898fb2..dacc62f6c 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -6,7 +6,7 @@ KEEP = README automath/*.aut CLEAN = etc/log.txt -TAGS = test test-si test-si-fast hal xml-si +TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old XMLS = xml/grundlagen/l/not.ld.xml xml/grundlagen/l/et.ld.xml \ xml/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ @@ -31,13 +31,18 @@ test-si-fast: $(MAIN).opt $(H)./$(MAIN).opt -o -r -u -S 1 $(O) $(INPUT) > etc/log.txt hal: $(MAIN).opt - @echo " HELENA -o -m $(INPUT)" - $(H)./$(MAIN).opt -o -m -s 1 -S 1 $(INPUT) > etc/log.txt + @echo " HELENA -o -x -m $(INPUT)" + $(H)./$(MAIN).opt -o -x -m -s 1 -S 1 $(INPUT) > etc/log.txt -xml-si: $(MAIN).opt - @echo " HELENA -o -u -x $(INPUT)" +xml-si-old: $(MAIN).opt + @echo " HELENA -o -u -x -s 2 $(INPUT)" $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt +xml-si-drg: $(MAIN).opt + @echo " HELENA -u -x -s 1 $(INPUT)" + $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt + + %.ld: BASEURL = --stringparam baseurl $(LDDLURL) %.ld: diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index cd8d493f5..8a07f55a8 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -32,6 +32,11 @@ type lenv = (int * id * bind) list (* location, name, binder *) type message = (lenv, term) Log.item list +(* helpers ******************************************************************) + +let mk_uri root s = + String.concat "/" ["ld:"; "bag"; root; s ^ ".ld"] + (* Currified constructors ***************************************************) let abst w = Abst w diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 373f5342f..baa83afed 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -33,6 +33,11 @@ type lenv = Null (* Cons: tail, relative local environment, binder *) | Cons of lenv * lenv option * bind +(* helpers ******************************************************************) + +let mk_uri root s = + String.concat "/" ["ld:"; "brg"; root; s ^ ".ld"] + (* Currified constructors ***************************************************) let abst a w = Abst (a, w) diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 4a16c77e7..3aa1ef6b5 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -33,6 +33,27 @@ let rec name err f = function | _ :: tl -> name err f tl | [] -> err () +let names f map l a = + let rec aux f i a = function + | [] -> f a + | Name (n, r) :: tl -> aux (map f i n r) false a tl + | _ :: tl -> aux f i a tl + in + aux f true a l + +let rec get_name err f j = function + | [] -> err () + | Name (n, r) :: _ when j = 0 -> f n r + | Name _ :: tl -> get_name err f (pred j) tl + | _ :: tl -> get_name err f j tl + +let rec get_names f = function + | [] -> f [] [] + | Name _ as n :: tl -> + let f a ns = f a (n :: ns) in get_names f tl + | e :: tl -> + let f a = f (e :: a) in get_names f tl + let rec apix err f = function | Apix i :: _ -> f i | _ :: tl -> apix err f tl diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 4951e8c60..ff4c54198 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -87,7 +87,7 @@ type och = string -> unit type attr = string * string -type 'a pp = (och -> int -> 'a) -> och -> int -> 'a +type pp = och -> int -> unit let attribute out (name, contents) = if contents <> "" then begin @@ -103,14 +103,14 @@ let xml out version encoding = let doctype out root system = out "\n\n" -let tag tag attrs ?contents f out indent = +let tag tag attrs ?contents out indent = let spc = String.make indent ' ' in - out spc; out "<"; out "tag"; List.iter (attribute out) attrs; + out spc; out "<"; out tag; List.iter (attribute out) attrs; match contents with - | None -> out "/>\n"; f out indent - | Some cont -> - let f _ _ = out spc; out "\n"; f out indent in - cont f out (indent + 3) + | None -> out "/>\n" + | Some cont -> + out ">\n"; cont out (indent + 3); out spc; + out "\n" let sort = "Sort" @@ -145,28 +145,27 @@ let arity n = "arity", contents let name a = - let err () = "name", "" in - let f s = function - | true -> "name", s - | false -> "name", ("^" ^ s) - in - Y.name err f a + let map f i n r s = + let n = if r then n else "^" ^ n in + let spc = if i then "" else " " in + f (s ^ n ^ spc) + in + let f s = "name", s in + Y.names f map a "" let mark a = let err () = "mark", "" in let f i = "mark", string_of_int i in Y.mark err f a -let export_entity f pp_term si g (a, uri, b) = - let path = path_of_uri uri in +let export_entity pp_term si g (a, u, b) = + let path = path_of_uri u in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in let och = open_out (path ^ obj_ext) in let out = output_string och in - let f _ _ = close_out och; f () in xml out "1.0" "UTF-8"; doctype out root system; - let str = U.string_of_uri uri in - let a = Y.Name (U.name_of_uri uri, true) :: a in - let attrs = ["uri", str; name a] in + let a = Y.Name (U.name_of_uri u, true) :: a in + let attrs = [uri u; name a; mark a] in let contents = match b with | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) @@ -174,4 +173,5 @@ let export_entity f pp_term si g (a, uri, b) = let opts = if si then "si" else "" in let shp = H.string_of_graph C.start g in let attrs = ["hierarchy", shp; "options", opts] in - tag root attrs ~contents f out 0; + tag root attrs ~contents out 0; + close_out och diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 95d5ba9b1..f364af329 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -13,13 +13,13 @@ type och = string -> unit type attr = string * string -type 'a pp = (och -> int -> 'a) -> och -> int -> 'a +type pp = och -> int -> unit val export_entity: - (unit ->'a) -> ('term -> 'a pp) -> - bool -> Hierarchy.graph -> 'term Entity.entity -> 'a + ('term -> pp) -> + bool -> Hierarchy.graph -> 'term Entity.entity -> unit -val tag: string -> attr list -> ?contents:'a pp -> 'a pp +val tag: string -> attr list -> ?contents:pp -> pp val sort: string diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index d44029615..ac4021c08 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -41,7 +41,15 @@ let mk_uri root s = let empty_lenv = ESort -let push f lenv a b = f (EBind (lenv, a, b)) +let push_bind f lenv a b = f (EBind (lenv, a, b)) + +let push_proj f lenv a e = f (EProj (lenv, a, e)) + +let push2 err f lenv attr ?t = match lenv, t with + | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws))) + | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs))) + | EBind (e, a, Void n), None -> f (EBind (e, (attr :: a), Void (succ n))) + | _ -> err () (* this id not tail recursive *) let resolve_lref err f id lenv = @@ -54,3 +62,14 @@ let resolve_lref err f id lenv = | EProj _ -> assert false (* TODO *) in aux f 0 0 lenv + +let rec get_name err f i j = function + | ESort -> err i + | EBind (_, a, _) when i = 0 -> + let err () = err i in + Entity.get_name err f j a + | EBind (tl, _, _) -> + get_name err f (pred i) j tl + | EProj (tl, _, e) -> + let err i = get_name err f i j tl in + get_name err f i j e diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index aaf9d20c7..bf42cc2ab 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -53,7 +53,7 @@ let add_abst (a, ws) id w = Y.Name (id, true) :: a, w :: ws let lenv_of_cnt (a, ws) = - D.push C.start D.empty_lenv a (D.Abst ws) + D.push_bind C.start D.empty_lenv a (D.Abst ws) let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) @@ -121,18 +121,22 @@ let rec xlate_term f st lenv = function let a, b = [Y.Name (name, true)], (D.Abst [ww]) in let f tt = f (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in - D.push f lenv a b + D.push_bind f lenv a b in xlate_term f st lenv w | A.GRef (name, args) -> let g qid (a, _) = + let gref = D.TGRef ([], uri_of_qid qid) in let map1 f = xlate_term f st lenv in let map2 f = function | Y.Name (id, _) -> D.resolve_lref Cps.err (mk_lref f) id lenv | _ -> assert false in let f tail = - let f args = f (D.TAppl ([], args, D.TGRef ([], uri_of_qid qid))) in + let f = function + | [] -> f gref + | args -> f (D.TAppl ([], args, gref)) + in let f a = C.list_rev_map_append f map2 a ~tail in C.list_sub_strict f a args in diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml index 2522b59f1..17def3850 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.ml +++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml @@ -9,55 +9,93 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module U = NUri +module C = Cps +module H = Hierarchy +module Y = Entity module X = Library module D = Drg -(* this is not tail recursive *) -let rec list_iter map l f = match l with - | [] -> f - | hd :: tl -> map hd (list_iter map tl f) - -let rec lenv_iter map1 map2 l f = match l with - | D.ESort -> f - | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f) - | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f) - -(* these are not tail recursive *) -let rec exp_term t f = match t with - | D.TSort (a, h) -> - let attrs = [X.position h; X.name a] in - X.tag X.sort attrs f +let list_iter map l out tab = + let rec aux f = function + | [] -> f () + | hd :: tl -> aux (fun () -> map hd out tab; f ()) tl + in + aux C.start l + +let list_rev_iter map e ns l out tab = + let rec aux err f e = function + | [], [] -> f e + | n :: ns, hd :: tl -> + let f e = map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) in + aux err f e (ns, tl) + | _ -> err () + in + ignore (aux C.err C.start e (ns, l)) + +let lenv_iter map1 map2 l out tab = + let rec aux f = function + | D.ESort -> f () + | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv + | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv + in + aux C.start l + +let rec exp_term e t out tab = match t with + | D.TSort (a, l) -> + let a = + let err _ = a in + let f s = Y.Name (s, true) :: a in + H.get_sort err f l + in + let attrs = [X.position l; X.name a] in + X.tag X.sort attrs out tab | D.TLRef (a, i, j) -> + let a = + let err _ = a in + let f n r = Y.Name (n, r) :: a in + D.get_name err f i j e + in let attrs = [X.position i; X.offset j; X.name a] in - X.tag X.lref attrs f + X.tag X.lref attrs out tab | D.TGRef (a, n) -> + let a = Y.Name (U.name_of_uri n, true) :: a in let attrs = [X.uri n; X.name a] in - X.tag X.gref attrs f + X.tag X.gref attrs out tab | D.TCast (a, u, t) -> let attrs = [] in - X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u) + X.tag X.cast attrs ~contents:(exp_term e u) out tab; + exp_term e t out tab | D.TAppl (a, vs, t) -> let attrs = [X.arity (List.length vs)] in - X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs) + X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; + exp_term e t out tab | D.TProj (a, lenv, t) -> let attrs = [] in - X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv) + X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; + exp_term (D.push_proj C.start e a lenv) t out tab | D.TBind (a, b, t) -> - exp_bind a b (exp_term t f) - -and exp_bind a b f = match b with - | D.Abst ws -> - let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in - X.tag X.abst attrs f ~contents:(list_iter exp_term ws) - | D.Abbr vs -> - let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in - X.tag X.abbr attrs f ~contents:(list_iter exp_term vs) - | D.Void n -> - let attrs = [X.name a; X.mark a; X.arity n] in - X.tag X.void attrs f - -and exp_eproj a lenv f = + exp_bind e a b out tab; + exp_term (D.push_bind C.start e a b) t out tab + +and exp_bind e a b out tab = + let f a ns = a, ns in + let a, ns = Y.get_names f a in + match b with + | D.Abst ws -> + let e = D.push_bind C.start e a (D.Abst []) in + let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in + X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab + | D.Abbr vs -> + let e = D.push_bind C.start e a (D.Abbr []) in + let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in + X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab + | D.Void n -> + let attrs = [X.name a; X.mark a; X.arity n] in + X.tag X.void attrs out tab + +and exp_eproj e a lenv out tab = let attrs = [] in - X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv) + X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab -let export_term = exp_term +let export_term = exp_term D.empty_lenv diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.mli b/helm/software/lambda-delta/dual_rg/drgOutput.mli index a1b9e6925..cceeba195 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.mli +++ b/helm/software/lambda-delta/dual_rg/drgOutput.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val export_term: Drg.term -> 'a Library.pp +val export_term: Drg.term -> Library.pp diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index aa0dbc7c1..10ec62376 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -69,9 +69,7 @@ let list_iter2 f map l1 l2 = let rec list_fold_right f map l a = match l with | [] -> f a - | hd :: tl -> - let f a = map f hd a in - list_fold_right f map tl a + | hd :: tl -> list_fold_right (map f hd) map tl a let list_map f map l = let map f hd a = diff --git a/helm/software/lambda-delta/lib/time.ml b/helm/software/lambda-delta/lib/time.ml index 13a4c0aba..42d7d39a7 100644 --- a/helm/software/lambda-delta/lib/time.ml +++ b/helm/software/lambda-delta/lib/time.ml @@ -18,7 +18,7 @@ let utime_stamp = let times = Unix.times () in let stamp = times.Unix.tms_utime in let lap = stamp -. !old in - L.warn (P.sprintf "UTC STAMP (%s): %f (%f)" msg stamp lap); + L.warn (P.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap); old := stamp let gmtime msg = @@ -30,5 +30,5 @@ let gmtime msg = let m = gmt.Unix.tm_min in let s = gmt.Unix.tm_sec in L.warn ( - P.sprintf "UTC STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s + P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s ) diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 4c1ee1903..3558dc8d0 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -24,6 +24,7 @@ module DA = DrgAut module MA = MetaAut module MO = MetaOutput module ML = MetaLibrary +module DrgO = DrgOutput module MBrg = MetaBrg module BrgO = BrgOutput module BrgR = BrgReduction @@ -97,13 +98,14 @@ let count_entity st = function | _ -> st let export_entity si g moch = function + | DrgEntity e -> X.export_entity DrgO.export_term si g e | BrgEntity e -> X.old_export_entity BrgO.export_term si g e | MetaEntity e -> begin match moch with | None -> () | Some och -> ML.write_entity C.start och e end - | _ -> () + | BagEntity _ -> () let type_check f st si g k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in @@ -144,7 +146,7 @@ let process_2 f st entity = let process_1 f st entity = let st = count_entity st entity in - export_entity !si !graph !moch entity; + if !export && !stage = 1 then export_entity !si !graph !moch entity; if !stage > 1 then xlate (process_2 f) st entity else f st let process_0 f st entity = @@ -205,6 +207,12 @@ try close_in ich; if !L.level > 0 then T.utime_stamp "parsed"; O.clear_reductions (); + let mk_uri = + if !stage < 2 then Drg.mk_uri else + match !kernel with + | Brg -> Brg.mk_uri + | Bag -> Bag.mk_uri + in let cover = if !use_cover then base_name else "" in let f st = if !L.level > 0 then T.utime_stamp "processed"; @@ -214,7 +222,7 @@ try if !L.level > 2 && !stage > 1 then print_counters st; if !L.level > 2 && !stage > 1 then O.print_reductions () in - process f book (initial_status Drg.mk_uri cover) + process f book (initial_status mk_uri cover) in let exit () = close !moch; -- 2.39.2