--- /dev/null
+.depend.opt
+Make*
+README
+examples/grundlagen/*.aut
+icons/*.ico
+icons/*.png
+src/*.ml
+src/Make*
+src/*/*
+xml/*.dtd
+xml/*.xsl
xml/brg-si/grundlagen/l/et.ld.xml \
xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
xml/brg-si/grundlagen/l/e/pairis1.ld.xml \
+ xml/brg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
xml/crg-si/grundlagen/l/not.ld.xml \
xml/crg-si/grundlagen/l/et.ld.xml \
xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
xml/crg-si/grundlagen/l/e/pairis1.ld.xml \
+ xml/crg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
xml/brg-si/grundlagen/ccs.ldc.xml
include Makefile.common
$(H)mkdir -p $(LOCALLDDLDIR)/$(@D)
$(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml
+%.ldc:
+ @echo " SKIP $@"
+
etc/make-html.sh xml/index.txt index:
@echo " GENERATE INDEXES"
$(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt
install-lddl: index
@echo " INSTALL lddl.tar.bz2"
- $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml
+ $(H)tar -cjf etc/lddl.tar.bz2 -X etc/exclude.txt xml
+ $(H)scp etc/lddl.tar.bz2 $(DOWNDIR)
install-dtd: xml/ld.dtd
@echo " INSTALL $<"
H=@
ifeq ($(origin OCAMLPATH), undefined)
- OCAMLFIND = OCAMLPATH=../components/METAS ocamlfind
+ OCAMLFIND = OCAMLPATH=$(HOME)/svn/software/components/METAS ocamlfind
else
OCAMLFIND = ocamlfind
endif
+RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
+
LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl
LDDLDIR = mowgli:/projects/helm/public_html/lambda-delta/static/lddl
DOWNDIR = mowgli:/projects/helm/public_html/lambda-delta/download
XMLDIR = mowgli:/projects/helm/public_html/lambda-delta/xml
-LOCALLDDLDIR = ../../../public_html/lddl
+LOCALLDDLDIR = $(HOME)/public_html/lddl
DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make))
@echo XMLLINT --valid
$(H)$(XMLLINT) --valid $^
+relise: clean
+ @echo " RELISE $(RELISE)"
+ $(H)mkdir -p $(RELISE)
+ $(H)$(foreach FILE, $(shell cat Make), cp --parents $(FILE) $(RELISE);)
+ $(H)tar -czf etc/$(RELISE).tar.gz $(RELISE)
+ $(H)scp etc/$(RELISE).tar.gz $(DOWNDIR)
+
tgz: clean
@echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)"
$(H)find -name "Make*" | xargs $(TAR) $(KEEP)
* type "make test-si" to parse the grundlagen
it generates a log.txt with the grundlagen contents statistics
-
-* type "make clean" to remove the products of compilation
-* type "make tgz" to make a tar.gz of the source files
+* type "make test-si-fast" to parse the grundlagen with minimum logging
+
+* type "make clean" to remove the products of compilation
let f nw ww =
let a = [E.Name (name, true)] in
let f nt tt =
- let b = D.Abst (nt, [ww]) in
+ let nnt = N.infinite (* if N.is_zero nt then N.infinite else nt *) in
+ let b = D.Abst (nnt, [ww]) in
f nt (D.TBind (a, b, tt))
in
let f lenv = xlate_term f st lenv t in
xlate_term xlate_bind f c t
| D.TProj (_, e, t) ->
xlate_term xlate_bind f c (D.tshift e t)
+(* this case should be removed by improving alpha-conversion *)
| D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
| D.TBind (a, b, t) ->
xlate_term f t
| D.TProj (_, e, t) ->
xlate_term f (D.tshift e t)
- | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
- xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
| D.TBind (a, b, t) ->
let f tt = f (xlate_bind tt a b) in xlate_term f t
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
- if N.is_zero n then Q.add_infinite st.S.cc a;
+ if N.is_zero n then Q.add_nonzero st.S.cc a;
O.add ~beta:1 ~upsilon:(List.length s) ();
let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in
step st {m with e = e; s = s} t
O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
| _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1),
- _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)
- when n1 = n2 || st.S.si ->
+ _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) ->
+ if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;
if ac {st with S.si = false} m1 w1 m2 w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
- | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)
- when N.is_zero n || st.S.si ->
+ | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t) ->
+ if N.is_zero n then () else Q.add_zero st.S.cc a;
O.add ~si:1 ();
ac st (push m1 a b) u (push m2 a b) t
| _ -> false
type csys = {
uri: E.uri;
- mutable is : int list
+ mutable tp : int list;
+ mutable t1 : int list;
+ mutable tn : (int * int) list;
}
let mark a = E.mark C.err C.start a
let init () = {
uri = U.uri_of_string (G.get_baseuri ());
- is = [];
+ tp = []; t1 = []; tn = []
}
-let add_infinite s a =
+let add_nonzero s a =
if !G.si && !G.cc then
let i = abs (mark a) in
- if L.mem i s.is then () else s.is <- i :: s.is
+ if L.mem i s.tp then () else s.tp <- i :: s.tp
+ else ()
+
+let add_zero s a =
+ if !G.si && !G.cc then
+ let i = abs (mark a) in
+ if L.mem i s.t1 then () else s.t1 <- i :: s.t1
+ else ()
+
+let add_equal s xa ia =
+ if !G.si && !G.cc then
+ let i = abs (mark xa), abs (mark ia) in
+ if L.mem i s.tn then () else s.tn <- i :: s.tn
else ()
type csys = {
uri: Entity.uri;
- mutable is : int list
+ mutable tp : int list;
+ mutable t1 : int list;
+ mutable tn : (int * int) list;
}
val init: unit -> csys
-val add_infinite: csys -> Entity.attrs -> unit
+val add_nonzero: csys -> Entity.attrs -> unit
+
+val add_zero: csys -> Entity.attrs -> unit
+
+val add_equal: csys -> Entity.attrs -> Entity.attrs -> unit
tag obj_root attrs ~contents out 0;
close_out och
+let prec_map (i, _) = string_of_int i
+
+let next_map (_, i) = string_of_int i
+
let marks = function
| [] -> "mark", ""
| l -> "mark", String.concat " " (List.rev_map string_of_int l)
+let precs = function
+ | [] -> "prec", ""
+ | l -> "prec", String.concat " " (List.rev_map prec_map l)
+
+let nexts = function
+ | [] -> "next", ""
+ | l -> "next", String.concat " " (List.rev_map next_map l)
+
let export_csys s =
let path = path_of_uri !G.xdir s.Q.uri in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out ccs_root system;
let attrs = [uri s.Q.uri] in
- let contents = tag "ToInfinity" [arity s.Q.is; marks s.Q.is] in
+ let contents out tab =
+ tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
+ tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
+ tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
+ in
tag ccs_root attrs ~contents out 0;
close_out och
<xsl:template name="lambda">
<a name="" title="{@mark}">
<span style="{$binder}">
- <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <xsl:choose>
+ <xsl:when test="@level=0">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:when>
+ <xsl:when test="@level=1">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ </xsl:when>
+ <xsl:when test="@level=2">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ </xsl:when>
+ <xsl:when test="not(@level)">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:text disable-output-escaping="yes">&infin;</xsl:text></sup>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:otherwise>
+ </xsl:choose>
</span>
</a>
</xsl:template>
<xsl:variable name="index">
<xsl:value-of select="@position"/>
<xsl:if test="@offset != 0">
- <xsl:call-template name="plus"/>
- <xsl:value-of select="@offset"/>
+ <xsl:call-template name="plus"/>
+ <xsl:value-of select="@offset"/>
</xsl:if>
</xsl:variable>
<a name="" title="{$index}">
<!-- CONVERSION CONSTRAINT SYSTEM -->
-<!ENTITY % ccs '(ToInfinity)'>
+<!ENTITY % cc '(ToPositive|ToOne|ToNext)'>
-<!ELEMENT ToInfinity EMPTY>
-<!ATTLIST ToInfinity
+<!ENTITY % ccs '(%cc;*)'>
+
+<!ELEMENT ToPositive EMPTY>
+<!ATTLIST ToPositive
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToOne EMPTY>
+<!ATTLIST ToOne
arity NMTOKEN #IMPLIED
mark NMTOKENS #IMPLIED
>
+<!ELEMENT ToNext EMPTY>
+<!ATTLIST ToNext
+ arity NMTOKEN #IMPLIED
+ prec NMTOKENS #IMPLIED
+ next NMTOKENS #IMPLIED
+>
+
<!ELEMENT CCS %ccs;>
<!ATTLIST CCS
uri CDATA #REQUIRED
projects / helm.git / commitdiff