From: Ferruccio Guidi Date: Fri, 19 Feb 2010 16:27:17 +0000 (+0000) Subject: - we added a parser for lambda-delta textual syntax (file extension .hln) X-Git-Tag: make_still_working~3033 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93205dc852fa208b48a05757d05d9910b7d45fa1;p=helm.git - we added a parser for lambda-delta textual syntax (file extension .hln) - we now parse the input files with a straming policy - we added a Meta attribute for explanatory metalinguistic comments - brg: missing type casts were not inserted (fixed) --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index c71e6771b..95ddf8e2c 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -10,6 +10,13 @@ lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +text/txt.cmo: +text/txt.cmx: +text/txtParser.cmi: text/txt.cmx +text/txtParser.cmo: text/txt.cmx text/txtParser.cmi +text/txtParser.cmx: text/txt.cmx text/txtParser.cmi +text/txtLexer.cmo: text/txtParser.cmi lib/log.cmi +text/txtLexer.cmx: text/txtParser.cmx lib/log.cmx automath/aut.cmo: automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx @@ -133,6 +140,11 @@ complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \ complete_rg/crgOutput.cmx: lib/nUri.cmx common/library.cmx \ common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ complete_rg/crgOutput.cmi +complete_rg/crgTxt.cmi: text/txt.cmx common/entity.cmx complete_rg/crg.cmx +complete_rg/crgTxt.cmo: text/txt.cmx lib/nUri.cmi common/hierarchy.cmi \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx complete_rg/crgTxt.cmi +complete_rg/crgTxt.cmx: text/txt.cmx lib/nUri.cmx common/hierarchy.cmx \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx complete_rg/crgTxt.cmi complete_rg/crgAut.cmi: common/entity.cmx complete_rg/crg.cmx \ automath/aut.cmx complete_rg/crgAut.cmo: lib/nUri.cmi common/entity.cmx complete_rg/crg.cmx \ @@ -169,23 +181,25 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx toplevel/metaBrg.cmi toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx toplevel/metaBrg.cmi -toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ - toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ - toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \ - common/library.cmi common/hierarchy.cmi common/entity.cmx \ +toplevel/top.cmo: text/txtParser.cmi text/txtLexer.cmx text/txt.cmx \ + lib/time.cmx common/output.cmi lib/nUri.cmi toplevel/metaOutput.cmi \ + toplevel/metaLibrary.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ + toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi common/library.cmi \ + common/hierarchy.cmi common/entity.cmx complete_rg/crgTxt.cmi \ complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi complete_rg/crgAut.cmi \ complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \ basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \ - automath/autOutput.cmi automath/autLexer.cmx -toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ - toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ - toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \ - common/library.cmx common/hierarchy.cmx common/entity.cmx \ + automath/autOutput.cmi automath/autLexer.cmx automath/aut.cmx +toplevel/top.cmx: text/txtParser.cmx text/txtLexer.cmx text/txt.cmx \ + lib/time.cmx common/output.cmx lib/nUri.cmx toplevel/metaOutput.cmx \ + toplevel/metaLibrary.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ + toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx common/library.cmx \ + common/hierarchy.cmx common/entity.cmx complete_rg/crgTxt.cmx \ complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx complete_rg/crgAut.cmx \ complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \ basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \ - automath/autOutput.cmx automath/autLexer.cmx + automath/autOutput.cmx automath/autLexer.cmx automath/aut.cmx diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make index 5730e32e6..ed00c8bbc 100644 --- a/helm/software/lambda-delta/Make +++ b/helm/software/lambda-delta/Make @@ -1 +1 @@ -lib automath common basic_ag basic_rg complete_rg toplevel +lib text automath common basic_ag basic_rg complete_rg toplevel diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index c772837b3..7bb9a4a6f 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -25,14 +25,18 @@ %{ module A = Aut + + let debug = false + + let _ = Parsing.set_trace debug %} %token NUM %token IDENT %token EOF MINUS PLUS TIMES AT FS CN CM SC QT TD OP CP OB CB OA CA %token TYPE PROP DEF EB E PN EXIT - %start book - %type book + %start entry + %type entry %% path: MINUS {} | FS {} ; oftype: CN {} | CM {} ; @@ -71,25 +75,28 @@ | term { [$1] } | term CM terms { $1 :: $3 } ; + + start: + | PLUS {} | MINUS {} | EXIT {} | eof {} + | star {} | IDENT {} | OB {} + ; entity: - | PLUS IDENT { A.Section (Some (true, $2)) } - | PLUS TIMES IDENT { A.Section (Some (false, $3)) } - | MINUS IDENT { A.Section None } - | EXIT { A.Section None } - | star { A.Context None } - | qid star { A.Context (Some $1) } - | IDENT DEF EB sc term { A.Block ($1, $5) } - | IDENT sc term DEF EB { A.Block ($1, $3) } - | OB IDENT oftype term CB { A.Block ($2, $4) } - | IDENT DEF PN sc term { A.Decl ($1, $5) } - | IDENT sc term DEF PN { A.Decl ($1, $3) } - | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) } - | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) } - ; - entities: - | { [] } - | entity entities { $1 :: $2 } - ; - book: - | entities eof { $1 } + | PLUS IDENT { Some (A.Section (Some (true, $2))) } + | PLUS TIMES IDENT { Some (A.Section (Some (false, $3))) } + | MINUS IDENT { Some (A.Section None) } + | EXIT { Some (A.Section None) } + | star { Some (A.Context None) } + | qid star { Some (A.Context (Some $1)) } + | IDENT DEF EB sc term { Some (A.Block ($1, $5)) } + | IDENT sc term DEF EB { Some (A.Block ($1, $3)) } + | OB IDENT oftype term CB { Some (A.Block ($2, $4)) } + | IDENT DEF PN sc term { Some (A.Decl ($1, $5)) } + | IDENT sc term DEF PN { Some (A.Decl ($1, $3)) } + | IDENT DEF expand term sc term { Some (A.Def ($1, $6, $3, $4)) } + | IDENT sc term DEF expand term { Some (A.Def ($1, $3, $5, $6)) } + | eof { None } ; + entry: + | entity { $1, false } + | entity start { $1, true } + diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 763f61af4..829ee82f8 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -101,7 +101,7 @@ let rec pp_term c frm = function | B.Sort h -> let err () = F.fprintf frm "@[*%u@]" h in let f s = F.fprintf frm "@[%s@]" s in - H.get_sort err f h + H.string_of_sort err f h | B.LRef i -> let f = function | Some (id, _) -> F.fprintf frm "@[%s@]" id diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index e4e7489ca..124f98974 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -158,7 +158,7 @@ let rec pp_term e frm = function | B.Sort (_, h) -> let err _ = F.fprintf frm "@[*%u@]" h in let f s = F.fprintf frm "@[%s@]" s in - H.get_sort err f h + H.string_of_sort err f h | B.LRef (_, i) -> let err _ = F.fprintf frm "@[#%u@]" i in if !O.indexes then err () else @@ -214,7 +214,7 @@ let rec exp_term e t out tab = match t with let a = let err _ = a in let f s = Y.Name (s, true) :: a in - H.get_sort err f l + H.string_of_sort err f l in let attrs = [X.position l; X.name a] in X.tag X.sort attrs out tab diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 311061aaa..4c1ae61db 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -28,6 +28,10 @@ let type_check err f st = function L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t | a, uri, Y.Abbr t -> let f xt tt = + let xt = match xt with + | B.Cast _ -> xt + | _ -> B.Cast ([], tt, xt) + in let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e in L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index d6314150b..0fa060321 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -15,6 +15,7 @@ type id = Aut.id type attr = Name of id * bool (* name, real? *) | Apix of int (* additional position index *) | Mark of int (* node marker *) + | Meta of string (* metaliguistic annotation *) | Priv (* private global definition *) type attrs = attr list (* attributes *) @@ -65,6 +66,14 @@ let rec get_names f = function | e :: tl -> let f a = f (e :: a) in get_names f tl +let count_names a = + let rec aux k = function + | [] -> k + | Name _ :: tl -> aux (succ k) tl + | _ :: tl -> aux k tl + in + aux 0 a + let rec apix err f = function | Apix i :: _ -> f i | _ :: tl -> apix err f tl diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index f8a58dc0f..7a1610e8b 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -28,9 +28,18 @@ let set_sort h s = let set_sorts ss i = List.fold_left set_sort i ss -let get_sort err f h = +let string_of_sort err f h = try f (H.find sort h) with Not_found -> err () +let sort_of_string err f s = + let map h n = function + | None when n = s -> Some h + | xh -> xh + in + match H.fold map sort None with + | None -> err () + | Some h -> f h + let string_of_graph (s, _) = s let apply (_, g) h = (g h) diff --git a/helm/software/lambda-delta/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli index 19e943054..da15a64dd 100644 --- a/helm/software/lambda-delta/common/hierarchy.mli +++ b/helm/software/lambda-delta/common/hierarchy.mli @@ -13,7 +13,9 @@ type graph val set_sorts: string list -> int -> int -val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a +val string_of_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a + +val sort_of_string: (unit -> 'a) -> (int -> 'a) -> string -> 'a val graph_of_string: (unit -> 'a) -> (graph -> 'a) -> string -> 'a diff --git a/helm/software/lambda-delta/complete_rg/Make b/helm/software/lambda-delta/complete_rg/Make index 71e141c30..33e3388fb 100644 --- a/helm/software/lambda-delta/complete_rg/Make +++ b/helm/software/lambda-delta/complete_rg/Make @@ -1 +1 @@ -crg crgOutput crgAut crgBrg +crg crgOutput crgTxt crgAut crgBrg diff --git a/helm/software/lambda-delta/complete_rg/crg.ml b/helm/software/lambda-delta/complete_rg/crg.ml index fa76c6164..0b0853386 100644 --- a/helm/software/lambda-delta/complete_rg/crg.ml +++ b/helm/software/lambda-delta/complete_rg/crg.ml @@ -46,7 +46,7 @@ let push_bind f lenv a b = f (EBind (lenv, a, b)) let push_proj f lenv a e = f (EProj (lenv, a, e)) -let push2 err f lenv attr ?t = match lenv, t with +let push2 err f lenv attr ?t () = match lenv, t with | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws))) | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs))) | EBind (e, a, Void n), None -> f (EBind (e, (attr :: a), Void (succ n))) @@ -55,20 +55,23 @@ let push2 err f lenv attr ?t = match lenv, t with (* this id not tail recursive *) let resolve_lref err f id lenv = let rec aux f i k = function - | ESort -> err () - | EBind (tl, a, _) -> + | ESort -> err () + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> aux f i k tl + | EBind (tl, a, _) -> let err kk = aux f (succ i) (k + kk) tl in let f j = f i j (k + j) in Entity.resolve err f id a - | EProj _ -> assert false (* TODO *) + | EProj _ -> assert false (* TODO *) in aux f 0 0 lenv let rec get_name err f i j = function | ESort -> err i - | EBind (tl, a, Abst []) -> get_name err f i j tl - | EBind (tl, a, Abbr []) -> get_name err f i j tl - | EBind (tl, a, Void 0) -> get_name err f i j tl + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> get_name err f i j tl | EBind (_, a, _) when i = 0 -> let err () = err i in Entity.get_name err f j a @@ -77,3 +80,17 @@ let rec get_name err f i j = function | EProj (tl, _, e) -> let err i = get_name err f i j tl in get_name err f i j e + +let get_index err f i j lenv = + let rec aux f i k = function + | ESort -> err i + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> aux f i k tl + | EBind (_, a, _) when i = 0 -> + if Entity.count_names a > j then f (k + j) else err i + | EBind (tl, a, _) -> + aux f (pred i) (k + Entity.count_names a) tl + | EProj _ -> assert false (* TODO *) + in + aux f i 0 lenv diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml index ecc4a33b1..593074ad8 100644 --- a/helm/software/lambda-delta/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml @@ -25,7 +25,8 @@ let pp_attrs out a = | Y.Name (s, false) -> out (P.sprintf "~%s;" s) | Y.Apix i -> out (P.sprintf "+%i;" i) | Y.Mark i -> out (P.sprintf "@%i;" i) - | Y.Priv -> out (P.sprintf "%s;" "~") + | Y.Meta s -> out (P.sprintf "\"%s\";" s) + | Y.Priv -> out (P.sprintf "%s;" "~") in List.iter map a @@ -71,7 +72,7 @@ let list_rev_iter map e ns l out tab = pp_lenv print_string e; print_string " |- "; pp_term print_string hd; print_newline (); *) - map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) + map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ()) in aux err f e (ns, tl) | _ -> err () @@ -91,7 +92,7 @@ let rec exp_term e t out tab = match t with let a = let err _ = a in let f s = Y.Name (s, true) :: a in - H.get_sort err f l + H.string_of_sort err f l in let attrs = [X.position l; X.name a] in X.tag X.sort attrs out tab diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml new file mode 100644 index 000000000..57e946070 --- /dev/null +++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml @@ -0,0 +1,139 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module U = NUri +module H = U.UriHash +module C = Cps +module Y = Entity +module T = Txt +module D = Crg + +type status = { + path: T.id list; (* current section path *) + line: int; (* line number *) + mk_uri:Y.uri_generator (* uri generator *) +} + +let henv_size = 7000 (* hash tables initial size *) + +let henv = H.create henv_size (* optimized global environment *) + +(* Internal functions *******************************************************) + +let initial_status mk_uri = { + path = []; line = 1; mk_uri = mk_uri +} + +let name_of_id id = Y.Name (id, true) + +let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) + +let mk_gref f uri = f (D.TGRef ([], uri)) + +let uri_of_id st id path = + let str = String.concat "/" path in + let str = Filename.concat str id in + let str = st.mk_uri str in + U.uri_of_string str + +let complete_id f st id = f id st.path + +let resolve_gref st id path = + let uri = uri_of_id st id path in + try H.find henv uri; Some uri + with Not_found -> None + +let rec resolve_gref_relaxed err f st id path = + match resolve_gref st id path, path with + | Some uri, _ -> f uri + | None, _ :: path -> resolve_gref_relaxed err f st id path + | None, [] -> err () + +let rec xlate_term f st lenv = function + | T.Sort h -> + f (D.TSort ([], h)) + | T.NSrt id -> + let f h = (D.TSort ([], h)) in + Hierarchy.sort_of_string C.err f id + | T.LRef (i, j) -> + D.get_index C.err (mk_lref f i j) i j lenv + | T.NRef id -> + let err () = complete_id (resolve_gref_relaxed C.err (mk_gref f) st) st id in + D.resolve_lref err (mk_lref f) id lenv + | T.Cast (u, t) -> + let f uu tt = f (D.TCast ([], uu, tt)) in + let f uu = xlate_term (f uu) st lenv t in + xlate_term f st lenv u + | T.Appl (vs, t) -> + let map f = xlate_term f st lenv in + let f vvs tt = f (D.TAppl ([], vvs, tt)) in + let f vvs = xlate_term (f vvs) st lenv t in + C.list_map f map vs + | T.Bind (b, t) -> + let lenv, a, bb = match b with + | T.Abst xws -> + let map (lenv, a, wws) (id, w) = + let attr = name_of_id id in + let ww = xlate_term C.start st lenv w in + D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws + in + let lenv = D.push_bind C.start lenv [] (D.Abst []) in + let lenv, a, wws = List.fold_left map (lenv, [], []) xws in + lenv, a, D.Abst wws + | T.Abbr xvs -> + let map (lenv, a, vvs) (id, v) = + let attr = name_of_id id in + let vv = xlate_term C.start st lenv v in + D.push2 C.err C.start lenv attr ~t:vv (), attr :: a, vv :: vvs + in + let lenv = D.push_bind C.start lenv [] (D.Abbr []) in + let lenv, a, vvs = List.fold_left map (lenv, [], []) xvs in + lenv, a, D.Abbr vvs + | T.Void ids -> + let map (lenv, a, n) id = + let attr = name_of_id id in + D.push2 C.err C.start lenv attr (), attr :: a, succ n + in + let lenv = D.push_bind C.start lenv [] (D.Void 0) in + let lenv, a, n = List.fold_left map (lenv, [], 0) ids in + lenv, a, D.Void n + in + let f tt = f (D.TBind (a, bb, tt)) in + xlate_term f st lenv t + + +let xlate_entity err f st = function + | T.Section (Some name) -> + err {st with path = name :: st.path} + | T.Section None -> + begin match st.path with + | _ :: ptl -> + err {st with path = ptl} + | _ -> assert false + end + | T.Global (def, id, meta, t) -> + let uri = uri_of_id st id st.path in + H.add henv uri (); + let tt = xlate_term C.start st D.empty_lenv t in +(* + print_newline (); CrgOutput.pp_term print_string tt; +*) + let a = if meta <> "" then [Y.Meta meta] else [] in + let b = if def then Y.Abbr tt else Y.Abst tt in + let entity = Y.Mark st.line :: a, uri, b in + f {st with line = succ st.line} entity + +(* Interface functions ******************************************************) + +let initial_status mk_uri = + initial_status mk_uri + +let crg_of_txt = xlate_entity diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.mli b/helm/software/lambda-delta/complete_rg/crgTxt.mli new file mode 100644 index 000000000..9570ffc6d --- /dev/null +++ b/helm/software/lambda-delta/complete_rg/crgTxt.mli @@ -0,0 +1,17 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type status + +val initial_status: Entity.uri_generator -> status + +val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) -> + status -> Txt.entity -> 'a diff --git a/helm/software/lambda-delta/text/Make b/helm/software/lambda-delta/text/Make new file mode 100644 index 000000000..bb0980c0f --- /dev/null +++ b/helm/software/lambda-delta/text/Make @@ -0,0 +1 @@ +txt txtParser txtLexer diff --git a/helm/software/lambda-delta/text/prova.hln b/helm/software/lambda-delta/text/prova.hln new file mode 100644 index 000000000..a782fda1c --- /dev/null +++ b/helm/software/lambda-delta/text/prova.hln @@ -0,0 +1,11 @@ +\open pippo + +\global a : *Set + +\global b : *Prop + +\global f = [x:*Set].[y:*Prop].x + +\global "commento\"" c = f(a,b) : *Set + +\close diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml new file mode 100644 index 000000000..f874a273e --- /dev/null +++ b/helm/software/lambda-delta/text/txt.ml @@ -0,0 +1,31 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type ix = int (* index *) + +type id = string (* identifier *) + +type comm = string (* comment *) + +type bind = Abst of (id * term) list (* name, domain *) + | Abbr of (id * term) list (* name, bodies *) + | Void of id list (* names *) + +and term = Sort of ix (* level *) + | NSrt of id (* named level *) + | LRef of ix * ix (* index, offset *) + | NRef of id (* name *) + | Cast of term * term (* domain, element *) + | Appl of term list * term (* arguments, function *) + | Bind of bind * term (* binder, scope *) + +type entity = Section of id option (* section: Some id = open, None = close last *) + | Global of bool * id * comm * term (* global entity: false = decl, true = def *) diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll new file mode 100644 index 000000000..6a53d828f --- /dev/null +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -0,0 +1,62 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +{ + module L = Log + module P = TxtParser + + let debug = false + let out s = if debug then L.warn s else () +} + +let BS = "\\" +let SPC = [' ' '\t' '\n']+ +let OC = "\\*" +let CC = "*\\" +let FIG = ['0'-'9'] +let ALPHA = ['A'-'Z' 'a'-'z' '_'] +let QT = '"' +let ID = ALPHA+ (ALPHA | FIG)* +let IX = FIG+ + +rule block_comment = parse + | CC { () } + | OC { block_comment lexbuf; block_comment lexbuf } + | _ { block_comment lexbuf } +and qstring = parse + | QT { "" } + | SPC { " " ^ qstring lexbuf } + | BS BS { "\\" ^ qstring lexbuf } + | BS QT { "\"" ^ qstring lexbuf } + | _ { Lexing.lexeme lexbuf ^ qstring lexbuf } +and token = parse + | SPC { token lexbuf } + | OC { block_comment lexbuf; token lexbuf } + | ID { out "ID"; P.ID (Lexing.lexeme lexbuf) } + | IX { out "IX"; P.IX (int_of_string (Lexing.lexeme lexbuf)) } + | QT { let s = qstring lexbuf in out "STR"; P.STR s } + | "\\open" { out "OPEN"; P.OPEN } + | "\\close" { out "CLOSE"; P.CLOSE } + | "\\global" { out "GLOBAL"; P.GLOBAL } + | "(" { out "OP"; P.OP } + | ")" { out "CP"; P.CP } + | "[" { out "OB"; P.OB } + | "]" { out "CB"; P.CB } + | "<" { out "OA"; P.OA } + | ">" { out "CA"; P.CA } + | "." { out "FS"; P.FS } + | ":" { out "CN"; P.CN } + | "," { out "CM"; P.CM } + | "=" { out "EQ"; P.EQ } + | "*" { out "STAR"; P.STAR } + | "#" { out "HASH"; P.HASH } + | "+" { out "PLUS"; P.PLUS } + | eof { out "EOF"; P.EOF } diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly new file mode 100644 index 000000000..b3c7037a3 --- /dev/null +++ b/helm/software/lambda-delta/text/txtParser.mly @@ -0,0 +1,108 @@ +/* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + */ + +%{ + module T = Txt + + let debug = false + + let _ = Parsing.set_trace debug +%} + %token IX + %token ID STR + %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS + %token OPEN CLOSE GLOBAL EOF + + %start entry + %type entry +%% + hash: + | {} + | HASH {} + ; + fs: + | {} + | FS {} + ; + comment: + | { "" } + | STR { $1 } + ; + ids: + | ID { [$1] } + | ID CM ids { $1 :: $3 } + ; + + abst: + | ID CN term { $1, $3 } + ; + abbr: + | ID EQ term { $1, $3 } + ; + absts: + | abst { [$1] } + | abst CM absts { $1 :: $3 } + ; + abbrs: + | abbr { [$1] } + | abbr CM abbrs { $1 :: $3 } + ; + binder: + | absts { T.Abst $1 } + | abbrs { T.Abbr $1 } + | ids { T.Void $1 } + ; + atom: + | STAR IX { T.Sort $2 } + | STAR ID { T.NSrt $2 } + | hash IX { T.LRef ($2, 0) } + | hash IX PLUS IX { T.LRef ($2, $4) } + | hash ID { T.NRef $2 } + ; + term: + | atom { $1 } + | OA term CA fs term { T.Cast ($2, $5) } + | OP terms CP fs term { T.Appl ($2, $5) } + | atom OP terms CP { T.Appl (List.rev $3, $1) } + | OB binder CB fs term { T.Bind ($2, $5) } + ; + terms: + | term { [$1] } + | term CM terms { $1 :: $3 } + ; + + start: OPEN {} | CLOSE {} | GLOBAL {} | EOF {} ; + xentity: + | OPEN ID { Some (T.Section (Some $2)) } + | CLOSE { Some (T.Section None) } + | GLOBAL comment ID CN term { Some (T.Global (false, $3, $2, $5)) } + | GLOBAL comment ID EQ term { Some (T.Global (true, $3, $2, $5)) } + | GLOBAL comment ID EQ term CN term { Some (T.Global (true, $3, $2, T.Cast ($7, $5))) } + | EOF { None } + ; + entry: + | xentity { $1, false } + | xentity start { $1, true } + ; diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 515e6590e..e9ae20eeb 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module F = Filename module P = Printf module U = NUri module C = Cps @@ -21,6 +22,7 @@ module X = Library module AL = AutLexer module AP = AutProcess module AO = AutOutput +module DT = CrgTxt module DA = CrgAut module MA = MetaAut module MO = MetaOutput @@ -40,6 +42,7 @@ type status = { ast : AP.status; dst : DA.status; mst : MA.status; + tst : DT.status; ac : AO.counters; mc : MO.counters; brgc: BrgO.counters; @@ -47,6 +50,14 @@ type status = { kst : Y.status } +let flush_all () = L.flush 0; L.flush_err () + +let bag_error s msg = + L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all () + +let brg_error s msg = + L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () + let initial_status mk_uri cover g expand si = { ac = AO.initial_counters; mc = MO.initial_counters; @@ -54,22 +65,11 @@ let initial_status mk_uri cover g expand si = { bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); dst = DA.initial_status (mk_uri si cover); + tst = DT.initial_status (mk_uri si cover); ast = AP.initial_status; kst = Y.initial_status g expand si } -let flush_all () = L.flush 0; L.flush_err () - -let bag_error s msg = - L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let brg_error s msg = - L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () - -let process_entity f st entity = - let f ast = f {st with ast = ast} in - AP.process_entity f st.ast entity - (* kernel related ***********************************************************) type kernel = Brg | Bag @@ -132,6 +132,65 @@ let type_check st k = | CrgEntity _ | MetaEntity _ -> st +(* extended lexer ***********************************************************) + +type 'token lexer = { + parse : Lexing.lexbuf -> 'token; + mutable tokbuf: 'token option; + mutable unget : bool +} + +let initial_lexer parse = { + parse = parse; tokbuf = None; unget = false +} + +let token xl lexbuf = match xl.tokbuf with + | Some token when xl.unget -> + xl.unget <- false; token + | _ -> + let token = xl.parse lexbuf in + xl.tokbuf <- Some token; token + +(* input related ************************************************************) + +type input = Text | Automath + +type input_entity = TxtEntity of Txt.entity + | AutEntity of Aut.entity + +let type_of_input name = + if F.check_suffix name ".hln" then Text + else if F.check_suffix name ".aut" then Automath + else begin + L.warn (P.sprintf "Unknown file type: %s" name); exit 2 + end + +let txt_xl = initial_lexer TxtLexer.token + +let aut_xl = initial_lexer AutLexer.token + +let entity_of_input lexbuf = function + | Text -> + begin match TxtParser.entry (token txt_xl) lexbuf with + | Some e, unget -> txt_xl.unget <- unget; Some (TxtEntity e) + | None, _ -> None + end + | Automath -> + begin match AutParser.entry (token aut_xl) lexbuf with + | Some e, unget -> aut_xl.unget <- unget; Some (AutEntity e) + | None, _ -> None + end + +let process_input f st = function + | AutEntity e -> + let f ast e = f {st with ast = ast} (AutEntity e) in + AP.process_entity f st.ast e + | xe -> f st xe + +let count_input st = function + | AutEntity e -> {st with ac = AO.count_entity C.start st.ac e} + | xe -> st + (****************************************************************************) let stage = ref 3 @@ -165,24 +224,32 @@ let process_0 st entity = let h mst e = process_1 {st with mst = mst} (MetaEntity e) in let err dst = {st with dst = dst} in let g dst e = process_1 {st with dst = dst} (CrgEntity e) in - if !old then MA.meta_of_aut frr h st.mst entity else - DA.crg_of_aut err g st.dst entity + let crr tst = {st with tst = tst} in + let d tst e = process_1 {st with tst = tst} (CrgEntity e) in + match entity, !old with + | AutEntity e, true -> MA.meta_of_aut frr h st.mst e + | AutEntity e, false -> DA.crg_of_aut err g st.dst e + | TxtEntity e, false -> DT.crg_of_txt crr d st.tst e + | _ -> assert false in - let st = - if !L.level > 2 then {st with ac = AO.count_entity C.start st.ac entity} - else st - in - if !preprocess then process_entity f st entity else f st entity + let st = if !L.level > 2 then count_input st entity else st in + if !preprocess then process_input f st entity else f st entity -let rec process st = function - | [] -> st - | entity :: tl -> process (process_0 st entity) tl +let process st name = + let input = type_of_input name in + let ich = open_in name in + let lexbuf = Lexing.from_channel ich in + let rec aux st = match entity_of_input lexbuf input with + | None -> close_in ich; st, input + | Some e -> aux (process_0 st e) + in + aux st (****************************************************************************) let main = try - let version_string = "Helena 0.8.1 M - January 2010" in + let version_string = "Helena 0.8.1 M - February 2010" in let set_hierarchy s = let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in let f g = graph := g in @@ -207,18 +274,13 @@ try | None -> () | Some och -> ML.close_out C.start och in - let read_file name = + let process_file name = if !L.level > 0 then T.gmtime version_string; if !L.level > 1 then L.warn (P.sprintf "Processing file: %s" name); if !L.level > 0 then T.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in if !meta then set_meta_file base_name; - let ich = open_in name in - let lexbuf = Lexing.from_channel ich in - let book = AutParser.book AutLexer.token lexbuf in - close_in ich; - if !L.level > 0 then T.utime_stamp "parsed"; O.clear_reductions (); let mk_uri = if !stage < 2 then Crg.mk_uri else @@ -228,7 +290,7 @@ try in let cover = if !use_cover then base_name else "" in let st = initial_status mk_uri cover !graph !expand !si in - let st = process st book in + let st, input = process st name in if !L.level > 0 then T.utime_stamp "processed"; if !L.level > 2 then begin AO.print_counters C.start st.ac; @@ -286,5 +348,5 @@ try ("-s", Arg.Int set_stage, help_s); ("-u", Arg.Set si, help_u); ("-x", Arg.Set export, help_x) - ] read_file help; + ] process_file help; with BagT.TypeError msg -> bag_error "Type Error" msg diff --git a/helm/software/lambda-delta/xml/ld-html-root.xsl b/helm/software/lambda-delta/xml/ld-html-root.xsl index 2b8edb470..13668ee51 100644 --- a/helm/software/lambda-delta/xml/ld-html-root.xsl +++ b/helm/software/lambda-delta/xml/ld-html-root.xsl @@ -24,14 +24,14 @@ href="http://helm.cs.unibo.it/lambda-delta/download/crux-16.ico" /> -

+

[lambda-delta home] -

+