From: Ferruccio Guidi Date: Tue, 16 Jun 2015 12:09:21 +0000 (+0000) Subject: new syntax of abstractions propagated to complete_rg X-Git-Tag: make_still_working~720 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1be981691870cca039b1af1fb954491c2020d483;p=helm.git new syntax of abstractions propagated to complete_rg --- diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index a92b6fea9..c17b83f07 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -47,7 +47,7 @@ let alpha id = let add_abst cnt id aw w = let id = if !G.alpha <> "" then alpha id else id in let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in - D.EBind (cnt, aw, D.Abst (N.two, w)) + D.EBind (cnt, aw, D.Abst (false, N.two, w)) let mk_lref f a i = f a (D.TLRef (a, i)) @@ -103,7 +103,7 @@ let get_cnt_relaxed f lst = get_cnt err f lst lst.node let push_abst f a w lenv = - let bw = D.Abst (N.infinite, w) in + let bw = D.Abst (false, N.infinite, w) in D.push_bind f a bw lenv let add_proj e t = match e with @@ -135,7 +135,7 @@ let rec xlate_term f st lst y lenv = function | _ -> assert false else N.infinite in - let b = D.Abst (l, ww) in + let b = D.Abst (false, l, ww) in let at = {at with E.n_name = name} in f at (D.TBind (at, b, tt)) in diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index 6a83282b3..08f342496 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -34,8 +34,8 @@ let rec xlate_term st f c = function | D.TProj (_, e, t) -> D.shift (xlate_term st f c) e t (* this case should be removed by improving alpha-conversion *) - | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> - xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t))) + | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) -> + xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t))) | D.TBind (a, b, t) -> let f cc = let a, l, b = List.hd cc in @@ -45,13 +45,13 @@ let rec xlate_term st f c = function xlate_bind st f c a b and xlate_bind st f c a = function - | D.Abst (_, w) -> + | D.Abst (_, _, w) -> let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in xlate_term st f c w - | D.Abbr v -> + | D.Abbr v -> let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in xlate_term st f c v - | D.Void -> + | D.Void -> Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void (* internal functions: bag to crg term **************************************) @@ -78,7 +78,7 @@ let rec xlate_bk_term f c = function and xlate_bk_bind f c = function | Z.Abst t -> - let f tt = f (D.Abst (N.infinite, tt)) in + let f tt = f (D.Abst (false, N.infinite, tt)) in xlate_bk_term f c t | Z.Abbr t -> let f tt = f (D.Abbr tt) in diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index 98d9fc26f..7be7dc939 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -74,7 +74,7 @@ let get e i = get i e (* used in BrgOutput.pp_lenv *) let rec fold_right f map e x = match e with | Null -> f x - | Cons (e, c, a, b) -> fold_right (map f e c a b) map e x + | Cons (e, c, a, b) -> fold_right (map f c a b) map e x let rec mem err f e b = match e with | Null -> err () diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index dd7f3b1e5..1715494d4 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -34,15 +34,15 @@ let rec xlate_term f = function | D.TBind (a, b, t) -> xlate_term (xlate_bind f a b) t -and xlate_bind f a b x = match b with - | D.Abst (n, w) -> - let f ww = f (B.Bind (a, B.Abst (false, n, ww), x)) in +and xlate_bind f a b t = match b with + | D.Abst (x, n, w) -> + let f ww = f (B.Bind (a, B.Abst (x, n, ww), t)) in xlate_term f w - | D.Abbr v -> - let f vv = f (B.Bind (a, B.Abbr vv, x)) in + | D.Abbr v -> + let f vv = f (B.Bind (a, B.Abbr vv, t)) in xlate_term f v - | D.Void -> - f (B.Bind (a, B.Void, x)) + | D.Void -> + f (B.Bind (a, B.Void, t)) (* internal functions: brg to crg term **************************************) @@ -64,8 +64,8 @@ let rec xlate_bk_term f = function xlate_bk_term f t and xlate_bk_bind f = function - | B.Abst (_, n, t) -> - let f tt = f (D.Abst (n, tt)) in + | B.Abst (x, n, t) -> + let f tt = f (D.Abst (x, n, tt)) in xlate_bk_term f t | B.Abbr t -> let f tt = f (D.Abbr tt) in diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index b5b60e8fd..ac873ec66 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -171,19 +171,18 @@ let rec pp_term st e och = function 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 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 KP.fprintf och "%s\n" "not shown" else + let pp_entry f c a b x = + let a = R.alpha B.mem e a in + let x = B.push x c a b in + match b with + | B.Abst (_, _, w) -> + KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x + | B.Abbr v -> + KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x + | B.Void -> + KP.fprintf och "[%a]" (name C.start) a; f x + in + if e = B.empty then KP.fprintf och "%s" "empty" 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 774b016a1..bb31fc976 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -93,7 +93,7 @@ let get m i = (* to share *) let rec step st m r = if !G.trace >= sublevel then - log1 st (Printf.sprintf "entering R.step: l:%u n:%s" m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r; + log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r; match r with | B.Sort (a, h) -> if assert_tstep m false then diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 013287243..d84012c2f 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -43,13 +43,11 @@ let add ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) () = -(* if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta); if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta); if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta); if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt); - if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); -*) + if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 455eb6ed4..ae1a81222 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -20,22 +20,22 @@ type uri = E.uri type id = E.id type attrs = E.node_attrs -type bind = Abst of N.layer * term (* layer, type *) - | Abbr of term (* body *) - | Void (* *) - -and term = TSort of attrs * int (* attrs, hierarchy index *) - | TLRef of attrs * int (* attrs, position indexe *) - | TGRef of attrs * uri (* attrs, reference *) - | TCast of attrs * term * term (* attrs, domain, element *) - | TAppl of attrs * term * term (* attrs, argument, function *) - | TBind of attrs * bind * term (* attrs, binder, scope *) - | TProj of attrs * lenv * term (* attrs, closure, member *) - -and lenv = ESort (* top *) - | EBind of lenv * attrs * bind (* environment, attrs, binder *) - | EAppl of lenv * attrs * term (* environment, attrs, argument *) - | EProj of lenv * attrs * lenv (* environment, attrs, closure *) +type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *) + | Abbr of term (* body *) + | Void (* *) + +and term = TSort of attrs * int (* attrs, hierarchy index *) + | TLRef of attrs * int (* attrs, position indexe *) + | TGRef of attrs * uri (* attrs, reference *) + | TCast of attrs * term * term (* attrs, domain, element *) + | TAppl of attrs * term * term (* attrs, argument, function *) + | TBind of attrs * bind * term (* attrs, binder, scope *) + | TProj of attrs * lenv * term (* attrs, closure, member *) + +and lenv = ESort (* top *) + | EBind of lenv * attrs * bind (* environment, attrs, binder *) + | EAppl of lenv * attrs * term (* environment, attrs, argument *) + | EProj of lenv * attrs * lenv (* environment, attrs, closure *) type entity = term E.entity @@ -117,11 +117,11 @@ let rec mem err f e b = match e with let replace f n0 e = let rec aux f = function - | ESort -> f ESort - | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e - | EBind (e, a, b) -> aux (push_bind f a b) e - | EAppl (e, a, v) -> aux (push_appl f a v) e - | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d + | ESort -> f ESort + | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e + | EBind (e, a, b) -> aux (push_bind f a b) e + | EAppl (e, a, v) -> aux (push_appl f a v) e + | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d in aux f e diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 7c9ab8172..dc5d78ce1 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -79,15 +79,15 @@ let rec count_term f c e = function count_binder f c e a b and count_binder f c e a b = match b with - | D.Abst (_, w) -> + | D.Abst (_, _, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in let f c = D.push_bind (f c) a b e in count_term f c e w - | D.Abbr v -> + | D.Abbr v -> let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in let f c = D.push_bind (f c) a b e in count_term f c e v - | D.Void -> + | D.Void -> let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in D.push_bind (f c) a b e @@ -134,23 +134,25 @@ let pp_attrs out a = E.name ignore f a; out (KP.sprintf "+%i;" a.E.n_apix) +let pp_state out x = if x then out "^" + let rec pp_term out st = function | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l) | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i) | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$") - | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y - | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y - | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y - | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y + | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t + | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t + | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t + | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t and pp_bind out st = function - | D.Abst (n, x) -> - 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 "[] " + | D.Abst (x, n, u) -> + out "[:"; pp_term out st u; out "]"; pp_state out x; out (N.to_string st n); out " " + | D.Abbr u -> out "[="; pp_term out st u; 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.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t + | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") " + | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} " diff --git a/helm/software/helena/src/lib/log.ml b/helm/software/helena/src/lib/log.ml index e248eddf4..42f7f214b 100644 --- a/helm/software/helena/src/lib/log.ml +++ b/helm/software/helena/src/lib/log.ml @@ -36,7 +36,7 @@ let pp_items och a st l items = let indent = KT.make (l+l) ' ' in let pp_item och = function | 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 + | LEnv c -> KP.fprintf och "%s%a\n" 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 diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 8a4b70b79..974145812 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -104,7 +104,7 @@ and xlate_bind st f (lenv, e) b = | 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)) + f a (D.Abst (false, n, ww)) in xlate_term f st lenv w | T.Abbr (id, v) -> diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 535682143..f04930851 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -80,13 +80,13 @@ and exp_appl st e a v out tab = XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab; and exp_bind st e a b out tab = match b with - | D.Abst (n, w) -> + | D.Abst (_, n, w) -> let attrs = [XL.layer st n; XL.name a; XL.kind a] in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab - | D.Abbr v -> + | D.Abbr v -> let attrs = [XL.name a] in XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab - | D.Void -> + | D.Void -> let attrs = [XL.name a] in XL.tag XL.void attrs out tab