From: Ferruccio Guidi Date: Sat, 30 Oct 2010 13:00:05 +0000 (+0000) Subject: - initial support for abstractions with explicit levels X-Git-Tag: make_still_working~2748 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22fd9c98a22929f0319286c0693fcdaee43a72df;p=helm.git - initial support for abstractions with explicit levels - some minor bug fixes --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 0c298824f..b71db9944 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -17,20 +17,23 @@ src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \ src/common/output.cmi src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \ src/common/output.cmi -src/common/entity.cmo: src/common/options.cmx -src/common/entity.cmx: src/common/options.cmx +src/common/level.cmi: +src/common/level.cmo: src/common/level.cmi +src/common/level.cmx: src/common/level.cmi +src/common/entity.cmo: src/common/options.cmx src/common/level.cmi +src/common/entity.cmx: src/common/options.cmx src/common/level.cmx src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmx: src/common/entity.cmx src/common/alpha.cmi: src/common/entity.cmx src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi -src/text/txt.cmo: -src/text/txt.cmx: +src/text/txt.cmo: src/common/level.cmi +src/text/txt.cmx: src/common/level.cmx src/text/txtParser.cmi: src/text/txt.cmx src/text/txtParser.cmo: src/text/txt.cmx src/common/options.cmx \ - src/text/txtParser.cmi + src/common/level.cmi src/text/txtParser.cmi src/text/txtParser.cmx: src/text/txt.cmx src/common/options.cmx \ - src/text/txtParser.cmi + src/common/level.cmx src/text/txtParser.cmi 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 \ @@ -105,13 +108,15 @@ src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi -src/complete_rg/crg.cmo: src/common/entity.cmx -src/complete_rg/crg.cmx: src/common/entity.cmx +src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx +src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo: src/common/hierarchy.cmi src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx: src/common/hierarchy.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmo: src/common/level.cmi src/common/hierarchy.cmi \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmx: src/common/level.cmx src/common/hierarchy.cmx \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/complete_rg/crgOutput.cmi src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \ src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \ @@ -120,17 +125,17 @@ src/complete_rg/crgTxt.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/complete_rg/crgTxt.cmi src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx -src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \ - src/complete_rg/crgAut.cmi -src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \ - src/complete_rg/crgAut.cmi -src/xml/xmlLibrary.cmi: src/common/entity.cmx -src/xml/xmlLibrary.cmo: src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/xml/xmlLibrary.cmi -src/xml/xmlLibrary.cmx: src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/xml/xmlLibrary.cmi +src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/level.cmi \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/automath/aut.cmx src/complete_rg/crgAut.cmi +src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/level.cmx \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/automath/aut.cmx src/complete_rg/crgAut.cmi +src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx +src/xml/xmlLibrary.cmo: src/common/level.cmi src/common/hierarchy.cmi \ + src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi +src/xml/xmlLibrary.cmx: src/common/level.cmx src/common/hierarchy.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi: src/xml/xmlLibrary.cmi src/complete_rg/crg.cmx src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ @@ -138,25 +143,25 @@ src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/common/alpha.cmx src/xml/xmlCrg.cmi -src/basic_rg/brg.cmo: src/common/entity.cmx -src/basic_rg/brg.cmx: src/common/entity.cmx +src/basic_rg/brg.cmo: src/common/level.cmi src/common/entity.cmx +src/basic_rg/brg.cmx: src/common/level.cmx src/common/entity.cmx src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx -src/basic_rg/brgCrg.cmo: src/common/marks.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgCrg.cmi -src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgCrg.cmi +src/basic_rg/brgCrg.cmo: src/common/marks.cmx src/common/level.cmi \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi +src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/level.cmx \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi src/basic_rg/brgOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \ - src/lib/log.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/lib/log.cmi src/common/level.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/brgOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \ - src/lib/log.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/lib/log.cmx src/common/level.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/brgEnvironment.cmi: src/basic_rg/brg.cmx src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgEnvironment.cmi @@ -180,15 +185,15 @@ src/basic_rg/brgReduction.cmx: src/lib/share.cmx src/common/output.cmx \ src/basic_rg/brgType.cmi: src/lib/log.cmi src/common/entity.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ - src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ - src/basic_rg/brgType.cmi + src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ + src/lib/cps.cmx src/basic_rg/brgSubstitution.cmi \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ + src/basic_rg/brg.cmx src/basic_rg/brgType.cmi src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ - src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgType.cmi + src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \ + src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ + src/basic_rg/brg.cmx src/basic_rg/brgType.cmi src/basic_rg/brgUntrusted.cmi: src/common/entity.cmx src/basic_rg/brgType.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ @@ -208,21 +213,23 @@ src/toplevel/metaOutput.cmx: src/toplevel/meta.cmx src/lib/log.cmx \ src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \ - src/toplevel/metaAut.cmi + src/common/level.cmi src/common/entity.cmx src/lib/cps.cmx \ + src/automath/aut.cmx src/toplevel/metaAut.cmi src/toplevel/metaAut.cmx: src/common/options.cmx src/toplevel/meta.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \ - src/toplevel/metaAut.cmi + src/common/level.cmx src/common/entity.cmx src/lib/cps.cmx \ + src/automath/aut.cmx src/toplevel/metaAut.cmi src/toplevel/metaBag.cmi: src/toplevel/meta.cmx src/basic_ag/bag.cmx src/toplevel/metaBag.cmo: src/toplevel/meta.cmx src/lib/cps.cmx \ src/basic_ag/bag.cmx src/toplevel/metaBag.cmi src/toplevel/metaBag.cmx: src/toplevel/meta.cmx src/lib/cps.cmx \ src/basic_ag/bag.cmx src/toplevel/metaBag.cmi src/toplevel/metaBrg.cmi: src/toplevel/meta.cmx src/basic_rg/brg.cmx -src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi -src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi +src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/level.cmi \ + src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ + src/toplevel/metaBrg.cmi +src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/level.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ + src/toplevel/metaBrg.cmi src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \ src/lib/time.cmx src/common/output.cmi src/common/options.cmx \ diff --git a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml index de954ed56..dfdc6e116 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml @@ -64,13 +64,13 @@ and count_term f c = function count_term f c t let count_entity f c = function - | _, _, E.Abst w -> + | _, _, E.Abst (_, w) -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | _, _, E.Abbr v -> + | _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | _, _, E.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml index e2e00e39b..52f04bf0e 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml @@ -113,14 +113,14 @@ let rec whd f c m x = let rec ho_whd f c m x = (* L.warn "entering R.ho_whd"; *) let aux m = function - | Sort_ h -> f (Sort h) - | Bind_ (_, _, w, _) -> + | Sort_ h -> f (Sort h) + | Bind_ (_, _, w, _) -> let f w = f (Abst w) in unwind_to_term f m w - | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, _, E.Abst w) -> ho_whd f c m w - | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v - | LRef_ (_, None) -> assert false - | GRef_ (_, _, E.Void) -> assert false + | LRef_ (_, Some w) -> ho_whd f c m w + | GRef_ (_, _, E.Abst (_, w)) -> ho_whd f c m w + | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v + | LRef_ (_, None) -> assert false + | GRef_ (_, _, E.Void) -> assert false in whd aux c m x diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml index d92e23272..1314218d3 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml @@ -65,7 +65,7 @@ let rec b_type_of f st c x = Z.get f c i | Z.GRef uri -> let f = function - | _, _, E.Abst w -> f x w + | _, _, E.Abst (_, w) -> f x w | _, _, E.Abbr (Z.Cast (w, v)) -> f x w | _, _, E.Abbr _ -> assert false | _, _, E.Void -> assert false diff --git a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml index 72223f778..5d04a3bf4 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml @@ -20,10 +20,10 @@ module ZT = BagType (* to share *) let type_check f st = function - | a, uri, E.Abst t -> - let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst xt) in + | a, uri, E.Abst (n, t) -> + let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t - | a, uri, E.Abbr t -> + | a, uri, E.Abbr t -> let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t - | _, _, E.Void -> assert false + | _, _, E.Void -> assert false diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml index d2a0b9987..bc6eb5727 100644 --- a/helm/software/lambda-delta/src/basic_rg/brg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brg.ml @@ -13,14 +13,15 @@ (* note : ufficial basic lambda-delta *) module E = Entity +module N = Level type uri = E.uri type id = E.id type attrs = E.attrs -type bind = Void (* *) - | Abst of term (* type *) - | Abbr of term (* body *) +type bind = Void (* *) + | Abst of N.level * term (* level, type *) + | Abbr of term (* body *) and term = Sort of attrs * int (* attrs, hierarchy index *) | LRef of attrs * int (* attrs, position index *) @@ -43,7 +44,7 @@ let mk_uri si root s = (* Currified constructors ***************************************************) -let abst w = Abst w +let abst n w = Abst (n, w) let abbr v = Abbr v @@ -55,7 +56,7 @@ let appl a u t = Appl (a, u, t) let bind a b t = Bind (a, b, t) -let bind_abst a u t = Bind (a, Abst u, t) +let bind_abst n a u t = Bind (a, Abst (n, u), t) let bind_abbr a v t = Bind (a, Abbr v, t) diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml index 32950e1cf..f844c2e51 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml @@ -12,6 +12,7 @@ module C = Cps module E = Entity module J = Marks +module N = Level module D = Crg module B = Brg @@ -37,8 +38,8 @@ let rec xlate_term f = function | D.TProj (a, e, t) -> let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in xlate_term f t - | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) -> - xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t))) + | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> + xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t))) | D.TBind (a, b, t) -> let f tt = f (xlate_bind tt a b) in xlate_term f t @@ -46,19 +47,19 @@ and xlate_bind x a b = let f a ns = a, ns in let a, ns = E.get_names f a in match b with - | D.Abst ws -> + | D.Abst (m, ws) -> let map x n w = - let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in + let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in xlate_term f w in List.fold_left2 map x ns ws - | D.Abbr vs -> + | D.Abbr vs -> let map x n v = let f vv = B.Bind (n :: a, B.Abbr vv, x) in xlate_term f v in List.fold_left2 map x ns vs - | D.Void _ -> + | D.Void _ -> let map x n = B.Bind (n :: a, B.Void, x) in List.fold_left map x ns @@ -85,13 +86,13 @@ let rec xlate_bk_term f = function xlate_bk_bind f b and xlate_bk_bind f = function - | B.Abst t -> - let f tt = f (D.Abst [tt]) in + | B.Abst (n, t) -> + let f tt = f (D.Abst (n, [tt])) in xlate_bk_term f t - | B.Abbr t -> + | B.Abbr t -> let f tt = f (D.Abbr [tt]) in xlate_bk_term f t - | B.Void -> f (D.Void 1) + | B.Void -> f (D.Void 1) (* interface functions ******************************************************) diff --git a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml index d4b851b76..ed024a68e 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml @@ -17,6 +17,7 @@ module L = Log module G = Options module E = Entity module H = Hierarchy +module N = Level module XD = XmlCrg module B = Brg module BD = BrgCrg @@ -48,13 +49,13 @@ let initial_counters = { } let rec count_term_binder f c e = function - | B.Abst w -> + | B.Abst (_, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in count_term f c e w - | B.Abbr v -> + | B.Abbr v -> let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in count_term f c e v - | B.Void -> + | B.Void -> let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in f c @@ -89,15 +90,15 @@ and count_term f c e = function count_term_binder f c e b let count_entity f c = function - | _, u, E.Abst w -> + | _, u, E.Abst (_, w) -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in count_term f c B.empty w - | _, _, E.Abbr v -> + | _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty v - | _, _, E.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = @@ -151,10 +152,13 @@ let rename f e a = let name err frm a = let f n = function | true -> F.fprintf frm "%s" n - | false -> F.fprintf frm "^%s" n + | false -> F.fprintf frm "-%s" n in E.name err f a +let pp_level frm n = + if N.is_infinite n then () else F.fprintf frm "^%s" (N.to_string n) + let rec pp_term e frm = function | B.Sort (_, h) -> let err _ = F.fprintf frm "@[*%u@]" h in @@ -171,10 +175,10 @@ let rec pp_term e frm = function F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t | B.Appl (_, v, t) -> F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t - | B.Bind (a, B.Abst w, t) -> + | B.Bind (a, B.Abst (n, w), t) -> let f a = - let ee = B.push e B.empty a (B.abst w) in - F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t + let ee = B.push e B.empty a (B.abst n w) in + F.fprintf frm "@[[%a:%a]%a.%a@]" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t in rename f e a | B.Bind (a, B.Abbr v, t) -> diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index bd78edc26..5a5559f7c 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -59,10 +59,10 @@ let are_alpha_convertible err f t1 t2 = aux_bind f (b1, b2) | _ -> err () and aux_bind f = function - | B.Abbr v1, B.Abbr v2 - | B.Abst v1, B.Abst v2 -> aux f (v1, v2) - | B.Void, B.Void -> f () - | _ -> err () + | B.Abbr v1, B.Abbr v2 -> aux f (v1, v2) + | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2) + | B.Void, B.Void -> f () + | _ -> err () in if S.eq t1 t2 then f () else aux f (t1, t2) @@ -73,41 +73,41 @@ let get m i = let rec step st m x = (* L.warn "entering R.step"; *) match x with - | B.Sort _ -> m, None, x - | B.GRef (_, uri) -> + | B.Sort _ -> m, None, x + | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abbr v when st.E.delta -> + | _, _, E.Abbr v when st.E.delta -> O.add ~gdelta:1 (); step st m v - | _, _, E.Abst w when st.E.rt -> + | _, _, E.Abst (_, w) when st.E.rt -> O.add ~grt:1 (); step st m w - | a, _, E.Abbr v -> + | a, _, E.Abbr v -> let e = E.apix C.err C.start a in m, Some (e, a, B.Abbr v), x - | a, _, E.Abst w -> + | a, _, E.Abst (n, w) -> let e = E.apix C.err C.start a in - m, Some (e, a, B.Abst w), x - | _, _, E.Void -> assert false + m, Some (e, a, B.Abst (n, w)), x + | _, _, E.Void -> assert false end - | B.LRef (_, i) -> + | B.LRef (_, i) -> begin match get m i with - | c, _, B.Abbr v -> + | c, _, B.Abbr v -> O.add ~ldelta:1 (); step st {m with e = c} v - | c, _, B.Abst w when st.E.rt -> + | c, _, B.Abst (_, w) when st.E.rt -> O.add ~lrt:1 (); step st {m with e = c} w - | c, _, B.Void -> + | c, _, B.Void -> assert false - | c, a, (B.Abst _ as b) -> + | c, a, (B.Abst _ as b) -> let e = E.apix C.err C.start a in {m with e = c}, Some (e, a, b), x end - | B.Cast (_, _, t) -> + | B.Cast (_, _, t) -> O.add ~tau:1 (); step st m t - | B.Appl (_, v, t) -> + | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t - | B.Bind (a, B.Abst w, t) -> + | B.Bind (a, B.Abst (n, w), t) -> begin match m.s with | [] -> m, None, x | (c, v) :: s -> @@ -154,9 +154,9 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = | Some (_, _, B.Abbr v1), _, _, _ -> O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) - | _, B.Bind (a1, (B.Abst w1 as b1), t1), - _, B.Bind (a2, (B.Abst w2 as b2), t2) -> - if ac {st with E.si = false} m1 w1 m2 w2 then + | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), + _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) -> + if (* n1 = n2 && *) ac {st with E.si = false} m1 w1 m2 w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false | _, B.Sort _, _, B.Bind (a, b, t) when st.E.si -> diff --git a/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml index 5c9d91a8b..4e5eb481f 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml @@ -15,18 +15,18 @@ module B = Brg let rec icm a = function | B.Sort _ | B.LRef _ - | B.GRef _ -> succ a - | B.Bind (_, B.Void, t) -> icm (succ a) t - | B.Cast (_, u, t) -> icm (icm a u) t + | B.GRef _ -> succ a + | B.Bind (_, B.Void, t) -> icm (succ a) t + | B.Cast (_, u, t) -> icm (icm a u) t | B.Appl (_, u, t) - | B.Bind (_, B.Abst u, t) - | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t + | B.Bind (_, B.Abst (_, u), t) + | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t let iter map d = let rec iter_bind d = function - | B.Void -> B.Void - | B.Abst w -> B.Abst (iter_term d w) - | B.Abbr v -> B.Abbr (iter_term d v) + | B.Void -> B.Void + | B.Abst (n, w) -> B.Abst (n, iter_term d w) + | B.Abbr v -> B.Abbr (iter_term d v) and iter_term d = function | B.Sort _ as t -> t | B.GRef _ as t -> t diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml index 5515e4404..2bead2d33 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml @@ -15,6 +15,7 @@ module S = Share module L = Log module H = Hierarchy module E = Entity +module N = Level module B = Brg module BE = BrgEnvironment module BS = BrgSubstitution @@ -55,11 +56,12 @@ let assert_convertibility err f st m u w v = let assert_applicability err f st m u w v = match BR.xwhd st m u with - | _, B.Sort _ -> error1 err "not a function type" m u - | mu, B.Bind (_, B.Abst u, _) -> + | _, B.Sort _ -> + error1 err "not a function type" m u + | mu, B.Bind (_, B.Abst (_, u), _) -> if BR.are_convertible st mu u m w then f () else error3 err m v w ~mu u - | _ -> assert false (**) + | _ -> assert false (**) let rec b_type_of err f st m x = log1 "Now checking" m x; @@ -68,7 +70,7 @@ let rec b_type_of err f st m x = let h = H.apply h in f x (B.Sort (a, h)) | B.LRef (_, i) -> begin match BR.get m i with - | B.Abst w -> + | B.Abst (_, w) -> f x (BS.lift (succ i) (0) w) | B.Abbr (B.Cast (_, w, _)) -> f x (BS.lift (succ i) (0) w) @@ -78,7 +80,7 @@ let rec b_type_of err f st m x = end | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abst w -> f x w + | _, _, E.Abst (_, w) -> f x w | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w | _, _, E.Abbr _ -> assert false | _, _, E.Void -> @@ -95,12 +97,12 @@ let rec b_type_of err f st m x = | _ -> f (B.Cast ([], vv, xv)) in type_of err f st m v - | B.Bind (a, B.Abst u, t) -> + | B.Bind (a, B.Abst (n, u), t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) + f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt) in let f xu m = b_type_of err (f xu) st m t in - let f xu _ = f xu (BR.push m a (B.abst xu)) in + let f xu _ = f xu (BR.push m a (B.abst n xu)) in type_of err f st m u | B.Bind (a, B.Void, t) -> let f xt tt = diff --git a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml index 160206198..27f471f9a 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml @@ -21,12 +21,12 @@ module BT = BrgType (* to share *) let type_check err f st = function - | a, uri, E.Abst t -> + | a, uri, E.Abst (n, t) -> let f xt tt = - let e = BE.set_entity (a, uri, E.Abst xt) in f tt e + let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e in L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t - | a, uri, E.Abbr t -> + | a, uri, E.Abbr t -> let f xt tt = let xt = match xt with | B.Cast _ -> xt @@ -35,4 +35,4 @@ let type_check err f st = function let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e in L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t - | _, _, E.Void -> assert false + | _, _, E.Void -> assert false diff --git a/helm/software/lambda-delta/src/common/Make b/helm/software/lambda-delta/src/common/Make index 09f15792b..5052ac0f3 100644 --- a/helm/software/lambda-delta/src/common/Make +++ b/helm/software/lambda-delta/src/common/Make @@ -1 +1 @@ -options hierarchy output entity marks alpha +options hierarchy output level entity marks alpha diff --git a/helm/software/lambda-delta/src/common/entity.ml b/helm/software/lambda-delta/src/common/entity.ml index 6da0b3aeb..f587a8d54 100644 --- a/helm/software/lambda-delta/src/common/entity.ml +++ b/helm/software/lambda-delta/src/common/entity.ml @@ -11,6 +11,7 @@ module U = NUri module G = Options +module N = Level type uri = U.uri @@ -28,9 +29,9 @@ type attr = Name of name (* name *) type attrs = attr list (* attributes *) -type 'term bind = Abst of 'term (* declaration: domain *) - | Abbr of 'term (* definition: body *) - | Void (* exclusion *) +type 'term bind = Abst of N.level * 'term (* declaration: level, domain *) + | Abbr of 'term (* definition: body *) + | Void (* exclusion *) type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) @@ -113,11 +114,11 @@ let rec rev_append_names ns = function | _ :: tl -> rev_append_names ns tl let xlate f xlate_term = function - | a, uri, Abst t -> - let f t = f (a, uri, Abst t) in xlate_term f t - | a, uri, Abbr t -> + | a, uri, Abst (n, t) -> + let f t = f (a, uri, Abst (n, t)) in xlate_term f t + | a, uri, Abbr t -> let f t = f (a, uri, Abbr t) in xlate_term f t - | _, _, Void -> + | _, _, Void -> assert false let initial_status () = { diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml index cc93d6dc3..d272bdea8 100644 --- a/helm/software/lambda-delta/src/complete_rg/crg.ml +++ b/helm/software/lambda-delta/src/complete_rg/crg.ml @@ -13,14 +13,15 @@ (* note : fragment of complete lambda-delta serving as abstract layer *) module E = Entity +module N = Level type uri = E.uri type id = E.id type attrs = E.attrs -type bind = Abst of term list (* domains *) - | Abbr of term list (* bodies *) - | Void of int (* number of exclusions *) +type bind = Abst of N.level * term list (* level, domains *) + | Abbr of term list (* bodies *) + | Void of int (* number of exclusions *) and term = TSort of attrs * int (* attrs, hierarchy index *) | TLRef of attrs * int * int (* attrs, position indexes *) @@ -49,20 +50,23 @@ let push_bind f lenv a b = f (EBind (lenv, a, b)) let push_proj f lenv a e = f (EProj (lenv, a, e)) let push2 err f lenv attr ?t () = match lenv, t with - | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws))) - | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs))) - | EBind (e, a, Void n), None -> f (EBind (e, (attr :: a), Void (succ n))) + | EBind (e, a, Abst (n, ws)), Some t -> + f (EBind (e, (attr :: a), Abst (n, t :: ws))) + | EBind (e, a, Abbr vs), Some t -> + f (EBind (e, (attr :: a), Abbr (t :: vs))) + | EBind (e, a, Void n), None -> + f (EBind (e, (attr :: a), Void (succ n))) | _ -> err () (* this id not tail recursive *) let resolve_lref err f id lenv = let rec aux f i k = function | ESort -> err () - | EBind (tl, _, Abst []) + | EBind (tl, _, Abst (_, [])) | EBind (tl, _, Abbr []) | EBind (tl, _, Void 0) -> aux f i k tl - | EBind (tl, a, _) -> - let err kk = aux f (succ i) (k + kk) tl in + | EBind (tl, a, b) -> + let err kk = aux f (succ i) (k + kk) tl in let f j = f i j (k + j) in E.resolve err f id a | EProj _ -> assert false (* TODO *) @@ -71,7 +75,7 @@ let resolve_lref err f id lenv = let rec get_name err f i j = function | ESort -> err i - | EBind (tl, _, Abst []) + | EBind (tl, _, Abst (_, [])) | EBind (tl, _, Abbr []) | EBind (tl, _, Void 0) -> get_name err f i j tl | EBind (_, a, _) when i = 0 -> @@ -86,7 +90,7 @@ let rec get_name err f i j = function let get_index err f i j lenv = let rec aux f i k = function | ESort -> err i - | EBind (tl, _, Abst []) + | EBind (tl, _, Abst (_, [])) | EBind (tl, _, Abbr []) | EBind (tl, _, Void 0) -> aux f i k tl | EBind (_, a, _) when i = 0 -> diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.ml b/helm/software/lambda-delta/src/complete_rg/crgAut.ml index 2221c3c06..388b0c2b9 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgAut.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgAut.ml @@ -14,6 +14,7 @@ module K = U.UriHash module C = Cps module G = Options module E = Entity +module N = Level module A = Aut module D = Crg @@ -43,15 +44,12 @@ let hcnt = K.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let empty_cnt = [], [] +let empty_cnt = [], [], [] -let add_abst (a, ws) id w = - E.Name (id, true) :: a, w :: ws +let add_abst (a, ws, ns) id w n = + E.Name (id, true) :: a, w :: ws, N.succ n :: ns -let lenv_of_cnt (a, ws) = - D.push_bind C.start D.empty_lenv a (D.Abst ws) - -let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) +let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -84,7 +82,7 @@ let relax_opt_qid f st = function | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_gref err f st qid = - try let cnt = K.find henv (uri_of_qid qid) in f qid cnt + try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt with Not_found -> err qid let resolve_gref_relaxed f st qid = @@ -93,7 +91,7 @@ let resolve_gref_relaxed f st qid = resolve_gref err f st qid let get_cnt err f st = function - | None -> f empty_cnt + | None -> f empty_cnt | Some qid as node -> try let cnt = K.find hcnt (uri_of_qid qid) in f cnt with Not_found -> err node @@ -103,21 +101,38 @@ let get_cnt_relaxed f st = let rec err node = relax_opt_qid (get_cnt err f st) st node in get_cnt err f st st.node +(****************************************************************************) + +let push_abst f (lenv, ns) a n w = + let bw = D.Abst (N.infinite, [w]) in + let f lenv = f (lenv, N.succ n :: ns) in + D.push_bind f lenv a bw + +let resolve_lref err f id (lenv, ns) = + let f i j k = f (List.nth ns k) i j k in + D.resolve_lref err f id lenv + +let lenv_of_cnt (a, ws, ns) = + D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns + (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function | A.Sort s -> - let f h = f (D.TSort ([], h)) in + let f h = f (N.finite 0) (D.TSort ([], h)) in if s then f 0 else f 1 | A.Appl (v, t) -> - let f vv tt = f (D.TAppl ([], [vv], tt)) in - let f vv = xlate_term (f vv) st lenv t in + let f vv n tt = f n (D.TAppl ([], [vv], tt)) in + let f _ vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> - let f ww = - let a, b = [E.Name (name, true)], (D.Abst [ww]) in - let f tt = f (D.TBind (a, b, tt)) in + let f nw ww = + let a = [E.Name (name, true)] in + let f nt tt = + let b = D.Abst (nt, [ww]) in + f nt (D.TBind (a, b, tt)) + in let f lenv = xlate_term f st lenv t in - D.push_bind f lenv a b + push_abst f lenv a nw ww in xlate_term f st lenv w | A.GRef (name, args) -> @@ -125,20 +140,22 @@ let rec xlate_term f st lenv = function | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) | _ -> C.err () in - let map2 f = xlate_term f st lenv in - let g qid (a, _) = + let map2 f t = + let f _ tt = f tt in xlate_term f st lenv t + in + let g n qid (a, _, _) = let gref = D.TGRef ([], uri_of_qid qid) in match args, a with - | [], [] -> f gref - | _ -> - let f args = f (D.TAppl ([], args, gref)) in - let f args = f (List.rev_map (map2 C.start) args) in + | [], [] -> f n gref + | _ -> + let f args = f n (D.TAppl ([], args, gref)) in + let f args = C.list_rev_map f map2 args in let f a = C.list_rev_map_append f map1 a ~tail:args in C.list_sub_strict f a args in let g qid = resolve_gref_relaxed g st qid in let err () = complete_qid g st name in - D.resolve_lref err (mk_lref f) (id_of_name name) lenv + resolve_lref err (mk_lref f) (id_of_name name) lenv let xlate_entity err f st = function | A.Section (Some (_, name)) -> @@ -158,53 +175,62 @@ let xlate_entity err f st = function let f qid = let f cnt = let lenv = lenv_of_cnt cnt in - let ww = xlate_term C.start st lenv w in - K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); - err {st with node = Some qid} + let f nw ww = + K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw); + err {st with node = Some qid} + in + xlate_term f st lenv w in get_cnt_relaxed f st in complete_qid f st (name, true, []) | A.Decl (name, w) -> let f cnt = - let a, ws = cnt in + let a, ws, _ = cnt in let lenv = lenv_of_cnt cnt in let f qid = - let ww = xlate_term C.start st lenv w in - K.add henv (uri_of_qid qid) cnt; - let t = match ws with - | [] -> ww - | _ -> D.TBind (a, D.Abst ws, ww) - in + let f nw ww = + K.add henv (uri_of_qid qid) (N.succ nw, cnt); + let t = match ws with + | [] -> ww + | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww) + in (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = E.Abst t in - let entity = [E.Mark st.line], uri_of_qid qid, b in - f {st with line = succ st.line} entity + let b = E.Abst (N.infinite, t) in + let entity = [E.Mark st.line], uri_of_qid qid, b in + f {st with line = succ st.line} entity + in + xlate_term f st lenv w in complete_qid f st (name, true, []) in get_cnt_relaxed f st | A.Def (name, w, trans, v) -> let f cnt = - let a, ws = cnt in + let a, ws, _ = cnt in let lenv = lenv_of_cnt cnt in let f qid = - let ww = xlate_term C.start st lenv w in - let vv = xlate_term C.start st lenv v in - K.add henv (uri_of_qid qid) cnt; - let t = match ws with - | [] -> D.TCast ([], ww, vv) - | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv)) - in + let f nw ww = + let f nv vv = + assert (nv = N.succ nw); (**) + K.add henv (uri_of_qid qid) (nv, cnt); + let t = match ws with + | [] -> D.TCast ([], ww, vv) + | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv)) + in (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = E.Abbr t in - let a = E.Mark st.line :: if trans then [] else [E.Priv] in - let entity = a, uri_of_qid qid, b in - f {st with line = succ st.line} entity + let b = E.Abbr t in + let a = E.Mark st.line :: if trans then [] else [E.Priv] in + let entity = a, uri_of_qid qid, b in + f {st with line = succ st.line} entity + in + xlate_term f st lenv v + in + xlate_term f st lenv w in complete_qid f st (name, true, []) in diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index efa39eec6..0b3964258 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -14,6 +14,7 @@ module U = NUri module C = Cps module H = Hierarchy module E = Entity +module N = Level module D = Crg (****************************************************************************) @@ -47,9 +48,11 @@ and pp_terms bg eg out vs = out bg; aux vs; out (eg ^ ".") and pp_bind out = function - | D.Abst x -> pp_terms "[:" "]" out x - | D.Abbr x -> pp_terms "[=" "]" out x - | D.Void x -> out (P.sprintf "[%u]" x) + | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x + | D.Abst (n, x) -> + pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x + | D.Abbr x -> pp_terms "[=" "]" out x + | D.Void x -> out (P.sprintf "[%u]" x) let rec pp_lenv out = function | D.ESort -> () diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml index 75aef2ae1..141b467bb 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml @@ -49,27 +49,27 @@ let resolve_gref err f st id = let rec xlate_term f st lenv = function | T.Inst _ - | T.Impl _ -> assert false - | T.Sort h -> + | T.Impl _ -> assert false + | T.Sort h -> f (D.TSort ([], h)) - | T.NSrt id -> + | T.NSrt id -> let f h = f (D.TSort ([], h)) in H.sort_of_string C.err f id - | T.LRef (i, j) -> + | T.LRef (i, j) -> D.get_index C.err (mk_lref f i j) i j lenv - | T.NRef id -> + | T.NRef id -> let err () = resolve_gref C.err (mk_gref f) st id in D.resolve_lref err (mk_lref f) id lenv - | T.Cast (u, t) -> + | T.Cast (u, t) -> let f uu tt = f (D.TCast ([], uu, tt)) in let f uu = xlate_term (f uu) st lenv t in xlate_term f st lenv u - | T.Appl (vs, t) -> + | T.Appl (vs, t) -> let map f = xlate_term f st lenv in let f vvs tt = f (D.TAppl ([], vvs, tt)) in let f vvs = xlate_term (f vvs) st lenv t in C.list_map f map vs - | T.Bind (b, t) -> + | 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 @@ -86,9 +86,9 @@ let rec xlate_term f st lenv = function in let lenv, aa, bb = match b with | T.Abst xws -> - let lenv = D.push_bind C.start lenv [] (D.Abst []) in + 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 wws + 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 @@ -104,9 +104,10 @@ let rec xlate_term f st lenv = function let xlate_term f st lenv t = TT.contract (xlate_term f st lenv) t -let mk_contents tt = function - | T.Decl -> [], E.Abst tt - | T.Ax -> [], E.Abst tt +let mk_contents n tt = function + | T.Decl -> [], E.Abst (n, tt) + | T.Ax -> [], E.Abst (n, tt) + | T.Cong -> [], E.Abst (n, tt) | T.Def -> [], E.Abbr tt | T.Th -> [], E.Abbr tt @@ -130,20 +131,20 @@ let xlate_entity err f gen st = function {st with sort = H.set_sorts ix [s]} in err (List.fold_left map st sorts) - | T.Graph id -> + | T.Graph id -> assert (H.set_graph id); err st - | T.Entity (kind, id, meta, t) -> + | T.Entity (kind, n, id, meta, 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 (* print_newline (); CrgOutput.pp_term print_string tt; *) - let a, b = mk_contents tt kind in + let a, b = mk_contents n tt kind in let a = if meta <> "" then E.Meta meta :: a else a in let entity = E.Mark st.line :: a, uri, b in f {st with line = succ st.line} entity - | T.Generate _ -> + | T.Generate _ -> err st (* Interface functions ******************************************************) diff --git a/helm/software/lambda-delta/src/modules.ml b/helm/software/lambda-delta/src/modules.ml index 7fad8b893..51b98a29d 100644 --- a/helm/software/lambda-delta/src/modules.ml +++ b/helm/software/lambda-delta/src/modules.ml @@ -1,4 +1,4 @@ -(* free = F I N P Q U V W *) +(* free = F I P Q U V W *) module U = NUri module K = NUri.UriHash @@ -14,6 +14,7 @@ module O = output module E = entity module J = marks (**) module R = alpha +module N = level module T = txt module TP = txtParser diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml index a2140585a..6ffe592de 100644 --- a/helm/software/lambda-delta/src/text/txt.ml +++ b/helm/software/lambda-delta/src/text/txt.ml @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module N = Level + type ix = int (* index *) type id = string (* identifier *) @@ -17,26 +19,48 @@ type desc = string (* description *) type kind = Decl (* generic declaration *) | Ax (* axiom *) + | Cong (* conjecture *) | Def (* generic definition *) | Th (* theorem *) -type bind = Abst of (id * bool * term) list (* name, real?, domain *) - | Abbr of (id * term) list (* name, bodies *) - | Void of id list (* names *) - -and term = Sort of ix (* level *) - | NSrt of id (* named level *) - | LRef of ix * ix (* index, offset *) - | NRef of id (* name *) - | Cast of term * term (* domain, element *) - | Appl of term list * term (* arguments, function *) - | Bind of bind * term (* binder, scope *) - | Inst of term * term list (* function, arguments *) - | Impl of bool * id * term * term (* strong?, label, source, target *) - -type command = Require of id list (* required files: names *) - | Graph of id (* hierarchy graph: name *) - | Sorts of (int option * id) list (* sorts: index, name *) - | Section of id option (* section: Some id = open, None = close last *) - | Entity of kind * id * desc * term (* entity: class, name, description, contents *) - | Generate of term list (* predefined generated entity: arguments *) +type bind = +(* name, real?, domain *) + | Abst of (id * bool * term) list +(* name, bodies *) + | Abbr of (id * term) list +(* names *) + | Void of id list + +and term = +(* level *) + | Sort of ix +(* named level *) + | NSrt of id +(* index, offset *) + | LRef of ix * ix +(* name *) + | NRef of id +(* domain, element *) + | Cast of term * term +(* arguments, function *) + | Appl of term list * term +(* level, binder, scope *) + | Bind of N.level * bind * term +(* function, arguments *) + | Inst of term * term list +(* level, strong?, label, source, target *) + | Impl of N.level * bool * id * term * term + +type command = +(* required files: names *) + | Require of id list +(* hierarchy graph: name *) + | Graph of id +(* sorts: index, name *) + | Sorts of (int option * id) list +(* section: Some id = open, None = close last *) + | Section of id option +(* entity: class, name, description, contents *) + | Entity of kind * N.level * id * desc * term +(* predefined generated entity: arguments *) + | Generate of term list diff --git a/helm/software/lambda-delta/src/text/txtLexer.mll b/helm/software/lambda-delta/src/text/txtLexer.mll index e5ced3806..efee66051 100644 --- a/helm/software/lambda-delta/src/text/txtLexer.mll +++ b/helm/software/lambda-delta/src/text/txtLexer.mll @@ -46,6 +46,7 @@ and token = parse | "\\graph" { out "GRAPH"; TP.GRAPH } | "\\decl" { out "DECL"; TP.DECL } | "\\ax" { out "AX"; TP.AX } + | "\\cong" { out "CONG"; TP.CONG } | "\\def" { out "DEF"; TP.DEF } | "\\th" { out "TH"; TP.TH } | "\\generate" { out "GEN"; TP.GEN } @@ -69,4 +70,5 @@ and token = parse | "~" { 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/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly index 415b594ca..1eae31980 100644 --- a/helm/software/lambda-delta/src/text/txtParser.mly +++ b/helm/software/lambda-delta/src/text/txtParser.mly @@ -25,14 +25,15 @@ %{ module G = Options + module N = Level 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 - %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF + %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT + %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF %start entry %type entry @@ -64,6 +65,10 @@ | sort { [$1] } | sort CM sorts { $1 :: $3 } ; + level: + | { N.infinite } + | CT IX { N.finite $2} + ; abst: | ID CN term { $1, true, $3 } @@ -97,16 +102,16 @@ | 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 fs term { T.Bind ($2, $5) } - | term WTO term { T.Impl (false, "", $1, $3) } - | ID TE term WTO term { T.Impl (false, $1, $3, $5) } - | term STO term { T.Impl (true, "", $1, $3) } - | ID TE term STO term { T.Impl (true, $1, $3, $5) } - | OP term CP { $2 } + | 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 } ; terms: | term CM term { [$1; $3] } @@ -116,6 +121,7 @@ decl: | DECL { T.Decl } | AX { T.Ax } + | CONG { T.Cong } ; def: | DEF { T.Def } @@ -123,25 +129,25 @@ ; xentity: | GRAPH ID - { T.Graph $2 } - | decl comment ID CN term - { T.Entity ($1, $3, $2, $5) } - | def comment ID EQ term - { T.Entity ($1, $3, $2, $5) } - | def comment ID EQ term CN term - { T.Entity ($1, $3, $2, T.Cast ($7, $5)) } + { T.Graph $2 } + | decl level comment ID CN term + { T.Entity ($1, $2, $4, $3, $6) } + | def level comment ID EQ term + { T.Entity ($1, $2, $4, $3, $6) } + | def level comment ID EQ term CN term + { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) } | GEN term - { T.Generate [$2] } + { T.Generate [$2] } | 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 {} | diff --git a/helm/software/lambda-delta/src/text/txtTxt.ml b/helm/software/lambda-delta/src/text/txtTxt.ml index 1d501fe0d..d2c85cb92 100644 --- a/helm/software/lambda-delta/src/text/txtTxt.ml +++ b/helm/software/lambda-delta/src/text/txtTxt.ml @@ -18,16 +18,16 @@ let rec contract f = function | T.Inst (t, vs) -> let tt = T.Appl (List.rev vs, t) in contract f tt - | T.Impl (false, id, w, t) -> - let tt = T.Bind (T.Abst [id, false, w], t) in + | T.Impl (n, false, id, w, t) -> + let tt = T.Bind (n, T.Abst [id, false, w], t) in contract f tt - | T.Impl (true, id, w, t) -> + | T.Impl (n, true, id, w, t) -> let f = function - | T.Bind (T.Abst [xw], T.Bind (T.Abst xws, tt)) -> - f (T.Bind (T.Abst (xw :: xws), tt)) + | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) -> + f (T.Bind (n, T.Abst (xw :: xws), tt)) | tt -> f tt in - let tt = T.Impl (false, id, w, t) in + let tt = T.Impl (n, false, id, w, t) in contract f tt | T.Sort _ | T.NSrt _ @@ -41,8 +41,8 @@ let rec contract f = function let f tt vvs = f (T.Appl (vvs, tt)) in let f tt = C.list_map (f tt) contract vs in contract f t - | T.Bind (b, t) -> - let f tt bb = f (T.Bind (bb, tt)) in + | 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 diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml index 6a45518b5..be6345007 100644 --- a/helm/software/lambda-delta/src/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/src/toplevel/metaAut.ml @@ -14,6 +14,7 @@ module K = U.UriHash module C = Cps module G = Options module E = Entity +module N = Level module M = Meta module A = Aut @@ -179,7 +180,7 @@ let xlate_entity err f st = function K.add henv (uri_of_qid qid) pars; let a = [E.Mark st.line] in let entry = pars, ww, None in - let entity = a, uri_of_qid qid, E.Abst entry in + let entity = a, uri_of_qid qid, E.Abst (N.infinite, entry) in f {st with line = succ st.line} entity in xlate_term f st pars w diff --git a/helm/software/lambda-delta/src/toplevel/metaBrg.ml b/helm/software/lambda-delta/src/toplevel/metaBrg.ml index 72298dd13..f1497697c 100644 --- a/helm/software/lambda-delta/src/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/src/toplevel/metaBrg.ml @@ -11,6 +11,7 @@ module C = Cps module E = Entity +module N = Level module B = Brg module M = Meta @@ -33,15 +34,15 @@ let rec xlate_term c f = function | M.Abst (id, w, t) -> let f w = let a = [E.Name (id, true)] in - let f t = f (B.Bind (a, B.Abst w, t)) in - xlate_term (B.push c B.empty a (B.Abst w)) f t + let f t = f (B.Bind (a, B.Abst (N.infinite, w), t)) in + xlate_term (B.push c B.empty a (B.Abst (N.infinite, w))) f t in xlate_term c f w let xlate_pars f pars = let map f (id, w) c = let a = [E.Name (id, true)] in - let f w = f (B.push c B.empty a (B.Abst w)) in + let f w = f (B.push c B.empty a (B.Abst (N.infinite, w))) in xlate_term c f w in C.list_fold_right f map pars B.empty diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml index 2d9246f5d..0f25e13e5 100644 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/src/toplevel/metaOutput.ml @@ -69,21 +69,21 @@ let count_xterm f c = function | Some v -> count_term f c v let count_entity f c = function - | _, u, E.Abst (pars, w, xv) -> + | _, u, E.Abst (_, (pars, w, xv)) -> let c = {c with eabsts = succ c.eabsts} in let c = {c with pabsts = c.pabsts + List.length pars} in let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in let f c = count_xterm f c xv in let f c = count_term f c w in Cps.list_fold_left f count_par c pars - | _, _, E.Abbr (pars, w, xv) -> + | _, _, E.Abbr (pars, w, xv) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in let c = {c with pabsts = c.pabsts + List.length pars} in let c = {c with nodes = c.nodes + List.length pars} in let f c = count_xterm f c xv in let f c = count_term f c w in Cps.list_fold_left f count_par c pars - | _, _, E.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 40a58673a..95ff41df3 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -249,9 +249,10 @@ let process_0 st entity = if !preprocess then process_input f st entity else f st entity let process_nostreaming st lexbuf input = + let id x = x in let rec aux1 book = match entity_of_input lexbuf input with | NoEntity -> List.rev book - | e -> aux1 (e :: book) + | e -> aux1 (id e :: book) in let rec aux2 st = function | [] -> st @@ -259,9 +260,12 @@ let process_nostreaming st lexbuf input = in aux2 st (aux1 []) -let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with - | NoEntity -> st - | e -> process_streaming (process_0 st e) lexbuf input +let process_streaming st lexbuf input = + let rec aux st = match entity_of_input lexbuf input with + | NoEntity -> st + | e -> aux (process_0 st e) + in + aux st (****************************************************************************) @@ -275,7 +279,7 @@ let process st name = let main = try - let version_string = "Helena 0.8.1 M - August 2010" in + let version_string = "Helena 0.8.1 M - October 2010" in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml index a0b5a7f1a..7b5dd8ddc 100644 --- a/helm/software/lambda-delta/src/xml/xmlCrg.ml +++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml @@ -90,15 +90,15 @@ and exp_bind e a b out tab = let f a ns = a, ns in let a, ns = Y.get_names f a in match b with - | D.Abst ws -> - let e = D.push_bind C.start e a (D.Abst []) in - let attrs = [XL.name ns; XL.mark a; XL.arity (List.length ws)] in + | D.Abst (n, ws) -> + let e = D.push_bind C.start e a (D.Abst (n, ws)) in + let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity (List.length ws)] in XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab - | D.Abbr vs -> - let e = D.push_bind C.start e a (D.Abbr []) in + | D.Abbr vs -> + let e = D.push_bind C.start e a (D.Abbr vs) in let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab - | D.Void n -> + | D.Void n -> let attrs = [XL.name a; XL.mark a; XL.arity n] in XL.tag XL.void attrs out tab diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml index a9b1e5a1c..af6245c9f 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -14,6 +14,7 @@ module U = NUri module C = Cps module H = Hierarchy module E = Entity +module N = Level (* internal functions *******************************************************) @@ -106,6 +107,9 @@ let mark a = let f i = "mark", string_of_int i in E.mark err f a +let level n = + "level", N.to_string n + (* TODO: the string s must be quoted *) let meta a = let err () = "meta", "" in @@ -121,9 +125,9 @@ let export_entity pp_term si xdir (a, u, b) = let a = E.Name (U.name_of_uri u, true) :: a in let attrs = [uri u; name a; mark a; meta a] in let contents = match b with - | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w) - | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) - | E.Void -> assert false + | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w) + | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) + | E.Void -> assert false in let opts = if si then "si" else "" in let shp = H.string_of_graph () in diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.mli b/helm/software/lambda-delta/src/xml/xmlLibrary.mli index ed3f7bb8f..28f056f06 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.mli +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.mli @@ -46,6 +46,8 @@ val uri: Entity.uri -> attr val arity: int -> attr +val level: Level.level -> attr + val name: Entity.attrs -> attr val mark: Entity.attrs -> attr