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 ()
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 =
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
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
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
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, _) ->
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
| 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
(* 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 ->
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))
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 ->
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
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
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
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
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 =
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
(* 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
projects / helm.git / commitdiff