From 28430d599505ac26b51e4887e5196d9b380c898a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 21 Feb 2010 19:09:07 +0000 Subject: [PATCH] - we added some syntactic sugar in the text parser --- helm/software/lambda-delta/.depend.opt | 13 ++-- .../lambda-delta/complete_rg/crgTxt.ml | 49 +++++++++------ .../lambda-delta/examples/exp_math/L.hln | 32 +++++----- .../lambda-delta/examples/exp_math/Makefile | 4 ++ helm/software/lambda-delta/text/Make | 2 +- helm/software/lambda-delta/text/txt.ml | 22 ++++--- helm/software/lambda-delta/text/txtLexer.mll | 3 + helm/software/lambda-delta/text/txtParser.mly | 25 +++++--- helm/software/lambda-delta/text/txtTxt.ml | 63 +++++++++++++++++++ helm/software/lambda-delta/text/txtTxt.mli | 12 ++++ helm/software/lambda-delta/toplevel/top.ml | 4 +- 11 files changed, 172 insertions(+), 57 deletions(-) create mode 100644 helm/software/lambda-delta/text/txtTxt.ml create mode 100644 helm/software/lambda-delta/text/txtTxt.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index e097ef6c9..c299acf63 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -17,6 +17,9 @@ 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 +text/txtTxt.cmi: text/txt.cmx +text/txtTxt.cmo: text/txt.cmx lib/cps.cmx text/txtTxt.cmi +text/txtTxt.cmx: text/txt.cmx lib/cps.cmx text/txtTxt.cmi automath/aut.cmo: automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx @@ -141,10 +144,12 @@ 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/crgTxt.cmo: text/txtTxt.cmi 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/txtTxt.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 \ diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml index 1cb2b3ee9..267ef384f 100644 --- a/helm/software/lambda-delta/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml @@ -9,12 +9,13 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module H = Hierarchy -module C = Cps -module Y = Entity -module T = Txt -module D = Crg +module U = NUri +module H = Hierarchy +module C = Cps +module Y = Entity +module T = Txt +module TT = TxtTxt +module D = Crg type status = { path: T.id list; (* current section path *) @@ -33,7 +34,7 @@ let initial_status mk_uri = { path = []; line = 1; sort = 0; mk_uri = mk_uri } -let name_of_id id = Y.Name (id, true) +let name_of_id ?(r=true) id = Y.Name (id, r) let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) @@ -50,52 +51,62 @@ let resolve_gref err f st id = with Not_found -> err () let rec xlate_term f st lenv = function - | T.Sort h -> + | T.Inst _ + | T.Impl _ -> assert false + | T.Sort h -> f (D.TSort ([], h)) - | T.NSrt id -> + | T.NSrt id -> let f h = f (D.TSort ([], h)) in H.sort_of_string C.err f id - | T.LRef (i, j) -> + | T.LRef (i, j) -> D.get_index C.err (mk_lref f i j) i j lenv - | T.NRef id -> + | T.NRef id -> let err () = resolve_gref C.err (mk_gref f) st id in D.resolve_lref err (mk_lref f) id lenv - | T.Cast (u, t) -> + | 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) -> + | 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 map1 (lenv, a, wws) (id, w) = + | T.Bind (b, t) -> + let abst_map (lenv, a, wws) (id, r, w) = + let attr = name_of_id ~r 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 abbr_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 map2 (lenv, a, n) id = + let void_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, aa, bb = match b with | T.Abst xws -> let lenv = D.push_bind C.start lenv [] (D.Abst []) in - let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in + let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in lenv, aa, D.Abst wws | T.Abbr xvs -> let lenv = D.push_bind C.start lenv [] (D.Abbr []) in - let lenv, aa, vvs = List.fold_left map1 (lenv, [], []) xvs in + let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in lenv, aa, D.Abbr vvs | T.Void ids -> let lenv = D.push_bind C.start lenv [] (D.Void 0) in - let lenv, aa, n = List.fold_left map2 (lenv, [], 0) ids in + let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in lenv, aa, D.Void n in let f tt = f (D.TBind (aa, bb, tt)) in xlate_term f st lenv t +let xlate_term f st lenv t = + TT.contract (xlate_term f st lenv) t + let mk_contents tt = function | T.Decl -> [], Y.Abst tt | T.Ax -> [], Y.Abst tt diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln index cb91d6784..fbcf44adf 100644 --- a/helm/software/lambda-delta/examples/exp_math/L.hln +++ b/helm/software/lambda-delta/examples/exp_math/L.hln @@ -4,36 +4,40 @@ \open syntax \* [1] 2.1. *\ - \decl "logical false" False : *Prop + \decl "logical false" False: *Prop - \decl "logical conjunction" And : [p:*Prop, q:*Prop] *Prop + \decl "logical conjunction" And: *Prop => *Prop -> *Prop - \decl "logical disjunction" Or : [p:*Prop, q:*Prop] *Prop + \decl "logical disjunction" Or: *Prop => *Prop -> *Prop - \decl "logical implication" Imp : [p:*Prop, q:*Prop] *Prop + \decl "logical implication" Imp: *Prop => *Prop -> *Prop - \decl "logical comprehension" All : [p:[x:*Set]*Prop] *Prop + \decl "logical comprehension" All: [~:*Set->*Prop] *Prop - \decl "logical existence" Ex : [p:[x:*Set]*Prop] *Prop + \decl "logical existence" Ex: [~:*Set->*Prop] *Prop - \decl "syntactical identity" Id : [x:*Set, y:*Set] *Prop + \decl "syntactical identity" Id: *Set => *Set -> *Prop - \decl "rule application" App : [f:*Set, x:*Set, y:*Set] *Prop + \decl "rule application" App: *Set => *Set => *Set -> *Prop - \decl "classification predicate" Cl : [a:*Set] *Prop + \decl "classification predicate" Cl: *Set -> *Prop - \decl "classification membership" Eta : [x:*Set, a:*Set] *Prop + \decl "classification membership" Eta: *Set => *Set -> *Prop - \decl "object-to-term-coercion" T : [x:*Set] *Term + \decl "object-to-term-coercion" T: *Set -> *Term - \decl "term application" At : [t:*Term, u:*Term] *Term + \decl "term application" At: *Term => *Term -> *Term - \decl "term-object equivalence" E : [t:*Term, x:*Set] *Prop + \decl "term-object equivalence" E: *Term => *Set -> *Prop \close \open non_logical_axioms - \decl "E: reflexivity" e_refl : [x:*Set] E(T(x), x) + \ax e_refl: [x:*Set] E(T(x), x) + + \ax e_at_in: [f:*Set][x:*Set][y:*Set] App(f,x,y) -> E(At(T(f), T(x)), y) + + \ax e_at_out: [f:*Set][x:*Set][y:*Set] E(At(T(f), T(x)), y) -> App(f,x,y) \close diff --git a/helm/software/lambda-delta/examples/exp_math/Makefile b/helm/software/lambda-delta/examples/exp_math/Makefile index 326001f32..ffc3343a0 100644 --- a/helm/software/lambda-delta/examples/exp_math/Makefile +++ b/helm/software/lambda-delta/examples/exp_math/Makefile @@ -10,6 +10,10 @@ all: $(HLNS) @echo " HELENA -r $(ROOT)" $(H)$(HELENA) -r $(ROOT) $^ +progress: $(HLNS) + @echo " HELENA -r $(ROOT) -j" + $(H)$(HELENA) -r $(ROOT) -j $^ + xml: $(HLNS) @echo " HELENA -r $(ROOT) -x" $(H)$(HELENA) -r $(ROOT) -x -s 2 $^ diff --git a/helm/software/lambda-delta/text/Make b/helm/software/lambda-delta/text/Make index bb0980c0f..f1c0ffe26 100644 --- a/helm/software/lambda-delta/text/Make +++ b/helm/software/lambda-delta/text/Make @@ -1 +1 @@ -txt txtParser txtLexer +txt txtParser txtLexer txtTxt diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml index 264b76873..81c210852 100644 --- a/helm/software/lambda-delta/text/txt.ml +++ b/helm/software/lambda-delta/text/txt.ml @@ -20,17 +20,19 @@ type kind = Decl (* generic declaration *) | Def (* generic definition *) | Th (* theorem *) -type bind = Abst of (id * term) list (* name, domain *) - | Abbr of (id * term) list (* name, bodies *) - | Void of id list (* names *) +type bind = Abst of (id * bool * term) list (* name, real?, 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 *) +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 *) + | Inst of term * term list (* function, arguments *) + | Impl of bool * id * term * term (* strong?, label, source, target *) type command = Graph of id (* hierarchy graph: name *) | Sorts of (int option * id) list (* sorts: index, name *) diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll index 05637286e..fc00064e5 100644 --- a/helm/software/lambda-delta/text/txtLexer.mll +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -64,4 +64,7 @@ and token = parse | "*" { out "STAR"; P.STAR } | "#" { out "HASH"; P.HASH } | "+" { out "PLUS"; P.PLUS } + | "~" { out "TE"; P.TE } + | "->" { out "WTO"; P.WTO } + | "=>" { out "STO"; P.STO } | eof { out "EOF"; P.EOF } diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly index 981225381..ee995aa2d 100644 --- a/helm/software/lambda-delta/text/txtParser.mly +++ b/helm/software/lambda-delta/text/txtParser.mly @@ -32,11 +32,14 @@ %} %token IX %token ID STR - %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS + %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO %token GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF %start entry %type entry + + %nonassoc CP CB CA + %right WTO STO %% hash: | {} @@ -64,7 +67,9 @@ ; abst: - | ID CN term { $1, $3 } + | ID CN term { $1, true, $3 } + | TE CN term { "", false, $3 } + | TE ID CN term { $2, false, $4 } ; abbr: | ID EQ term { $1, $3 } @@ -90,11 +95,17 @@ | 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) } + | 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.Inst ($1, $3) } + | OB binder CB fs term { T.Bind ($2, $5) } + | term WTO term { T.Impl (false, "", $1, $3) } + | TE CN term WTO term { T.Impl (false, "", $3, $5) } + | TE ID CN term WTO term { T.Impl (false, $2, $4, $6) } + | term STO term { T.Impl (true, "", $1, $3) } + | TE CN term STO term { T.Impl (true, "", $3, $5) } + | TE ID CN term STO term { T.Impl (true, $2, $4, $6) } ; terms: | term { [$1] } diff --git a/helm/software/lambda-delta/text/txtTxt.ml b/helm/software/lambda-delta/text/txtTxt.ml new file mode 100644 index 000000000..4564adca4 --- /dev/null +++ b/helm/software/lambda-delta/text/txtTxt.ml @@ -0,0 +1,63 @@ +(* + ||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 C = Cps +module T = Txt + +(* Interface functions ******************************************************) + +let rec contract f = function + | T.Inst (t, vs) -> + let tt = T.Appl (List.rev vs, t) in + contract f tt + | T.Impl (false, id, w, t) -> + let tt = T.Bind (T.Abst [id, false, w], t) in + contract f tt + | T.Impl (true, id, w, t) -> + let f = function + | T.Bind (T.Abst [xw], T.Bind (T.Abst xws, tt)) -> + f (T.Bind (T.Abst (xw :: xws), tt)) + | tt -> f tt + in + let tt = T.Impl (false, id, w, t) in + contract f tt + | T.Sort _ + | T.NSrt _ + | T.LRef _ + | T.NRef _ as t -> f t + | T.Cast (u, t) -> + let f tt uu = f (T.Cast (uu, tt)) in + let f tt = contract (f tt) u in + contract f t + | T.Appl (vs, t) -> + let f tt vvs = f (T.Appl (vvs, tt)) in + let f tt = C.list_map (f tt) contract vs in + contract f t + | T.Bind (b, t) -> + let f tt bb = f (T.Bind (bb, tt)) in + let f tt = contract_binder (f tt) b in + contract f t + +and contract_binder f = function + | T.Void n as b -> f b + | T.Abbr xvs -> + let map f (id, v) = + let f vv = f (id, vv) in contract f v + in + let f xvvs = f (T.Abbr xvvs) in + C.list_map f map xvs + | T.Abst xws -> + let map f (id, real, w) = + let f ww = f (id, real, ww) in contract f w + in + let f xwws = f (T.Abst xwws) in + C.list_map f map xws + diff --git a/helm/software/lambda-delta/text/txtTxt.mli b/helm/software/lambda-delta/text/txtTxt.mli new file mode 100644 index 000000000..357487625 --- /dev/null +++ b/helm/software/lambda-delta/text/txtTxt.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 contract: (Txt.term -> 'a) -> Txt.term -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 66fbed460..6c6691354 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -305,7 +305,7 @@ try flush_all () in let help = - "Usage: helena [ -Vcgijmopqrux | -Ss | -hk ] ...\n\n" ^ + "Usage: helena [ -Vcgijmopqux | -Ss | -hkr ] ...\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -315,7 +315,7 @@ try let help_c = " output conversion constraints" in let help_g = " always expand global definitions" in - let help_h = " set type hierarchy (default: Z2)" in + let help_h = " set type hierarchy (default: Z1)" in let help_i = " show local references by index" in let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: brg)" in -- 2.39.2