-lib/nUri.cmi:
lib/nUri.cmo: lib/nUri.cmi
lib/nUri.cmx: lib/nUri.cmi
-lib/cps.cmo:
-lib/cps.cmx:
-lib/share.cmo:
-lib/share.cmx:
-lib/log.cmi:
lib/log.cmo: lib/cps.cmx lib/log.cmi
lib/log.cmx: lib/cps.cmx lib/log.cmi
lib/time.cmo: lib/log.cmi
lib/time.cmx: lib/log.cmx
-automath/aut.cmo:
-automath/aut.cmx:
automath/autProcess.cmi: automath/aut.cmx
automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi
automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi
automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi
automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi
automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx
-common/hierarchy.cmi:
common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi
common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi
-common/output.cmi:
common/output.cmo: lib/log.cmi common/output.cmi
common/output.cmx: lib/log.cmx common/output.cmi
common/entity.cmo: lib/nUri.cmi automath/aut.cmx
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/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
+ 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
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/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
+ 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
INPUT-ORIG = automath/grundlagen-orig.aut
test: $(MAIN).opt
- @echo " HELENA -p -r $(INPUT)"
- $(H)./$(MAIN).opt -p -r -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -o -p -r $(INPUT)"
+ $(H)./$(MAIN).opt -o -p -r -S 3 $(O) $(INPUT) > etc/log.txt
test-si: $(MAIN).opt
- @echo " HELENA -p -r -u $(INPUT)"
- $(H)./$(MAIN).opt -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -o -p -r -u $(INPUT)"
+ $(H)./$(MAIN).opt -o -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt
test-si-fast: $(MAIN).opt
- @echo " HELENA -r -u $(INPUT)"
- $(H)./$(MAIN).opt -r -u -S 1 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -o -r -u $(INPUT)"
+ $(H)./$(MAIN).opt -o -r -u -S 1 $(O) $(INPUT) > etc/log.txt
hal: $(MAIN).opt
- @echo " HELENA -m $(INPUT)"
- $(H)./$(MAIN).opt -m -s 1 -S 1 $(INPUT) > etc/log.txt
+ @echo " HELENA -o -m $(INPUT)"
+ $(H)./$(MAIN).opt -o -m -s 1 -S 1 $(INPUT) > etc/log.txt
xml-si: $(MAIN).opt
- @echo " HELENA -u -x $(INPUT)"
- $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
+ @echo " HELENA -o -u -x $(INPUT)"
+ $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
-type 'a uri_generator = (string -> 'a) -> string -> 'a
+type uri_generator = string -> string (* this could be in CPS *)
(* helpers ******************************************************************)
| Abbr of term list (* bodies *)
| Void of int (* number of exclusions *)
-and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int * int (* attrs, position indexes *)
- | GRef of attrs * uri (* attrs, reference *)
- | Cast of attrs * term * term (* attrs, domain, element *)
- | Appl of attrs * term list * term (* attrs, arguments, function *)
- | Proj of attrs * lenv * term (* attrs, closure, member *)
- | Bind of attrs * bind * term (* attrs, binder, scope *)
-
-and lenv = Null
- | Cons of lenv * attrs * bind (* closure, attrs, binder *)
+and term = TSort of attrs * int (* attrs, hierarchy index *)
+ | TLRef of attrs * int * int (* attrs, position indexes *)
+ | TGRef of attrs * uri (* attrs, reference *)
+ | TCast of attrs * term * term (* attrs, domain, element *)
+ | TAppl of attrs * term list * term (* attrs, arguments, function *)
+ | TProj of attrs * lenv * term (* attrs, closure, member *)
+ | TBind of attrs * bind * term (* attrs, binder, scope *)
+
+and lenv = ESort (* top *)
+ | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
+ | EBind of lenv * attrs * bind (* environment, attrs, binder *)
type entity = term Entity.entity
(* helpers ******************************************************************)
-let mk_uri root f s =
- let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
- f str
+let mk_uri root s =
+ String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"]
-let empty_lenv = Null
+let empty_lenv = ESort
-let push f lenv a b = f (Cons (lenv, a, b))
+let push f lenv a b = f (EBind (lenv, a, b))
let resolve_lref err f id lenv =
let rec aux f i k = function
- | Null -> err ()
- | Cons (tl, a, _) ->
+ | ESort -> err ()
+ | EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
let f j = f i j k in
Entity.resolve err f id a
+ | EProj _ -> assert false (* TODO *)
in
aux f 0 0 lenv
type context_node = qid option (* context node: None = root *)
-type 'a status = {
+type 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:'a Y.uri_generator (* uri generator *)
+ mk_uri:Y.uri_generator (* uri generator *)
}
type resolver = Local of int
let lenv_of_cnt (a, ws) =
D.push C.start D.empty_lenv a (D.Abst ws)
-let mk_lref f i j k = f (D.LRef ([Y.Apix k], i, j))
+let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
let id_of_name (id, _, _) = id
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
+ f (st.mk_uri str)
let uri_of_qid (uri, _, _) = uri
let rec xlate_term f st lenv = function
| A.Sort s ->
- let f h = f (D.Sort ([], h)) in
+ let f h = f (D.TSort ([], 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 tt = f (D.TAppl ([], [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 a, b = [Y.Name (name, true)], (D.Abst [ww]) in
- let f tt = f (D.Bind (a, b, tt)) 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
in
| _ -> assert false
in
let f tail =
- let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
+ let f args = f (D.TAppl ([], args, D.TGRef ([], uri_of_qid qid))) in
let f a = C.list_rev_map_append f map2 a ~tail in
C.list_sub_strict f a args
in
let f qid =
let f ww =
H.add st.henv (uri_of_qid qid) cnt;
- let b = Y.Abst (D.Bind (a, D.Abst ws, ww)) in
+ let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in
let entity = [Y.Mark st.line], uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
let f qid =
let f ww vv =
H.add st.henv (uri_of_qid qid) cnt;
- let b = Y.Abbr (D.Bind (a, D.Abst ws, D.Cast ([], ww, vv))) in
+ let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in
let a =
if trans then [Y.Mark st.line] else [Y.Mark st.line; Y.Priv]
in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type 'a status
+type status
-val initial_status: 'a Entity.uri_generator -> 'a status
+val initial_status: Entity.uri_generator -> status
-val drg_of_aut: ('a status -> 'a) -> ('a status -> Drg.entity -> 'a) ->
- 'a status -> Aut.entity -> 'a
+val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) ->
+ status -> Aut.entity -> 'a
| [] -> f
| hd :: tl -> map hd (list_iter map tl f)
-let rec lenv_iter map l f = match l with
- | D.Null -> f
- | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b 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)
let rec exp_term t f = match t with
- | D.Sort (a, h) ->
+ | D.TSort (a, h) ->
let attrs = [X.position h; X.name a] in
X.tag X.sort attrs f
- | D.LRef (a, i, j) ->
+ | D.TLRef (a, i, j) ->
let attrs = [X.position i; X.offset j; X.name a] in
X.tag X.lref attrs f
- | D.GRef (a, n) ->
+ | D.TGRef (a, n) ->
let attrs = [X.uri n; X.name a] in
X.tag X.gref attrs f
- | D.Cast (a, u, t) ->
+ | D.TCast (a, u, t) ->
let attrs = [] in
X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
- | D.Appl (a, vs, t) ->
+ | 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)
- | D.Proj (a, lenv, t) ->
+ | D.TProj (a, lenv, t) ->
let attrs = [] in
- X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
- | D.Bind (a, b, t) ->
- exp_lenv a b (exp_term t f)
+ X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv)
+ | D.TBind (a, b, t) ->
+ exp_bind a b (exp_term t f)
-and exp_lenv a b f = match b with
+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)
let attrs = [X.name a; X.mark a; X.arity n] in
X.tag X.void attrs f
+and exp_eproj a lenv f =
+ let attrs = [] in
+ X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv)
+
let export_term = exp_term
module X = Library
module AP = AutProcess
module AO = AutOutput
-(* module DA = DrgAut *)
+module DA = DrgAut
module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
module BagT = BagType
module BagU = BagUntrusted
-type 'a status = {
+type status = {
ast : AP.status;
-(* dst : 'a DA.status; *)
+ dst : DA.status;
mst : MA.status;
ac : AO.counters;
mc : MO.counters;
brgc = BrgO.initial_counters;
bagc = BagO.initial_counters;
mst = MA.initial_status ~cover ();
-(* dst = DA.initial_status (mk_uri cover); *)
+ dst = DA.initial_status (mk_uri cover);
ast = AP.initial_status
}
type kernel_entity = BrgEntity of Brg.entity
| BagEntity of Bag.entity
-(* | DrgEntity of Drg.entity *)
+ | DrgEntity of Drg.entity
| MetaEntity of Meta.entity
let kernel = ref Brg
| MetaEntity e -> {st with mc = count MO.count_entity st.mc e}
| BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e}
| BagEntity e -> {st with bagc = count BagO.count_entity st.bagc e}
-(* | _ -> st *)
+ | _ -> st
let export_entity si g moch = function
| BrgEntity e -> X.old_export_entity BrgO.export_term si g e
match k with
| BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
| BagEntity entity -> BagU.type_check ok ~si g entity
-(* | DrgEntity (a, u, _) *)
+ | DrgEntity (a, u, _)
| MetaEntity (a, u, _) -> f st a u
(****************************************************************************)
let moch = ref None
let meta = ref false
let progress = ref false
-let process = ref false
+let preprocess = ref false
let use_cover = ref true
let si = ref false
let cc = ref false
let export = ref false
let graph = ref (H.graph_of_string C.err C.start "Z2")
-let old = ref true
+let old = ref false
let process_3 f st a u =
if !progress then
export_entity !si !graph !moch entity;
if !stage > 1 then xlate (process_2 f) st entity else f st
-let rec process_0 f st = function
+let process_0 f st entity =
+ let f st entity =
+ if !stage = 0 then f st else
+ let frr mst = f {st with mst = mst} in
+ let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in
+ let err dst = f {st with dst = dst} in
+ let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in
+ if !old then MA.meta_of_aut frr h st.mst entity else
+ DA.drg_of_aut err g st.dst entity
+ in
+ let st = {st with ac = count AO.count_entity st.ac entity} in
+ if !preprocess then process_entity f st entity else f st entity
+
+let rec process f book st = match book with
| [] -> f st
- | entity :: tl ->
- let f st = process_0 f st tl in
- let frr st mst = {st with mst = mst} in
- let h st mst e =
- process_1 C.start {st with mst = mst} (MetaEntity e)
- in
- let f st entity =
- if !stage = 0 then f st else
-(* let err st dst = f {st with dst = dst} in
- let g st dst e = process_1 f {st with dst = dst} (DrgEntity e) in
- if !old then *) f (MA.meta_of_aut (frr st) (h st) st.mst entity) (* else
- DA.drg_of_aut (err st) (g st) st.dst entity *)
- in
- let st = {st with ac = count AO.count_entity st.ac entity} in
- if !process then process_entity f st entity else f st entity
+ | entity :: tl ->
+ process f tl (process_0 C.start st entity)
+(* process_0 (process f tl) st entity *) (* CPS variant of the above *)
(****************************************************************************)
let main =
try
- let version_string = "Helena 0.8.1 M - September 2009" in
+ let version_string = "Helena 0.8.1 M - October 2009" in
let set_hierarchy s =
let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in
let f g = graph := g in
let f st =
if !L.level > 0 then T.utime_stamp "processed";
if !L.level > 2 then AO.print_counters C.start st.ac;
- if !L.level > 2 && !process then AO.print_process_counters C.start st.ast;
+ if !L.level > 2 && !preprocess then AO.print_process_counters C.start st.ast;
if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
if !L.level > 2 && !stage > 1 then print_counters st;
if !L.level > 2 && !stage > 1 then O.print_reductions ()
in
- process_0 f (initial_status Drg.mk_uri cover) book
+ process f book (initial_status Drg.mk_uri cover)
in
let exit () =
close !moch;
flush_all ()
in
let help =
- "Usage: helena [ -Vcijmpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vcijmopux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
"Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
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_o = " use old abstract language instead of drg" in
let help_p = " preprocess Automath source" in
let help_r = " disable initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
("-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);
+ ("-o", Arg.Set old, help_o);
+ ("-p", Arg.Set preprocess, help_p);
("-r", Arg.Clear use_cover, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set si, help_u);
projects / helm.git / commitdiff