From 2cf2e883f91164ce614bdc86b5c5e2419b98f68d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 27 Jun 2015 18:35:52 +0000 Subject: [PATCH] - bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite) - new option -y allows to use infinity-abstraction in contexts - ages removed from global references (the RTM computes them) - new semantics of the -g option (w.i.p.) for a comparison with Coq --- helm/software/helena/.depend.opt | 8 +- helm/software/helena/Makefile | 38 +++++---- helm/software/helena/coq/grundlagen_2.v | 2 +- helm/software/helena/matita/grundlagen_2.ma | 40 +++++----- helm/software/helena/src/automath/autCrg.ml | 79 +++++++++++-------- helm/software/helena/src/basic_ag/bagCrg.ml | 2 +- helm/software/helena/src/basic_rg/brg.ml | 2 + .../helena/src/basic_rg/brgEnvironment.ml | 6 +- .../helena/src/basic_rg/brgGallina.ml | 12 +-- .../helena/src/basic_rg/brgGrafite.ml | 12 +-- .../helena/src/basic_rg/brgReduction.ml | 10 +-- helm/software/helena/src/common/entity.ml | 16 +++- helm/software/helena/src/common/layer.ml | 2 +- helm/software/helena/src/common/layer.mli | 2 +- helm/software/helena/src/common/options.ml | 10 ++- helm/software/helena/src/common/output.ml | 2 + helm/software/helena/src/complete_rg/crg.ml | 17 +++- helm/software/helena/src/text/txtCrg.ml | 4 +- helm/software/helena/src/text/txtParser.mly | 2 +- helm/software/helena/src/toplevel/top.ml | 15 ++-- helm/software/helena/src/xml/xmlCrg.ml | 8 +- helm/software/helena/src/xml/xmlLibrary.ml | 19 +++-- helm/software/helena/src/xml/xmlLibrary.mli | 6 +- 23 files changed, 191 insertions(+), 123 deletions(-) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 7babc30d3..a07afc02e 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -126,10 +126,10 @@ src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \ src/basic_rg/brg.cmx src/common/alpha.cmx src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx -src/basic_rg/brgEnvironment.cmo : src/common/entity.cmx \ - src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgEnvironment.cmx : src/common/entity.cmx \ - src/basic_rg/brgEnvironment.cmi +src/basic_rg/brgEnvironment.cmo : src/common/options.cmx \ + src/common/entity.cmx src/basic_rg/brgEnvironment.cmi +src/basic_rg/brgEnvironment.cmx : src/common/options.cmx \ + src/common/entity.cmx src/basic_rg/brgEnvironment.cmi src/basic_rg/brgSubstitution.cmi : src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmo : src/common/options.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 8ae171cd0..991d490f0 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -11,7 +11,7 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt TAGS = test-si-fast test-si test2 test3 test6 \ - profile-fast profile profile-coq \ + profile-fast profile profile-coq profile-coq-byte \ xml-si xml-si-v3 xml xml-v3 \ export-coq export-matita \ export-lp1 export-lp2 export-tj2 export-tj3 \ @@ -19,7 +19,11 @@ TAGS = test-si-fast test-si test2 test3 test6 \ include Makefile.common -COQC = coqc +TIME = `which time` -p -a -o etc/log.txt + +NULL = >/dev/null 2>&1 + +COQTOP = coqtop MATITAC = ../../../../matita/matita/matitac.opt @@ -51,32 +55,32 @@ test-si: $(MAIN).opt etc $(H)./$(MAIN).opt -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt test2: $(MAIN).opt etc - @echo " HELENA -T 2 -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 2 -d -l $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 2 -l $(INPUT)" + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l $(O) $(INPUT) > etc/log.txt test3: $(MAIN).opt etc - @echo " HELENA -T 3 -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 3 -d -l $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 3 -l $(INPUT)" + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 3 -l $(O) $(INPUT) > etc/log.txt test6: $(MAIN).opt etc - @echo " HELENA -T 6 -d -l -n $(INPUT)" - $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 6 -d -l -n $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 6 -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 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(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 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(O) $(INPUT) > etc/log.txt xml: $(MAIN).opt etc @echo " HELENA -l -o -s 1 $(INPUT)" - $(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(O) $(INPUT) > etc/log.txt xml-v3: $(MAIN).opt etc @echo " HELENA -l -o -s 2 $(INPUT)" - $(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(O) $(INPUT) > etc/log.txt export-coq coq/$(V): $(MAIN).opt etc @echo " HELENA -l -m V8 -u $(INPUT)" @@ -115,9 +119,15 @@ profile: $(MAIN).opt etc $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile-coq: $(MAIN).opt etc - @echo " COQC $(V) (31 TIMES)" + @echo " COQTOP $(V) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done + $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt + +profile-coq-byte: $(MAIN).opt etc + @echo " COQTOP $(V) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do `which time` -p -a -u etc/log.txt $(COQC) coq/$(V); done + $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt matita: matita/$(MA) diff --git a/helm/software/helena/coq/grundlagen_2.v b/helm/software/helena/coq/grundlagen_2.v index b04a3e5dc..0d4f57cec 100644 --- a/helm/software/helena/coq/grundlagen_2.v +++ b/helm/software/helena/coq/grundlagen_2.v @@ -9,7 +9,7 @@ (* *) (**************************************************************************) -(* This file was generated by Helena 0.8.2 M (February 2015): do not edit *) +(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****) (* constant 1 *) Definition l_imp := (fun (a:Prop) => (fun (b:Prop) => ((forall (x:a), b) : Prop))). diff --git a/helm/software/helena/matita/grundlagen_2.ma b/helm/software/helena/matita/grundlagen_2.ma index 773c8a9de..304439b02 100644 --- a/helm/software/helena/matita/grundlagen_2.ma +++ b/helm/software/helena/matita/grundlagen_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* This file was generated by Helena 0.8.2 M (February 2015): do not edit *) +(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****) include "basics/pts.ma". @@ -584,13 +584,13 @@ definition l_orec3_th1 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3 definition l_orec3_th2 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3i c a b (l_or3_th5 a b c (l_orec3e1 a b c o)) (l_ec3_th5 a b c (l_orec3e2 a b c o)) : l_orec3 c a b). (* constant 190 *) -axiom l_e_is : Πsigma:Type[0].Πs:sigma.Πt:sigma.Prop. +axiom l_e_is : ∀sigma:Type[0].∀s:sigma.∀t:sigma.Prop. (* constant 191 *) -axiom l_e_refis : Πsigma:Type[0].Πs:sigma.l_e_is sigma s s. +axiom l_e_refis : ∀sigma:Type[0].∀s:sigma.l_e_is sigma s s. (* constant 192 *) -axiom l_e_isp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.Πt:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t. +axiom l_e_isp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀t:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t. (* constant 193 *) definition l_e_symis ≝ λsigma:Type[0].λs:sigma.λt:sigma.λi:l_e_is sigma s t.(l_e_isp sigma (λx:sigma.l_e_is sigma x s) s t (l_e_refis sigma s) i : l_e_is sigma t s). @@ -650,10 +650,10 @@ definition l_e_onee1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma definition l_e_onee2 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.(l_ande2 (l_e_amone sigma p) (l_some sigma p) o1 : l_some sigma p). (* constant 212 *) -axiom l_e_ind : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.sigma. +axiom l_e_ind : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_one sigma p.sigma. (* constant 213 *) -axiom l_e_oneax : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1). +axiom l_e_oneax : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1). (* constant 214 *) definition l_e_one_th1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.λs:sigma.λsp:p s.(l_e_amonee sigma p (l_e_onee1 sigma p o1) (l_e_ind sigma p o1) s (l_e_oneax sigma p o1) sp : l_e_is sigma (l_e_ind sigma p o1) s). @@ -788,25 +788,25 @@ definition l_e_bij_th1 ≝ λsigma:Type[0].λtau:Type[0].λupsilon:Type[0].λf: definition l_e_fise ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.(l_e_isp (Πx:sigma.tau) (λy:Πx:sigma.tau.l_e_is tau (f s) (y s)) f g (l_e_refis tau (f s)) i : l_e_is tau (f s) (g s)). (* constant 258 *) -axiom l_e_fisi : Πsigma:Type[0].Πtau:Type[0].Πf:Πx:sigma.tau.Πg:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g. +axiom l_e_fisi : ∀sigma:Type[0].∀tau:Type[0].∀f:Πx:sigma.tau.∀g:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g. (* constant 259 *) definition l_e_fis_th1 ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.λt:sigma.λj:l_e_is sigma s t.(l_e_tris tau (f s) (f t) (g t) (l_e_isf sigma tau f s t j) (l_e_fise sigma tau f g i t) : l_e_is tau (f s) (g t)). (* constant 260 *) -axiom l_e_ot : Πsigma:Type[0].∀p:∀x:sigma.Prop.Type[0]. +axiom l_e_ot : Πsigma:Type[0].Πp:∀x:sigma.Prop.Type[0]. (* constant 261 *) -axiom l_e_in : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma. +axiom l_e_in : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma. (* constant 262 *) -axiom l_e_inp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.p (l_e_in sigma p o1). +axiom l_e_inp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_ot sigma p.p (l_e_in sigma p o1). (* constant 263 *) -axiom l_e_otax1 : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x). +axiom l_e_otax1 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x). (* constant 264 *) -axiom l_e_otax2 : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s. +axiom l_e_otax2 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s. (* constant 265 *) definition l_e_isini ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_ot sigma p.λo2:l_e_ot sigma p.λi:l_e_is (l_e_ot sigma p) o1 o2.(l_e_isf (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) o1 o2 i : l_e_is sigma (l_e_in sigma p o1) (l_e_in sigma p o2)). @@ -842,19 +842,19 @@ axiom l_e_first : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.sigm axiom l_e_second : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.tau. (* constant 276 *) -axiom l_e_pairis1 : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1. +axiom l_e_pairis1 : ∀sigma:Type[0].∀tau:Type[0].∀p1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1. (* constant 277 *) definition l_e_pairis2 ≝ λsigma:Type[0].λtau:Type[0].λp1:l_e_pairtype sigma tau.(l_e_symis (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1 (l_e_pairis1 sigma tau p1) : l_e_is (l_e_pairtype sigma tau) p1 (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1))). (* constant 278 *) -axiom l_e_firstis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s. +axiom l_e_firstis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s. (* constant 279 *) definition l_e_firstis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s (l_e_firstis1 sigma tau s t) : l_e_is sigma s (l_e_first sigma tau (l_e_pair sigma tau s t))). (* constant 280 *) -axiom l_e_secondis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t. +axiom l_e_secondis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t. (* constant 281 *) definition l_e_secondis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t (l_e_secondis1 sigma tau s t) : l_e_is tau t (l_e_second sigma tau (l_e_pair sigma tau s t))). @@ -1208,16 +1208,16 @@ definition l_r_itef ≝ λa:Prop.λksi:Type[0].λx:Πt:a.ksi.λy:Πt:l_not a.ksi axiom l_e_st_set : Πsigma:Type[0].Type[0]. (* constant 398 *) -axiom l_e_st_esti : Πsigma:Type[0].Πs:sigma.Πs0:l_e_st_set sigma.Prop. +axiom l_e_st_esti : ∀sigma:Type[0].∀s:sigma.∀s0:l_e_st_set sigma.Prop. (* constant 399 *) -axiom l_e_st_setof : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_st_set sigma. +axiom l_e_st_setof : Πsigma:Type[0].Πp:∀x:sigma.Prop.l_e_st_set sigma. (* constant 400 *) -axiom l_e_st_estii : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p). +axiom l_e_st_estii : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p). (* constant 401 *) -axiom l_e_st_estie : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s. +axiom l_e_st_estie : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s. (* constant 402 *) definition l_e_st_empty ≝ λsigma:Type[0].λs0:l_e_st_set sigma.(l_none sigma (λx:sigma.l_e_st_esti sigma x s0) : Prop). @@ -1286,7 +1286,7 @@ definition l_e_st_isset_th1 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_s definition l_e_st_isset_th2 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λi:l_e_is (l_e_st_set sigma) s0 t0.(λx:sigma.λy:l_e_st_esti sigma x t0.l_e_st_issete2 sigma s0 t0 i x y : l_e_st_incl sigma t0 s0). (* constant 424 *) -axiom l_e_st_isseti : Πsigma:Type[0].Πs0:l_e_st_set sigma.Πt0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0. +axiom l_e_st_isseti : ∀sigma:Type[0].∀s0:l_e_st_set sigma.∀t0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0. (* constant 425 *) definition l_e_st_isset_th3 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λs:sigma.λses0:l_e_st_esti sigma s s0.λn:l_not (l_e_st_esti sigma s t0).(l_imp_th3 (l_e_is (l_e_st_set sigma) s0 t0) (l_e_st_esti sigma s t0) n (λt:l_e_is (l_e_st_set sigma) s0 t0.l_e_st_issete1 sigma s0 t0 t s ses0) : l_not (l_e_is (l_e_st_set sigma) s0 t0)). diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 667b18cc1..22b3e799c 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -44,10 +44,19 @@ let empty_cnt = D.empty_lenv let alpha id = if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id -let add_abst cnt id aw w = +let attrs_for_abst id aw = let id = if !G.alpha <> "" then alpha id else id in - let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in - D.EBind (cnt, aw, D.Abst (false, N.two, w)) + let main = E.succ aw.E.n_main in + E.node_attrs ~name:(id, true) ~side:aw.E.n_main ~main () + +let attrs_for_decl aw = + let main = E.succ aw.E.n_main in + E.node_attrs ~side:aw.E.n_main ~main () + +let add_abst cnt id aw w = + let a = attrs_for_abst id aw in + let l = if !G.infinity then N.infinity else N.two in + D.EBind (cnt, a, D.Abst (false, l, w)) let mk_lref f a i = f a (D.TLRef (a, i)) @@ -103,58 +112,66 @@ let get_cnt_relaxed f lst = get_cnt err f lst lst.node let push_abst f a w lenv = - let bw = D.Abst (false, N.infinite, w) in + let bw = D.Abst (false, N.infinity, w) in D.push_bind f a bw lenv -let add_proj e t = match e with +let add_proj at e t = match e with | D.ESort -> t - | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) - | _ -> D.TProj (E.empty_node, e, t) + | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) + | _ -> + let e = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start at e else e in + D.TProj (at, e, t) (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lst y lenv = function | A.Sort s -> let h = if s then 0 else 1 in - let a = E.node_attrs ~sort:h () in + let a = E.node_attrs ~main:(h, 0) () in f a (D.TSort (a, h)) | A.Appl (v, t) -> - let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in - let f _ vv = xlate_term (f vv) st lst y lenv t in + let f av vv at tt = + let at = E.compose av at in + f at (D.TAppl (at, !G.extended, vv, tt)) + in + let f av vv = xlate_term (f av vv) st lst y lenv t in xlate_term f st lst false lenv v | A.Abst (name, w, t) -> - let name = if !G.alpha <> "" then alpha name else name in - let name = Some (name, true) in - let f aw ww = + let f aw ww = + let aw = attrs_for_abst name aw in let f at tt = + let at = E.compose aw at in let l = - if !G.cc then match y, at.E.n_degr with + if !G.cc then match y, snd at.E.n_main with | true, _ -> N.one | _ , 0 -> N.one | _ , 1 -> N.unknown st | _ , 2 -> N.two | _ -> assert false - else N.infinite + else N.infinity in let b = D.Abst (false, l, ww) in - let at = {at with E.n_name = name} in f at (D.TBind (at, b, tt)) in let f lenv = xlate_term f st lst y lenv t in - push_abst f {aw with E.n_name = name; E.n_degr = succ aw.E.n_degr} ww lenv + push_abst f aw ww lenv in xlate_term f st lst true lenv w | A.GRef (name, args) -> let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in let map2 f arg args = - let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in + let f av v = f (D.EAppl (args, E.shift av, !G.extended, v)) in xlate_term f st lst false lenv arg in let g qid a cnt = let gref = D.TGRef (a, uri_of_qid qid) in if cnt = D.ESort then f a gref else let f = function - | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref)) - | args -> f a (D.TProj (a, args, gref)) + | D.EAppl (D.ESort, av, x, v) -> + let a = E.compose av a in + f a (D.TAppl (a, x, v, gref)) + | args -> + let args = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start a args else args in + f a (D.TProj (a, args, gref)) in let f args = C.list_fold_right f map2 args D.ESort in D.sub_list_strict (D.fold_names f map1 args) cnt args @@ -193,14 +210,14 @@ let xlate_entity err f st lst = function let f lenv = let f qid = let f aw ww = - let aw = {aw with E.n_apix = lst.line; E.n_degr = succ aw.E.n_degr} in - UH.add henv (uri_of_qid qid) (aw, lenv); - let t = add_proj lenv ww in + let a = attrs_for_decl aw in + UH.add henv (uri_of_qid qid) (a, lenv); + let t = add_proj aw lenv ww in (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = E.Abst t in - let entity = E.empty_root, aw, uri_of_qid qid, b in + let na = {aw with E.n_apix = lst.line} in + let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in G.set_current_trace lst.line; f {lst with line = succ lst.line} entity in @@ -208,21 +225,21 @@ let xlate_entity err f st lst = function in complete_qid f lst (name, true, []) in - get_cnt_relaxed (D.replace f N.one) lst + let f = if !G.infinity then f else D.set_layer f N.one in + get_cnt_relaxed f lst | A.Def (name, w, trans, v) -> let f lenv = let f qid = let f _ ww = let f av vv = - let na = {av with E.n_apix = lst.line} in - UH.add henv (uri_of_qid qid) (na, lenv); - let t = add_proj lenv (D.TCast (na, ww, vv)) in + UH.add henv (uri_of_qid qid) (av, lenv); + let t = add_proj av lenv (D.TCast (av, ww, vv)) in (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = E.Abbr t in + let na = {av with E.n_apix = lst.line} in let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in - let entity = ra, na, uri_of_qid qid, b in + let entity = ra, na, uri_of_qid qid, E.Abbr t in G.set_current_trace lst.line; f {lst with line = succ lst.line} entity in diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index b9ce1d344..cb21d0247 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -78,7 +78,7 @@ let rec xlate_bk_term f c = function and xlate_bk_bind f c = function | Z.Abst t -> - let f tt = f (D.Abst (false, N.infinite, tt)) in + let f tt = f (D.Abst (false, N.infinity, tt)) in xlate_bk_term f c t | Z.Abbr t -> let f tt = f (D.Abbr tt) in diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index a321a32b0..a39010f80 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -46,6 +46,8 @@ let abbr v = Abbr v let lref a i = LRef (a, i) +let gref a u = GRef (a, u) + let cast a u t = Cast (a, u, t) let appl a x u t = Appl (a, x, u, t) diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml index 0fbbd9a54..1b3f744e2 100644 --- a/helm/software/helena/src/basic_rg/brgEnvironment.ml +++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml @@ -11,6 +11,7 @@ module U = NUri module UH = U.UriHash +module G = Options module E = Entity let hsize = 7000 @@ -20,8 +21,9 @@ let env = UH.create hsize (* decps *) let set_entity entity = - let _, _, uri, _ = entity in - UH.add env uri entity; entity + let ra, na, uri, b = entity in + let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in + UH.add env uri entity0; entity let get_entity uri = try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml index caa8ab465..bdb78144a 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgGallina.ml @@ -111,13 +111,14 @@ let rec out_term st p e och = function let close_out och () = close_out och -let output_entity och st (_, na, s, b) = +let output_entity och st (_, na, u, b) = out_comment och (KP.sprintf "constant %u" na.E.n_apix); match b with - | E.Abbr t -> - KP.fprintf och "Definition %a := %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok - | E.Abst t -> - KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok + | E.Abbr v -> + KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v; +(* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok + | E.Abst w -> + KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok | E.Void -> C.err () (* Interface functions ******************************************************) @@ -128,5 +129,4 @@ let open_out fname = let och = open_out (path ^ ext) in out_preamble och; out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); -(* out_include och "basics/pts"; *) output_entity och, close_out och diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index 71b189dac..b1cfe21ca 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -88,7 +88,7 @@ let rec out_term st p e och = function let op, cp = if p then "(", ")" else "", "" in let a = R.alpha B.mem e a in let ee = B.push e B.empty a (B.abst r n w) in - let binder = match N.to_string st n, a.E.n_sort with + let binder = match N.to_string st n, fst a.E.n_main with | "1", 0 -> "Π" | "1", 1 -> "∀" | "2", _ -> "λ" @@ -106,13 +106,13 @@ let rec out_term st p e och = function let close_out och () = close_out och -let output_entity och st (_, na, s, b) = +let output_entity och st (_, na, u, b) = out_comment och (KP.sprintf "constant %u" na.E.n_apix); match b with - | E.Abbr t -> - KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok - | E.Abst t -> - KP.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok + | E.Abbr v -> + KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok + | E.Abst w -> + KP.fprintf och "axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok | E.Void -> C.err () (* Interface functions ******************************************************) diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 1a5a3f1cf..f20335193 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -101,12 +101,8 @@ let rec step st m r = else m, r, None | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, _, E.Abbr v -> - if !G.expand then begin - if !G.summary then O.add ~gdelta:1 (); - step st m v - end else - m, r, Some v + | _, a, _, E.Abbr v -> + m, B.gref a uri, Some v | _, _, _, E.Abst w -> if assert_tstep m true then begin if !G.summary then O.add ~grt:1 (); @@ -126,7 +122,7 @@ let rec step st m r = if !G.summary then O.add ~lrt:1 (); step st {(tstep m) with e = c} w end else - m, B.LRef (a, i), None + m, B.lref a i, None | _, _, B.Void -> assert false end diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml index c53db162b..d834ed53e 100644 --- a/helm/software/helena/src/common/entity.ml +++ b/helm/software/helena/src/common/entity.ml @@ -18,6 +18,8 @@ type id = string (* identifier *) type name = id * bool (* token, real? *) +type arity = int * int (* sort, degree *) + type meta = Main (* main object *) | InProp (* inhabitant of a proposition *) | Progress (* uncompleted object *) @@ -26,8 +28,8 @@ type meta = Main (* main object *) type node_attrs = { n_name: name option; (* name *) n_apix: int; (* additional position index *) - n_degr: int; (* degree *) - n_sort: int; (* sort *) + n_main: arity; (* main arity *) + n_side: arity; (* side arity *) } type root_attrs = { @@ -43,8 +45,8 @@ type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, bi (* helpers ******************************************************************) -let node_attrs ?(apix=0) ?name ?(degr=0) ?(sort=0) () = { - n_apix = apix; n_name = name; n_degr = degr; n_sort = sort +let node_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = { + n_apix = 0; n_name = name; n_main = main; n_side = side; } let root_attrs ?(meta=[]) ?info () = { @@ -57,6 +59,12 @@ let empty_root = root_attrs () let common f (ra, na, u, _) = f ra na u +let succ (sort, degr) = sort, succ degr + +let compose av at = {av with n_main = at.n_main} + +let shift av = {av with n_side = av.n_main} + let rec name err f a = match a.n_name with | Some (n, r) -> f n r | None -> err () diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index 1ad6cf28c..de8b98254 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -123,7 +123,7 @@ let initial_status () = let refresh_status st = st -let infinite = cell true Inf +let infinity = cell true Inf let finite i = cell true (Fin i) diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli index 40ada03a1..f6abb1195 100644 --- a/helm/software/helena/src/common/layer.mli +++ b/helm/software/helena/src/common/layer.mli @@ -17,7 +17,7 @@ val initial_status: unit -> status val refresh_status: status -> status -val infinite: layer +val infinity: layer val finite: int -> layer diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 3ac27296d..b2dc97292 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -27,7 +27,7 @@ type manager = Quiet (* interface functions ******************************************************) -let version_string = "Helena 0.8.2 M (June 2015)" +let version_string = "Helena 0.8.3 M (June 2015)" let stage = ref 3 (* stage *) @@ -37,6 +37,8 @@ let ct = ref 0 (* current trace level *) let summary = ref false (* log summary information *) +let export = ref false (* export entities to XML *) + let xdir = ref "" (* directory for XML output *) let kernel = ref V3 (* kernel type *) @@ -73,6 +75,8 @@ let last = ref max_int (* end trace here *) let extended = ref false (* extended applications *) +let infinity = ref false (* use ∞-abstractions in contexts *) + let short = ref false (* short global constants *) let set_current_trace n = @@ -96,8 +100,8 @@ let get_mk_uri () = fun s -> KF.concat bu (s ^ ".ld") let clear () = - stage := 3; trace := 0; summary := false; first := 0; last := max_int; - xdir := ""; kernel := V3; si := false; extended := false; cover := ""; + stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int; + xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := ""; expand := false; indexes := false; icm := 0; unquote := false; short := false; debug_parser := false; debug_lexer := false; manager_dir := ""; manager := Quiet diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 94bf217da..3c813b275 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -43,6 +43,7 @@ let add ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) () = +(* if !G.ct >= level then begin if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta); if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta); @@ -50,6 +51,7 @@ let add if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt); if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); end; +*) reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index ea3ec54bf..a250d3edd 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -115,13 +115,28 @@ let rec mem err f e b = match e with | EProj (e, _, d) -> let err () = mem err f e b in mem err f d b -let replace f n0 e = +let set_layer f n0 e = let rec aux f = function | ESort -> f ESort | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e | EBind (e, a, b) -> aux (push_bind f a b) e | EAppl (e, a, x, v) -> aux (push_appl f a x v) e | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d + in + aux f e +let set_attrs f a0 e = + let rec aux f = function + | ESort -> f ESort + | EBind (e, a, b) -> + let a = E.compose a a0 in + aux (push_bind f a b) e + | EAppl (e, a, x, v) -> + let a = E.compose a a0 in + aux (push_appl f a x v) e + | EProj (e, a, d) -> + let a = E.compose a a0 in + let f d = aux (push_proj f a d) e in + aux f d in aux f e diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index b2d0c99e1..1ba830669 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -66,7 +66,7 @@ let rec xlate_term f st lenv = function Printf.printf "\n"; *) | T.Sort h -> - let a = E.node_attrs ~sort:h () in + let a = E.node_attrs ~main:(h, 0) () in f a (D.TSort (a, h)) | T.NSrt id -> let f h = xlate_term f st lenv (T.Sort h) in @@ -115,7 +115,7 @@ and xlate_bind st f (lenv, e) b = in xlate_term f st lenv v | T.Void id -> - let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in + let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in f a D.Void let mk_contents main kind tt = diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly index d08fb87d9..32d0df309 100644 --- a/helm/software/helena/src/text/txtParser.mly +++ b/helm/software/helena/src/text/txtParser.mly @@ -68,7 +68,7 @@ | sort CM sorts { $1 :: $3 } ; layer: - | { N.infinite } + | { N.infinity } | CT IX { N.finite $2 } ; diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 0f953949e..3e7f8aa91 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -219,7 +219,6 @@ let count_input st = function let version = ref true let preprocess = ref false let root = ref "" -let export = ref false let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) @@ -230,7 +229,7 @@ let process_2 st entity = let f = if !version then validate else type_check in f st entity else st in - if !export then export_entity st entity; + if !G.export then export_entity st entity; match st.mst with | None -> st | Some (export_entity, _) -> manager st export_entity entity @@ -238,7 +237,7 @@ let process_2 st entity = let process_1 st entity = if !G.ct >= 3 then pp_progress entity; let st = if !G.summary then count_entity st entity else st in - if !export && !G.stage = 1 then export_entity st entity; + if !G.export && !G.stage = 1 then export_entity st entity; if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st let process_0 st entity = @@ -322,7 +321,7 @@ let main = | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) in let clear_options () = - export := false; preprocess := false; + preprocess := false; root := ""; G.clear (); H.clear (); O.clear_reductions (); streaming := false; @@ -363,7 +362,7 @@ let main = if !G.trace >= 1 then Y.utime_stamp "at exit" in let help = - "Usage: helena [ -LPVXdgilnoqtux01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^ " 4 typing information, 5 conversion information, 6 reduction information,\n" ^ " 7 level disambiguation\n\n" ^ @@ -396,7 +395,8 @@ let main = let help_s = " [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_x = " [extended] Use extended applications (Automath)" 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 let help_1 = " [one] parse files with streaming policy" in at_exit exit; @@ -419,7 +419,7 @@ let main = ("-l", Arg.Set G.cc, help_l); ("-m", Arg.String set_manager, help_m); ("-n", Arg.Set G.short, help_n); - ("-o", Arg.Set export, help_o); + ("-o", Arg.Set G.export, help_o); ("-p", Arg.String ((:=) G.preamble), help_p); ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String ((:=) root), help_r); @@ -427,6 +427,7 @@ let main = ("-t", Arg.Clear version, help_t); ("-u", Arg.Set G.si, help_u); ("-x", Arg.Set G.extended, help_x); + ("-y", Arg.Set G.infinity, help_y); ("-0", Arg.Unit set_preprocess, help_0); ("-1", Arg.Set streaming, help_1); ] process_file help diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index b5e3b9b40..b04f5f6e1 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -22,7 +22,7 @@ module D = Crg let lenv_iter map_bind map_appl map_proj st e lenv out tab = let rec aux = function | D.ESort -> e - | D.EBind (e, a, b) -> + | D.EBind (e, a, b) -> let e = aux e in (* NOTE: the inner binders are alpha-converted first *) let a = R.alpha D.mem e a in @@ -51,11 +51,11 @@ let rec exp_term st e t out tab = match t with 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.position 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; XL.apix 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 @@ -81,7 +81,7 @@ and exp_appl st e a x v out tab = 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.kind a] in + let attrs = XL.layer st n :: XL.name a :: XL.main a in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab | D.Abbr v -> let attrs = [XL.name a] in diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 3c77fe68b..dcc18c94b 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -96,14 +96,23 @@ let name a = let f n r = "name", if r then n else "-" ^ n in E.name err f a -let apix a = - "position", string_of_int a.E.n_apix - let layer st n = "layer", N.to_string st n -let kind a = - "position", string_of_int a.E.n_sort +let main a = + let sort, degr = a.E.n_main in + ["main-sort", 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-degree", string_of_int degr; + ] + +let apix a = + "level", string_of_int a.E.n_apix let meta a = let map = function diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 4ac5dc913..e49d0e8d8 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -45,9 +45,11 @@ val layer: Layer.status -> Layer.layer -> attr val name: Entity.node_attrs -> attr -val apix: Entity.node_attrs -> attr +val main: Entity.node_attrs -> attr list + +val side: Entity.node_attrs -> attr list -val kind: Entity.node_attrs -> attr +val apix: Entity.node_attrs -> attr val meta: Entity.root_attrs -> attr -- 2.39.2