From edf9e34100f49d4aa5ba8f3ce53e34af7718d88e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 31 Dec 2014 22:23:34 +0000 Subject: [PATCH] last commit for helena 0.8.2 - a check was missing in the comparator - new textual syntax for \lambda\delta "Version 4" (exp_math files updated accordingly) - minor bug fixes (BrgOutput now uses the new alpha-conversion) --- helm/software/helena/.depend.opt | 19 +- helm/software/helena/MakeVersion | 2 +- helm/software/helena/Makefile.common | 2 +- helm/software/helena/README | 8 +- .../automath/{omega.aut => Omega.aut} | 3 +- .../helena/examples/automath/README.txt | 2 + helm/software/helena/examples/exp_math/L.hln | 22 +- .../helena/examples/exp_math/Makefile | 18 +- helm/software/helena/examples/exp_math/T0.hln | 58 +++--- helm/software/helena/src/automath/Omega.aut | 10 - .../software/helena/src/automath/autOutput.ml | 44 ++-- .../helena/src/basic_rg/brgGrafite.ml | 59 +++--- .../software/helena/src/basic_rg/brgOutput.ml | 119 ++++------- .../helena/src/basic_rg/brgReduction.ml | 6 +- helm/software/helena/src/common/alpha.ml | 2 +- helm/software/helena/src/common/hierarchy.ml | 20 +- helm/software/helena/src/common/layer.ml | 14 +- helm/software/helena/src/common/layer.mli | 1 + helm/software/helena/src/common/output.ml | 38 ++-- helm/software/helena/src/complete_rg/crg.ml | 3 +- .../helena/src/complete_rg/crgOutput.ml | 10 +- .../helena/src/complete_rg/crgOutput.mli | 2 + helm/software/helena/src/lib/log.ml | 16 +- helm/software/helena/src/lib/time.ml | 6 +- helm/software/helena/src/modules.ml | 4 +- helm/software/helena/src/text/Make | 2 +- helm/software/helena/src/text/prova.hln | 11 - helm/software/helena/src/text/txt.ml | 24 +-- helm/software/helena/src/text/txtCrg.ml | 197 ++++++++++-------- helm/software/helena/src/text/txtLexer.mll | 5 +- helm/software/helena/src/text/txtParser.mly | 117 +++++------ helm/software/helena/src/text/txtTxt.ml | 62 ------ helm/software/helena/src/text/txtTxt.mli | 12 -- 33 files changed, 399 insertions(+), 519 deletions(-) rename helm/software/helena/examples/automath/{omega.aut => Omega.aut} (83%) delete mode 100644 helm/software/helena/src/automath/Omega.aut delete mode 100644 helm/software/helena/src/text/prova.hln delete mode 100644 helm/software/helena/src/text/txtTxt.ml delete mode 100644 helm/software/helena/src/text/txtTxt.mli diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 7c4fa4e93..0d53d1bfd 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -52,16 +52,13 @@ src/text/txtLexer.cmo : src/text/txtParser.cmi src/common/options.cmx \ 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 @@ -123,11 +120,11 @@ src/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ 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 diff --git a/helm/software/helena/MakeVersion b/helm/software/helena/MakeVersion index 6f4eebdf6..100435be1 100644 --- a/helm/software/helena/MakeVersion +++ b/helm/software/helena/MakeVersion @@ -1 +1 @@ -0.8.1 +0.8.2 diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index babfcf50f..0db660fe6 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -7,7 +7,7 @@ endif RELISE = $(MAIN:%=%_$(shell cat MakeVersion)) -DOWNDIR = $(HOME)/svn/helm_stable/www/lambdadelta/download +DOWNDIR = ../../www/lambdadelta/download DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make)) diff --git a/helm/software/helena/README b/helm/software/helena/README index a21142fea..0636f4559 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -1,10 +1,10 @@ -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 diff --git a/helm/software/helena/examples/automath/omega.aut b/helm/software/helena/examples/automath/Omega.aut similarity index 83% rename from helm/software/helena/examples/automath/omega.aut rename to helm/software/helena/examples/automath/Omega.aut index 9e6c30e6f..ba90125f2 100644 --- a/helm/software/helena/examples/automath/omega.aut +++ b/helm/software/helena/examples/automath/Omega.aut @@ -1,8 +1,9 @@ +# 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:[y:'type']'type']'type' -@ Omega := Delta : 'type' + Omega := Delta : 'type' -l diff --git a/helm/software/helena/examples/automath/README.txt b/helm/software/helena/examples/automath/README.txt index 5d12c4666..8b6c026ea 100644 --- a/helm/software/helena/examples/automath/README.txt +++ b/helm/software/helena/examples/automath/README.txt @@ -3,3 +3,5 @@ This directory contains: 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 diff --git a/helm/software/helena/examples/exp_math/L.hln b/helm/software/helena/examples/exp_math/L.hln index 4b84f65fd..6d6c4a683 100644 --- a/helm/software/helena/examples/exp_math/L.hln +++ b/helm/software/helena/examples/exp_math/L.hln @@ -6,37 +6,37 @@ \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 diff --git a/helm/software/helena/examples/exp_math/Makefile b/helm/software/helena/examples/exp_math/Makefile index 9e7ed164e..c19636b78 100644 --- a/helm/software/helena/examples/exp_math/Makefile +++ b/helm/software/helena/examples/exp_math/Makefile @@ -1,6 +1,6 @@ HOME = ../.. ROOT = exp_math -HELENAOPTS = -r $(ROOT) -u +HELENAOPTS = -r $(ROOT) H = @ @@ -9,17 +9,9 @@ HELENA = $(HOME)/helena.opt 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) $^ diff --git a/helm/software/helena/examples/exp_math/T0.hln b/helm/software/helena/examples/exp_math/T0.hln index 8321246c6..fdc962d01 100644 --- a/helm/software/helena/examples/exp_math/T0.hln +++ b/helm/software/helena/examples/exp_math/T0.hln @@ -4,67 +4,67 @@ \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 @@ -74,15 +74,15 @@ \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 diff --git a/helm/software/helena/src/automath/Omega.aut b/helm/software/helena/src/automath/Omega.aut deleted file mode 100644 index 727f9fe6a..000000000 --- a/helm/software/helena/src/automath/Omega.aut +++ /dev/null @@ -1,10 +0,0 @@ -# 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:[y:'type']'type']'type' - Omega := Delta : 'type' --l diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml index 028fdd23c..a1f5ae18c 100644 --- a/helm/software/helena/src/automath/autOutput.ml +++ b/helm/software/helena/src/automath/autOutput.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module C = Cps module L = Log @@ -73,31 +73,31 @@ let count_command f c = function 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 diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index cb4935f1e..493ad3cac 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -9,16 +9,16 @@ \ / 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 *******************************************************) @@ -32,19 +32,19 @@ let width = 70 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 @@ -63,26 +63,27 @@ let out_uri och u = 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 @@ -93,34 +94,34 @@ let rec out_term st p e och = function | "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 diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index a49177855..78200e7e9 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module U = NUri module C = Cps @@ -18,6 +18,7 @@ module G = Options module H = Hierarchy module N = Layer module E = Entity +module R = Alpha module XD = XmlCrg module B = Brg module BD = BrgCrg @@ -109,107 +110,77 @@ let print_counters f c = 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 = { diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 6f9f5f09f..9a14a11fb 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -208,9 +208,9 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = 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 diff --git a/helm/software/helena/src/common/alpha.ml b/helm/software/helena/src/common/alpha.ml index 8da7e563b..67293fac8 100644 --- a/helm/software/helena/src/common/alpha.ml +++ b/helm/software/helena/src/common/alpha.ml @@ -16,7 +16,7 @@ module E = Entity 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 diff --git a/helm/software/helena/src/common/hierarchy.ml b/helm/software/helena/src/common/hierarchy.ml index 6e8c98fd6..3484faba7 100644 --- a/helm/software/helena/src/common/hierarchy.ml +++ b/helm/software/helena/src/common/hierarchy.ml @@ -9,29 +9,29 @@ \ / 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) @@ -41,14 +41,14 @@ let set_sorts i ss = 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 @@ -62,4 +62,4 @@ let set_graph s = 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 diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index ea02538d2..ede703d6d 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -11,9 +11,9 @@ 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 *) @@ -192,5 +192,11 @@ let assert_equal st n1 n2 = 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 diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli index 7ff8609bd..40ada03a1 100644 --- a/helm/software/helena/src/common/layer.mli +++ b/helm/software/helena/src/common/layer.mli @@ -39,3 +39,4 @@ val assert_equal: status -> layer -> layer -> bool val is_not_zero: status -> layer -> bool +val are_equal: status -> layer -> layer -> bool diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 5fba63786..23829c095 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -9,10 +9,10 @@ \ / 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; @@ -60,19 +60,19 @@ let print_reductions () = 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) diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 4624e4c8c..455eb6ed4 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -73,7 +73,8 @@ let resolve_lref err f id lenv = | 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 diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 7275dd462..7c9ab8172 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -145,12 +145,12 @@ let rec pp_term out st = function 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 "} " diff --git a/helm/software/helena/src/complete_rg/crgOutput.mli b/helm/software/helena/src/complete_rg/crgOutput.mli index a3f636381..86ea0f6c9 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.mli +++ b/helm/software/helena/src/complete_rg/crgOutput.mli @@ -18,3 +18,5 @@ val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a 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 diff --git a/helm/software/helena/src/lib/log.ml b/helm/software/helena/src/lib/log.ml index 6d3c2a783..e248eddf4 100644 --- a/helm/software/helena/src/lib/log.ml +++ b/helm/software/helena/src/lib/log.ml @@ -9,8 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module S = String -module P = Printf +module KT = String +module KP = Printf module U = NUri @@ -33,15 +33,15 @@ let std = stdout 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 ******************************************************) diff --git a/helm/software/helena/src/lib/time.ml b/helm/software/helena/src/lib/time.ml index eea82103e..2ca44689f 100644 --- a/helm/software/helena/src/lib/time.ml +++ b/helm/software/helena/src/lib/time.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module L = Log @@ -21,7 +21,7 @@ let utime_stamp = 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 @@ -33,5 +33,5 @@ let gmtime msg = 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; diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 3de74e13f..72e1a7493 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -2,7 +2,10 @@ 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 @@ -26,7 +29,6 @@ module DO = CrgOutput module T = Txt module TP = TxtParser module TL = TxtLexer -module TT = TxtTxt module TD = TxtCrg module A = Aut diff --git a/helm/software/helena/src/text/Make b/helm/software/helena/src/text/Make index 3690bbaeb..2cdbfd792 100644 --- a/helm/software/helena/src/text/Make +++ b/helm/software/helena/src/text/Make @@ -1 +1 @@ -txt txtParser txtLexer txtTxt txtCrg +txt txtParser txtLexer txtCrg diff --git a/helm/software/helena/src/text/prova.hln b/helm/software/helena/src/text/prova.hln deleted file mode 100644 index a782fda1c..000000000 --- a/helm/software/helena/src/text/prova.hln +++ /dev/null @@ -1,11 +0,0 @@ -\open pippo - -\global a : *Set - -\global b : *Prop - -\global f = [x:*Set].[y:*Prop].x - -\global "commento\"" c = f(a,b) : *Set - -\close diff --git a/helm/software/helena/src/text/txt.ml b/helm/software/helena/src/text/txt.ml index 0633d39a9..db92bc8ad 100644 --- a/helm/software/helena/src/text/txt.ml +++ b/helm/software/helena/src/text/txt.ml @@ -24,12 +24,14 @@ type kind = Decl (* generic declaration *) | 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 *) @@ -37,19 +39,17 @@ and term = (* 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 *) @@ -61,6 +61,6 @@ type command = (* 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 diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 21af0f511..8a4b70b79 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -9,13 +9,16 @@ \ / 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 = { @@ -27,102 +30,115 @@ 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 @@ -130,30 +146,31 @@ let xlate_entity err f gen st = function 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 () } @@ -161,4 +178,4 @@ let refresh_status st = {st with mk_uri = G.get_mk_uri () } -let crg_of_txt _ _ = assert false (* xlate_entity *) +let crg_of_txt = xlate_entity diff --git a/helm/software/helena/src/text/txtLexer.mll b/helm/software/helena/src/text/txtLexer.mll index ec97a8b83..9191f11bf 100644 --- a/helm/software/helena/src/text/txtLexer.mll +++ b/helm/software/helena/src/text/txtLexer.mll @@ -61,6 +61,8 @@ and token = parse | ")" { 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 } @@ -69,9 +71,6 @@ and token = parse | "=" { 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 } diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly index d9336b189..d08fb87d9 100644 --- a/helm/software/helena/src/text/txtParser.mly +++ b/helm/software/helena/src/text/txtParser.mly @@ -24,22 +24,19 @@ */ %{ - 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 IX %token 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 entry - - %nonassoc CP CB CA - %right WTO STO %% hash: | {} @@ -70,59 +67,46 @@ | 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 } @@ -132,33 +116,32 @@ | 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 } ; diff --git a/helm/software/helena/src/text/txtTxt.ml b/helm/software/helena/src/text/txtTxt.ml deleted file mode 100644 index fe0988401..000000000 --- a/helm/software/helena/src/text/txtTxt.ml +++ /dev/null @@ -1,62 +0,0 @@ -(* - ||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 diff --git a/helm/software/helena/src/text/txtTxt.mli b/helm/software/helena/src/text/txtTxt.mli deleted file mode 100644 index 357487625..000000000 --- a/helm/software/helena/src/text/txtTxt.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* - ||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 -- 2.39.2