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
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 \
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
$(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)"
$(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)
(* *)
(**************************************************************************)
-(* 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))).
(* *)
(**************************************************************************)
-(* 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".
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).
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).
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)).
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))).
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).
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)).
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))
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
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
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
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
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)
module U = NUri
module UH = U.UriHash
+module G = Options
module E = Entity
let hsize = 7000
(* 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
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 ******************************************************)
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
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", _ -> "λ"
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 ******************************************************)
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 ();
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
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 *)
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 = {
(* 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 () = {
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 ()
let refresh_status st = st
-let infinite = cell true Inf
+let infinity = cell true Inf
let finite i = cell true (Fin i)
val refresh_status: status -> status
-val infinite: layer
+val infinity: layer
val finite: int -> layer
(* 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 *)
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 *)
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 =
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
?(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);
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;
| 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
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
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 =
| sort CM sorts { $1 :: $3 }
;
layer:
- | { N.infinite }
+ | { N.infinity }
| CT IX { N.finite $2 }
;
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) *)
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
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 =
| 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;
if !G.trace >= 1 then Y.utime_stamp "at exit"
in
let help =
- "Usage: helena [ -LPVXdgilnoqtux01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
+ "Usage: helena [ -LPVXdgilnoqtux
y01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\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" ^
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_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;
("-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);
("-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
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
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
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
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
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
projects / helm.git / commitdiff