From: Ferruccio Guidi Date: Sun, 2 Jan 2011 15:47:01 +0000 (+0000) Subject: - ld-html-root: ported to permanent lambda-delta url X-Git-Tag: make_still_working~2610 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;p=helm.git - ld-html-root: ported to permanent lambda-delta url - ld.dtd: we can specify a language encoding for the metalinguistic annotation, moreover we export the metalinguistic classification - the other files are modified in order to support this feature --- diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 806379008..80019a800 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -7,7 +7,7 @@ endif 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 diff --git a/helm/software/lambda-delta/src/automath/autCrg.ml b/helm/software/lambda-delta/src/automath/autCrg.ml index bba3fc265..548e1ec73 100644 --- a/helm/software/lambda-delta/src/automath/autCrg.ml +++ b/helm/software/lambda-delta/src/automath/autCrg.ml @@ -217,7 +217,7 @@ let xlate_entity err f st = function 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 diff --git a/helm/software/lambda-delta/src/common/entity.ml b/helm/software/lambda-delta/src/common/entity.ml index b88af255c..9915dd3c3 100644 --- a/helm/software/lambda-delta/src/common/entity.ml +++ b/helm/software/lambda-delta/src/common/entity.ml @@ -20,11 +20,16 @@ type name = id * bool (* token, real? *) 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 *) @@ -82,15 +87,15 @@ let rec mark err f = function | _ :: 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 diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index 5d2faf900..072073c18 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -142,8 +142,8 @@ let pp_attrs out a = | 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 diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml index 6ffe592de..bdd96bf6b 100644 --- a/helm/software/lambda-delta/src/text/txt.ml +++ b/helm/software/lambda-delta/src/text/txt.ml @@ -15,7 +15,7 @@ type ix = int (* index *) type id = string (* identifier *) -type desc = string (* description *) +type info = string * string (* language, text *) type kind = Decl (* generic declaration *) | Ax (* axiom *) @@ -60,7 +60,7 @@ type command = | 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 diff --git a/helm/software/lambda-delta/src/text/txtCrg.ml b/helm/software/lambda-delta/src/text/txtCrg.ml index 980b74a08..ce3853fcb 100644 --- a/helm/software/lambda-delta/src/text/txtCrg.ml +++ b/helm/software/lambda-delta/src/text/txtCrg.ml @@ -105,24 +105,24 @@ let xlate_term f st lenv t = 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 @@ -131,20 +131,23 @@ let xlate_entity err f gen st = function {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 ******************************************************) diff --git a/helm/software/lambda-delta/src/text/txtLexer.mll b/helm/software/lambda-delta/src/text/txtLexer.mll index efee66051..ea5c6e004 100644 --- a/helm/software/lambda-delta/src/text/txtLexer.mll +++ b/helm/software/lambda-delta/src/text/txtLexer.mll @@ -44,6 +44,7 @@ and token = parse | 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 } diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly index 1eae31980..2c9abe079 100644 --- a/helm/software/lambda-delta/src/text/txtParser.mly +++ b/helm/software/lambda-delta/src/text/txtParser.mly @@ -33,7 +33,7 @@ %token IX %token 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 entry @@ -49,9 +49,14 @@ | {} | FS {} ; + main: + | { false } + | MAIN { true } + ; comment: - | { "" } - | STR { $1 } + | { "", "" } + | STR { "", $1 } + | STR STR { $1, $2 } ; ids: | ID { [$1] } @@ -129,25 +134,25 @@ ; 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 {} | diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml index 7355c98a7..2796bae24 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -30,7 +30,11 @@ let ccs_name = "ccs.ldc" 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 @@ -120,12 +124,23 @@ let mark a = 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 @@ -133,7 +148,7 @@ let export_entity pp_term (a, u, b) = 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) @@ -141,7 +156,7 @@ let export_entity pp_term (a, u, b) = 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 @@ -168,7 +183,7 @@ let export_csys s = 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; diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.mli b/helm/software/lambda-delta/src/xml/xmlLibrary.mli index ebd4157d9..5fd4dc38b 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.mli +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.mli @@ -54,3 +54,6 @@ val name: Entity.attrs -> attr val mark: Entity.attrs -> attr val meta: Entity.attrs -> attr + +val info: Entity.attrs -> attr list + diff --git a/helm/software/lambda-delta/xml/ld-html-root.xsl b/helm/software/lambda-delta/xml/ld-html-root.xsl index 79cf8352a..72958381b 100644 --- a/helm/software/lambda-delta/xml/ld-html-root.xsl +++ b/helm/software/lambda-delta/xml/ld-html-root.xsl @@ -26,17 +26,17 @@ lambda-delta digital library (LDDL)
- + [lambda-delta home]
@@ -45,7 +45,7 @@
[Spacer]
@@ -66,13 +66,13 @@ [Generated from XML via XSL] - + [Powered by Helena lambda-delta processor] @@ -130,5 +135,6 @@