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
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 \
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
-lib automath common basic_ag basic_rg complete_rg toplevel
+lib text automath common basic_ag basic_rg complete_rg toplevel
%{
module A = Aut
+
+ let debug = false
+
+ let _ = Parsing.set_trace debug
%}
%token <int> NUM
%token <string> 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 <Aut.entity list> book
+ %start entry
+ %type <Aut.entity option * bool> entry
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
| 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 }
+
| 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
| 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
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
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
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 *)
| 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
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)
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
-crg crgOutput crgAut crgBrg
+crg crgOutput crgTxt crgAut crgBrg
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)))
(* 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
| 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
| 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
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 ()
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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+txt txtParser txtLexer
--- /dev/null
+\open pippo
+
+\global a : *Set
+
+\global b : *Prop
+
+\global f = [x:*Set].[y:*Prop].x
+
+\global "commento\"" c = f(a,b) : *Set
+
+\close
--- /dev/null
+(*
+ ||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 *)
--- /dev/null
+(*
+ ||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 }
--- /dev/null
+/* 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 <int> IX
+ %token <string> ID STR
+ %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS
+ %token OPEN CLOSE GLOBAL EOF
+
+ %start entry
+ %type <Txt.entity option * bool> 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 }
+ ;
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module F = Filename
module P = Printf
module U = NUri
module C = Cps
module AL = AutLexer
module AP = AutProcess
module AO = AutOutput
+module DT = CrgTxt
module DA = CrgAut
module MA = MetaAut
module MO = MetaOutput
ast : AP.status;
dst : DA.status;
mst : MA.status;
+ tst : DT.status;
ac : AO.counters;
mc : MO.counters;
brgc: BrgO.counters;
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;
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
| 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
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
| 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
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;
("-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
href="http://helm.cs.unibo.it/lambda-delta/download/crux-16.ico"
/>
</head><body>
- <h1 style="text-align: center;">
+ <div style="text-align: center;"><br>
<a href="http://helm.cs.unibo.it/lambda-delta/">
<img style="border: 0px solid; width: 32px; height: 32px;"
alt="[lambda-delta home]"
title="lambda-delta home"
src="http://helm.cs.unibo.it/lambda-delta/download/crux-32.png"
/></a>
- </h1>
+ </div>
<xsl:apply-templates/><h2/>
<div style="text-align: center;">
<a href="http://validator.w3.org/check?uri=referer">
style="border: 0px solid ; width: 147px; height: 42px;"
/></a>
<img style="width: 88px; height: 31px;"
- alt="[png used here]"
- title="png used here"
+ alt="[PNG used here]"
+ title="PNG used here"
src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"
/>
</div>
projects / helm.git / commitdiff