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
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
-aut autOutput autParser autLexer autItem
+aut autOutput autParser autLexer
+++ /dev/null
-(*
- ||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"
+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:=<a1>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:=<a1>i:b
a@refimp:=[x:a]x:imp(a,a)
b@[c:'prop'][i:imp(a,b)][j:imp(b,c)]
trimp:=[x:a]<<x>i>j:imp(a,c)
a@not:=imp(con):'prop'
wel:=not(not(a)):'prop'
[a1:a]
-weli:=[x:not(a)]<a1>x:wel(a) %original line
+weli:=[x:not(a)]<a1>x:wel(a)
a@[w:wel(a)]
et:='prim':a
a@[c1:con]
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]<x>p:'prop' %suggestion by van Daalen to remove eta-reduction
-all:='prim':'prop'
-%end of modification
+all:=[x:sigma]<x>p:'prop'
+%end of suggestion
[a1:all(sigma,p)][s:sigma]
-%modification by Guidi to remove prop inclusion
-%alle:=<s>a1:<s>p %original line
-alle:='prim':<s>p
-p@[f:[s:sigma]<s>p] % we define modus tollens
-alli:='prim':all(sigma,p)
-%end of modification
+alle:=<s>a1:<s>p
+all
p@[s:sigma][n:not(<s>p)]
th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
-all
p@non:=[x:sigma]not(<x>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:<s>p]
somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)
module U = NUri
module C = Cps
module L = Log
-module I = AutItem
module B = Bag
module O = BagOutput
module E = BagEnvironment
| 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
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
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) ->
| 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
| 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
module S = Share
module L = Log
module H = Hierarchy
-module I = AutItem
module B = Bag
module O = BagOutput
module E = BagEnvironment
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 =
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
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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module L = Log
module B = Bag
module E = BagEnvironment
module T = BagType
| 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)
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
| Context of 'a
| Warn of string
| String of string
+ | Loc
type ('a, 'b) specs = {
pp_term : 'a -> F.formatter -> 'b -> unit;
let level = ref 0
+let loc = ref 0
+
(* Internal functions *******************************************************)
let std = F.std_formatter
| 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
| 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
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
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
("-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 ()
projects / helm.git / commitdiff