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
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
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 \
$(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:
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
(* 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)
| _ :: 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
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
let doctype out root system =
out "<!DOCTYPE "; out root; out " SYSTEM \""; out 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 "</"; out tag; 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 "</"; out tag; out ">\n"
let sort = "Sort"
"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)
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
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
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 =
| 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
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))
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
\ / 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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val export_term: Drg.term -> 'a Library.pp
+val export_term: Drg.term -> Library.pp
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 =
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 =
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
)
module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
+module DrgO = DrgOutput
module MBrg = MetaBrg
module BrgO = BrgOutput
module BrgR = BrgReduction
| _ -> 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
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 =
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";
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;
projects / helm.git / commitdiff