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
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 \
\ / 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 *)
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))
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
\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
@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 $^
-txt txtParser txtLexer
+txt txtParser txtLexer txtTxt
| 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 *)
| "*" { 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 }
%}
%token <int> IX
%token <string> 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 <Txt.command option * bool> entry
+
+ %nonassoc CP CB CA
+ %right WTO STO
%%
hash:
| {}
;
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 }
| 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] }
--- /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 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
+
--- /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_______________________________________________________________ *)
+
+val contract: (Txt.term -> 'a) -> Txt.term -> 'a
flush_all ()
in
let help =
- "Usage: helena [ -Vcgijmopqrux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\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"
let help_c = " output conversion constraints" in
let help_g = " always expand global definitions" in
- let help_h = "<string> set type hierarchy (default: Z2)" in
+ let help_h = "<string> 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 = "<string> set kernel version (default: brg)" in
projects / helm.git / commitdiff