basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx
basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
-basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx
+basic_rg/brgReduction.cmi: lib/log.cmi common/entity.cmx basic_rg/brg.cmx
basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \
lib/log.cmi common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmi \
basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi
basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \
lib/log.cmx common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi
-basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi \
+basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi common/entity.cmx \
basic_rg/brgReduction.cmi basic_rg/brg.cmx
basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
| _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs} in
count_term f c v
+ | _, _, Y.Void -> assert false
let print_counters f c =
let terms =
| GRef_ (_, _, Y.Abst w) -> ho_whd f c m w
| GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
| LRef_ (_, None) -> assert false
+ | GRef_ (_, _, Y.Void) -> assert false
in
whd aux c m x
| _, _, Y.Abst w -> f x w
| _, _, Y.Abbr (B.Cast (w, v)) -> f x w
| _, _, Y.Abbr _ -> assert false
+ | _, _, Y.Void -> assert false
in
E.get_entity f uri
| B.Bind (l, id, B.Abbr v, t) ->
| a, uri, Y.Abbr t ->
let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in
L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t
+ | _, _, Y.Void -> assert false
let empty_lenv = Null
-let push f es ?c b =
- let es = Cons (es, c, b) in f es
+let push es ?c b = Cons (es, c, b)
let get err f es i =
let rec aux j = function
in
aux i es
+(* check closure *)
let rec rev_iter f map = function
| Null -> f ()
| Cons (tl, None, b) ->
| Cons (tl, Some c, b) ->
let f _ = map f c b in rev_iter f map tl
-let rec fold_left f map x = function
- | Null -> f x
- | Cons (tl, _, b) ->
- let f x = fold_left f map x tl in
- map f x b
+let rec fold_left map x = function
+ | Null -> x
+ | Cons (tl, _, b) -> fold_left map (map x b) tl
(* Interface functions ******************************************************)
-let set_entity f (a, uri, b) =
+(* decps *)
+let set_entity (a, uri, b) =
let age = get_age () in
let entity = (Y.Apix age :: a), uri, b in
- H.add env uri entity; f entity
+ H.add env uri entity; entity
-let get_entity err f uri =
- try f (H.find env uri) with Not_found -> err ()
+let get_entity uri =
+ try H.find env uri with Not_found -> [], uri, Y.Void
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val set_entity: (Brg.entity -> 'a) -> Brg.entity -> 'a
+val set_entity: Brg.entity -> Brg.entity
-val get_entity: (unit -> 'a) -> (Brg.entity -> 'a) -> Brg.uri -> 'a
+val get_entity: Brg.uri -> Brg.entity
let f c = count_term f c e t in
count_term f c e v
| B.Bind (b, t) ->
- let f c e = count_term f c e t in
- let f c = B.push (f c) e b in
+ let f c = count_term f c (B.push e b) t in
count_term_binder f c e b
let count_entity f c = function
| _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
count_term f c B.empty_lenv v
+ | _, _, Y.Void -> assert false
let print_counters f c =
let terms =
| B.Appl (_, v, t) ->
F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
| B.Bind (B.Abst (a, w), t) ->
- let f a cc =
- F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
+ let f a =
+ let cc = B.push c (B.abst a w) in
+ F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
in
- let f a = B.push (f a) c (B.abst a w) in
rename f c a
| B.Bind (B.Abbr (a, v), t) ->
- let f a cc =
- F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
+ let f a =
+ let cc = B.push c (B.abbr a v) in
+ F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
in
- let f a = B.push (f a) c (B.abbr a v) in
rename f c a
| B.Bind (B.Void a, t) ->
- let f a cc = F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t in
- let f a = B.push (f a) c (B.Void a) in
+ let f a =
+ let cc = B.push c (B.Void a) in
+ F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t
+ in
rename f c a
let pp_lenv frm c =
| B.Bind (b, t) ->
let b = rename_bind C.start e b in
exp_bind e b out tab;
- exp_term (B.push C.start e b) t out tab
+ exp_term (B.push e b) t out tab
and exp_bind e b out tab = match b with
| B.Abst (a, w) ->
let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+let rec list_and map = function
+ | hd1 :: tl1, hd2 :: tl2 ->
+ if map hd1 hd2 then list_and map (tl1, tl2) else false
+ | l1, l2 -> l1 = l2
+
+(* check closure *)
let are_alpha_convertible err f t1 t2 =
let rec aux f = function
| B.Sort (_, p1), B.Sort (_, p2)
in
if S.eq t1 t2 then f () else aux f (t1, t2)
-let get err f m i =
- B.get err f m.c i
+let get m i =
+ let f c b = c, b in
+ B.get C.err f m.c i
(* to share *)
-let rec step f ?(delta=false) ?(rt=false) m x =
+let rec step st m x =
(* L.warn "entering R.step"; *)
match x with
- | B.Sort _ -> f m None x
+ | B.Sort _ -> m, None, x
| B.GRef (_, uri) ->
- let f = function
- | _, _, Y.Abbr v when delta ->
- P.add ~gdelta:1 (); step f ~delta ~rt m v
- | _, _, Y.Abst w when rt ->
- P.add ~grt:1 (); step f ~delta ~rt m w
- | a, _, Y.Abbr v ->
- let f e = f m (Some (e, B.Abbr (a, v))) x in
- Y.apix C.err f a
- | a, _, Y.Abst w ->
- let f e = f m (Some (e, B.Abst (a, w))) x in
- Y.apix C.err f a
- in
- E.get_entity C.err f uri
+ begin match E.get_entity uri with
+ | _, _, Y.Abbr v when st.Y.delta ->
+ P.add ~gdelta:1 (); step st m v
+ | _, _, Y.Abst w when st.Y.rt ->
+ P.add ~grt:1 (); step st m w
+ | a, _, Y.Abbr v ->
+ let e = Y.apix C.err C.start a in
+ m, Some (e, B.Abbr (a, v)), x
+ | a, _, Y.Abst w ->
+ let e = Y.apix C.err C.start a in
+ m, Some (e, B.Abst (a, w)), x
+ | _, _, Y.Void -> assert false
+ end
| B.LRef (_, i) ->
- let f c = function
- | B.Abbr (_, v) ->
+ begin match get m i with
+ | c, B.Abbr (_, v) ->
P.add ~ldelta:1 ();
- step f ~delta ~rt {m with c = c} v
- | B.Abst (_, w) when rt ->
+ step st {m with c = c} v
+ | c, B.Abst (_, w) when st.Y.rt ->
P.add ~lrt:1 ();
- step f ~delta ~rt {m with c = c} w
- | B.Void _ ->
+ step st {m with c = c} w
+ | c, B.Void _ ->
assert false
- | B.Abst (a, _) as b ->
- let f e = f {m with c = c} (Some (e, b)) x in
- Y.apix C.err f a
- in
- get C.err f m i
+ | c, (B.Abst (a, _) as b) ->
+ let e = Y.apix C.err C.start a in
+ {m with c = c}, Some (e, b), x
+ end
| B.Cast (_, _, t) ->
P.add ~tau:1 ();
- step f ~delta ~rt m t
+ step st m t
| B.Appl (_, v, t) ->
- step f ~delta ~rt {m with s = (m.c, v) :: m.s} t
+ step st {m with s = (m.c, v) :: m.s} t
| B.Bind (B.Abst (a, w), t) ->
begin match m.s with
- | [] -> f m None x
+ | [] -> m, None, x
| (c, v) :: s ->
P.add ~beta:1 ~upsilon:(List.length s) ();
- let f c = step f ~delta ~rt {m with c = c; s = s} t in
- B.push f m.c ~c (B.abbr a v) (* (B.Cast ([], w, v)) *)
+ let c = B.push m.c ~c (B.abbr a v) (* (B.Cast ([], w, v)) *) in
+ step st {m with c = c; s = s} t
end
| B.Bind (b, t) ->
P.add ~upsilon:(List.length m.s) ();
- let f c = step f ~delta ~rt {m with c = c} t in
- B.push f m.c ~c:m.c b
+ let c = B.push m.c ~c:m.c b in
+ step st {m with c = c} t
-let push f m b =
+let push m b =
assert (m.s = []);
let b, i = match b with
| B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
| b -> b, m.i
in
- let f c = f {m with c = c; i = i} in
- B.push f m.c ~c:m.c b
+ let c = B.push m.c ~c:m.c b in
+ {m with c = c; i = i}
-let rec ac_nfs err f ~si m1 a1 u m2 a2 t =
+let rec ac_nfs st (m1, a1, u) (m2, a2, t) =
log2 "Now converting nfs" m1.c u m2.c t;
match a1, u, a2, t with
| _, B.Sort (_, h1), _, B.Sort (_, h2) ->
- if h1 = h2 then f () else err ()
+ h1 = h2
| Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ ->
- if e1 = e2 then ac_stacks err f m1 m2 else err ()
+ if e1 = e2 then ac_stacks st m1 m2 else false
| Some (e1, B.Abbr (_, v1)), _, Some (e2, B.Abbr (_, v2)), _ ->
if e1 = e2 then
- let err _ = P.add ~gdelta:2 (); ac err f ~si m1 v1 m2 v2 in
- ac_stacks err f m1 m2
+ if ac_stacks st m1 m2 then true else begin
+ P.add ~gdelta:2 (); ac st m1 v1 m2 v2
+ end
else if e1 < e2 then begin
P.add ~gdelta:1 ();
- step (ac_nfs err f ~si m1 a1 u) m2 v2
+ ac_nfs st (m1, a1, u) (step st m2 v2)
end else begin
P.add ~gdelta:1 ();
- step (ac_nfs_rev err f ~si m2 a2 t) m1 v1
+ ac_nfs st (step st m1 v1) (m2, a2, t)
end
| _, _, Some (_, B.Abbr (_, v2)), _ ->
P.add ~gdelta:1 ();
- step (ac_nfs err f ~si m1 a1 u) m2 v2
+ ac_nfs st (m1, a1, u) (step st m2 v2)
| Some (_, B.Abbr (_, v1)), _, _, _ ->
P.add ~gdelta:1 ();
- step (ac_nfs_rev err f ~si m2 a2 t) m1 v1
+ ac_nfs st (step st m1 v1) (m2, a2, t)
| _, B.Bind ((B.Abst (_, w1) as b1), t1),
_, B.Bind ((B.Abst (_, w2) as b2), t2) ->
- let f m1 m2 = ac err f ~si m1 t1 m2 t2 in
- let f m1 = push (f m1) m2 b2 in
- let f _ = push f m1 b1 in
- ac err f ~si:false m1 w1 m2 w2
- | _, B.Sort _, _, B.Bind (b, t) when si ->
+ if ac {st with Y.si = false} m1 w1 m2 w2 then
+ ac st (push m1 b1) t1 (push m2 b2) t2
+ else false
+ | _, B.Sort _, _, B.Bind (b, t) when st.Y.si ->
P.add ~si:1 ();
- let f m1 m2 = ac err f ~si m1 u m2 t in
- let f m1 = push (f m1) m2 b in
- push f m1 b
- | _ -> err ()
-
-and ac_nfs_rev err f ~si m2 a2 t m1 a1 u = ac_nfs err f ~si m1 a1 u m2 a2 t
+ ac st (push m1 b) u (push m2 b) t
+ | _ -> false
-and ac err f ~si m1 t1 m2 t2 =
+and ac st m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
- let f m1 a1 t1 = step (ac_nfs err f ~si m1 a1 t1) m2 t2 in
- step f m1 t1
+ ac_nfs st (step st m1 t1) (step st m2 t2)
-and ac_stacks err f m1 m2 =
+and ac_stacks st m1 m2 =
(* L.warn "entering R.are_convertible_stacks"; *)
- if List.length m1.s <> List.length m2.s then err () else
- let map f (c1, v1) (c2, v2) =
+(* if List.length m1.s <> List.length m2.s then false else *)
+ let map (c1, v1) (c2, v2) =
let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
- ac err f ~si:false m1 v1 m2 v2
+ ac {st with Y.si = false} m1 v1 m2 v2
in
- C.list_iter2 f map m1.s m2.s
+ list_and map (m1.s, m2.s)
(* Interface functions ******************************************************)
let get err f m i =
assert (m.s = []);
let f c = f in
- get err f m i
-
-let xwhd f m t =
- L.box level; log1 "Now scanning" m.c t;
- let f m _ t = L.unbox level; f m t in
- step f ~delta:true ~rt:true m t
-
-let are_convertible err f ?(si=false) mu u mw w =
- L.box level; log2 "Now converting" mu.c u mw.c w;
- let f x = L.unbox level; f x in
- let err _ = ac err f ~si mu u mw w in
-(* if S.eq mu mw then are_alpha_convertible err f u w else *) err ()
+ B.get err f m.c i
+
+let xwhd st m t =
+ L.box level; log1 "Now scanning" m.c t;
+ let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in
+ L.unbox level; m, t
+
+let are_convertible st mu u mw w =
+ L.box level; log2 "Now converting" mu.c u mw.c w;
+ let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in
+ L.unbox level; r
+(* let err _ = in
+ if S.eq mu mw then are_alpha_convertible err f u w else err () *)
(* error reporting **********************************************************)
val get: (unit -> 'a) -> (Brg.bind -> 'a) -> kam -> int -> 'a
-val push: (kam -> 'a) -> kam -> Brg.bind -> 'a
+val push: kam -> Brg.bind -> kam
-val xwhd: (kam -> Brg.term -> 'a) -> kam -> Brg.term -> 'a
+val xwhd: Entity.status -> kam -> Brg.term -> kam * Brg.term
(* arguments: expected type, inferred type *)
-val are_convertible:
- (unit -> 'a) -> (unit -> 'a) ->
- ?si:bool -> kam -> Brg.term -> kam -> Brg.term -> 'a
+val are_convertible:
+ Entity.status -> kam -> Brg.term -> kam -> Brg.term -> bool
val specs: (kam, Brg.term) Log.specs
let lift_map h _ a i =
if i + h >= 0 then B.LRef (a, i + h) else assert false
-let lift g h d t =
- if h = 0 then g t else g (iter (lift_map h) d t)
+let lift h d t =
+ if h = 0 then t else iter (lift_map h) d t
-let lift_bind g h d = function
- | B.Void _ as b -> g b
- | B.Abst (a, w) -> let g w = g (B.abst a w) in lift g h d w
- | B.Abbr (a, v) -> let g v = g (B.abbr a v) in lift g h d v
+let lift_bind h d = function
+ | B.Void _ as b -> b
+ | B.Abst (a, w) -> B.abst a (lift h d w)
+ | B.Abbr (a, v) -> B.abbr a (lift h d v)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val lift: (Brg.term -> 'a) -> int -> int -> Brg.term -> 'a
+val lift: int -> int -> Brg.term -> Brg.term
(*
val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a
*)
let error3 err m t1 t2 ?mu t3 =
err (message3 m t1 t2 ?mu t3)
-let assert_convertibility err f ~si m u w v =
- let err _ = error3 err m v w u in
- R.are_convertible err f ~si m u m w
+let assert_convertibility err f st m u w v =
+ if R.are_convertible st m u m w then f () else
+ error3 err m v w u
-let assert_applicability err f ~si m u w v =
- let f mu = function
- | B.Sort _ -> error1 err "not a function type" m u
- | B.Bind (B.Abst (_, u), _) ->
- let err _ = error3 err m v w ~mu u in
- R.are_convertible err f ~si mu u m w
- | _ -> assert false
- in
- R.xwhd f m u
+let assert_applicability err f st m u w v =
+ match R.xwhd st m u with
+ | _, B.Sort _ -> error1 err "not a function type" m u
+ | mu, B.Bind (B.Abst (_, u), _) ->
+ if R.are_convertible st mu u m w then f () else
+ error3 err m v w ~mu u
+ | _ -> assert false (**)
-let rec b_type_of err f ~si g m x =
+let rec b_type_of err f st g m x =
log1 "Now checking" m x;
match x with
| B.Sort (a, h) ->
| B.LRef (_, i) ->
let f = function
| B.Abst (_, w) ->
- S.lift (f x) (succ i) (0) w
+ f x (S.lift (succ i) (0) w)
| B.Abbr (_, B.Cast (_, w, _)) ->
- S.lift (f x) (succ i) (0) w
+ f x (S.lift (succ i) (0) w)
| B.Abbr _ -> assert false
| B.Void _ ->
error1 err "reference to excluded variable" m x
let err _ = error1 err "reference to unknown variable" m x in
R.get err f m i
| B.GRef (_, uri) ->
- let f = function
+ begin match E.get_entity uri with
| _, _, Y.Abst w -> f x w
| _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, Y.Abbr _ -> assert false
- in
- let err _ = error1 err "reference to unknown entry" m x in
- E.get_entity err f uri
+ | _, _, Y.Void ->
+ error1 err "reference to unknown entry" m x
+ end
| B.Bind (B.Abbr (a, v), t) ->
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 m = b_type_of err (f xv) ~si g m t in
- let f xv = R.push (f xv) m (B.abbr a xv) in
+ let f xv m = b_type_of err (f xv) st g m t in
+ let f xv = f xv (R.push m (B.abbr a xv)) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> f (B.Cast ([], vv, xv))
in
- type_of err f ~si g m v
+ type_of err f st g m v
| B.Bind (B.Abst (a, 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 m = b_type_of err (f xu) ~si g m t in
- let f xu _ = R.push (f xu) m (B.abst a xu) in
- type_of err f ~si g m u
+ let f xu m = b_type_of err (f xu) st g m t in
+ let f xu _ = f xu (R.push m (B.abst a xu)) in
+ type_of err f st g m u
| B.Bind (B.Void a as b, t) ->
let f xt tt =
f (A.sh1 t xt x (B.bind b)) (B.bind b tt)
in
- let f m = b_type_of err f ~si g m t in
- R.push f m b
+ b_type_of err f st g (R.push m b) t
+
| B.Appl (a, v, t) ->
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
- assert_applicability err f ~si m tt vv xv
+ assert_applicability err f st m tt vv xv
in
- let f xv vv = b_type_of err (f xv vv) ~si g m t in
- type_of err f ~si g m v
+ let f xv vv = b_type_of err (f xv vv) st g m t in
+ type_of err f st g m v
| B.Cast (a, u, t) ->
let f xu xt tt =
let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in
- assert_convertibility err f ~si m xu tt xt
+ assert_convertibility err f st m xu tt xt
in
- let f xu _ = b_type_of err (f xu) ~si g m t in
- type_of err f ~si g m u
+ let f xu _ = b_type_of err (f xu) st g m t in
+ type_of err f st g m u
(* Interface functions ******************************************************)
-and type_of err f ?(si=false) g m x =
+and type_of err f st g m x =
let f t u = L.unbox level; f t u in
- L.box level; b_type_of err f ~si g m x
+ L.box level; b_type_of err f st g m x
val type_of:
(message -> 'a) -> (Brg.term -> Brg.term -> 'a) ->
- ?si:bool -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a
+ Entity.status -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a
(* to share *)
let type_check err f ?(si=false) g = function
| a, uri, Y.Abst t ->
- let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in
- L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t
+ let f xt tt =
+ let e = E.set_entity (a, uri, Y.Abst xt) in f tt e
+ in
+ let st = Y.initial_status si in
+ L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t
| a, uri, Y.Abbr t ->
- let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in
- L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t
+ let f xt tt =
+ let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e
+ in
+ let st = Y.initial_status si in
+ L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t
+ | _, _, Y.Void -> assert false
type 'term bind = Abst of 'term (* declaration: domain *)
| Abbr of 'term (* definition: body *)
+ | Void (* exclusion *)
type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
-type uri_generator = string -> string (* this could be in CPS *)
+type uri_generator = string -> string
+
+type status = {
+ delta: bool; (* global delta-expansion *)
+ rt: bool; (* reference typing *)
+ si: bool (* sort inclusion *)
+}
(* helpers ******************************************************************)
let f t = f (a, uri, Abst t) in xlate_term f t
| a, uri, Abbr t ->
let f t = f (a, uri, Abbr t) in xlate_term f t
+ | _, _, Void ->
+ assert false
+
+let initial_status si = {
+ delta = false; rt = false; si = si
+}
(* Internal functions *******************************************************)
-let set_sort f (h:int) (s:string) =
- H.add sort h s; f (succ h)
+let set_sort h s =
+ H.add sort h s; succ h
(* Interface functions ******************************************************)
let set_sorts f ss i =
- C.list_fold_left f set_sort i ss
+ f (List.fold_left set_sort i ss)
let get_sort err f h =
try f (H.find sort h) with Not_found -> err ()
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Format
-module N = Filename
+module F = Filename
module U = NUri
module C = Cps
module H = Hierarchy
let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
let path_of_uri uri =
- N.concat base (Str.string_after (U.string_of_uri uri) 3)
+ F.concat base (Str.string_after (U.string_of_uri uri) 3)
(* interface functions ******************************************************)
let export_entity pp_term si g (a, u, b) =
let path = path_of_uri u in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let och = open_out (path ^ obj_ext) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out root system;
let attrs = [uri u; name a; mark a] in
let contents = match b with
| Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
- | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+ | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+ | Y.Void -> assert false
in
let opts = if si then "si" else "" in
let shp = H.string_of_graph C.start g in
let f w =
let a = [Y.Name (id, true)] in
let f t = f (B.Bind (B.abst a w, t)) in
- let f c = xlate_term c f t in
- B.push f c (B.abst a w)
+ xlate_term (B.push c (B.abst a w)) f t
in
xlate_term c f w
let xlate_pars f pars =
let map f (id, w) c =
let a = [Y.Name (id, true)] in
- let f w = B.push f c (B.abst a w) in
+ let f w = f (B.push c (B.abst a w)) in
xlate_term c f w
in
C.list_fold_right f map pars B.empty_lenv
let unwind_to_xlate_term f c t =
- let map f t b = f (B.bind b t) in
- let f t = B.fold_left f map t c in
+ let map t b = B.bind b t in
+ let f t = f (B.fold_left map t c) in
xlate_term c f t
let xlate_entry f = function
let f c = count_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
+ | _, _, Y.Void -> assert false
let print_counters f c =
let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
(Y.mark C.err C.start a) (U.string_of_uri uri)
pp_pars pars (pp_body a) body pp_term u
+ | _, _, Y.Void -> assert false
let pp_entity f frm entity =
pp_entity frm entity; f ()
ast = AP.initial_status
}
-let count count_fun c entity =
- if !L.level > 2 then count_fun C.start c entity else c
-
let flush_all () = L.flush 0; L.flush_err ()
let bag_error s msg =
let brg_error s msg =
L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
-let process_entity f st =
+let process_entity f st entity =
let f ast = f {st with ast = ast} in
- AP.process_entity f st.ast
+ AP.process_entity f st.ast entity
(* kernel related ***********************************************************)
| Brg -> BrgO.print_counters C.start st.brgc
| Bag -> BagO.print_counters C.start st.bagc
-let xlate f st entity = match !kernel, entity with
+let xlate_entity entity = match !kernel, entity with
| Brg, CrgEntity e ->
- let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
+ let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
| Brg, MetaEntity e ->
- let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+ let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
| Bag, MetaEntity e ->
- let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e
- | _, entity -> f st entity
+ let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e
+ | _, entity -> entity
let pp_progress e =
let f a u =
| MetaEntity e -> Y.common f e
let count_entity st = function
- | MetaEntity e -> {st with mc = count MO.count_entity st.mc e}
- | BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e}
- | BagEntity e -> {st with bagc = count BagO.count_entity st.bagc e}
+ | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e}
+ | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e}
+ | BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e}
| _ -> st
let export_entity si g moch = function
end
| BagEntity _ -> ()
-let type_check f st si g k =
+let type_check st si g k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
- let ok _ _ = f st in
+ let ok _ _ = st in
match k with
| BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
| BagEntity entity -> BagU.type_check ok ~si g entity
| CrgEntity _
- | MetaEntity _ -> f st
+ | MetaEntity _ -> st
(****************************************************************************)
let graph = ref (H.graph_of_string C.err C.start "Z2")
let old = ref false
-let process_3 f st =
- f st
-
-let process_2 f st entity =
- let st = count_entity st entity in
+let process_2 st entity =
+ let st = if !L.level > 2 then count_entity st entity else st in
if !export then export_entity !si !graph !moch entity;
- if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st
+ if !stage > 2 then type_check st !si !graph entity else st
-let process_1 f st entity =
+let process_1 st entity =
if !progress then pp_progress entity;
- let st = count_entity st entity in
+ let st = if !L.level > 2 then count_entity st entity else st in
if !export && !stage = 1 then export_entity !si !graph !moch entity;
- if !stage > 1 then xlate (process_2 f) st entity else f st
+ if !stage > 1 then process_2 st (xlate_entity entity) else st
-let process_0 f st entity =
+let process_0 st entity =
let f st entity =
- if !stage = 0 then f st else
- let frr mst = f {st with mst = mst} in
- let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in
- let err dst = f {st with dst = dst} in
- let g dst e = process_1 f {st with dst = dst} (CrgEntity e) in
+ if !stage = 0 then st else
+ let frr mst = {st with mst = mst} in
+ let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
+ let err dst = {st with dst = dst} in
+ let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
if !old then MA.meta_of_aut frr h st.mst entity else
DA.crg_of_aut err g st.dst entity
in
- let st = {st with ac = count AO.count_entity st.ac entity} in
+ let st =
+ if !L.level > 2 then {st with ac = AO.count_entity C.start st.ac entity}
+ else st
+ in
if !preprocess then process_entity f st entity else f st entity
-let rec process f book st = match book with
- | [] -> f st
- | entity :: tl ->
-(* we exploit tail recursion rather than CPS *)
- process f tl (process_0 C.start st entity)
+let rec process st = function
+ | [] -> st
+ | entity :: tl -> process (process_0 st entity) tl
(****************************************************************************)
| Bag -> Bag.mk_uri
in
let cover = if !use_cover then base_name else "" in
- let f st =
- 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 && !preprocess then AO.print_process_counters C.start st.ast;
- if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
- if !L.level > 2 && !stage > 1 then print_counters st;
- if !L.level > 2 && !stage > 1 then O.print_reductions ()
- in
- process f book (initial_status mk_uri cover)
+ let st = process (initial_status mk_uri cover) book in
+ if !L.level > 0 then T.utime_stamp "processed";
+ if !L.level > 2 then begin
+ AO.print_counters C.start st.ac;
+ if !preprocess then AO.print_process_counters C.start st.ast;
+ if !stage > 0 then MO.print_counters C.start st.mc;
+ if !stage > 1 then print_counters st;
+ if !stage > 2 then O.print_reductions ()
+ end
in
let exit () =
close !moch;
projects / helm.git / commitdiff