src/lib/log.cmi
src/text/txtLexer.cmx : src/text/txtParser.cmx src/common/options.cmx \
src/lib/log.cmx
-src/text/txtTxt.cmi : src/text/txt.cmx
-src/text/txtTxt.cmo : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
-src/text/txtTxt.cmx : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
src/text/txtCrg.cmi : src/text/txt.cmx src/complete_rg/crg.cmx
-src/text/txtCrg.cmo : src/text/txtTxt.cmi src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
-src/text/txtCrg.cmx : src/text/txtTxt.cmx src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
+src/text/txtCrg.cmo : src/text/txt.cmx src/common/options.cmx \
+ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/text/txtCrg.cmi
+src/text/txtCrg.cmx : src/text/txt.cmx src/common/options.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/text/txtCrg.cmi
src/automath/aut.cmo : src/common/entity.cmx
src/automath/aut.cmx : src/common/entity.cmx
src/automath/autProcess.cmi : src/automath/aut.cmx
src/basic_rg/brgOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \
src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \
src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmi \
- src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
+ src/basic_rg/brg.cmx src/common/alpha.cmi src/basic_rg/brgOutput.cmi
src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \
src/lib/log.cmx src/common/layer.cmx src/common/hierarchy.cmx \
src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \
- src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
+ src/basic_rg/brg.cmx src/common/alpha.cmx src/basic_rg/brgOutput.cmi
src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx
src/basic_rg/brgEnvironment.cmo : src/common/entity.cmx \
src/basic_rg/brgEnvironment.cmi
RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
-DOWNDIR = $(HOME)/svn/helm_stable/www/lambdadelta/download
+DOWNDIR = ../../www/lambdadelta/download
DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make))
-Helena 0.8.1 M
+Helena 0.8.2 M
* type "make" or "make opt" to compile the native executable
-* type "make test-si" to parse the grundlagen
- it generates a log.txt with the grundlagen contents statistics
+* type "make test" to validate the "grundlagen" in \lambda\delta "Version 3"
+ it generates log.txt with the grundlagen contents statistics
-* type "make test-si-fast" to parse the grundlagen with minimum logging
+* type "make test-si-fast" to validate the grundlagen with minimum logging
* type "make clean" to remove the products of compilation
--- /dev/null
+# The term \Omega
+# This book is not valid in AUT-QE because [y:'type'] is not allowed
+# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
+# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
+
++l
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+ Omega := <Delta>Delta : 'type'
+-l
grundlagen_0.aut: original specification valid in AutQE with η-reduction enabled
grundlagen_1.aut: "η-equivalent" specification valid also in λδ version 3
grundlagen_2.aut: "η-equivalent" specification valid also in a Pure Type System
+
+Omega.aut : the invalid term \Omega
+++ /dev/null
-# This book is not valid in AUT-QE because [y:'type'] is not allowed
-# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
-# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
-
-+l
-@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
-@ Omega := <Delta>Delta : 'type'
--l
\decl "logical false" False: *Prop
- \decl "logical conjunction" And: *Prop => *Prop -> *Prop
+ \decl "logical conjunction" And: { [*Prop] [*Prop] } *Prop
- \decl "logical disjunction" Or: *Prop => *Prop -> *Prop
+ \decl "logical disjunction" Or: { [*Prop] [*Prop] } *Prop
\* implication and non-dependent abstraction are isomorphic *\
\def "logical implication"
- Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
+ Imp = { [p:*Prop] [q:*Prop] } [p]^1 q : { [*Prop] [*Prop] } *Prop
\* comprehension and dependent abstraction are isomorphic *\
\def "unrestricted logical comprehension"
- All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
+ All = [q:[*Obj]^1 *Prop] [x:*Obj]^1 q(x) : [[*Obj]^1 *Prop] *Prop
- \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
+ \decl "unrestricted logical existence" Ex: [[*Obj]^1 *Prop] *Prop
- \decl "syntactical identity" Id: *Obj => *Obj -> *Prop
+ \decl "syntactical identity" Id: { [*Obj] [*Obj] } *Prop
\close
\open abbreviations \* [1] 2.3. *\
\def "logical negation"
- Not = [p:*Prop] p -> False : *Prop -> *Prop
+ Not = [p:*Prop] Imp(p, False) : [*Prop] *Prop
\def "logical equivalence"
- Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
+ Iff = { [p:*Prop] [q:*Prop] } And(Imp(p, q), Imp(q, p)) : { [*Prop] [*Prop] } *Prop
\def "unrestricted strict logical existence"
- EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
- : (*Obj -> *Prop) -> *Prop
+ EX = [p:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(p(x), All([y:*Obj]^2 Imp(p(y), Id(x, y)))))
+ : [[*Obj]^1 *Prop] *Prop
\def "negated syntactical identity"
- NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop
+ NId = { [x:*Obj] [y:*Obj] } Not(Id(x, y)) : { [*Obj] [*Obj] } *Prop
\close
HOME = ../..
ROOT = exp_math
-HELENAOPTS = -r $(ROOT) -u
+HELENAOPTS = -r $(ROOT)
H = @
HLNS = $(shell cat Make)
all: $(HLNS)
- @echo " HELENA -u"
- $(H)$(HELENA) $(HELENAOPTS) $^
-
-progress: $(HLNS)
- @echo " HELENA -u -j"
- $(H)$(HELENA) $(HELENAOPTS) -j $^
+ @echo " HELENA"
+ $(H)$(HELENA) $(HELENAOPTS) $(O) $^
xml: $(HLNS)
- @echo " HELENA -u -x"
- $(H)$(HELENA) $(HELENAOPTS) -x $(HOME) -s 2 $^
-
-xml-crg: $(HLNS)
- @echo " HELENA -u -x"
- $(H)$(HELENA) $(HELENAOPTS) -x $(HOME) -s 1 $^
+ @echo " HELENA -s 1 -x"
+ $(H)$(HELENA) -O $(HOME) $(HELENAOPTS) -s 1 -x $(O) $^
\open elements \* [1] 2.1. 2.2. 2.4. *\
- \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
+ \decl "rule application" App: { [*Obj] [*Obj] [*Obj] } *Prop
- \decl "classification predicate" Cl: *Obj -> *Prop
+ \decl "classification predicate" Cl: [*Obj] *Prop
- \decl "classification membership" Eta: *Obj => *Obj -> *Prop
+ \decl "classification membership" Eta: { [*Obj] [*Obj] } *Prop
\* we must make an explicit coercion from *Obj to *Term *\
- \decl "object-to-term-coercion" T: *Obj -> *Term
+ \decl "object-to-term-coercion" T: [*Obj] *Term
- \decl "term application" At: *Term => *Term -> *Term
+ \decl "term application" At: { [*Term] [*Term] } *Term
- \decl "term-object equivalence" E: *Term => *Obj -> *Prop
+ \decl "term-object equivalence" E: { [*Term] [*Obj] } *Prop
\close
\open logical_abbreviations \* [1] 2.3. 2.5. *\
\def "logical comprehension restricted to classifications"
- CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)
- : (*Obj -> *Prop) -> *Prop
+ CAll = [q:[*Obj]^1 *Prop] All([x:*Obj]^2 Imp(Cl(x), q(x)))
+ : [[*Obj]^1 *Prop] *Prop
\def "logical existence restricted to classifications"
- CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))
- : (*Obj -> *Prop) -> *Prop
+ CEx = [q:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(Cl(x), q(x)))
+ : [[*Obj]^1 *Prop] *Prop
\def "logical comprehension restricted to a classification"
- EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)
- : *Obj => (*Obj -> *Prop) -> *Prop
+ EAll = { [a:*Obj] [q:[*Obj]^1 *Prop] } All([x:*Obj]^2 Imp(Eta(x, a), q(x)))
+ : { [*Obj] [[*Obj]^1 *Prop] } *Prop
\def "logical existence restricted to a classification"
- EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))
- : *Obj => (*Obj -> *Prop) -> *Prop
+ EEx = { [a:*Obj] [q:[*Obj]^1 *Prop] } Ex([x:*Obj]^2 And(Eta(x, a), q(x)))
+ : { [*Obj] [[*Obj]^1 *Prop] } *Prop
\close
\open non_logical_abbreviations \* [1] 2.4. 2.7 *\
\def "object application"
- OAt = [f:*Obj, x:*Obj] At(T(f), T(x)) : *Obj => *Obj -> *Term
+ OAt = { [f:*Obj] [x:*Obj] } At(T(f), T(x)) : { [*Obj] [*Obj] } *Term
\def "convergence of a term to an object"
- Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
+ Conv = [t:*Term] EX([y:*Obj]^2 E(t, y)) : [*Term] *Prop
\def "term-term equivalence"
- Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
- : *Term => *Term -> *Prop
+ Eq = { [t1:*Term] [t2:*Term] } All([y:*Obj]^2 Iff(E(t1, y), E(t2, y)))
+ : { [*Term] [*Term] } *Prop
\def "classification membership of a term"
- TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
- : *Term => *Obj -> *Prop
+ TEta = { [t:*Term] [a:*Obj] } EEx(a, [y:*Obj]^2 E(t, y))
+ : { [*Term] [*Obj] } *Prop
\def "operation (rule with inhabited domain)"
- Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
+ Op = [f:*Obj] Ex([x:*Obj]^2 Conv(OAt(f, x))) : [*Obj] *Prop
\def "classification inclusion"
- ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
- : *Obj => *Obj -> *Prop
+ ESub = { [a1:*Obj] [a2:*Obj] } EAll(a1, [x:*Obj]^2 Eta(x, a2))
+ : { [*Obj] [*Obj] } *Prop
\def "classification morphism"
- ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
- : *Obj => *Obj => *Obj -> *Prop
+ ETo = { [f:*Obj] [a:*Obj] [ b:*Obj] } EAll(a, [x:*Obj]^2 TEta(OAt(f, x), b))
+ : { [*Obj] [*Obj] [*Obj] } *Prop
\close
\ax e_refl: [y:*Obj] E(T(y), y)
\ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj]
- E(t1, f) -> E(t2, x) -> App(f, x, y) -> E(At(t1, t2), y)
+ [E(t1, f)] [E(t2, x)] [App(f, x, y)] E(At(t1, t2), y)
\*
- \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y)
+ \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] [E(At(T(f), T(x)), y)] App(f, x, y)
*\
\ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
\ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
- E(OAt(f, x), y1) -> E(OAt(f, x), y2) -> Id(y1, y2)
+ [E(OAt(f, x), y1)] [E(OAt(f, x), y2)] Id(y1, y2)
- \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] Eta(x, a) -> Cl(a)
+ \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] [Eta(x, a)] Cl(a)
\close
+++ /dev/null
-# The term \Omega
-# This book is not accepted in AUT-QE because [y:'type'] is not allowed
-# This book is accepted in \lambda\delta with sort inclusion but Omega is not
-# valid if sort inclusion is allowed on the term backbone only
-# This book is valid in \lambda\delta with unrestricted sort inclusion
-
-+l
-@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
- Omega := <Delta>Delta : 'type'
--l
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
module C = Cps
module L = Log
let print_counters f c =
let terms = c.sorts + c.grefs + c.appls + c.absts in
let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in
- L.warn level (P.sprintf "Automath representation summary");
- L.warn level (P.sprintf " Total book entities: %7u" entities);
- L.warn level (P.sprintf " Section entities: %7u" c.sections);
- L.warn level (P.sprintf " Context entities: %7u" c.contexts);
- L.warn level (P.sprintf " Block entities: %7u" c.blocks);
- L.warn level (P.sprintf " Declaration entities: %7u" c.decls);
- L.warn level (P.sprintf " Definition entities: %7u" c.defs);
- L.warn level (P.sprintf " Total Parameter items: %7u" c.pars);
- L.warn level (P.sprintf " Application items: %7u" c.pars);
- L.warn level (P.sprintf " Total term items: %7u" terms);
- L.warn level (P.sprintf " Sort items: %7u" c.sorts);
- L.warn level (P.sprintf " Reference items: %7u" c.grefs);
- L.warn level (P.sprintf " Application items: %7u" c.appls);
- L.warn level (P.sprintf " Abstraction items: %7u" c.absts);
- L.warn level (P.sprintf " Global Int. Complexity: unknown");
- L.warn level (P.sprintf " + Abbreviation nodes: %7u" c.xnodes);
+ L.warn level (KP.sprintf "Automath representation summary");
+ L.warn level (KP.sprintf " Total book entities: %7u" entities);
+ L.warn level (KP.sprintf " Section entities: %7u" c.sections);
+ L.warn level (KP.sprintf " Context entities: %7u" c.contexts);
+ L.warn level (KP.sprintf " Block entities: %7u" c.blocks);
+ L.warn level (KP.sprintf " Declaration entities: %7u" c.decls);
+ L.warn level (KP.sprintf " Definition entities: %7u" c.defs);
+ L.warn level (KP.sprintf " Total Parameter items: %7u" c.pars);
+ L.warn level (KP.sprintf " Application items: %7u" c.pars);
+ L.warn level (KP.sprintf " Total term items: %7u" terms);
+ L.warn level (KP.sprintf " Sort items: %7u" c.sorts);
+ L.warn level (KP.sprintf " Reference items: %7u" c.grefs);
+ L.warn level (KP.sprintf " Application items: %7u" c.appls);
+ L.warn level (KP.sprintf " Abstraction items: %7u" c.absts);
+ L.warn level (KP.sprintf " Global Int. Complexity: unknown");
+ L.warn level (KP.sprintf " + Abbreviation nodes: %7u" c.xnodes);
f ()
let print_process_counters f c =
let f iao iar iac iag =
- L.warn level (P.sprintf "Automath process summary");
- L.warn level (P.sprintf " Implicit after opening: %7u" iao);
- L.warn level (P.sprintf " Implicit after reopening: %7u" iar);
- L.warn level (P.sprintf " Implicit after closing: %7u" iac);
- L.warn level (P.sprintf " Implicit after global: %7u" iag);
+ L.warn level (KP.sprintf "Automath process summary");
+ L.warn level (KP.sprintf " Implicit after opening: %7u" iao);
+ L.warn level (KP.sprintf " Implicit after reopening: %7u" iar);
+ L.warn level (KP.sprintf " Implicit after closing: %7u" iac);
+ L.warn level (KP.sprintf " Implicit after global: %7u" iag);
f ()
in
AA.get_counters f c
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
-module P = Printf
+module KF = Filename
+module KP = Printf
-module U = NUri
-module C = Cps
-module G = Options
-module N = Layer
-module E = Entity
-module R = Alpha
-module B = Brg
+module U = NUri
+module C = Cps
+module G = Options
+module N = Layer
+module E = Entity
+module R = Alpha
+module B = Brg
(* Internal functions *******************************************************)
let out_preamble och =
let ich = open_in !G.ma_preamble in
- let rec aux () = P.fprintf och "%s\n" (input_line ich); aux () in
+ let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in
try aux () with End_of_file -> close_in ich
let out_top_comment och msg =
let padding = width - String.length msg in
let padding = if padding >= 0 then padding else 0 in
- P.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*')
+ KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*')
let out_comment och msg =
- P.fprintf och "(* %s *)\n" msg
+ KP.fprintf och "(* %s *)\n" msg
let out_include och src =
- P.fprintf och "include \"%s.ma\".\n\n" src
+ KP.fprintf och "include \"%s.ma\".\n\n" src
let out_uri och u =
let str = U.string_of_uri u in
let out_name och a =
let f n = function
- | true -> P.fprintf och "%s" n
- | false -> C.err ()
+ | true -> KP.fprintf och "%s" n
+ | false -> KP.fprintf och "_"
in
- E.name C.err f a
+ let err () = f "" false in
+ E.name err f a
let rec out_term st p e och = function
| B.Sort (_, h) ->
let sort = if h = 0 then "Type[0]" else if h = 1 then "Prop" else assert false in
- P.fprintf och "%s" sort
+ KP.fprintf och "%s" sort
| B.LRef (_, i) ->
let _, _, a, b = B.get e i in
- P.fprintf och "%a" out_name a
+ KP.fprintf och "%a" out_name a
| B.GRef (_, s) ->
- P.fprintf och "%a" out_uri s
+ KP.fprintf och "%a" out_uri s
| B.Cast (_, u, t) ->
- P.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
+ KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
| B.Appl (_, v, t) ->
let pt = match t with B.Appl _ -> false | _ -> true in
let op, cp = if p then "(", ")" else "", "" in
- P.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
+ KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
| B.Bind (a, B.Abst (n, w), t) ->
let op, cp = if p then "(", ")" else "", "" in
let a = R.alpha B.mem e a in
| "2", _ -> "λ"
| _ -> ok := false; "?"
in
- P.fprintf och "%s%s%a:%a.%a%s"
+ KP.fprintf och "%s%s%a:%a.%a%s"
op binder out_name a (out_term st false e) w (out_term st false ee) t cp
| B.Bind (a, B.Abbr v, t) ->
let op, cp = if p then "(", ")" else "", "" in
let a = R.alpha B.mem e a in
let ee = B.push e B.empty a (B.abbr v) in
- P.fprintf och "%slet %a ≝ %a in %a%s"
+ KP.fprintf och "%slet %a ≝ %a in %a%s"
op out_name a (out_term st false e) v (out_term st false ee) t cp
| B.Bind (a, B.Void, t) -> C.err ()
(* Interface functions ******************************************************)
let open_out fname =
- let dir = F.concat !G.ma_dir base in
- let path = F.concat dir fname in
+ let dir = KF.concat !G.ma_dir base in
+ let path = KF.concat dir fname in
let och = open_out (path ^ ext) in
out_preamble och;
- out_top_comment och (P.sprintf "This file was generated by %s: do not edit" G.version_string);
+ out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
out_include och "basics/pts";
och
let output_entity st och (_, na, s, b) =
- out_comment och (P.sprintf "constant %u" na.E.n_apix);
+ out_comment och (KP.sprintf "constant %u" na.E.n_apix);
match b with
| E.Abbr t ->
- P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+ KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
| E.Abst t ->
- P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+ KP.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
| E.Void -> C.err ()
let close_out och = close_out och
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
module U = NUri
module C = Cps
module H = Hierarchy
module N = Layer
module E = Entity
+module R = Alpha
module XD = XmlCrg
module B = Brg
module BD = BrgCrg
in
let items = c.eabsts + c.eabbrs in
let nodes = c.nodes + c.xnodes in
- L.warn level (P.sprintf "Kernel representation summary (basic_rg)");
- L.warn level (P.sprintf " Total entry items: %7u" items);
- L.warn level (P.sprintf " Declaration items: %7u" c.eabsts);
- L.warn level (P.sprintf " Definition items: %7u" c.eabbrs);
- L.warn level (P.sprintf " Total term items: %7u" terms);
- L.warn level (P.sprintf " Sort items: %7u" c.tsorts);
- L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs);
- L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs);
- L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts);
- L.warn level (P.sprintf " Application items: %7u" c.tappls);
- L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts);
- L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs);
- L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes);
- L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes);
+ L.warn level (KP.sprintf "Kernel representation summary (basic_rg)");
+ L.warn level (KP.sprintf " Total entry items: %7u" items);
+ L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts);
+ L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs);
+ L.warn level (KP.sprintf " Total term items: %7u" terms);
+ L.warn level (KP.sprintf " Sort items: %7u" c.tsorts);
+ L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs);
+ L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs);
+ L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts);
+ L.warn level (KP.sprintf " Application items: %7u" c.tappls);
+ L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts);
+ L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs);
+ L.warn level (KP.sprintf " Global Int. Complexity: %7u" c.nodes);
+ L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes);
f ()
-(* supplementary annotation *************************************************)
-
-let rec does_not_occur f n r = function
- | B.Null -> f true
- | B.Cons (e, _, a, _) ->
- let f n1 r1 =
- if n1 = n && r1 = r then f false else does_not_occur f n r e
- in
- E.name C.err f a
-
-let rename f e a =
- let rec aux f e n r =
- let f = function
- | true -> f n r
- | false -> aux f e (n ^ "_") r
- in
- does_not_occur f n r e
- in
- let f n0 r0 =
- let f n r = if n = n0 && r = r0 then f a else f {a with E.n_name = Some (n, r)} in
- aux f e n0 r0
- in
- E.name C.err f a
-
(* lenv/term pretty printing ************************************************)
let name err och a =
let f n = function
- | true -> P.fprintf och "%s" n
- | false -> P.fprintf och "-%s" n
- in
+ | true -> KP.fprintf och "%s" n
+ | false -> KP.fprintf och "-%s" n
+ in
E.name err f a
let pp_level st och n =
- P.fprintf och "%s" (N.to_string st n)
+ KP.fprintf och "%s" (N.to_string st n)
let rec pp_term st e och = function
| B.Sort (_, h) ->
- let err _ = P.fprintf och "*%u" h in
- let f s = P.fprintf och "%s" s in
+ let err _ = KP.fprintf och "*%u" h in
+ let f s = KP.fprintf och "%s" s in
H.string_of_sort err f h
| B.LRef (_, i) ->
- let err _ = P.fprintf och "#%u" i in
+ let err _ = KP.fprintf och "#%u" i in
if !G.indexes then err () else
let _, _, a, b = B.get e i in
- P.fprintf och "%a" (name err) a
+ KP.fprintf och "%a" (name err) a
| B.GRef (_, s) ->
- P.fprintf och "$%s" (U.string_of_uri s)
+ KP.fprintf och "$%s" (U.string_of_uri s)
| B.Cast (_, u, t) ->
- P.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
+ KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
| B.Appl (_, v, t) ->
- P.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
+ KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
| B.Bind (a, B.Abst (n, w), t) ->
- let f a =
- let ee = B.push e B.empty a (B.abst n w) in
- P.fprintf och "%a[%a:%a].%a" (pp_level st) n (name C.err) a (pp_term st e) w (pp_term st ee) t
- in
- rename f e a
+ let a = R.alpha B.mem e a in
+ let ee = B.push e B.empty a (B.abst n w) in
+ KP.fprintf och "%a[%a:%a].%a" (pp_level st) n (name C.start) a (pp_term st e) w (pp_term st ee) t
| B.Bind (a, B.Abbr v, t) ->
- let f a =
- let ee = B.push e B.empty a (B.abbr v) in
- P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term st e) v (pp_term st ee) t
- in
- rename f e a
+ let a = R.alpha B.mem e a in
+ let ee = B.push e B.empty a (B.abbr v) in
+ KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t
| B.Bind (a, B.Void, t) ->
- let f a =
- let ee = B.push e B.empty a B.Void in
- P.fprintf och "[%a].%a" (name C.err) a (pp_term st ee) t
- in
- rename f e a
+ let a = R.alpha B.mem e a in
+ let ee = B.push e B.empty a B.Void in
+ KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t
let pp_lenv st och e =
let pp_entry f e c a b x = f x (* match b with
| B.Abst (a, w) ->
- let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term st e) w; f a in
- rename f x a
- | B.Abbr (a, v) ->
- let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term st e) v; f a in
- rename f c a
- | B.Void a ->
- let f a = P.fprintf och "%a\n" (name C.err) a; f a in
- rename f c a
+ let a = R.alpha B.mem e a in
+ KP.fprintf och "%a : %a\n" (name C.start) a (pp_term st e) w; f a
+ | B.Abbr (a, v) ->
+ let a = R.alpha B.mem e a in
+ KP.fprintf och "%a = %a\n" (name C.start) a (pp_term st e) v; f a
+ | B.Void a ->
+ let a = R.alpha B.mem e a in
+ KP.fprintf och "%a\n" (name C.start) a; f a
*) in
let e = B.empty in
- if e = B.empty then P.fprintf och "%s\n" "not shown" else
+ if e = B.empty then KP.fprintf och "%s\n" "not shown" else
B.fold_right ignore pp_entry e B.empty
let specs = {
ac_nfs st (step st m1 v1) (m2, t2, r2)
| B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _,
B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ ->
- if !G.cc && not (N.assert_equal st n1 n2) then false else
- if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
- ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
+ if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) &&
+ ac st (reset m1 zero) w1 (reset m2 zero) w2
+ then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
| B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
if !G.si then
let rec alpha mem x a =
let err () = a in
let f () = match a.E.n_name with
- | None -> assert false
+ | None -> a
| Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)}
in
mem err f x a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module K = Hashtbl
-module P = Scanf
+module KH = Hashtbl
+module KS = Scanf
-module C = Cps
+module C = Cps
type graph = string * (int -> int)
let sorts = 3
-let sort = K.create sorts
+let sort = KH.create sorts
let default_graph = "Z1"
(* Internal functions *******************************************************)
let set_sort h s =
- K.add sort h s; succ h
+ KH.add sort h s; succ h
let graph_of_string err f s =
try
- let x = P.sscanf s "Z%u" C.start in
+ let x = KS.sscanf s "Z%u" C.start in
if x > 0 then f (s, fun h -> x + h) else err ()
with
- P.Scan_failure _ | Failure _ | End_of_file -> err ()
+ KS.Scan_failure _ | Failure _ | End_of_file -> err ()
let graph = ref (graph_of_string C.err C.start default_graph)
List.fold_left set_sort i ss
let string_of_sort err f h =
- try f (K.find sort h) with Not_found -> err ()
+ try f (KH.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 K.fold map sort None with
+ match KH.fold map sort None with
| None -> err ()
| Some h -> f h
graph_of_string err f s
let clear () =
- K.clear sort; graph := graph_of_string C.err C.start default_graph
+ KH.clear sort; graph := graph_of_string C.err C.start default_graph
module KH = Hashtbl
-module L = Log
-module P = Marks
-module G = Options
+module L = Log
+module P = Marks
+module G = Options
type value = Inf (* infinite layer *)
| Fin of int (* finite layer *)
end; b end
let is_not_zero st n =
- let _, n = resolve_layer st n in n.v <> zero
+(* let _, n = resolve_layer st n in *) n.v <> zero
+let are_equal st n1 n2 =
+(*
+ let _, n1 = resolve_layer st n1 in
+ let _, n2 = resolve_layer st n2 in
+*)
+ n1.v = n2.v
val is_not_zero: status -> layer -> bool
+val are_equal: status -> layer -> layer -> bool
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
-module L = Log
-module G = Options
+module L = Log
+module G = Options
type reductions = {
beta : int;
let prs = r.lrt + r.grt + r.e in
let delta = r.ldelta + r.gdelta in
let rt = r.lrt + r.grt in
- L.warn level (P.sprintf "Reductions summary");
- L.warn level (P.sprintf " Proper reductions: %7u" rs);
- L.warn level (P.sprintf " Beta: %7u" r.beta);
- L.warn level (P.sprintf " Delta: %7u" delta);
- L.warn level (P.sprintf " Local: %7u" r.ldelta);
- L.warn level (P.sprintf " Global: %7u" r.gdelta);
- L.warn level (P.sprintf " Theta: %7u" r.theta);
- L.warn level (P.sprintf " Zeta for abbreviation: %7u" r.zeta);
- L.warn level (P.sprintf " Zeta for cast: %7u" r.epsilon);
- L.warn level (P.sprintf " Sort inclusion: %7u" r.upsilon);
- L.warn level (P.sprintf " Pseudo reductions: %7u" prs);
- L.warn level (P.sprintf " Reference typing: %7u" rt);
- L.warn level (P.sprintf " Local: %7u" r.lrt);
- L.warn level (P.sprintf " Global: %7u" r.grt);
- L.warn level (P.sprintf " Cast typing: %7u" r.e);
- L.warn level (P.sprintf "Relocated nodes (icm): %7u" !G.icm)
+ L.warn level (KP.sprintf "Reductions summary");
+ L.warn level (KP.sprintf " Proper reductions: %7u" rs);
+ L.warn level (KP.sprintf " Beta: %7u" r.beta);
+ L.warn level (KP.sprintf " Delta: %7u" delta);
+ L.warn level (KP.sprintf " Local: %7u" r.ldelta);
+ L.warn level (KP.sprintf " Global: %7u" r.gdelta);
+ L.warn level (KP.sprintf " Theta: %7u" r.theta);
+ L.warn level (KP.sprintf " Zeta for abbreviation: %7u" r.zeta);
+ L.warn level (KP.sprintf " Zeta for cast: %7u" r.epsilon);
+ L.warn level (KP.sprintf " Sort inclusion: %7u" r.upsilon);
+ L.warn level (KP.sprintf " Pseudo reductions: %7u" prs);
+ L.warn level (KP.sprintf " Reference typing: %7u" rt);
+ L.warn level (KP.sprintf " Local: %7u" r.lrt);
+ L.warn level (KP.sprintf " Global: %7u" r.grt);
+ L.warn level (KP.sprintf " Cast typing: %7u" r.e);
+ L.warn level (KP.sprintf "Relocated nodes (icm): %7u" !G.icm)
| EAppl (tl, _, _) -> aux i tl
| EBind (tl, a, _) ->
let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
- E.name err f a
+ let err () = aux (succ i) tl in
+ E.name err f a
| EProj (tl, _, d) -> append (aux i) tl d
in
aux 0 lenv
and pp_bind out st = function
| D.Abst (n, x) ->
- out "[:"; pp_term out st x; out "]"; out (N.to_string st n)
- | D.Abbr x -> out "[="; pp_term out st x; out "]";
- | D.Void -> out "[]"
+ out "[:"; pp_term out st x; out "]"; out (N.to_string st n); out " "
+ | D.Abbr x -> out "[="; pp_term out st x; out "] ";
+ | D.Void -> out "[] "
and pp_lenv out st = function
| D.ESort -> ()
| D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
- | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
- | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"
+ | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ") "
+ | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "} "
val print_counters: (unit -> 'a) -> counters -> 'a
val pp_term: (string -> unit) -> Layer.status -> Crg.term -> unit
+
+val pp_lenv: (string -> unit) -> Layer.status -> Crg.lenv -> unit
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module S = String
-module P = Printf
+module KT = String
+module KP = Printf
module U = NUri
let err = stderr
let pp_items och a st l items =
- let indent = S.make (l+l) ' ' in
+ let indent = KT.make (l+l) ' ' in
let pp_item och = function
- | Term (c, t) -> P.fprintf och "%s%a\n" indent (st.pp_term a c) t
- | LEnv c -> P.fprintf och "%s%a" indent (st.pp_lenv a) c
- | Warn s -> P.fprintf och "%s%s\n" indent s
- | Uri u -> P.fprintf och "%s<%s>\n" indent (U.string_of_uri u)
+ | Term (c, t) -> KP.fprintf och "%s%a\n" indent (st.pp_term a c) t
+ | LEnv c -> KP.fprintf och "%s%a" indent (st.pp_lenv a) c
+ | Warn s -> KP.fprintf och "%s%s\n" indent s
+ | Uri u -> KP.fprintf och "%s<%s>\n" indent (U.string_of_uri u)
in
let iter map och l = List.iter (map och) l in
- P.fprintf och "%a%!" (iter pp_item) items
+ KP.fprintf och "%a%!" (iter pp_item) items
(* Interface functions ******************************************************)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
module L = Log
let times = Unix.times () in
let stamp = times.Unix.tms_utime in
let lap = stamp -. !old in
- let str = P.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in
+ let str = KP.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in
L.warn level str;
old := stamp
let h = gmt.Unix.tm_hour in
let m = gmt.Unix.tm_min in
let s = gmt.Unix.tm_sec in
- let str = P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s in
+ let str = KP.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s in
L.warn level str;
module KF = Filename
module KH = Hashtbl
+module KL = List
module KP = Printf
+module KS = Scanf
+module KT = String
module U = NUri
module UH = NUri.UriHash
module T = Txt
module TP = TxtParser
module TL = TxtLexer
-module TT = TxtTxt
module TD = TxtCrg
module A = Aut
-txt txtParser txtLexer txtTxt txtCrg
+txt txtParser txtLexer txtCrg
+++ /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
| Th (* theorem *)
type bind =
-(* name, real?, domain *)
- | Abst of (id * bool * term) list
+(* layer, name, real?, domain *)
+ | Abst of N.layer * id * bool * term
(* name, bodies *)
- | Abbr of (id * term) list
-(* names *)
- | Void of id list
+ | Abbr of id * term
+(* name *)
+ | Void of id
+
+and lenv = bind list
and term =
(* level *)
(* named level *)
| NSrt of id
(* index, offset *)
- | LRef of ix * ix
+ | LRef of ix
(* name *)
| NRef of id
(* domain, element *)
| Cast of term * term
(* arguments, function *)
- | Appl of term list * term
-(* level, binder, scope *)
- | Bind of N.layer * bind * term
+ | Appl of term * term
+(* environment, scope *)
+ | Proj of lenv * term
(* function, arguments *)
| Inst of term * term list
-(* level, strong?, label, source, target *)
- | Impl of N.layer * bool * id * term * term
type command =
(* required files: names *)
(* section: Some id = open, None = close last *)
| Section of id option
(* entity: main?, class, name, info, contents *)
- | Entity of bool * kind * N.layer * id * info * term
+ | Constant of bool * kind * id * info * term
(* predefined generated entity: arguments *)
| Generate of term list
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module KF = Filename
+module KH = Hashtbl
+module KL = List
+
module U = NUri
module C = Cps
module G = Options
module H = Hierarchy
module E = Entity
module T = Txt
-module TT = TxtTxt
module D = Crg
type status = {
let henv_size = 7000 (* hash tables initial size *)
-let henv = Hashtbl.create henv_size (* optimized global environment *)
+let henv = KH.create henv_size (* optimized global environment *)
+
+let xerr s () =
+ Printf.printf "%s\n%!" s; C.err ()
(* Internal functions *******************************************************)
-(*
-let name_of_id ?(r=true) id = E.Name (id, r)
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
+let mk_lref f a i = f a (D.TLRef (a, i))
+
+let mk_gref f a uri = f a (D.TGRef (a, uri))
+
+let get err f e i = match D.get e i with
+ | _, _, D.Void -> err ()
+ | _, a, _ -> mk_lref f a i
+
+let resolve_gref err f st id =
+ try
+ let a, uri = KH.find henv id in f a uri
+ with Not_found -> err ()
-let mk_gref f uri = f (D.TGRef ([], uri))
+let name_of_id ?(r=true) id =
+ if id = "" then None else Some (id, r)
let uri_of_id st id path =
let str = String.concat "/" path in
- let str = Filename.concat str id in
+ let str = KF.concat str id in
let str = st.mk_uri str in
U.uri_of_string str
-let resolve_gref err f st id =
- try f (Hashtbl.find henv id)
- with Not_found -> err ()
-
let rec xlate_term f st lenv = function
- | T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
- f (D.TSort ([], h))
- | T.NSrt id ->
- let f h = f (D.TSort ([], h)) in
- H.sort_of_string C.err f id
- | T.LRef (i, j) ->
- D.get_index C.err (mk_lref f i j) i j lenv
+(*
+ CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
+ Printf.printf "\n";
+*)
+ | T.Sort h ->
+ let a = E.node_attrs ~sort:h () in
+ f a (D.TSort (a, h))
+ | T.NSrt id ->
+ let f h = xlate_term f st lenv (T.Sort h) in
+ H.sort_of_string (xerr "sort not found") f id
+ | T.LRef i ->
+ get (xerr "index out of bounds") f lenv i
| T.NRef id ->
- let err () = resolve_gref C.err (mk_gref f) st id in
+ let err () = resolve_gref (xerr "global constant not found") (mk_gref f) 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
+ let f uu a tt = f a (D.TCast (a, 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 (n, 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 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
+ | T.Appl (v, t) ->
+ let f vv a tt = f a (D.TAppl (a, vv, tt)) in
+ let f _ vv = xlate_term (f vv) st lenv t in
+ xlate_term f st lenv v
+ | T.Proj (bs, t) ->
+ let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f (lenv, e) = xlate_term (f e) st lenv t in
+ C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
+ | T.Inst (t, vs) ->
+ let map f v e =
+ let f _ vv = D.push_appl f E.empty_node vv e in
+ xlate_term f st lenv v
in
- let lenv, aa, bb = match b with
- | T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
- let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst (n, wws)
- | T.Abbr xvs ->
- let lenv = D.push_bind C.start lenv [] (D.Abbr []) 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 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 n tt = function
- | T.Decl -> [] , E.Abst (n, tt)
- | T.Ax -> [E.InProp] , E.Abst (n, tt)
- | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f e = xlate_term (f e) st lenv t in
+ C.list_fold_right f map vs D.empty_lenv
+
+and xlate_bind st f (lenv, e) b =
+ let f lenv e = f (lenv, e) in
+ let f a b lenv = D.push_bind (f lenv) a b e in
+ let f a b = D.push_bind (f a b) a b lenv in
+ match b with
+ | T.Abst (n, id, r, w) ->
+ let f a ww =
+ let a = {a with E.n_name = name_of_id ~r id} in
+ f a (D.Abst (n, ww))
+ in
+ xlate_term f st lenv w
+ | T.Abbr (id, v) ->
+ let f a vv =
+ let a = {a with E.n_name = name_of_id id} in
+ f a (D.Abbr vv)
+ in
+ xlate_term f st lenv v
+ | T.Void id ->
+ let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
+ f a D.Void
+
+let mk_contents main kind tt =
+ let ms, b = match kind with
+ | T.Decl -> [] , E.Abst tt
+ | T.Ax -> [E.InProp] , E.Abst tt
+ | T.Cong -> [E.InProp; E.Progress], E.Abst tt
+ | T.Def -> [] , E.Abbr tt
+ | T.Th -> [E.InProp] , E.Abbr tt
+ in
+ if main then E.Main :: ms, b else ms, b
let xlate_entity err f gen st = function
- | T.Require _ ->
+ | T.Require _ ->
err st
- | T.Section (Some name) ->
+ | T.Section (Some name) ->
err {st with path = name :: st.path}
- | T.Section None ->
+ | T.Section None ->
begin match st.path with
| _ :: ptl ->
err {st with path = ptl}
| _ -> assert false
end
- | T.Sorts sorts ->
+ | T.Sorts sorts ->
let map st (xix, s) =
let ix = match xix with
| None -> st.sort
in
{st with sort = H.set_sorts ix [s]}
in
- err (List.fold_left map st sorts)
- | T.Graph id ->
+ err (KL.fold_left map st sorts)
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (main, kind, n, id, info, t) ->
+ | T.Constant (main, kind, id, info, t) ->
let uri = uri_of_id st id st.path in
- Hashtbl.add henv id uri;
- let tt = xlate_term C.start st D.empty_lenv t in
+ let g na tt =
(*
- print_newline (); CrgOutput.pp_term print_string tt;
-*)
- let a = [] in
- let ms, b = mk_contents n tt kind in
- let ms = if main then E.Main :: ms else ms in
- let a = if ms <> [] then E.Meta ms :: a else a in
- let a = if info <> ("", "") then E.Info info :: a else a in
- let entity = E.Mark st.line :: a, uri, b in
- f {st with line = succ st.line} entity
- | T.Generate _ ->
+ print_newline (); CrgOutput.pp_term print_string tt;
+*)
+ let na = {na with E.n_apix = st.line} in
+ KH.add henv id (na, uri);
+ let meta, b = mk_contents main kind tt in
+ let ra = E.root_attrs ~meta ~info () in
+ let entity = ra, na, uri, b in
+ f {st with line = succ st.line} entity
+
+ in
+ xlate_term g st D.empty_lenv t
+ | T.Generate _ ->
err st
(* Interface functions ******************************************************)
-*)
+
let initial_status () =
- Hashtbl.clear henv; {
+ KH.clear henv; {
path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
}
mk_uri = G.get_mk_uri ()
}
-let crg_of_txt _ _ = assert false (* xlate_entity *)
+let crg_of_txt = xlate_entity
| ")" { out "CP"; TP.CP }
| "[" { out "OB"; TP.OB }
| "]" { out "CB"; TP.CB }
+ | "{" { out "OC"; TP.OC }
+ | "}" { out "CC"; TP.CC }
| "<" { out "OA"; TP.OA }
| ">" { out "CA"; TP.CA }
| "." { out "FS"; TP.FS }
| "=" { out "EQ"; TP.EQ }
| "*" { out "STAR"; TP.STAR }
| "#" { out "HASH"; TP.HASH }
- | "+" { out "PLUS"; TP.PLUS }
| "~" { out "TE"; TP.TE }
- | "->" { out "WTO"; TP.WTO }
- | "=>" { out "STO"; TP.STO }
| "^" { out "CT"; TP.CT }
| eof { out "EOF"; TP.EOF }
*/
%{
- module G = Options
- module N = Layer
- module T = Txt
+ module G = Options
+ module N = Layer
+ module T = Txt
let _ = Parsing.set_trace !G.debug_parser
%}
%token <int> IX
%token <string> ID STR
- %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
+ %token OP CP OB CB OA CA OC CC FS CN CM EQ STAR HASH TE CT
%token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option> entry
-
- %nonassoc CP CB CA
- %right WTO STO
%%
hash:
| {}
| sort { [$1] }
| sort CM sorts { $1 :: $3 }
;
- level:
- | { N.infinite }
- | CT IX { N.finite $2}
+ layer:
+ | { N.infinite }
+ | CT IX { N.finite $2 }
+ ;
+
+ binder:
+ | OB ID CN term CB layer { T.Abst ($6, $2, true, $4) }
+ | OB term CB layer { T.Abst ($4, "", false, $2) }
+ | OB ID TE term CB layer { T.Abst ($6, $2, false, $4) }
+ | OB ID EQ term CB { T.Abbr ($2, $4) }
+ ;
+ binders:
+ | binder fs binder { [$1; $3] }
+ | binder fs binders { $1 :: $3 }
+ ;
+ lenv:
+ | binder { [$1] }
+ | OC binders CC { $2 }
;
- abst:
- | ID CN term { $1, true, $3 }
- | TE term { "", false, $2 }
- | ID TE term { $1, false, $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) }
- | ID { T.NRef $1 }
- | HASH ID { T.NRef $2 }
- | atom OP term CP { T.Inst ($1, [$3]) }
- | atom OP terms CP { T.Inst ($1, $3) }
+ | STAR IX { T.Sort $2 }
+ | STAR ID { T.NSrt $2 }
+ | hash IX { T.LRef $2 }
+ | ID { T.NRef $1 }
+ | HASH ID { T.NRef $2 }
+ | atom OP terms CP { T.Inst ($1, $3) }
;
term:
- | atom { $1 }
- | OA term CA fs term { T.Cast ($2, $5) }
- | OP term CP fs term { T.Appl ([$2], $5) }
- | OP terms CP fs term { T.Appl ($2, $5) }
- | OB binder CB level fs term { T.Bind ($4, $2, $6) }
- | term WTO level term { T.Impl ($3, false, "", $1, $4) }
- | ID TE term WTO level term { T.Impl ($5, false, $1, $3, $6) }
- | term STO level term { T.Impl ($3, true, "", $1, $4) }
- | ID TE term STO level term { T.Impl ($5, true, $1, $3, $6) }
- | OP term CP { $2 }
+ | atom { $1 }
+ | OA term CA fs term { T.Cast ($2, $5) }
+ | OP term CP fs term { T.Appl ($2, $5) }
+ | lenv fs term { T.Proj ($1, $3) }
+ | OP term CP { $2 }
;
terms:
- | term CM term { [$1; $3] }
+ | term { [$1] }
| term CM terms { $1 :: $3 }
;
-
+
decl:
| DECL { T.Decl }
| AX { T.Ax }
| DEF { T.Def }
| TH { T.Th }
;
- xentity:
+ command:
| GRAPH ID
- { T.Graph $2 }
- | main decl level comment ID CN term
- { T.Entity ($1, $2, $3, $5, $4, $7) }
- | main def level comment ID EQ term
- { T.Entity ($1, $2, $3, $5, $4, $7) }
- | main def level comment ID EQ term CN term
- { T.Entity ($1, $2, $3, $5, $4, T.Cast ($9, $7)) }
- | GEN term
- { T.Generate [$2] }
+ { T.Graph $2 }
+ | main decl comment ID CN term
+ { T.Constant ($1, $2, $4, $3, $6) }
+ | main def comment ID EQ term
+ { T.Constant ($1, $2, $4, $3, $6) }
+ | main def comment ID EQ term CN term
+ { T.Constant ($1, $2, $4, $3, T.Cast ($8, $6)) }
| GEN terms
- { T.Generate $2 }
+ { T.Generate $2 }
| REQ ids
- { T.Require $2 }
+ { T.Require $2 }
| OPEN ID
- { T.Section (Some $2) }
+ { T.Section (Some $2) }
| CLOSE
- { T.Section None }
+ { T.Section None }
| SORTS sorts
- { T.Sorts $2 }
+ { T.Sorts $2 }
;
+
start:
| GRAPH {} | decl {} | def {} | GEN {} |
| REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
- | xentity start { Some $1 }
+ | command start { Some $1 }
| EOF { None }
;
+++ /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 (n, false, id, w, t) ->
- let tt = T.Bind (n, T.Abst [id, false, w], t) in
- contract f tt
- | T.Impl (n, true, id, w, t) ->
- let f = function
- | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
- f (T.Bind (n, T.Abst (xw :: xws), tt))
- | tt -> f tt
- in
- let tt = T.Impl (n, 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 (n, b, t) ->
- let f tt bb = f (T.Bind (n, 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
projects / helm.git / commitdiff