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
-basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx
-basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx
+common/common.cmo: lib/nUri.cmi automath/aut.cmx
+common/common.cmx: lib/nUri.cmx automath/aut.cmx
+basic_rg/brg.cmo: lib/log.cmi lib/cps.cmx common/common.cmx
+basic_rg/brg.cmx: lib/log.cmx lib/cps.cmx common/common.cmx
basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx
basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \
lib/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
-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/bag.cmo: lib/log.cmi lib/cps.cmx common/common.cmx
+basic_ag/bag.cmx: lib/log.cmx lib/cps.cmx common/common.cmx
basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx
basic_ag/bagOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \
lib/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi
toplevel/top.cmo: lib/time.cmx lib/output.cmi lib/nUri.cmi \
toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \
toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi lib/cps.cmx \
- basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \
- basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \
+ basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \
toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \
toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \
- basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \
- basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \
+ basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
automath/autLexer.cmx
-lib automath basic_rg basic_ag toplevel
+lib automath common basic_rg basic_ag toplevel
-Helena 0.8.0 M (July 2008)
+Helena 0.8.0 M
* type "make" or "make opt" to compile the native executable
(* kernel version: basic, absolute, global *)
(* note : experimental *)
-type uri = NUri.uri
-type id = Aut.id
+type uri = Common.uri
+type id = Common.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type obj = int * uri * bind (* age, uri, binder, contents *)
+type obj = bind Common.obj (* age, uri, binder *)
-type item = obj option
+type item = bind Common.item
type context = (int * id * bind) list (* location, name, binder *)
module E = BagEnvironment
module S = BagSubstitution
-exception LRefNotFound of B.message
+exception TypeError of B.message
type machine = {
i: int;
let level = 5
-let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+let error i =
+ let s = Printf.sprintf "local reference not found %u" i in
+ raise (TypeError (L.items1 s))
let log1 s c t =
let sc, st = s ^ " in the context", "the term" in
L.log O.specs level (L.ct_items1 sc c st t)
-let log2 s c u t =
- let sc, su, st = s ^ " in the context", "the term", "and the term" in
- L.log O.specs level (L.ct_items2 sc c su u st t)
+let log2 s cu u ct t =
+ let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
+ L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t)
let empty_machine = {i = 0; c = B.empty_context; s = []}
(* Interface functions ******************************************************)
-let nsi = ref false
-
let rec ho_whd f c m x =
(* L.warn "entering R.ho_whd"; *)
let aux m = function
L.box level; log1 "Now scanning" c t;
ho_whd f c empty_machine t
-let rec are_convertible f a c m1 t1 m2 t2 =
+let rec are_convertible f ~si 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;
+ log2 "Now really converting" c u c t;
match r1, r2 with
| 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 a c m1 m2 else f false
+ if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
| GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) ->
- if a1 = a2 then are_convertible_stacks f a c m1 m2 else f false
+ if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
| GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
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
+ let f a =
+ if a then f a else are_convertible f ~si true c m1 v1 m2 v2
+ in
+ are_convertible_stacks f ~si 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
let l = B.new_location () in
let h c =
let m1, m2 = inc m1, inc m2 in
- let f t1 = S.subst (are_convertible f a c m1 t1 m2) l l2 t2 in
+ let f t1 = S.subst (are_convertible f ~si 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 l id1 w1 else f false in
- are_convertible f a c m1 w1 m2 w2
+ are_convertible f ~si 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 ->
+ | Sort_ _, Bind_ (l2, id2, w2, t2) when si ->
let m1, m2 = inc m1, inc m2 in
- let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in
+ let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in
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 =
+and are_convertible_stacks f ~si 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
+ let map f a v1 v2 = are_convertible f ~si 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"
else
C.list_fold_left2 f map a m1.s m2.s
-let are_convertible f c u t =
+let are_convertible f ?(si=false) c u t =
let f b = L.unbox level; f b in
- L.box level; log2 "Now converting" c u t;
- are_convertible f true c empty_machine u empty_machine t
+ L.box level; log2 "Now converting" c u c t;
+ are_convertible f ~si true c empty_machine u empty_machine t
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-exception LRefNotFound of Bag.message
+exception TypeError of Bag.message
type ho_whd_result =
| Sort of int
(ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a
val are_convertible:
- (bool -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a
-
-val nsi: bool ref
+ (bool -> 'a) -> ?si:bool -> Bag.context -> Bag.term -> Bag.term -> 'a
module E = BagEnvironment
module R = BagReduction
-exception TypeError of B.message
-
(* Internal functions *******************************************************)
let level = 4
let error1 st c t =
let sc = "In the context" in
- raise (TypeError (L.ct_items1 sc c st t))
+ raise (R.TypeError (L.ct_items1 sc c st t))
let error3 c t1 t2 t3 =
let sc, st1, st2, st3 =
"In the context", "the term", "is of type", "but must be of type"
in
- raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
+ raise (R.TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
let mk_gref u l =
let map t v = B.Appl (v, t) in
(* Interface functions ******************************************************)
-let rec b_type_of f g c x =
+let rec b_type_of f ~si g c x =
(* L.warn "Entering T.b_type_of"; *)
log1 "Now checking" c x;
match x with
let f xv xt tt =
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 cc = b_type_of (f xv) ~si g cc t 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))
in
- type_of f g c v
+ type_of f ~si g c v
| B.Bind (l, id, B.Abst u, t) ->
let f xu xt tt =
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 cc = b_type_of (f xu) ~si g cc t in
let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in
- type_of f g c u
+ type_of f ~si 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
+ let f cc = b_type_of f ~si g cc t in
B.push "type void" f c l id B.Void
| B.Appl (v, t) ->
let f xv vv xt tt = function
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
+ R.are_convertible f ~si c w vv
| _ ->
error1 "not a function" c xt
in
let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in
- let f xv vv = b_type_of (f xv vv) g c t in
- type_of f g c v
+ let f xv vv = b_type_of (f xv vv) ~si g c t in
+ type_of f ~si g c v
| B.Cast (u, t) ->
let f xu xt tt a =
(* 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 f xu _ = b_type_of (f xu) g c t in
- type_of f g c u
+ let f xu xt tt = R.are_convertible (f xu xt tt) ~si c xu tt in
+ let f xu _ = b_type_of (f xu) ~si g c t in
+ type_of f ~si g c u
-and type_of f g c x =
+and type_of f ?(si=false) g c x =
let f t u = L.unbox level; f t u in
- L.box level; b_type_of f g c x
+ L.box level; b_type_of f ~si g c x
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-exception TypeError of Bag.message
-
val type_of:
- (Bag.term -> Bag.term -> 'a) ->
+ (Bag.term -> Bag.term -> 'a) -> ?si:bool ->
Hierarchy.graph -> Bag.context -> Bag.term -> 'a
(* Interface functions ******************************************************)
(* to share *)
-let type_check f g = function
+let type_check f ?(si=false) g = function
| None -> f None None
| 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
- L.loc := a; T.type_of f g B.empty_context t
+ L.loc := a; T.type_of f ~si 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
- L.loc := a; T.type_of f g B.empty_context t
+ L.loc := a; T.type_of f ~si g B.empty_context t
| Some (a, uri, B.Void) ->
let f obj = f None (Some obj) in
L.loc := a; E.set_obj f (a, uri, B.Void)
V_______________________________________________________________ *)
val type_check:
- (Bag.term option -> Bag.item -> 'a) -> Hierarchy.graph -> Bag.item -> 'a
+ (Bag.term option -> Bag.item -> 'a) -> ?si:bool ->
+ Hierarchy.graph -> Bag.item -> 'a
(* kernel version: basic, relative, global *)
(* note : ufficial basic lambda-delta *)
-type uri = NUri.uri
-type id = Aut.id
+type uri = Common.uri
+type id = Common.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
and attrs = attr list
-type obj = int * uri * bind (* age, uri, binder, contents *)
+type obj = bind Common.obj (* age, uri, binder *)
-type item = obj option
+type item = bind Common.item
type context = (attrs * bind) list (* attrs, binder *)
module E = BrgEnvironment
module S = BrgSubstitution
-exception LRefNotFound of B.message
+exception TypeError of B.message
type machine = {
c: B.context;
let level = 5
-let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
-
let log1 s c t =
let sc, st = s ^ " in the context", "the term" in
L.log O.specs level (L.ct_items1 sc c st t)
-let log2 s c u t =
- let sc, su, st = s ^ " in the context", "the term", "and the term" in
- L.log O.specs level (L.ct_items2 sc c su u st t)
+let log2 s cu u ct t =
+ let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
+ L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t)
+
+let error0 i =
+ let s = Printf.sprintf "local reference not found %u" i in
+ raise (TypeError (L.items1 s))
+
+let error1 st c t =
+ let sc = "In the context" in
+ raise (TypeError (L.ct_items1 sc c st t))
-let empty_machine = {
- c = B.empty_context; s = []
+let error3 c t1 t2 t3 =
+ let sc, st1, st2, st3 =
+ "In the context", "the term", "is of type", "but must be of type"
+ in
+ raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
+
+let empty_machine c = {
+ c = c; s = []
}
-let get f c m i =
+let get f m i =
let f e = function
| Some (_, b) -> f e b
- | None -> error i
+ | None -> error0 i
in
- let f c = B.get f c i in
- B.append f c m.c
+ B.get f m.c i
let lift_stack f s =
let map f (v, i) = f (v, succ i) in
Cps.list_map f map s
-let unwind_to_term f m t =
- let map f t (a, b) = f (B.Bind (a, b, t)) in
- let f mc = C.list_fold_left f map t mc in
- assert (m.s = []);
- B.contents f m.c
-
let push f m a b =
assert (m.s = []);
f {m with c = (a, b) :: m.c}
(* to share *)
-let rec step f ?(delta=false) ?(rt=false) c m x =
+let rec step f ?(delta=false) ?(rt=false) m x =
(* L.warn "entering R.step"; *)
match x with
| B.Sort _ -> f m x
let f = function
| _, _, B.Abbr v when delta ->
P.add ~gdelta:1 ();
- step f ~delta ~rt c m v
+ step f ~delta ~rt m v
| _, _, B.Abst w when rt ->
P.add ~grt:1 ();
- step f ~delta ~rt c m w
+ step f ~delta ~rt m w
| e, _, b ->
f m (B.GRef (B.Entry (e, b) :: a, uri))
in
let f e = function
| B.Abbr v ->
P.add ~ldelta:1 ();
- step f ~delta ~rt c m v
+ step f ~delta ~rt m v
| B.Abst w when rt ->
P.add ~lrt:1 ();
- step f ~delta ~rt c m w
+ step f ~delta ~rt m w
| b ->
f m (B.LRef (B.Entry (e, b) :: a, i))
in
let f e = S.lift_bind (f e) (succ i) (0) in
- get f c m i
+ get f m i
| B.Cast (_, _, t) ->
P.add ~tau:1 ();
- step f ~delta ~rt c m t
+ step f ~delta ~rt m t
| B.Appl (_, v, t) ->
- step f ~delta ~rt c {m with s = (v, 0) :: m.s} t
+ step f ~delta ~rt {m with s = (v, 0) :: m.s} t
| B.Bind (a, B.Abst w, t) ->
begin match m.s with
| [] -> f m x
| (v, h) :: tl ->
P.add ~beta:1 ~upsilon:(List.length tl) ();
- let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in
- let f mc = lift_stack (f mc) tl in
+ let f c s = step f ~delta ~rt {c = c; s = s} t in
+ let f c = lift_stack (f c) tl in
let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in
S.lift f h (0) v
end
| B.Bind (a, b, t) ->
P.add ~upsilon:(List.length m.s) ();
- let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in
- let f sc = B.push (f sc) m.c a b in
+ let f s c = step f ~delta ~rt {c = c; s = s} t in
+ let f s = B.push (f s) m.c a b in
lift_stack f m.s
(* Interface functions ******************************************************)
-
-let domain f c t =
+
+let domain f m t =
let f r = L.unbox level; f r in
let f m = function
- | B.Bind (_, B.Abst w, _) ->
- let f w = f (Some w) in unwind_to_term f m w
- | x -> f None
+ | B.Bind (_, B.Abst w, _) -> f m w
+ | _ -> error1 "not a function" m.c t
in
- L.box level; log1 "Now scanning" c t;
- step f ~delta:true ~rt:true c empty_machine t
+ L.box level; log1 "Now scanning" m.c t;
+ step f ~delta:true ~rt:true m t
-let rec ac_nfs f ~si r c m1 u m2 t =
-(* L.warn "entering R.are_convertible_aux"; *)
- log2 "Now converting nfs" c u t;
+let rec ac_nfs f ~si r m1 u m2 t =
+ log2 "Now converting nfs" m1.c u m2.c t;
match u, t with
| B.Sort (_, h1), B.Sort (_, h2) ->
if h1 = h2 then f r else f false
| B.LRef (B.Entry (e1, B.Abst _) :: _, i1),
B.LRef (B.Entry (e2, B.Abst _) :: _, i2) ->
P.add ~zeta:(i1+i2-e1-e2) ();
- if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
+ if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
| B.GRef (B.Entry (e1, B.Abst _) :: _, _),
B.GRef (B.Entry (e2, B.Abst _) :: _, _) ->
- if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
+ if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
| B.GRef (B.Entry (e1, B.Abbr v1) :: _, _),
B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) ->
if e1 = e2 then
if r then f r
else begin
P.add ~gdelta:2 ();
- ac f ~si true c m1 v1 m2 v2
+ ac f ~si true m1 v1 m2 v2
end
in
- ac_stacks f ~si r c m1 m2
+ ac_stacks f ~si r m1 m2
else if e1 < e2 then begin
P.add ~gdelta:1 ();
- step (ac_nfs f ~si r c m1 u) c m2 v2
+ step (ac_nfs f ~si r m1 u) m2 v2
end else begin
P.add ~gdelta:1 ();
- step (ac_nfs_rev f ~si r c m2 t) c m1 v1
+ step (ac_nfs_rev f ~si r m2 t) m1 v1
end
| _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
P.add ~gdelta:1 ();
- step (ac_nfs f ~si r c m1 u) c m2 v2
+ step (ac_nfs f ~si r m1 u) m2 v2
| B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
P.add ~gdelta:1 ();
- step (ac_nfs_rev f ~si r c m2 t) c m1 v1
+ step (ac_nfs_rev f ~si r m2 t) m1 v1
| B.Bind (a1, (B.Abst w1 as b1), t1),
B.Bind (a2, (B.Abst w2 as b2), t2) ->
- let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in
+ let g m1 m2 = ac f ~si r m1 t1 m2 t2 in
let g m1 = push (g m1) m2 a2 b2 in
let f r = if r then push g m1 a1 b1 else f false in
- ac f ~si r c m1 w1 m2 w2
+ ac f ~si r m1 w1 m2 w2
| B.Sort _, B.Bind (a, b, t) when si ->
P.add ~si:1 ();
- let f m1 m2 = ac f ~si r c m1 u m2 t in
+ let f m1 m2 = ac f ~si r m1 u m2 t in
let f m1 = push (f m1) m2 a b in
push f m1 a b
| _ -> f false
-and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t
+and ac_nfs_rev f ~si r m2 t m1 u = ac_nfs f ~si r m1 u m2 t
-and ac f ~si r c m1 t1 m2 t2 =
+and ac f ~si r m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
- let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in
- if r = false then f false else step g c m1 t1
+ let g m1 t1 = step (ac_nfs f ~si r m1 t1) m2 t2 in
+ if r = false then f false else step g m1 t1
-and ac_stacks f ~si r c m1 m2 =
+and ac_stacks f ~si r m1 m2 =
(* L.warn "entering R.are_convertible_stacks"; *)
let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
let map f r (v1, h1) (v2, h2) =
- let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in
+ let f v1 = S.lift (ac f ~si r mm1 v1 mm2) h2 (0) v2 in
S.lift f h1 (0) v1
in
if List.length m1.s <> List.length m2.s then
else
C.list_fold_left2 f map r m1.s m2.s
-let are_convertible f ?(si=false) c u t =
+let assert_conversion f ?(si=false) ?(rt=false) c u w v =
let f b = L.unbox level; f b in
- L.box level; log2 "Now converting" c u t;
- ac f ~si true c empty_machine u empty_machine t
+ let mw = empty_machine c in
+ let f mu u =
+ let f = function
+ | true -> f ()
+ | false -> error3 c v w u
+ in
+ L.box level; log2 "Now converting" c u c w;
+ ac f ~si true mu u mw w
+ in
+ if rt then domain f mw u else f mw u
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+exception TypeError of Brg.message
-exception LRefNotFound of Brg.message
-
-val domain:
- (Brg.term option -> 'a) -> Brg.context -> Brg.term -> 'a
-
-val are_convertible:
- (bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a
+(* arguments: expected type, inferred type, typed term *)
+val assert_conversion:
+ (unit -> 'a) -> ?si:bool -> ?rt:bool ->
+ Brg.context -> Brg.term -> Brg.term -> Brg.term -> 'a
module S = BrgSubstitution
module R = BrgReduction
-exception TypeError of B.message
-
(* Internal functions *******************************************************)
let level = 4
let error1 st c t =
let sc = "In the context" in
- raise (TypeError (L.ct_items1 sc c st t))
-
-let error3 c t1 t2 t3 =
- let sc, st1, st2, st3 =
- "In the context", "the term", "is of type", "but must be of type"
- in
- raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
+ raise (R.TypeError (L.ct_items1 sc c st t))
(* Interface functions ******************************************************)
-let si = ref false
-
-let rec b_type_of f g c x =
-(* L.warn "Entering T.b_type_of"; *)
+let rec b_type_of f ~si g c x =
log1 "Now checking" c x;
match x with
| B.Sort (a, h) ->
let f xv xt tt =
f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
in
- let f xv cc = b_type_of (f xv) g cc t in
+ let f xv cc = b_type_of (f xv) ~si g cc t in
let f xv = B.push (f xv) c a (B.Abbr xv) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> assert false (* f (B.Cast ([], vv, xv)) *)
in
- type_of f g c v
+ type_of f ~si g c v
| B.Bind (a, B.Abst u, t) ->
let f xu xt tt =
f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
in
- let f xu cc = b_type_of (f xu) g cc t in
+ let f xu cc = b_type_of (f xu) ~si g cc t in
let f xu _ = B.push (f xu) c a (B.Abst xu) in
- type_of f g c u
+ type_of f ~si g c u
| B.Bind (a, B.Void, t) ->
let f xt tt =
f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
in
- let f cc = b_type_of f g cc t in
+ let f cc = b_type_of f ~si g cc t in
B.push f c a B.Void
| B.Appl (a, v, t) ->
- let f xv vv xt tt = function
- | Some w ->
- L.box (succ level);
- L.log O.specs (succ level) (L.t_items1 "Just scanned" c w);
- L.unbox (succ level);
- let f r =
-(* L.warn (Printf.sprintf "Convertible: %b" a); *)
- if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt)
- else error3 c xv vv w
- in
- R.are_convertible f ~si:!si c w vv
- | None ->
- error1 "not a function" c xt
+ let f xv vv xt tt =
+ let f () = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+ R.assert_conversion f ~si ~rt:true c tt vv xv
in
- let f xv vv xt tt = R.domain (f xv vv xt tt) c tt in
- let f xv vv = b_type_of (f xv vv) g c t in
- type_of f g c v
+ let f xv vv = b_type_of (f xv vv) ~si g c t in
+ type_of f ~si g c v
| B.Cast (a, u, t) ->
- let f xu xt tt r =
- (* L.warn (Printf.sprintf "Convertible: %b" a); *)
- if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu
+ let f xu xt tt =
+ let f () = f (A.sh2 u xu t xt x (B.cast a)) xu in
+ R.assert_conversion f ~si c xu tt xt
in
- let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in
- let f xu _ = b_type_of (f xu) g c t in
- type_of f g c u
+ let f xu _ = b_type_of (f xu) ~si g c t in
+ type_of f ~si g c u
-and type_of f g c x =
+and type_of f ?(si=false) g c x =
let f t u = L.unbox level; f t u in
- L.box level; b_type_of f g c x
+ L.box level; b_type_of f ~si g c x
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-exception TypeError of Brg.message
-
val type_of:
- (Brg.term -> Brg.term -> 'a) ->
+ (Brg.term -> Brg.term -> 'a) -> ?si:bool ->
Hierarchy.graph -> Brg.context -> Brg.term -> 'a
-
-val si: bool ref
(* Interface functions ******************************************************)
(* to share *)
-let type_check f g = function
+let type_check f ?(si=false) g = function
| None -> f None None
| Some (e, uri, B.Abst t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (e, uri, B.Abst xt) in
- L.loc := e; T.type_of f g B.empty_context t
+ L.loc := e; T.type_of f ~si g B.empty_context t
| Some (e, uri, B.Abbr t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (e, uri, B.Abbr xt) in
- L.loc := e; T.type_of f g B.empty_context t
+ L.loc := e; T.type_of f ~si g B.empty_context t
| Some (e, uri, B.Void) ->
let f obj = f None (Some obj) in
L.loc := e; E.set_obj f (e, uri, B.Void)
V_______________________________________________________________ *)
val type_check:
- (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a
+ (Brg.term option -> Brg.item -> 'a) -> ?si:bool ->
+ Hierarchy.graph -> Brg.item -> 'a
--- /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_______________________________________________________________ *)
+
+type uri = NUri.uri
+type id = Aut.id
+
+type 'bind obj = int * uri * 'bind (* age, uri, binder *)
+
+type 'bind item = 'bind obj option
let ct_items1 sc c st t =
[Warn sc; Context c; Warn st; Term (c, t)]
-let ct_items2 sc c st1 t1 st2 t2 =
- ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2)]
+let ct_items2 sc1 c1 st1 t1 sc2 c2 st2 t2 =
+ ct_items1 sc1 c1 st1 t1 @ ct_items1 sc2 c2 st2 t2
let ct_items3 sc c st1 t1 st2 t2 st3 t3 =
- ct_items2 sc c st1 t1 st2 t2 @ [Warn st3; Term (c, t3)]
+ ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2); Warn st3; Term (c, t3)]
let warn msg = F.fprintf std "@,%s" msg
string -> 'a -> string -> 'b -> ('a, 'b) item list
val ct_items2:
- string -> 'a -> string -> 'b -> string -> 'b -> ('a, 'b) item list
+ string -> 'a -> string -> 'b -> string -> 'a -> string -> 'b ->
+ ('a, 'b) item list
val ct_items3:
string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b ->
module U = NUri
module C = Cps
module L = Log
+module T = Time
module H = Hierarchy
module O = Output
module AP = AutProcess
module MO = MetaOutput
module MBrg = MetaBrg
module BrgO = BrgOutput
-module BrgT = BrgType
+module BrgR = BrgReduction
module BrgU = BrgUntrusted
module MBag = MetaBag
module BagO = BagOutput
ac : AO.counters;
mc : MO.counters;
brgc: BrgO.counters;
- bagc: BagO.counters
+ bagc: BagO.counters;
+ si : bool
}
-let initial_status cover = {
+let initial_status cover si = {
ac = AO.initial_counters;
mc = MO.initial_counters;
brgc = BrgO.initial_counters;
bagc = BagO.initial_counters;
mst = MA.initial_status ~cover ();
- ast = AP.initial_status
+ ast = AP.initial_status;
+ si = si
}
let count count_fun c item =
| BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item}
| BagItem item -> {st with bagc = count BagO.count_item st.bagc item}
-let type_check f st g = function
- | BrgItem item ->
- let f _ = function
- | None -> f st None
- | Some (i, u, _) -> f st (Some (i, u))
- in
- BrgU.type_check f g item
- | BagItem item ->
- let f _ = function
- | None -> f st None
- | Some (i, u, _) -> f st (Some (i, u))
- in
- BagU.type_check f g item
-
-let si () = match !kernel with
- | Brg -> BrgT.si := true
- | Bag -> BagR.nsi := true
+let type_check f st g k =
+ let f _ = function
+ | None -> f st None
+ | Some (i, u, _) -> f st (Some (i, u))
+ in
+ match k with
+ | BrgItem item -> BrgU.type_check f ~si:st.si g item
+ | BagItem item -> BagU.type_check f ~si:st.si g item
(****************************************************************************)
let main =
try
- let version_string = "Helena 0.8.0 M - July 2009" in
+ let version_string = "Helena 0.8.0 M - August 2009" in
let stage = ref 3 in
let meta_file = ref None in
let progress = ref false in
let use_cover = ref true in
+ let si = ref false in
let set_hierarchy s =
let f = function
| Some g -> H.graph := g
meta_file := Some (och, frm)
in
let read_file name =
- if !L.level > 0 then Time.gmtime version_string;
+ if !L.level > 0 then T.gmtime version_string;
if !L.level > 1 then
L.warn (P.sprintf "Processing file: %s" name);
- if !L.level > 0 then Time.utime_stamp "started";
+ if !L.level > 0 then T.utime_stamp "started";
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
let book = AutParser.book AutLexer.token lexbuf in
close_in ich;
- if !L.level > 0 then Time.utime_stamp "parsed";
+ if !L.level > 0 then T.utime_stamp "parsed";
let rec aux st = function
| [] -> st
| item :: tl ->
| None -> st
| Some (i, u) ->
if !progress then
- Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u));
+ L.warn (P.sprintf "[%u] %s" i (U.string_of_uri u));
st
in
(* stage 2 *)
if !use_cover then Filename.chop_extension (Filename.basename name)
else ""
in
- let st = aux (initial_status cover) book in
- if !L.level > 0 then Time.utime_stamp "processed";
+ let st = aux (initial_status cover !si) book in
+ if !L.level > 0 then T.utime_stamp "processed";
if !L.level > 2 then AO.print_counters C.start st.ac;
if !L.level > 2 then AO.print_process_counters C.start st.ast;
if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
("-k", Arg.String set_kernel, help_k);
("-m", Arg.String set_meta_file, help_m);
("-p", Arg.Set progress, help_p);
- ("-u", Arg.Unit si, help_u);
+ ("-u", Arg.Set si, help_u);
("-s", Arg.Int set_stage, help_s)
] read_file help;
- if !L.level > 0 then Time.utime_stamp "at exit";
+ if !L.level > 0 then T.utime_stamp "at exit";
flush ()
-with BagType.TypeError msg -> bag_error "Type Error" msg
- | BrgT.TypeError msg -> brg_error "Type Error" msg
+with BagR.TypeError msg -> bag_error "Type Error" msg
+ | BrgR.TypeError msg -> brg_error "Type Error" msg
projects / helm.git / commitdiff