From 939f76e2fd4a50fd49c010a64e49b5625569d712 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 15 Jun 2009 21:15:57 +0000 Subject: [PATCH] we removed some old code and fixed a reduction bug: two instances fo the same constant applied to a different number of arguments may be convertible We now check grundlagen up to item 109 :) (with naive sort inclusion :( puah) --- helm/software/lambda-delta/.depend.opt | 20 ++-- helm/software/lambda-delta/automath/Make | 2 +- .../software/lambda-delta/automath/autItem.ml | 34 ------- .../lambda-delta/automath/grundlagen.aut | 31 ++----- .../lambda-delta/basic_ag/bagReduction.ml | 91 ++++++++----------- .../lambda-delta/basic_ag/bagReduction.mli | 8 +- .../software/lambda-delta/basic_ag/bagType.ml | 74 +++------------ .../lambda-delta/basic_ag/bagUntrusted.ml | 7 +- helm/software/lambda-delta/lib/cps.ml | 4 +- helm/software/lambda-delta/lib/log.ml | 4 + helm/software/lambda-delta/lib/log.mli | 3 + helm/software/lambda-delta/toplevel/top.ml | 7 +- 12 files changed, 84 insertions(+), 201 deletions(-) delete mode 100644 helm/software/lambda-delta/automath/autItem.ml diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index c3ab0a209..d2b1d720f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -16,8 +16,6 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx -automath/autItem.cmo: lib/nUri.cmi -automath/autItem.cmx: lib/nUri.cmx basic_ag/bag.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx basic_ag/bag.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx @@ -38,26 +36,24 @@ basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \ basic_ag/bagReduction.cmi: lib/nUri.cmi basic_ag/bag.cmx basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \ - basic_ag/bagEnvironment.cmi basic_ag/bag.cmx automath/autItem.cmx \ - basic_ag/bagReduction.cmi + basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagReduction.cmi basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ - basic_ag/bagEnvironment.cmx basic_ag/bag.cmx automath/autItem.cmx \ - basic_ag/bagReduction.cmi + basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi basic_ag/bagType.cmi: lib/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ lib/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \ basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \ - automath/autItem.cmx basic_ag/bagType.cmi + basic_ag/bagType.cmi basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ lib/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \ basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \ - automath/autItem.cmx basic_ag/bagType.cmi + basic_ag/bagType.cmi basic_ag/bagUntrusted.cmi: lib/hierarchy.cmi basic_ag/bag.cmx -basic_ag/bagUntrusted.cmo: basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi \ - basic_ag/bag.cmx basic_ag/bagUntrusted.cmi -basic_ag/bagUntrusted.cmx: basic_ag/bagType.cmx basic_ag/bagEnvironment.cmx \ - basic_ag/bag.cmx basic_ag/bagUntrusted.cmi +basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \ + basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi +basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \ + basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx diff --git a/helm/software/lambda-delta/automath/Make b/helm/software/lambda-delta/automath/Make index 4b46c0bbd..9a773e0fc 100644 --- a/helm/software/lambda-delta/automath/Make +++ b/helm/software/lambda-delta/automath/Make @@ -1 +1 @@ -aut autOutput autParser autLexer autItem +aut autOutput autParser autLexer diff --git a/helm/software/lambda-delta/automath/autItem.ml b/helm/software/lambda-delta/automath/autItem.ml deleted file mode 100644 index dae038cce..000000000 --- a/helm/software/lambda-delta/automath/autItem.ml +++ /dev/null @@ -1,34 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module U = NUri - -(* Internal functions *******************************************************) - -let uri s = U.uri_of_string ("ld:" ^ s) - -(* Interface functions ******************************************************) - -let imp = uri "/l/imp" - -let mp = uri "/l/mp" - -let mt = uri "/l/mt" - -let all = uri "/l/all" - -let alle = uri "/l/alle" - -let alli = uri "/l/alli" - -let non = uri "/l/non" - -let lppc0 = uri "/l/lppc0" diff --git a/helm/software/lambda-delta/automath/grundlagen.aut b/helm/software/lambda-delta/automath/grundlagen.aut index 186ebdbcc..4a856c245 100644 --- a/helm/software/lambda-delta/automath/grundlagen.aut +++ b/helm/software/lambda-delta/automath/grundlagen.aut @@ -5,17 +5,9 @@ +l @[a:'prop'][b:'prop'] -%modification by Guidi to avoid prop inclusion -%imp:=[x:a]b:'prop' %original line -imp:='prim':'prop' -%end of modification +imp:=[x:a]b:'prop' [a1:a][i:imp(a,b)] -%modification by Guidi to avoid prop inclusion -%mp:=i:b %original line -mp:='prim':b -b@[f:[x:a]b] % we define modus tollens -mt:='prim':imp(a,b) -%end of modification +mp:=i:b a@refimp:=[x:a]x:imp(a,a) b@[c:'prop'][i:imp(a,b)][j:imp(b,c)] trimp:=[x:a]<i>j:imp(a,c) @@ -23,7 +15,7 @@ trimp:=[x:a]<i>j:imp(a,c) a@not:=imp(con):'prop' wel:=not(not(a)):'prop' [a1:a] -weli:=[x:not(a)]x:wel(a) %original line +weli:=[x:not(a)]x:wel(a) a@[w:wel(a)] et:='prim':a a@[c1:con] @@ -233,26 +225,17 @@ i@[o:orec(c,a)] thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b) -iff @[sigma:'type'][p:[x:sigma]'prop'] -%modification by Guidi to remove prop inclusion +%suggestion by van Daalen to remove the first eta-reduction %all:=p:'prop' %original line -%all:=[x:sigma]p:'prop' %suggestion by van Daalen to remove eta-reduction -all:='prim':'prop' -%end of modification +all:=[x:sigma]p:'prop' +%end of suggestion [a1:all(sigma,p)][s:sigma] -%modification by Guidi to remove prop inclusion -%alle:=a1:p %original line -alle:='prim':p -p@[f:[s:sigma]p] % we define modus tollens -alli:='prim':all(sigma,p) -%end of modification +alle:=a1:p +all p@[s:sigma][n:not(p)] th1:=[x:all(sigma,p)]<x>n:not(all(sigma,p)) -all p@non:=[x:sigma]not(p):[x:sigma]'prop' -%modification by Guidi to remove prop inclusion -p@lppc0:='prim':'prop' -%end of modification some:=not(non(p)):'prop' [s:sigma][sp:p] somei:=th1".all"(non(p),s,weli(p,sp)):some(sigma,p) diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index f8fed7786..edd1eeaf7 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -12,7 +12,6 @@ module U = NUri module C = Cps module L = Log -module I = AutItem module B = Bag module O = BagOutput module E = BagEnvironment @@ -37,10 +36,6 @@ type ho_whd_result = | GRef of U.uri * B.term list | Abst of B.term -type ac_result = (int * NUri.uri * Bag.term list) list option - -type extension = No | NSI - (* Internal functions *******************************************************) let term_of_whdr = function @@ -113,31 +108,20 @@ let rec whd f c m x = match x with let f mc = whd f c {m with c = mc} t in B.push f m.c l id b -let insert f i uri vs = function - | Some l -> f (Some ((i, uri, vs) :: l)) - | None -> assert false - (* Interface functions ******************************************************) -let ext = ref No +let nsi = ref false let rec ho_whd f c m x = 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_ (_, uri, B.Abst w) -> - let h = function - | Abst _ as r -> f r - | GRef _ as r -> f r - | Sort _ -> - let f vs = f (GRef (uri, vs)) in unwind_stack f m - in - if !ext = No then ho_whd h c m w else ho_whd f c m w - | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v - | LRef_ (_, None) -> assert false - | GRef_ (_, _, B.Void) -> assert false + | LRef_ (_, Some w) -> ho_whd f c m w + | GRef_ (_, _, B.Abst w) -> ho_whd f c m w + | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v + | LRef_ (_, None) -> assert false + | GRef_ (_, _, B.Void) -> assert false in whd aux c m x @@ -146,19 +130,22 @@ let ho_whd f c t = L.box level; log1 "Now scanning" c t; ho_whd f c empty_machine t -let rec are_convertible f xl c m1 t1 m2 t2 = +let rec are_convertible f a c m1 t1 m2 t2 = let rec aux m1 r1 m2 r2 = let u, t = term_of_whdr r1, term_of_whdr r2 in log2 "Now really converting" c u t; match r1, r2 with - | Sort_ h1, Sort_ h2 -> - if h1 = h2 then f xl else f None + | Sort_ h1, Sort_ h2 -> + if h1 = h2 then f a else f false | LRef_ (i1, _), LRef_ (i2, _) -> - if i1 = i2 then are_convertible_stacks f xl c m1 m2 else f None + if i1 = i2 then are_convertible_stacks f a c m1 m2 else f false | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) -> - if a1 = a2 then are_convertible_stacks f xl c m1 m2 else f None + if a1 = a2 then are_convertible_stacks f a c m1 m2 else f false | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) -> - if a1 = a2 then are_convertible_stacks f xl c m1 m2 else + if a1 = a2 then + let f a = if a then f a else are_convertible f true c m1 v1 m2 v2 in + are_convertible_stacks f a c m1 m2 + else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 | _, GRef_ (_, _, B.Abbr v2) -> @@ -166,36 +153,36 @@ let rec are_convertible f xl 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 f xl = - let h c = - let m1, m2 = inc m1, inc m2 in - S.subst (are_convertible f xl c m1 t1 m2) l1 l2 t2 - in - if xl = None then f xl else push h c m1 l1 id1 w1 + let h c = + let m1, m2 = inc m1, inc m2 in + S.subst (are_convertible f a c m1 t1 m2) l1 l2 t2 in - are_convertible f xl c m1 w1 m2 w2 + let f r = if r then push h c m1 l1 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 *) - | GRef_ (_, uri, B.Abst _), Bind_ (l1, _, _, _) when !ext = No -> - let g vs = insert f l1 uri vs xl in - if U.eq uri I.imp then unwind_stack g m1 else - if U.eq uri I.all then unwind_stack g m1 else - begin L.warn (U.string_of_uri uri); f None end - | Sort_ _, Bind_ (l2, id2, w2, t2) when !ext = NSI -> + | Sort_ _, Bind_ (l2, id2, w2, t2) when !nsi -> let m1, m2 = inc m1, inc m2 in - let f c = are_convertible f xl c m1 (term_of_whdr r1) m2 t2 in + let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in push f c m2 l2 id2 w2 - | _ -> f None + | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in - let f m1 r1 = whd (aux m1 r1) c m2 t2 in - whd f c m1 t1 + 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 xl c m1 m2 = +and are_convertible_stacks f a c m1 m2 = let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in - let map f xl v1 v2 = are_convertible f xl c mm1 v1 mm2 v2 in - if List.length m1.s <> List.length m2.s then f None else - C.list_fold_left2 f map xl m1.s m2.s + 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) + ); + f false + end + else + C.list_fold_left2 f map a m1.s m2.s let are_convertible f c u t = let f b = L.unbox level; f b in L.box level; log2 "Now converting" c u t; - are_convertible f (Some []) c empty_machine u empty_machine t + are_convertible f true c empty_machine u empty_machine t diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index 1456d3cc6..a07e65cb0 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -17,14 +17,10 @@ type ho_whd_result = | GRef of NUri.uri * Bag.term list | Abst of Bag.term -type ac_result = (int * NUri.uri * Bag.term list) list option - -type extension = No | NSI - val ho_whd: (ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a val are_convertible: - (ac_result -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a + (bool -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a -val ext: extension ref +val nsi: bool ref diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 9bae115df..0520883d5 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -14,7 +14,6 @@ module C = Cps module S = Share module L = Log module H = Hierarchy -module I = AutItem module B = Bag module O = BagOutput module E = BagEnvironment @@ -44,47 +43,6 @@ let mk_gref u l = let map t v = B.Appl (v, t) in List.fold_left map (B.GRef u) l -let add_coercion f t (i, uri, vs) = - let rec add f x = match x with - | B.Sort _ - | B.LRef _ - | B.GRef _ -> f x - | B.Cast (u, t) -> - let f uu = - let f tt = f (S.sh2 u uu t tt x B.cast) in - add f t - in - add f u - | B.Appl (v, t) -> - let f vv = - let f tt = f (S.sh2 v vv t tt x B.appl) in - add f t - in - add f v - | B.Bind (l, _, _, _) when i = l -> - if U.eq uri I.imp then f (mk_gref I.mt (vs @ [x])) else - if U.eq uri I.all then f (mk_gref I.alli (vs @ [x])) else - assert false - | B.Bind (l, id, B.Abst w, t) -> - let f ww = - let f tt = f (S.sh2 w ww t tt x (B.bind_abst l id)) in - add f t - in - add f w - | B.Bind (l, id, B.Abbr v, t) -> - let f vv = - let f tt = f (S.sh2 v vv t tt x (B.bind_abbr l id)) in - add f t - in - add f v - | B.Bind (l, id, B.Void, t) -> - let f tt = f (S.sh1 t tt x (B.bind l id B.Void)) in - add f t - in - add f t - -let add_coercions f = C.list_fold_left f add_coercion - (* Interface functions ******************************************************) let rec b_type_of f g c x = @@ -142,22 +100,14 @@ let rec b_type_of f g c x = L.box (succ level); L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); L.unbox (succ level); - let f = function - | Some [] -> f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) - | Some l -> - L.log O.specs level (L.items1 "Rechecking coerced term"); - let f xv = b_type_of f g c (S.sh2 v xv t xt x B.appl) in - add_coercions f xv l - | None -> error3 c xv vv w + let f a = + L.box (succ level); + L.warn (Printf.sprintf "Convertible: %b" a); + L.unbox (succ level); + if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) + else error3 c xv vv w in R.are_convertible f c w vv -(* inserting a missing "modus ponens" *) - | R.GRef (uri, vs) when U.eq uri I.imp && !R.ext = R.No -> - L.log O.specs level (L.items1 "Rechecking coerced term"); - b_type_of f g c (mk_gref I.mp (vs @ [xv; xt])) - | R.GRef (uri, vs) when U.eq uri I.all && !R.ext = R.No -> - L.log O.specs level (L.items1 "Rechecking coerced term"); - b_type_of f g c (mk_gref I.alle (vs @ [xt; xv])) | _ -> error1 "not a function" c xt in @@ -165,13 +115,11 @@ let rec b_type_of f g c x = let f xv vv = b_type_of (f xv vv) g c t in type_of f g c v | B.Cast (u, t) -> - let f xu xt tt = function - | Some [] -> f (S.sh2 u xu t xt x B.cast) xu - | Some l -> - L.log O.specs level (L.items1 "Rechecking coerced term"); - let f xt = b_type_of f g c (S.sh2 u xu t xt x B.cast) in - add_coercions f xt l - | None -> error3 c xt tt xu + let f xu xt tt a = + L.box (succ level); + L.warn (Printf.sprintf "Convertible: %b" a); + L.unbox (succ level); + 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 f xu _ = b_type_of (f xu) g c t in diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index e80a06125..600807c67 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module L = Log module B = Bag module E = BagEnvironment module T = BagType @@ -21,11 +22,11 @@ let type_check f g = function | Some (a, uri, B.Abst t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in - T.type_of f g B.empty_context t + L.loc := a; T.type_of f g B.empty_context t | Some (a, uri, B.Abbr t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in - T.type_of f g B.empty_context t + L.loc := a; T.type_of f g B.empty_context t | Some (a, uri, B.Void) -> let f obj = f None (Some obj) in - E.set_obj f (a, uri, B.Void) + L.loc := a; E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index b61fccfa4..3875d88fa 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -60,6 +60,6 @@ let list_iter f map l = let rec list_fold_left2 f map a l1 l2 = match l1, l2 with | [], [] -> f a | hd1 :: tl1, hd2 :: tl2 -> - let f a = if a = None then f a else list_fold_left2 f map a tl1 tl2 in + let f a = list_fold_left2 f map a tl1 tl2 in map f a hd1 hd2 - | _ -> f None + | _ -> assert false diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 4cea12cda..9c2ecefa2 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -17,6 +17,7 @@ type ('a, 'b) item = Term of 'a * 'b | Context of 'a | Warn of string | String of string + | Loc type ('a, 'b) specs = { pp_term : 'a -> F.formatter -> 'b -> unit; @@ -25,6 +26,8 @@ type ('a, 'b) specs = { let level = ref 0 +let loc = ref 0 + (* Internal functions *******************************************************) let std = F.std_formatter @@ -37,6 +40,7 @@ let pp_items frm st l items = | Context c -> F.fprintf frm "%a" st.pp_context c | Warn s -> F.fprintf frm "@,%s" s | String s -> F.fprintf frm "%s " s + | Loc -> F.fprintf frm " (line %u)" !loc in let iter map frm l = List.iter (map frm) l in if !level >= l then F.fprintf frm "%a" (iter pp_item) items diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index bdaee06e0..241247c18 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -13,12 +13,15 @@ type ('a, 'b) item = Term of 'a * 'b | Context of 'a | Warn of string | String of string + | Loc type ('a, 'b) specs = { pp_term : 'a -> Format.formatter -> 'b -> unit; pp_context: Format.formatter -> 'a -> unit } +val loc: int ref + val level: int ref val warn: string -> unit diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 4c90fcea7..70234ba13 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -42,7 +42,7 @@ let count count_fun c item = let flush () = L.flush 0; L.flush_err () let bag_error s msg = - L.error BagO.specs (L.Warn s :: msg); flush () + L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () let main = try @@ -70,7 +70,6 @@ try Format.pp_set_margin frm max_int; meta_file := Some (och, frm) in - let set_nsi () = BagR.ext := BagR.NSI in let read_file name = if !L.level > 0 then Time.gmtime version_string; if !L.level > 1 then @@ -140,8 +139,8 @@ try ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set BagO.indexes, help_i); ("-m", Arg.String set_meta_file, help_m); - ("-n", Arg.Unit set_nsi, help_n); - ("-s", Arg.Int set_stage, help_s); + ("-n", Arg.Set BagR.nsi, help_n); + ("-s", Arg.Int set_stage, help_s) ] read_file help; if !L.level > 0 then Time.utime_stamp "at exit"; flush () -- 2.39.2