PREAMBLE_LP = lp/lp.template
test-si-fast: $(MAIN).opt etc
- @echo " HELENA -q -u -x -1 $(INPUTFAST)"
- $(H)./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) > etc/log.txt
+ @echo " HELENA -q -u -x -y -1 $(INPUTFAST)"
+ $(H)./$(MAIN).opt -T 1 -q -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt
test-si: $(MAIN).opt etc
@echo " HELENA -d -l -u -0 $(INPUT)"
test2: $(MAIN).opt etc
@echo " HELENA -T 2 -l $(INPUT)"
- $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l $(O) $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l -q -1 $(O) $(INPUT) > etc/log.txt
test3: $(MAIN).opt etc
@echo " HELENA -T 3 -l $(INPUT)"
$(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt
xml-si: $(MAIN).opt etc
- @echo " HELENA -l -o -s 1 -u $(INPUT)"
- $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -l -o -s 1 -u -y $(INPUT)"
+ $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u -y $(O) $(INPUT) > etc/log.txt
xml-si-v3: $(MAIN).opt etc
- @echo " HELENA -l -o -s 2 -u $(INPUT)"
- $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -l -o -s 2 -u -y $(INPUT)"
+ $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u -y $(O) $(INPUT) > etc/log.txt
xml: $(MAIN).opt etc
- @echo " HELENA -l -o -s 1 $(INPUT)"
- $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -l -o -s 1 -y $(INPUT)"
+ $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 -y $(O) $(INPUT) > etc/log.txt
xml-v3: $(MAIN).opt etc
@echo " HELENA -l -o -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(O) $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 -y $(O) $(INPUT) > etc/log.txt
export-coq coq/$(V): $(MAIN).opt etc
@echo " HELENA -l -m V8 -u $(INPUT)"
profile-fast: $(MAIN).opt etc
@echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)"
$(H)rm -f etc/log.txt
- $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x $(O) $(INPUTFAST) >> etc/log.txt; done
+ $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
profile: $(MAIN).opt etc
@echo " HELENA -l -u $(INPUT) (31 TIMES)"
$(H)rm -f etc/log.txt
- $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -u $(O) $(INPUT) >> etc/log.txt; done
+ $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -q -u -1 $(O) $(INPUT) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
profile-coq: $(MAIN).opt etc
(* elpi variant 1 ***********************************************************)
-let output_entity_lp1 och st (_, na, s, b) =
+let output_entity_lp1 och st (_, na, u, b) =
if na.E.n_apix <= !G.last then begin
match b with
- | E.Abbr t ->
- KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
- uris := (true, s) :: !uris; !ok
- | E.Abst u ->
- KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
- uris := (false, s) :: !uris; !ok
+ | E.Abbr v ->
+ KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) v out_uri u;
+ uris := (true, u) :: !uris; !ok
+ | E.Abst w ->
+ KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) w out_uri u;
+ uris := (false, u) :: !uris; !ok
| E.Void -> C.err ()
end else !ok
(* elpi variant 2 ***********************************************************)
-let output_entity_lp2 och st (_, na, s, b) =
+let output_entity_lp2 och st (_, na, u, b) =
if na.E.n_apix <= !G.last then begin
match b with
- | E.Abbr t ->
+ | E.Abbr v ->
KP.fprintf och "g+line %a c+%u\n %a\n.\n\n"
- out_uri s na.E.n_apix (out_term st B.empty) t;
- uris := (true, s) :: !uris; !ok
- | E.Abst u ->
+ out_uri u na.E.n_apix (out_term st B.empty) v;
+ uris := (true, u) :: !uris; !ok
+ | E.Abst w ->
KP.fprintf och "g+line %a c+%u\n %a\n.\n\n"
- out_uri s na.E.n_apix (out_term st B.empty) u;
- uris := (false, s) :: !uris; !ok
+ out_uri u na.E.n_apix (out_term st B.empty) w;
+ uris := (false, u) :: !uris; !ok
| E.Void -> C.err ()
end else !ok
out_clause och "tv+c C T :- tv+ T."
end;
out_clause och "main :- grundlagen.";
- out_clause och "grundlagen :- gv+ ";
+ out_clause och "grundlagen :- gv+";
List.iter aux_name (List.rev !uris);
KP.fprintf och "%s" "gtop";
List.iter aux_sep !uris;
(* teyjus variant 2 *************************************************)
-let output_entity_tj2 och st (_, na, s, b) =
+let output_entity_tj2 och st (_, na, u, b) =
if na.E.n_apix <= !G.last then begin
out_comment och (KP.sprintf "constant %u" na.E.n_apix);
match b with
- | E.Abbr t ->
+ | E.Abbr v ->
KP.fprintf och "g+line %a %u\n %a\n.\n\n"
- out_uri s (top_age - na.E.n_apix) (out_term st B.empty) t;
- uris := (true, s) :: !uris; !ok
- | E.Abst u ->
+ out_uri u (top_age - na.E.n_apix) (out_term st B.empty) v;
+ uris := (true, u) :: !uris; !ok
+ | E.Abst w ->
KP.fprintf och "g+line %a %u\n %a\n.\n\n"
- out_uri s (top_age - na.E.n_apix) (out_term st B.empty) u;
- uris := (false, s) :: !uris; !ok
+ out_uri u (top_age - na.E.n_apix) (out_term st B.empty) w;
+ uris := (false, u) :: !uris; !ok
| E.Void -> C.err ()
end else !ok
let close_out_tj2 och () =
- let aux_name (b, s) =
+ let aux_name (b, u) =
let gde = if b then "gdef+2" else "gdec+2" in
- KP.fprintf och "(%s %a\n" gde out_uri s
+ KP.fprintf och "(%s %a\n" gde out_uri u
in
let aux_sep _ = KP.fprintf och "%s" ")" in
if !G.first > 0 then begin
out_clause och "tv+c C T :- tv+ T."
end;
out_clause och "main :- grundlagen.";
- out_clause och "grundlagen :- gv+ ";
+ out_clause och "grundlagen :- gv+";
List.iter aux_name (List.rev !uris);
KP.fprintf och "%s" "gtop";
List.iter aux_sep !uris;
| [] ->
m, B.Bind (a, B.Abst (true, n, w), t), None
| (c, v) :: s ->
-(*
- if !G.cc && not (N.assert_not_zero st n) then assert false;
-*)
if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
let v = B.Cast (E.empty_node, w, v) in
let e = B.push m.e c a (B.abbr v) in
if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
| B.GRef ({E.n_apix = e1}, u1), Some v1,
B.GRef ({E.n_apix = e2}, u2), Some v2 ->
- if e1 < e2 then begin
+ if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
+ else if e1 < e2 then begin
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
end else if e2 < e1 then begin
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, t2, r2)
- end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
- else begin
+ end else begin
if !G.summary then O.add ~gdelta:2 ();
ac st m1 v1 m2 v2
- end
+ end
| _, _, B.GRef _, Some v2 ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
let help_b = "<age> [begin] Begin trace at this global constant (default: first)" in
let help_d = " [data] Show summary information (requires trace >= 2)" in
let help_e = "<age> [end] End trace at this global constant (default: last)" in
- let help_g = " [global] Always expand global definitions (default: false)" in
+ let help_g = " [global] Disable age-driven expansion of global definitions (default: enable)" in
let help_h = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
let help_i = " [indexes] Show local references by index" in
let help_k = "<string> [kernel] Set kernel version (default: \"V3\")" in
let help_n = " [names] Show short constants (default: qualified constants)" in
let help_o = " [objects] Export kernel entities (XML)" in
let help_p = "<file> [preamble] Set preamble to this file (default: empty)" in
- let help_q = " [quote] Disable quotation of identifiers (default: false)" in
+ let help_q = " [quote] Disable quotation of identifiers (default: enable)" in
let help_r = "<string> [root] Set initial segment of URI hierarchy (default: empty)" in
let help_s = "<number> [stage] Set translation stage (see above)" in
let help_t = " [type] Type check (default: validate)" in
- let help_u = " [upsilon] Activate type comparison by sort inclusion (default: false)" in
+ let help_u = " [upsilon] Activate type comparison by sort inclusion (default: deactivate)" in
let help_x = " [extended] Use extended applications (Automath)" in
let help_y = " [infinity] Use ∞-abstractions in contexts" in
let help_0 = " [zero] Preprocess source (Automath)" in
ignore (aux lenv)
let rec exp_term st e t out tab = match t with
- | D.TSort (a, l) ->
+ | D.TSort (a, h) ->
let a =
let err _ = a in
let f s = {a with E.n_name = Some (s, true)} in
- H.string_of_sort err f l
+ H.string_of_sort err f h
in
- let attrs = [XL.position l; XL.name a] in
+ let attrs = [XL.position h; XL.name a] in
XL.tag XL.sort attrs out tab
| D.TLRef (a, i) ->
let a =
let f n r = {a with E.n_name = Some (n, r)} in
D.get_name err f i e
in
- let attrs = [XL.position i; XL.name a ] in
+ let attrs = [XL.depth i; XL.name a] in
XL.tag XL.lref attrs out tab
| D.TGRef (a, n) ->
let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
- let attrs = [XL.uri n; XL.name a ] in
+ let attrs = [XL.uri n; XL.name a] in
XL.tag XL.gref attrs out tab
| D.TCast (a, u, t) ->
let attrs = [] in
and exp_bind st e a b out tab = match b with
| D.Abst (_, n, w) ->
- let attrs = XL.layer st n :: XL.name a :: XL.main a in
+ let attrs = [XL.layer st n; XL.name a] in
XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
| D.Abbr v ->
let attrs = [XL.name a] in
let position i =
"position", string_of_int i
+let depth i =
+ "depth", string_of_int i
+
let uri u =
"uri", U.string_of_uri u
let main a =
let sort, degr = a.E.n_main in
- ["main-sort", string_of_int sort;
+ ["main-position", string_of_int sort;
"main-degree", string_of_int degr;
]
let side a =
let sort, degr = a.E.n_side in
- ["side-sort", string_of_int sort;
+ ["side-position", string_of_int sort;
"side-degree", string_of_int degr;
]
val position: int -> attr
+val depth: int -> attr
+
val uri: Entity.uri -> attr
val layer: Layer.status -> Layer.layer -> attr
projects / helm.git / commitdiff