RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
-LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl
+LDDLURL = http://lambda-delta.info/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
print_newline (); CrgOutput.pp_term print_string t;
*)
let b = E.Abbr t in
- let a = E.Mark st.line :: if trans then [] else [E.Priv] in
+ let a = E.Mark st.line :: if trans then [] else [E.Meta [E.Private]] in
let entity = a, uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
type names = name list
-type attr = Name of name (* name *)
- | Apix of int (* additional position index *)
- | Mark of int (* node marker *)
- | Meta of string (* metaliguistic annotation *)
- | Priv (* private global definition *)
+type meta = Main (* main object *)
+ | InProp (* inhabitant of a proposition *)
+ | Progress (* uncompleted object *)
+ | Private (* private global definition *)
+
+type attr = Name of name (* name *)
+ | Apix of int (* additional position index *)
+ | Mark of int (* node marker *)
+ | Meta of meta list (* metaliguistic classification *)
+ | Info of (string * string) (* metaliguistic annotation: language (defaults to "en-US"), text *)
type attrs = attr list (* attributes *)
| _ :: tl -> mark err f tl
| [] -> err ()
-let rec priv err f = function
- | Priv :: _ -> f ()
- | _ :: tl -> priv err f tl
- | [] -> err ()
-
let rec meta err f = function
- | Meta s :: _ -> f s
- | _ :: tl -> meta err f tl
- | [] -> err ()
+ | Meta ms :: _ -> f ms
+ | _ :: tl -> meta err f tl
+ | [] -> err ()
+
+let rec info err f = function
+ | Info (lg, tx) :: _ -> f lg tx
+ | _ :: tl -> info err f tl
+ | [] -> err ()
let resolve err f name a =
let rec aux i = function
| E.Name (s, false) -> out (P.sprintf "~%s;" s)
| E.Apix i -> out (P.sprintf "+%i;" i)
| E.Mark i -> out (P.sprintf "@%i;" i)
- | E.Meta s -> out (P.sprintf "\"%s\";" s)
- | E.Priv -> out (P.sprintf "%s;" "~")
+ | E.Meta _ -> ()
+ | E.Info _ -> ()
in
List.iter map a
type id = string (* identifier *)
-type desc = string (* description *)
+type info = string * string (* language, text *)
type kind = Decl (* generic declaration *)
| Ax (* axiom *)
| Sorts of (int option * id) list
(* section: Some id = open, None = close last *)
| Section of id option
-(* entity: class, name, description, contents *)
- | Entity of kind * N.level * id * desc * term
+(* entity: main?, class, name, info, contents *)
+ | Entity of bool * kind * N.level * id * info * term
(* predefined generated entity: arguments *)
| Generate of term list
TT.contract (xlate_term f st lenv) t
let mk_contents n tt = function
- | T.Decl -> [], E.Abst (n, tt)
- | T.Ax -> [], E.Abst (n, tt)
- | T.Cong -> [], E.Abst (n, tt)
- | T.Def -> [], E.Abbr tt
- | T.Th -> [], E.Abbr tt
+ | T.Decl -> [] , E.Abst (n, tt)
+ | T.Ax -> [E.InProp] , E.Abst (n, tt)
+ | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
+ | T.Def -> [] , E.Abbr tt
+ | T.Th -> [E.InProp] , E.Abbr tt
let xlate_entity err f gen st = function
- | T.Require _ ->
+ | T.Require _ ->
err st
- | T.Section (Some name) ->
+ | T.Section (Some name) ->
err {st with path = name :: st.path}
- | T.Section None ->
+ | T.Section None ->
begin match st.path with
| _ :: ptl ->
err {st with path = ptl}
| _ -> assert false
end
- | T.Sorts sorts ->
+ | T.Sorts sorts ->
let map st (xix, s) =
let ix = match xix with
| None -> st.sort
{st with sort = H.set_sorts ix [s]}
in
err (List.fold_left map st sorts)
- | T.Graph id ->
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (kind, n, id, meta, t) ->
+ | T.Entity (main, kind, n, id, info, t) ->
let uri = uri_of_id st id st.path in
Hashtbl.add henv id uri;
let tt = xlate_term C.start st D.empty_lenv t in
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let a, b = mk_contents n tt kind in
- let a = if meta <> "" then E.Meta meta :: a else a in
+ let a = [] in
+ let ms, b = mk_contents n tt kind in
+ let ms = if main then E.Main :: ms else ms in
+ let a = if ms <> [] then E.Meta ms :: a else a in
+ let a = if info <> ("", "") then E.Info info :: a else a in
let entity = E.Mark st.line :: a, uri, b in
f {st with line = succ st.line} entity
- | T.Generate _ ->
+ | T.Generate _ ->
err st
(* Interface functions ******************************************************)
| IX as ix { out ("IX " ^ ix); TP.IX (int_of_string ix) }
| QT { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s }
| "\\graph" { out "GRAPH"; TP.GRAPH }
+ | "\\main" { out "MAIN"; TP.MAIN }
| "\\decl" { out "DECL"; TP.DECL }
| "\\ax" { out "AX"; TP.AX }
| "\\cong" { out "CONG"; TP.CONG }
%token <int> IX
%token <string> ID STR
%token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
- %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
+ %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option> entry
| {}
| FS {}
;
+ main:
+ | { false }
+ | MAIN { true }
+ ;
comment:
- | { "" }
- | STR { $1 }
+ | { "", "" }
+ | STR { "", $1 }
+ | STR STR { $1, $2 }
;
ids:
| ID { [$1] }
;
xentity:
| GRAPH ID
- { T.Graph $2 }
- | decl level comment ID CN term
- { T.Entity ($1, $2, $4, $3, $6) }
- | def level comment ID EQ term
- { T.Entity ($1, $2, $4, $3, $6) }
- | def level comment ID EQ term CN term
- { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) }
+ { T.Graph $2 }
+ | main decl level comment ID CN term
+ { T.Entity ($1, $2, $3, $5, $4, $7) }
+ | main def level comment ID EQ term
+ { T.Entity ($1, $2, $3, $5, $4, $7) }
+ | main def level comment ID EQ term CN term
+ { T.Entity ($1, $2, $3, $5, $4, T.Cast ($9, $7)) }
| GEN term
- { T.Generate [$2] }
+ { T.Generate [$2] }
| GEN terms
- { T.Generate $2 }
+ { T.Generate $2 }
| REQ ids
- { T.Require $2 }
+ { T.Require $2 }
| OPEN ID
- { T.Section (Some $2) }
+ { T.Section (Some $2) }
| CLOSE
- { T.Section None }
+ { T.Section None }
| SORTS sorts
- { T.Sorts $2 }
+ { T.Sorts $2 }
;
start:
| GRAPH {} | decl {} | def {} | GEN {} |
let ccs_root = "CCS"
-let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
+let home = "http://lambda-delta.info"
+
+let system = home ^ "/" ^ base ^ "/ld.dtd"
+
+let xmlns = "xmlns", home
let path_of_uri xdir uri =
let base = F.concat xdir base in
let level n =
"level", N.to_string n
-(* TODO: the string s must be quoted *)
let meta a =
+ let map = function
+ | E.Main -> "Main"
+ | E.InProp -> "InProp"
+ | E.Progress -> "Progress"
+ | E.Private -> "Private"
+ in
let err () = "meta", "" in
- let f s = "meta", s in
+ let f ms = "meta", String.concat " " (List.rev_map map ms) in
E.meta err f a
+(* TODO: the string tx must be quoted *)
+let info a =
+ let err () = ["lang", ""; "info", ""] in
+ let f lg tx = ["lang", lg; "info", tx] in
+ E.info err f a
+
let export_entity pp_term (a, u, b) =
let path = path_of_uri !G.xdir u in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out obj_root system;
let a = E.Name (U.name_of_uri u, true) :: a in
- let attrs = [uri u; name a; mark a; meta a] in
+ let attrs = uri u :: name a :: mark a :: meta a :: info a in
let contents = match b with
| E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w)
| E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
in
let opts = if !G.si then "si" else "" in
let shp = H.string_of_graph () in
- let attrs = ["hierarchy", shp; "options", opts] in
+ let attrs = [xmlns; "hierarchy", shp; "options", opts] in
tag obj_root attrs ~contents out 0;
close_out och
let och = open_out name 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 attrs = [xmlns; uri s.Q.uri] 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;
val mark: Entity.attrs -> attr
val meta: Entity.attrs -> attr
+
+val info: Entity.attrs -> attr list
+
<meta name="description" content="lambda-delta digital library"/>
<title>lambda-delta digital library (LDDL)</title>
<link rel="stylesheet" type="text/css"
- href="http://helm.cs.unibo.it/lambda-delta/static/lddl/ld-html.css"
+ href="http://lambda-delta.info/static/lddl/ld-html.css"
/>
<link rel="shortcut icon"
- href="http://helm.cs.unibo.it/lambda-delta/download/crux-16.ico"
+ href="http://lambda-delta.info/download/crux-16.ico"
/>
</head><body>
<div class="spacer">
- <a href="http://helm.cs.unibo.it/lambda-delta/">
+ <a href="http://lambda-delta.info/">
<img class="icon32"
alt="[lambda-delta home]" title="lambda-delta home"
- src="http://helm.cs.unibo.it/lambda-delta/download/crux-32.png"
+ src="http://lambda-delta.info/download/crux-32.png"
/></a>
</div>
<div class="head1">
<div class="spacer">
<img class="rule"
alt="[Spacer]" title="lambda-delta rainbow rule"
- src="http://helm.cs.unibo.it/lambda-delta/download/rainbow.png"
+ src="http://lambda-delta.info/download/rainbow.png"
/>
</div>
<xsl:apply-templates/>
<img class="w3c"
alt="[Generated from XML via XSL]"
title="Generated from XML via XSL"
- src="http://helm.cs.unibo.it/lambda-delta/download/xml_xsl2.png"
+ src="http://lambda-delta.info/download/xml_xsl2.png"
/></a>
- <a href="http://helm.cs.unibo.it/lambda-delta/implementation.html#helena">
+ <a href="http://lambda-delta.info/implementation.html#helena">
<img class="w3c"
alt="[Powered by Helena lambda-delta processor]"
title="Powered by Helena lambda-delta processor"
- src="http://helm.cs.unibo.it/lambda-delta/download/helena-label.png"
+ src="http://lambda-delta.info/download/helena-label.png"
/></a>
<a href="http://www.w3.org/Graphics/PNG/">
<img class="w3c"
<!ELEMENT ABST %term;>
<!ATTLIST ABST
- uri CDATA #REQUIRED
- level NMTOKEN #IMPLIED
- name NMTOKEN #IMPLIED
- mark NMTOKEN #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ level NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
>
<!ELEMENT ABBR %term;>
<!ATTLIST ABBR
- uri CDATA #REQUIRED
- name NMTOKEN #IMPLIED
- mark NMTOKEN #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
>
<!ELEMENT ENTITY %entity;>
<!ATTLIST ENTITY
- hierarchy NMTOKEN #REQUIRED
+ xmlns CDATA #FIXED "http://lambda-delta.info"
+ hierarchy NMTOKEN #REQUIRED
options NMTOKENS #IMPLIED
>
<!ELEMENT CCS %ccs;>
<!ATTLIST CCS
- uri CDATA #REQUIRED
+ xmlns CDATA #FIXED "http://lambda-delta.info"
+ uri CDATA #REQUIRED
>
projects / helm.git / commitdiff