From: Ferruccio Guidi Date: Fri, 6 Aug 2010 10:21:49 +0000 (+0000) Subject: txtLexer: bug fix in parsing the string tokens X-Git-Tag: make_still_working~2853 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b1375e4b44e2ef351a6341a5bb0a4823e8daae5;hp=a3b9fc77770f42070632bcb575546678025e09b2;p=helm.git txtLexer: bug fix in parsing the string tokens library: we now export the "meta" attribute crgXml: crg exportation factorized and alpha conversion now works crgBrg: we now mark the abstraction and the reverse translation works ld.dtd: updated to export crg contents --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 4d5194ea4..a89eae37a 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -20,6 +20,11 @@ common/output.cmo: common/options.cmx lib/log.cmi common/output.cmi common/output.cmx: common/options.cmx lib/log.cmx common/output.cmi common/entity.cmo: common/options.cmx lib/nUri.cmi automath/aut.cmx common/entity.cmx: common/options.cmx lib/nUri.cmx automath/aut.cmx +common/marks.cmo: common/entity.cmx +common/marks.cmx: common/entity.cmx +common/alpha.cmi: common/entity.cmx +common/alpha.cmo: common/entity.cmx common/alpha.cmi +common/alpha.cmx: common/entity.cmx common/alpha.cmi common/library.cmi: common/entity.cmx common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \ lib/cps.cmx common/library.cmi @@ -140,13 +145,20 @@ basic_rg/brgUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi complete_rg/crg.cmo: common/entity.cmx complete_rg/crg.cmx: common/entity.cmx -complete_rg/crgOutput.cmi: common/library.cmi complete_rg/crg.cmx -complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \ - common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ +complete_rg/crgOutput.cmi: complete_rg/crg.cmx +complete_rg/crgOutput.cmo: lib/nUri.cmi common/hierarchy.cmi \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ complete_rg/crgOutput.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.cmx: lib/nUri.cmx common/hierarchy.cmx \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ complete_rg/crgOutput.cmi +complete_rg/crgXml.cmi: common/library.cmi complete_rg/crg.cmx +complete_rg/crgXml.cmo: lib/nUri.cmi common/library.cmi common/hierarchy.cmi \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx common/alpha.cmi \ + complete_rg/crgXml.cmi +complete_rg/crgXml.cmx: lib/nUri.cmx common/library.cmx common/hierarchy.cmx \ + common/entity.cmx complete_rg/crg.cmx lib/cps.cmx common/alpha.cmx \ + complete_rg/crgXml.cmi complete_rg/crgTxt.cmi: text/txt.cmx complete_rg/crg.cmx complete_rg/crgTxt.cmo: text/txtTxt.cmi text/txt.cmx common/options.cmx \ lib/nUri.cmi common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx \ @@ -160,10 +172,10 @@ complete_rg/crgAut.cmo: common/options.cmx lib/nUri.cmi common/entity.cmx \ complete_rg/crgAut.cmx: common/options.cmx lib/nUri.cmx common/entity.cmx \ complete_rg/crg.cmx lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi complete_rg/crgBrg.cmi: complete_rg/crg.cmx basic_rg/brg.cmx -complete_rg/crgBrg.cmo: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ - basic_rg/brg.cmx complete_rg/crgBrg.cmi -complete_rg/crgBrg.cmx: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ - basic_rg/brg.cmx complete_rg/crgBrg.cmi +complete_rg/crgBrg.cmo: common/marks.cmx common/entity.cmx \ + complete_rg/crg.cmx lib/cps.cmx basic_rg/brg.cmx complete_rg/crgBrg.cmi +complete_rg/crgBrg.cmx: common/marks.cmx common/entity.cmx \ + complete_rg/crg.cmx lib/cps.cmx basic_rg/brg.cmx complete_rg/crgBrg.cmi toplevel/meta.cmo: common/entity.cmx toplevel/meta.cmx: common/entity.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx @@ -194,7 +206,7 @@ toplevel/top.cmo: text/txtParser.cmi text/txtLexer.cmx text/txt.cmx \ 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/crgXml.cmi complete_rg/crgTxt.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 \ @@ -206,7 +218,7 @@ toplevel/top.cmx: text/txtParser.cmx text/txtLexer.cmx text/txt.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/crgXml.cmx complete_rg/crgTxt.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 \ diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index 1ec685637..de13dd4c9 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -options hierarchy output entity library +options hierarchy output entity marks alpha library diff --git a/helm/software/lambda-delta/common/alpha.ml b/helm/software/lambda-delta/common/alpha.ml new file mode 100644 index 000000000..01c2aafe8 --- /dev/null +++ b/helm/software/lambda-delta/common/alpha.ml @@ -0,0 +1,39 @@ +(* + ||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 Y = Entity + +(* internal functions *******************************************************) + +let rec rename ns n = + let token, mode = n in + let n = token ^ "_", mode in + if List.mem n ns then rename ns n else n + +let alpha_name acc attr = + let ns, a = acc in + match attr with + | Y.Name n -> + if List.mem n ns then + let n = rename ns n in + n :: ns, Y.Name n :: a + else + n :: ns, attr :: a + | _ -> assert false + +(* interface functions ******************************************************) + +let alpha ns a = + let f a names = + let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in + List.rev_append a names + in + Y.get_names f a diff --git a/helm/software/lambda-delta/common/alpha.mli b/helm/software/lambda-delta/common/alpha.mli new file mode 100644 index 000000000..a08e98e59 --- /dev/null +++ b/helm/software/lambda-delta/common/alpha.mli @@ -0,0 +1,12 @@ +(* + ||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_______________________________________________________________ *) + +val alpha: Entity.names -> Entity.attrs -> Entity.attrs diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index de06f2924..e32b347a8 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -13,8 +13,11 @@ module O = Options type uri = NUri.uri type id = Aut.id +type name = id * bool (* token, real? *) -type attr = Name of id * bool (* name, 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 *) @@ -88,6 +91,11 @@ let rec priv err f = function | _ :: tl -> priv err f tl | [] -> err () +let rec meta err f = function + | Meta s :: _ -> f s + | _ :: tl -> meta err f tl + | [] -> err () + let resolve err f name a = let rec aux i = function | Name (n, true) :: _ when n = name -> f i @@ -96,6 +104,11 @@ let resolve err f name a = in aux 0 a +let rec rev_append_names ns = function + | [] -> ns + | Name n :: tl -> rev_append_names (n :: ns) tl + | _ :: tl -> rev_append_names ns tl + let xlate f xlate_term = function | a, uri, Abst t -> let f t = f (a, uri, Abst t) in xlate_term f t @@ -111,3 +124,4 @@ let initial_status () = { let refresh_status st = {st with si = !O.si; expand = !O.expand } + diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 91272c6f8..8a6801159 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -106,6 +106,12 @@ let mark a = let f i = "mark", string_of_int i in Y.mark err f a +(* TODO: the string s must be quoted *) +let meta a = + let err () = "meta", "" in + let f s = "meta", s in + Y.meta err f a + let export_entity pp_term si xdir (a, u, b) = let path = path_of_uri xdir u in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in @@ -113,7 +119,7 @@ let export_entity pp_term si xdir (a, u, b) = let out = output_string och in xml out "1.0" "UTF-8"; doctype out root system; let a = Y.Name (U.name_of_uri u, true) :: a in - let attrs = [uri u; name a; mark a] in + let attrs = [uri u; name a; mark a; meta a] in let contents = match b with | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 74c9fb424..ed3f7bb8f 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -49,3 +49,5 @@ val arity: int -> attr val name: Entity.attrs -> attr val mark: Entity.attrs -> attr + +val meta: Entity.attrs -> attr diff --git a/helm/software/lambda-delta/common/marks.ml b/helm/software/lambda-delta/common/marks.ml new file mode 100644 index 000000000..026414e2a --- /dev/null +++ b/helm/software/lambda-delta/common/marks.ml @@ -0,0 +1,21 @@ +(* + ||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 Y = Entity + +(* interface functions ******************************************************) + +let new_location = + let location = ref 0 in + fun () -> incr location; !location + +let new_mark () = + Y.Mark (new_location ()) diff --git a/helm/software/lambda-delta/complete_rg/Make b/helm/software/lambda-delta/complete_rg/Make index 33e3388fb..d7a45f9d2 100644 --- a/helm/software/lambda-delta/complete_rg/Make +++ b/helm/software/lambda-delta/complete_rg/Make @@ -1 +1 @@ -crg crgOutput crgTxt crgAut crgBrg +crg crgOutput crgXml crgTxt crgAut crgBrg diff --git a/helm/software/lambda-delta/complete_rg/crg.ml b/helm/software/lambda-delta/complete_rg/crg.ml index 0b02f1c48..07a4cb3ee 100644 --- a/helm/software/lambda-delta/complete_rg/crg.ml +++ b/helm/software/lambda-delta/complete_rg/crg.ml @@ -12,9 +12,11 @@ (* kernel version: complete, relative, global *) (* note : fragment of complete lambda-delta serving as abstract layer *) -type uri = Entity.uri -type id = Entity.id -type attrs = Entity.attrs +module Y = Entity + +type uri = Y.uri +type id = Y.id +type attrs = Y.attrs type bind = Abst of term list (* domains *) | Abbr of term list (* bodies *) @@ -32,7 +34,7 @@ and lenv = ESort (* top *) | EProj of lenv * attrs * lenv (* environment, attrs, closure *) | EBind of lenv * attrs * bind (* environment, attrs, binder *) -type entity = term Entity.entity +type entity = term Y.entity (* helpers ******************************************************************) @@ -59,7 +61,7 @@ let resolve_lref err f id lenv = | 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 + Y.resolve err f id a | EProj _ -> assert false (* TODO *) in aux f 0 0 lenv @@ -68,7 +70,7 @@ let rec get_name err f i j = function | ESort -> err i | EBind (_, a, _) when i = 0 -> let err () = err i in - Entity.get_name err f j a + Y.get_name err f j a | EBind (tl, _, _) -> get_name err f (pred i) j tl | EProj (tl, _, e) -> @@ -79,9 +81,14 @@ let get_index err f i j lenv = let rec aux f i k = function | ESort -> err i | EBind (_, a, _) when i = 0 -> - if Entity.count_names a > j then f (k + j) else err i + if Y.count_names a > j then f (k + j) else err i | EBind (tl, a, _) -> - aux f (pred i) (k + Entity.count_names a) tl + aux f (pred i) (k + Y.count_names a) tl | EProj _ -> assert false (* TODO *) in aux f i 0 lenv + +let rec names_of_lenv ns = function + | ESort -> ns + | EBind (tl, a, _) -> names_of_lenv (Y.rev_append_names ns a) tl + | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl diff --git a/helm/software/lambda-delta/complete_rg/crgBrg.ml b/helm/software/lambda-delta/complete_rg/crgBrg.ml index bfed7ad9e..2b3129339 100644 --- a/helm/software/lambda-delta/complete_rg/crgBrg.ml +++ b/helm/software/lambda-delta/complete_rg/crgBrg.ml @@ -11,9 +11,12 @@ module C = Cps module Y = Entity +module M = Marks module D = Crg module B = Brg +(* internal functions: crg to brg term **************************************) + let rec lenv_fold_left map1 map2 x = function | D.ESort -> x | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl @@ -45,12 +48,14 @@ and xlate_bind x a b = match b with | D.Abst ws -> let map x n w = - let f ww = B.Bind (n :: a, B.Abst ww, x) in xlate_term f w + let f ww = B.Bind (n :: M.new_mark () :: a, B.Abst ww, x) in + xlate_term f w in List.fold_left2 map x ns ws | D.Abbr vs -> let map x n v = - let f vv = B.Bind (n :: a, B.Abbr vv, x) in xlate_term f v + let f vv = B.Bind (n :: a, B.Abbr vv, x) in + xlate_term f v in List.fold_left2 map x ns vs | D.Void _ -> @@ -60,5 +65,37 @@ and xlate_bind x a b = and xlate_proj x _ e = lenv_fold_left xlate_bind xlate_proj x e +(* internal functions: brg to crg term **************************************) + +let rec xlate_bk_term f = function + | B.Sort (a, l) -> f (D.TSort (a, l)) + | B.GRef (a, n) -> f (D.TGRef (a, n)) + | B.LRef (a, i) -> f (D.TLRef (a, i, 0)) + | B.Cast (a, u, t) -> + let f uu tt = f (D.TCast (a, uu, tt)) in + let f uu = xlate_bk_term (f uu) t in + xlate_bk_term f u + | B.Appl (a, u, t) -> + let f uu tt = f (D.TAppl (a, [uu], tt)) in + let f uu = xlate_bk_term (f uu) t in + xlate_bk_term f u + | B.Bind (a, b, t) -> + let f bb tt = f (D.TBind (a, bb, tt)) in + let f bb = xlate_bk_term (f bb) t in + xlate_bk_bind f b + +and xlate_bk_bind f = function + | B.Abst t -> + let f tt = f (D.Abst [tt]) in + xlate_bk_term f t + | B.Abbr t -> + let f tt = f (D.Abbr [tt]) in + xlate_bk_term f t + | B.Void -> f (D.Void 1) + +(* interface functions ******************************************************) + let brg_of_crg f t = f (xlate_term C.start t) + +let crg_of_brg = xlate_bk_term diff --git a/helm/software/lambda-delta/complete_rg/crgBrg.mli b/helm/software/lambda-delta/complete_rg/crgBrg.mli index db4e54221..84c7f2368 100644 --- a/helm/software/lambda-delta/complete_rg/crgBrg.mli +++ b/helm/software/lambda-delta/complete_rg/crgBrg.mli @@ -10,3 +10,5 @@ V_______________________________________________________________ *) val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a + +val crg_of_brg: (Crg.term -> 'a) -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml index 3634f9e80..6da54cbc3 100644 --- a/helm/software/lambda-delta/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml @@ -14,7 +14,6 @@ module U = NUri module C = Cps module H = Hierarchy module Y = Entity -module X = Library module D = Crg (****************************************************************************) @@ -58,92 +57,3 @@ let rec pp_lenv out = function | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y (****************************************************************************) - -let rec list_iter map l out tab = match l with - | [] -> () - | hd :: tl -> map hd out tab; list_iter map tl out tab - -let list_rev_iter map e ns l out tab = - let rec aux err f e = function - | [], [] -> f e - | n :: ns, hd :: tl -> - let f e = -(* - 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 ()) - in - aux err f e (ns, tl) - | _ -> err () - in - ignore (aux C.err C.start e (ns, l)) - -let lenv_iter map1 map2 l out tab = - let rec aux f = function - | D.ESort -> f () - | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv - | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv - in - aux C.start l - -let rec exp_term e t out tab = match t with - | D.TSort (a, l) -> - let a = - let err _ = a in - let f s = Y.Name (s, true) :: a in - H.string_of_sort err f l - in - let attrs = [X.position l; X.name a] in - X.tag X.sort attrs out tab - | D.TLRef (a, i, j) -> - let a = - let err _ = a in - let f n r = Y.Name (n, r) :: a in - D.get_name err f i j e - in - let attrs = [X.position i; X.offset j; X.name a] in - X.tag X.lref attrs out tab - | D.TGRef (a, n) -> - let a = Y.Name (U.name_of_uri n, true) :: a in - let attrs = [X.uri n; X.name a] in - X.tag X.gref attrs out tab - | D.TCast (a, u, t) -> - let attrs = [] in - X.tag X.cast attrs ~contents:(exp_term e u) out tab; - exp_term e t out tab - | D.TAppl (a, vs, t) -> - let attrs = [X.arity (List.length vs)] in - X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; - exp_term e t out tab - | D.TProj (a, lenv, t) -> - let attrs = [] in - X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; - exp_term (D.push_proj C.start e a lenv) t out tab - | D.TBind (a, b, t) -> - exp_bind e a b out tab; - exp_term (D.push_bind C.start e a b) t out tab - -and exp_bind e a b out tab = - let f a ns = a, ns in - let a, ns = Y.get_names f a in - match b with - | D.Abst ws -> - let e = D.push_bind C.start e a (D.Abst []) in - let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in - X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab - | D.Abbr vs -> - let e = D.push_bind C.start e a (D.Abbr []) in - let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in - X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab - | D.Void n -> - let attrs = [X.name a; X.mark a; X.arity n] in - X.tag X.void attrs out tab - -and exp_eproj e a lenv out tab = - let attrs = [] in - X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab - -(****************************************************************************) - -let export_term = exp_term D.empty_lenv diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.mli b/helm/software/lambda-delta/complete_rg/crgOutput.mli index 4d3f747fd..d804937f8 100644 --- a/helm/software/lambda-delta/complete_rg/crgOutput.mli +++ b/helm/software/lambda-delta/complete_rg/crgOutput.mli @@ -9,6 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val export_term: Crg.term -> Library.pp - val pp_term: (string -> unit) -> Crg.term -> unit diff --git a/helm/software/lambda-delta/complete_rg/crgXml.ml b/helm/software/lambda-delta/complete_rg/crgXml.ml new file mode 100644 index 000000000..111cfed06 --- /dev/null +++ b/helm/software/lambda-delta/complete_rg/crgXml.ml @@ -0,0 +1,114 @@ +(* + ||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 C = Cps +module H = Hierarchy +module Y = Entity +module A = Alpha +module X = Library +module D = Crg + +(* internal functions *******************************************************) + +let rec list_iter map l out tab = match l with + | [] -> () + | hd :: tl -> map hd out tab; list_iter map tl out tab + +let list_rev_iter map e ns l out tab = + let rec aux err f e = function + | [], [] -> f e + | n :: ns, hd :: tl -> + let f e = +(* + 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 ()) + in + aux err f e (ns, tl) + | _ -> err () + in + ignore (aux C.err C.start e (ns, l)) + +let lenv_iter map1 map2 l out tab = + let rec aux f = function + | D.ESort -> f () + | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv + | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv + in + aux C.start l + +let rec exp_term e t out tab = match t with + | D.TSort (a, l) -> + let a = + let err _ = a in + let f s = Y.Name (s, true) :: a in + H.string_of_sort err f l + in + let attrs = [X.position l; X.name a] in + X.tag X.sort attrs out tab + | D.TLRef (a, i, j) -> + let a = + let err _ = a in + let f n r = Y.Name (n, r) :: a in + D.get_name err f i j e + in + let attrs = [X.position i; X.offset j; X.name a] in + X.tag X.lref attrs out tab + | D.TGRef (a, n) -> + let a = Y.Name (U.name_of_uri n, true) :: a in + let attrs = [X.uri n; X.name a] in + X.tag X.gref attrs out tab + | D.TCast (a, u, t) -> + let attrs = [] in + X.tag X.cast attrs ~contents:(exp_term e u) out tab; + exp_term e t out tab + | D.TAppl (a, vs, t) -> + let attrs = [X.arity (List.length vs)] in + X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; + exp_term e t out tab + | D.TProj (a, lenv, t) -> + let attrs = [] in + X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; + exp_term (D.push_proj C.start e a lenv) t out tab + | D.TBind (a, b, t) -> +(* NOTE: the inner binders are alpha-converted first *) +(* so undesirable renamings might occur *) +(* EX: we rename [x][x]x to [x][x_]x_ *) +(* whereas [x_][x]x would be more desirable *) + let a = A.alpha (D.names_of_lenv [] e) a in + exp_bind e a b out tab; + exp_term (D.push_bind C.start e a b) t out tab + +and exp_bind e a b out tab = + let f a ns = a, ns in + let a, ns = Y.get_names f a in + match b with + | D.Abst ws -> + let e = D.push_bind C.start e a (D.Abst []) in + let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in + X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab + | D.Abbr vs -> + let e = D.push_bind C.start e a (D.Abbr []) in + let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in + X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab + | D.Void n -> + let attrs = [X.name a; X.mark a; X.arity n] in + X.tag X.void attrs out tab + +and exp_eproj e a lenv out tab = + let attrs = [] in + X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab + +(* interface functions ******************************************************) + +let export_term = exp_term D.empty_lenv diff --git a/helm/software/lambda-delta/complete_rg/crgXml.mli b/helm/software/lambda-delta/complete_rg/crgXml.mli new file mode 100644 index 000000000..c326a9822 --- /dev/null +++ b/helm/software/lambda-delta/complete_rg/crgXml.mli @@ -0,0 +1,12 @@ +(* + ||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_______________________________________________________________ *) + +val export_term: Crg.term -> Library.pp diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll index 624454b67..dc293bdcf 100644 --- a/helm/software/lambda-delta/text/txtLexer.mll +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -32,17 +32,17 @@ rule block_comment = parse | 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 } + | QT { "" } + | SPC { " " ^ qstring lexbuf } + | BS BS { "\\" ^ qstring lexbuf } + | BS QT { "\"" ^ qstring lexbuf } + | _ as c { String.make 1 c ^ qstring lexbuf } and token = parse - | SPC { token lexbuf } - | OC { block_comment lexbuf; token lexbuf } - | ID as id { out "ID"; P.ID id } - | IX as ix { out "IX"; P.IX (int_of_string ix) } - | QT { let s = qstring lexbuf in out "STR"; P.STR s } + | SPC { token lexbuf } + | OC { block_comment lexbuf; token lexbuf } + | ID as id { out ("ID " ^ id); P.ID id } + | IX as ix { out ("IX " ^ ix); P.IX (int_of_string ix) } + | QT { let s = qstring lexbuf in out ("STR " ^ s); P.STR s } | "\\graph" { out "GRAPH"; P.GRAPH } | "\\decl" { out "DECL"; P.DECL } | "\\ax" { out "AX"; P.AX } diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 57bdfdae8..40fcda5e1 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -28,7 +28,7 @@ module DA = CrgAut module MA = MetaAut module MO = MetaOutput module ML = MetaLibrary -module DO = CrgOutput +module DX = CrgXml module DBrg = CrgBrg module MBrg = MetaBrg module BrgO = BrgOutput @@ -122,7 +122,7 @@ let count_entity st = function | _ -> st let export_entity si xdir moch = function - | CrgEntity e -> X.export_entity DO.export_term si xdir e + | CrgEntity e -> X.export_entity DX.export_term si xdir e | BrgEntity e -> X.export_entity BrgO.export_term si xdir e | MetaEntity e -> begin match moch with diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index 83cfc0596..c16764021 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -15,6 +15,7 @@ position NMTOKEN #REQUIRED name NMTOKENS #IMPLIED mark NMTOKENS #IMPLIED + meta CDATA #IMPLIED > @@ -22,6 +23,7 @@ position NMTOKEN #REQUIRED name NMTOKENS #IMPLIED mark NMTOKENS #IMPLIED + meta CDATA #IMPLIED > @@ -29,36 +31,47 @@ uri CDATA #REQUIRED name NMTOKENS #IMPLIED mark NMTOKENS #IMPLIED + meta CDATA #IMPLIED > @@ -70,6 +83,7 @@ uri CDATA #REQUIRED name NMTOKENS #IMPLIED mark NMTOKENS #IMPLIED + meta CDATA #IMPLIED > @@ -77,6 +91,7 @@ uri CDATA #REQUIRED name NMTOKENS #IMPLIED mark NMTOKENS #IMPLIED + meta CDATA #IMPLIED >