From: Ferruccio Guidi Date: Tue, 16 Jun 2009 14:20:34 +0000 (+0000) Subject: we corrected some reduction bugs about renaming. X-Git-Tag: make_still_working~3865 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13c3708fc59d999727ee214e8ece1f03661a9737;p=helm.git we corrected some reduction bugs about renaming. The grundlagen is now fully typechecked :) --- diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 3bda05f9e..26a2d7b16 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -67,17 +67,17 @@ let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in L.warn (P.sprintf " Automath representation summary"); - L.warn (P.sprintf " Total book items: %6u" items); - L.warn (P.sprintf " Section items: %6u" c.sections); - L.warn (P.sprintf " Context items: %6u" c.contexts); - L.warn (P.sprintf " Block items: %6u" c.blocks); - L.warn (P.sprintf " Declaration items: %6u" c.decls); - L.warn (P.sprintf " Definition items: %6u" c.defs); - L.warn (P.sprintf " Total Parameter items: %6u" c.pars); - L.warn (P.sprintf " Application items: %6u" c.pars); - L.warn (P.sprintf " Total term items: %6u" terms); - L.warn (P.sprintf " Sort items: %6u" c.sorts); - L.warn (P.sprintf " Reference items: %6u" c.grefs); - L.warn (P.sprintf " Application items: %6u" c.appls); - L.warn (P.sprintf " Abstraction items: %6u" c.absts); + L.warn (P.sprintf " Total book items: %7u" items); + L.warn (P.sprintf " Section items: %7u" c.sections); + L.warn (P.sprintf " Context items: %7u" c.contexts); + L.warn (P.sprintf " Block items: %7u" c.blocks); + L.warn (P.sprintf " Declaration items: %7u" c.decls); + L.warn (P.sprintf " Definition items: %7u" c.defs); + L.warn (P.sprintf " Total Parameter items: %7u" c.pars); + L.warn (P.sprintf " Application items: %7u" c.pars); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.sorts); + L.warn (P.sprintf " Reference items: %7u" c.grefs); + L.warn (P.sprintf " Application items: %7u" c.appls); + L.warn (P.sprintf " Abstraction items: %7u" c.absts); f () diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 0ca314015..624b47cbb 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -61,7 +61,13 @@ let locations () = !location let empty_context = [] -let push f es l id b = +let push msg f es l id b = + let rec does_not_occur loc = function + | [] -> true + | (l, _, _) :: _ when l = loc -> false + | _ :: es -> does_not_occur l es + in + if not (does_not_occur l es) then failwith msg else let c = (l, id, b) :: es in f c let append f es1 es2 = diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 4e7ab87a0..3eb96a2d5 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -86,18 +86,18 @@ let print_counters f c = let items = c.eabsts + c.eabbrs in let locations = B.locations () in L.warn (P.sprintf " Kernel representation summary (basic_ag)"); - L.warn (P.sprintf " Total entry items: %6u" items); - L.warn (P.sprintf " Declaration items: %6u" c.eabsts); - L.warn (P.sprintf " Definition items: %6u" c.eabbrs); - L.warn (P.sprintf " Total term items: %6u" terms); - L.warn (P.sprintf " Sort items: %6u" c.tsorts); - L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts); - L.warn (P.sprintf " Application items: %6u" c.tappls); - L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs); - L.warn (P.sprintf " Total binder locations: %6u" locations); + L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.tsorts); + L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn (P.sprintf " Application items: %7u" c.tappls); + L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn (P.sprintf " Total binder locations: %7u" locations); f () let indexes = ref false @@ -127,15 +127,15 @@ let rec pp_term c frm = function let f cc = F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t in - B.push f c l id (B.Abst w) + B.push "output abst" f c l id (B.Abst w) | B.Bind (l, id, B.Abbr v, t) -> let f cc = F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t in - B.push f c l id (B.Abbr v) + B.push "output abbr" f c l id (B.Abbr v) | B.Bind (l, id, B.Void, t) -> let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in - B.push f c l id B.Void + B.push "output void" f c l id B.Void let pp_context frm c = let pp_entry frm = function diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index edd1eeaf7..518f7061b 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -77,13 +77,15 @@ let get f c m i = let f c = B.get f c i in B.append f c m.c -let push f c m l id w = +let push msg f c m l id w = assert (m.s = []); - let f w = B.push f c l id (B.Abst w) in + let f w = B.push msg f c l id (B.Abst w) in unwind_to_term f m w (* to share *) -let rec whd f c m x = match x with +let rec whd f c m x = +(* L.warn "entering R.whd"; *) + match x with | B.Sort h -> f m (Sort_ h) | B.GRef uri -> let f obj = f m (GRef_ obj) in @@ -101,18 +103,21 @@ let rec whd f c m x = match x with begin match m.s with | [] -> f m (Bind_ (l, id, w, t)) | v :: tl -> - let f mc = whd f c {m with c = mc; s = tl} t in - B.push f m.c l id (B.Abbr (B.Cast (w, v))) + let nl = B.new_location () in + let f mc = S.subst (whd f c {m with c = mc; s = tl}) nl l t in + B.push "!" f m.c nl id (B.Abbr (B.Cast (w, v))) end | B.Bind (l, id, b, t) -> - let f mc = whd f c {m with c = mc} t in - B.push f m.c l id b + let nl = B.new_location () in + let f mc = S.subst (whd f c {m with c = mc}) nl l t in + B.push "!" f m.c nl id b (* Interface functions ******************************************************) let nsi = ref false 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, _) -> @@ -131,7 +136,9 @@ let ho_whd f c t = ho_whd f c empty_machine t let rec are_convertible f a c m1 t1 m2 t2 = +(* L.warn "entering R.are_convertible"; *) let rec aux m1 r1 m2 r2 = +(* L.warn "entering R.are_convertible_aux"; *) let u, t = term_of_whdr r1, term_of_whdr r2 in log2 "Now really converting" c u t; match r1, r2 with @@ -153,32 +160,35 @@ let rec are_convertible f a c m1 t1 m2 t2 = | GRef_ (_, _, B.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) -> + let l = B.new_location () in let h c = let m1, m2 = inc m1, inc m2 in - S.subst (are_convertible f a c m1 t1 m2) l1 l2 t2 + let f t1 = S.subst (are_convertible f a c m1 t1 m2) l l2 t2 in + S.subst f l l1 t1 in - let f r = if r then push h c m1 l1 id1 w1 else f false in + let f r = if r then push "!" h c m1 l id1 w1 else f false in are_convertible f a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) | Sort_ _, Bind_ (l2, id2, w2, t2) when !nsi -> let m1, m2 = inc m1, inc m2 in let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in - push f c m2 l2 id2 w2 + push "nsi" f c m2 l2 id2 w2 | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in let g m1 r1 = whd (aux m1 r1) c m2 t2 in if a = false then f false else whd g c m1 t1 and are_convertible_stacks f a c m1 m2 = +(* L.warn "entering R.are_convertible_stacks"; *) let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in let map f a v1 v2 = are_convertible f a c mm1 v1 mm2 v2 in if List.length m1.s <> List.length m2.s then begin - L.warn (Printf.sprintf "Different lengths: %u %u" - (List.length m1.s) (List.length m2.s) - ); +(* L.warn (Printf.sprintf "Different lengths: %u %u" + (List.length m1.s) (List.length m2.s) + ); *) f false - end + end else C.list_fold_left2 f map a m1.s m2.s diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 0520883d5..9cf5c5cb7 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -46,6 +46,7 @@ let mk_gref u l = (* Interface functions ******************************************************) let rec b_type_of f g c x = +(* L.warn "Entering T.b_type_of"; *) log1 "Now checking" c x; match x with | B.Sort h -> @@ -75,7 +76,7 @@ let rec b_type_of f g c x = f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) in let f xv cc = b_type_of (f xv) g cc t in - let f xv = B.push (f xv) c l id (B.Abbr xv) in + let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast (vv, xv)) @@ -86,14 +87,14 @@ let rec b_type_of f g c x = f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt) in let f xu cc = b_type_of (f xu) g cc t in - let f xu _ = B.push (f xu) c l id (B.Abst xu) in + let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in type_of f g c u | B.Bind (l, id, B.Void, t) -> let f xt tt = f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) in let f cc = b_type_of f g cc t in - B.push f c l id B.Void + B.push "type void" f c l id B.Void | B.Appl (v, t) -> let f xv vv xt tt = function | R.Abst w -> @@ -101,9 +102,7 @@ let rec b_type_of f g c x = L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); L.unbox (succ level); let f a = - L.box (succ level); - L.warn (Printf.sprintf "Convertible: %b" a); - L.unbox (succ level); +(* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else error3 c xv vv w in @@ -116,9 +115,7 @@ let rec b_type_of f g c x = type_of f g c v | B.Cast (u, t) -> let f xu xt tt a = - L.box (succ level); - L.warn (Printf.sprintf "Convertible: %b" a); - L.unbox (succ level); + (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu in let f xu xt tt = R.are_convertible (f xu xt tt) c xu tt in diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml index cf2c009f4..4f909bdca 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.ml +++ b/helm/software/lambda-delta/toplevel/metaBag.ml @@ -35,14 +35,14 @@ let rec xlate_term c f = function let l = B.new_location () in let f t = f (B.Bind (l, id, B.Abst w, t)) in let f c = xlate_term c f t in - B.push f c l id (B.Abst w) + B.push "meta" f c l id (B.Abst w) in xlate_term c f w let xlate_pars f pars = let map f (id, w) c = let l = B.new_location () in - let f w = B.push f c l id (B.Abst w) in + let f w = B.push "meta" f c l id (B.Abst w) in xlate_term c f w in C.list_fold_right f map pars B.empty_context diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 03995e153..5fe20f0f4 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -74,18 +74,18 @@ let print_counters f c = let pars = c.pabsts + c.pappls in let items = c.eabsts + c.eabbrs in L.warn (P.sprintf " Intermediate representation summary"); - L.warn (P.sprintf " Total entry items: %6u" items); - L.warn (P.sprintf " Declaration items: %6u" c.eabsts); - L.warn (P.sprintf " Definition items: %6u" c.eabbrs); - L.warn (P.sprintf " Total parameter items: %6u" pars); - L.warn (P.sprintf " Application items: %6u" c.pappls); - L.warn (P.sprintf " Abstraction items: %6u" c.pabsts); - L.warn (P.sprintf " Total term items: %6u" terms); - L.warn (P.sprintf " Sort items: %6u" c.tsorts); - L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); - L.warn (P.sprintf " Application items: %6u" c.tappls); - L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); + L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn (P.sprintf " Total parameter items: %7u" pars); + L.warn (P.sprintf " Application items: %7u" c.pappls); + L.warn (P.sprintf " Abstraction items: %7u" c.pabsts); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.tsorts); + L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn (P.sprintf " Application items: %7u" c.tappls); + L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); f () let string_of_sort = function diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 70234ba13..de064c2d6 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -87,7 +87,8 @@ try let f st _ = function | None -> st | Some (i, u, _) -> - Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st +(* Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); *) + st in (* stage 2 *) let f st item = @@ -95,7 +96,7 @@ try if !stage > 2 then BagU.type_check (f st) !H.graph item else st in (* stage 1 *) - let f mst item = + let f st mst item = let st = {st with mst = mst; mc = count MO.count_item st.mc item } in @@ -108,7 +109,7 @@ try (* stage 0 *) let st = {st with ac = count AO.count_item st.ac item} in let st = - if !stage > 0 then MA.meta_of_aut f st.mst item else st + if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st in aux st tl in