lib/nUri.cmo: lib/nUri.cmi
lib/nUri.cmx: lib/nUri.cmi
-lib/log.cmo: lib/log.cmi
-lib/log.cmx: lib/log.cmi
+lib/log.cmo: lib/cps.cmx lib/log.cmi
+lib/log.cmx: lib/cps.cmx lib/log.cmi
lib/time.cmo: lib/log.cmi
lib/time.cmx: lib/log.cmx
automath/autOutput.cmi: automath/aut.cmx
automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx
basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx
basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx
-basic_rg/brgOutput.cmi: basic_rg/brg.cmx
-basic_rg/brgOutput.cmo: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi
-basic_rg/brgOutput.cmx: lib/log.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx
basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
-basic_rg/brgReduction.cmi: basic_rg/brg.cmx
-basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/cps.cmx \
+basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx
+basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi lib/cps.cmx \
basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi
-basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/cps.cmx \
+basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx lib/cps.cmx \
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi
-basic_rg/brgType.cmi: basic_rg/brgReduction.cmi basic_rg/brg.cmx
-basic_rg/brgType.cmo: basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi \
- basic_rg/brg.cmx basic_rg/brgType.cmi
-basic_rg/brgType.cmx: basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx \
- basic_rg/brg.cmx basic_rg/brgType.cmi
+basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brg.cmx
+basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \
+ basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi
+basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \
+ basic_rg/brgReduction.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
+basic_rg/brgType.cmi: lib/log.cmi basic_rg/brgReduction.cmi basic_rg/brg.cmx
+basic_rg/brgType.cmo: lib/log.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
+ basic_rg/brgType.cmi
+basic_rg/brgType.cmx: lib/log.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
+ basic_rg/brgType.cmi
basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx
basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgReduction.cmi \
- basic_rg/brgEnvironment.cmi basic_rg/brgUntrusted.cmi
+ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgReduction.cmx \
- basic_rg/brgEnvironment.cmx basic_rg/brgUntrusted.cmi
+ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.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
toplevel/metaBrg.cmi
toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
toplevel/metaBrg.cmi
-toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \
- toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
- basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \
- automath/autLexer.cmx
-toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \
- toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
- basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \
- automath/autLexer.cmx
+toplevel/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \
+ toplevel/metaBrg.cmi toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx \
+ basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \
+ automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
+toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.cmx \
+ toplevel/metaBrg.cmx toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx \
+ basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \
+ automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
test: $(MAIN).opt
@echo " HELENA automath/*.aut"
$(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt
+
+meta: $(MAIN).opt
+ @echo " HELENA -m meta.txt automath/*.aut"
+ $(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 automath/*.aut > /dev/null
+
+ifeq ($(MAKECMDGOALS), test)
+ include .depend.opt
+endif
+
+ifeq ($(MAKECMDGOALS), meta)
+ include .depend.opt
+endif
ifeq ($(MAKECMDGOALS), $(MAIN).opt)
include .depend.opt
endif
-
-ifeq ($(MAKECMDGOALS), test)
- include .depend.opt
-endif
-brg brgOutput brgEnvironment brgReduction brgType brgUntrusted
+brg brgEnvironment brgReduction brgOutput brgType brgUntrusted
type uri = NUri.uri
type id = Aut.id
-type bind = Abst | Abbr (* abstraction, abbreviation *)
+type bind = Void (* exclusion *)
+ | Abst of term (* abstraction *)
+ | Abbr of term (* abbreviation *)
-type term = Sort of int (* hierarchy index *)
- | LRef of int (* reverse de Bruijn index *)
- | GRef of uri (* reference *)
- | Cast of term * term (* type, term *)
- | Appl of term * term (* argument, function *)
- | Bind of id * bind * term * term (* name, binder, content, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of int (* reverse de Bruijn index *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* type, term *)
+ | Appl of term * term (* argument, function *)
+ | Bind of id * bind * term (* name, binder, scope *)
-type obj = int * uri * bind * term (* age, uri, binder, contents *)
+type obj = int * uri * bind (* age, uri, binder, contents *)
type item = obj option
(* Currified constructors ***************************************************)
+let abst w = Abst w
+
+let abbr v = Abbr v
+
let cast u t = Cast (u, t)
let appl u t = Appl (u, t)
-let bind id b u t = Bind (id, b, u, t)
+let bind id b t = Bind (id, b, t)
(* Interface functions ******************************************************)
let set_obj f obj =
- let _, uri, b, t = obj in
- let obj = !entry, uri, b, t in
+ let _, uri, b = obj in
+ let obj = !entry, uri, b in
incr entry; H.add env uri obj; f obj
let get_obj f uri =
V_______________________________________________________________ *)
module P = Printf
+module F = Format
+module U = NUri
+module C = Cps
module L = Log
module B = Brg
+module R = BrgReduction
type counters = {
eabsts: int;
tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
}
-let count_term_binder f c = function
- | B.Abst -> f {c with tabsts = succ c.tabsts}
- | B.Abbr -> f {c with tabbrs = succ c.tabbrs}
+let rec count_term_binder f c = function
+ | B.Abst w ->
+ let c = {c with tabsts = succ c.tabsts} in
+ count_term f c w
+ | B.Abbr v ->
+ let c = {c with tabbrs = succ c.tabbrs} in
+ count_term f c v
+ | B.Void -> f c
-let rec count_term f c = function
+and count_term f c = function
| B.Sort _ ->
f {c with tsorts = succ c.tsorts}
| B.LRef _ ->
let c = {c with tappls = succ c.tappls} in
let f c = count_term f c t in
count_term f c v
- | B.Bind (_, b, u, t) ->
+ | B.Bind (_, b, t) ->
let f c = count_term_binder f c b in
- let f c = count_term f c t in
- count_term f c u
+ count_term f c t
let count_obj_binder f c = function
- | B.Abst -> f {c with eabsts = succ c.eabsts}
- | B.Abbr -> f {c with eabbrs = succ c.eabbrs}
+ | B.Abst w ->
+ let c = {c with eabsts = succ c.eabsts} in
+ count_term f c w
+ | B.Abbr v ->
+ let c = {c with eabbrs = succ c.eabbrs} in
+ count_term f c v
+ | B.Void -> f c
-let count_obj f c (_, _, b, t) =
- let f c = count_obj_binder f c b in
- count_term f c t
+let count_obj f c (_, _, b) =
+ count_obj_binder f c b
let count_item f c = function
| Some obj -> count_obj f c obj
L.warn (P.sprintf " Abstraction items: %6u" c.tabsts);
L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs);
f ()
+
+let rec pp_term c frm = function
+ | B.Sort h -> F.fprintf frm "@[*%u@]" h
+ | B.LRef i -> F.fprintf frm "@[#%u@]" i
+ | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+ | B.Cast (u, t) ->
+ F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
+ | B.Appl (v, t) ->
+ F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
+ | B.Bind (id, B.Abst w, t) ->
+ F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term c) t
+ | B.Bind (id, B.Abbr v, t) ->
+ F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term c) t
+ | B.Bind (id, B.Void, t) ->
+ F.fprintf frm "@[[%s].%a@]" id (pp_term c) t
+
+let pp_context frm c =
+ let pp_entry f = function
+ | B.Abst w ->
+ F.fprintf frm "%s %a\n%!" "\\decl" (pp_term c) w; f ()
+ | B.Abbr v ->
+ F.fprintf frm "%s %a\n%!" "\\def " (pp_term c) v; f ()
+ | B.Void ->
+ F.fprintf frm "%s\n%!" "\\void"; f ()
+ in
+ R.iter C.start pp_entry c
+
+let pp_term frm c t =
+ F.fprintf frm "%a\n%!" (pp_term c) t
+
+let specs = {
+ L.pp_term = pp_term; L.pp_context = pp_context
+}
val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
+
+val specs: (BrgReduction.context, Brg.term) Log.specs
module U = NUri
module C = Cps
module S = Share
+module L = Log
module B = Brg
module E = BrgEnvironment
-exception LRefNotFound of string Lazy.t
-
-type bind = Void_
- | Abst_ of B.term
- | Abbr_ of B.term
-
-type environment = int * bind list
+type environment = int * B.bind list
type stack = B.term list
s: stack
}
+exception LRefNotFound of (context, B.term) L.item list
+
type whd_result =
| Sort_ of int
| LRef_ of int * B.term option
- | GRef_ of int * B.bind * B.term
+ | GRef_ of int * B.bind
| Bind_ of B.term * B.term
type ho_whd_result =
(* Internal functions *******************************************************)
+let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+
let empty_e = 0, []
let push_e f b (l, e) =
let get_e f c i =
let (gl, ge), (ll, le) = c.g, c.l in
- if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
+ if i >= gl + ll then error i;
let b =
if i < gl then List.nth ge (gl - (succ i))
else List.nth le (gl + ll - (succ i))
in
f b
-let rec lref_map f map t = match t with
- | B.LRef i -> f (B.LRef (map i))
- | B.GRef _ -> f t
- | B.Sort _ -> f t
- | B.Cast (w, u) ->
+let rec lref_map_bind f map b = match b with
+ | B.Abbr v ->
+ let f v' = f (S.sh1 v v' b B.abbr) in
+ lref_map f map v
+ | B.Abst w ->
+ let f w' = f (S.sh1 w w' b B.abst) in
+ lref_map f map w
+ | B.Void -> f b
+
+and lref_map f map t = match t with
+ | B.LRef i -> f (B.LRef (map i))
+ | B.GRef _ -> f t
+ | B.Sort _ -> f t
+ | B.Cast (w, u) ->
let f w' u' = f (S.sh2 w w' u u' t B.cast) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | B.Appl (w, u) ->
+ | B.Appl (w, u) ->
let f w' u' = f (S.sh2 w w' u u' t B.appl) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | B.Bind (id, b, w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in
- let f w' = lref_map (f w') map u in
- lref_map f map w
+ | B.Bind (id, b, u) ->
+ let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in
+ let f b' = lref_map (f b') map u in
+ lref_map_bind f map b
(* to share *)
let lift f c =
let (gl, _), (ll, le) = c.g, c.l in
let map i = if i >= gl then succ i else i in
let map f = function
- | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
+ | B.Abbr t -> let f t' = f (B.Abbr t') in lref_map f map t
| _ -> assert false
in
let f le' = f {c with l = (ll, le')} in
let rec whd f c t = match t with
| B.Sort h -> f c (Sort_ h)
| B.GRef uri ->
- let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
+ let f (i, _, b) = f c (GRef_ (i, b)) in
E.get_obj f uri
- | B.LRef i ->
+ | B.LRef i ->
let f = function
- | Void_ -> f c (LRef_ (i, None))
- | Abst_ t -> f c (LRef_ (i, Some t))
- | Abbr_ t -> whd f c t
+ | B.Void -> f c (LRef_ (i, None))
+ | B.Abst t -> f c (LRef_ (i, Some t))
+ | B.Abbr t -> whd f c t
in
get_e f c i
- | B.Appl (v, t) -> whd f {c with s = v :: c.s} t
- | B.Bind (_, B.Abbr, v, t) ->
- let f l = whd f {c with l = l} t in
- push_e f (Abbr_ v) c.l
- | B.Bind (_, B.Abst, w, t) ->
+ | B.Cast (_, t) -> whd f c t
+ | B.Appl (v, t) -> whd f {c with s = v :: c.s} t
+ | B.Bind (_, B.Abst w, t) ->
begin match c.s with
| [] -> f c (Bind_ (w, t))
| v :: tl ->
let f tl l = whd f {c with l = l; s = tl} t in
- push_e (f tl) (Abbr_ v) c.l
+ push_e (f tl) (B.Abbr v) c.l
end
- | B.Cast (_, t) -> whd f c t
+ | B.Bind (_, b, t) ->
+ let f l = whd f {c with l = l} t in
+ push_e f b c.l
let push f c t =
assert (c.s = []);
let f c g = xchg f {c with g = g} t in
- let f c = push_e (f c) Void_ c.g in
+ let f c = push_e (f c) B.Void c.g in
lift f c
(* Interface functions ******************************************************)
let rec are_convertible f c1 t1 c2 t2 =
let rec aux c1' r1 c2' r2 = match r1, r2 with
- | Sort_ h1, Sort_ h2 -> f (h1 = h2)
- | LRef_ (i1, _), LRef_ (i2, _) ->
+ | Sort_ h1, Sort_ h2 -> f (h1 = h2)
+ | LRef_ (i1, _), LRef_ (i2, _) ->
if i1 = i2 then are_convertible_stacks f c1' c2' else f false
- | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _) ->
+ | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) ->
if a1 = a2 then are_convertible_stacks f c1' c2' else f false
- | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
+ | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
if a1 = a2 then are_convertible_stacks f c1' c2' else
if a1 < a2 then whd (aux c1' r1) c2' v2 else
whd (aux_rev c2' r2) c1' v1
- | _, GRef_ (_, B.Abbr, v2) ->
+ | _, GRef_ (_, B.Abbr v2) ->
whd (aux c1' r1) c2' v2
- | GRef_ (_, B.Abbr, v1), _ ->
+ | GRef_ (_, B.Abbr v1), _ ->
whd (aux_rev c2' r2) c1' v1
- | Bind_ (w1, t1), Bind_ (w2, t2) ->
+ | Bind_ (w1, t1), Bind_ (w2, t2) ->
let f b =
if b then
let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
let rec ho_whd f c t =
let aux c' = function
- | Sort_ h -> f c' (Sort h)
- | Bind_ (w, t) -> f c' (Abst w)
- | LRef_ (_, Some w) -> ho_whd f c w
- | GRef_ (_, _, u) -> ho_whd f c u
- | LRef_ (_, None) -> assert false
+ | Sort_ h -> f c' (Sort h)
+ | Bind_ (w, t) -> f c' (Abst w)
+ | LRef_ (_, Some w) -> ho_whd f c w
+ | GRef_ (_, B.Abst u) -> ho_whd f c u
+ | GRef_ (_, B.Abbr u) -> ho_whd f c u
+ | LRef_ (_, None) -> assert false
+ | GRef_ (_, B.Void) -> assert false
in
whd aux c t
-let push f c b t =
+let push f c b =
assert (c.l = empty_e && c.s = []);
let f g = f {c with g = g} in
- let b = match b with
- | B.Abbr -> Abbr_ t
- | B.Abst -> Abst_ t
- in
push_e f b c.g
let get f c i =
let gl, ge = c.g in
- if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
- match List.nth ge (gl - (succ i)) with
- | Abbr_ v -> f (B.Abbr, v)
- | Abst_ w -> f (B.Abst, w)
- | Void_ -> assert false
+ if i >= gl then error i;
+ f (List.nth ge (gl - (succ i)))
let empty_context = {
g = empty_e; l = empty_e; s = []
}
+
+let iter f map c =
+ let _, ge = c.g in
+ C.list_iter f map ge
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-exception LRefNotFound of string Lazy.t
-
type context
+exception LRefNotFound of (context, Brg.term) Log.item list
+
type ho_whd_result =
| Sort of int
| Abst of Brg.term
val empty_context: context
-val push: (context -> 'a) -> context -> Brg.bind -> Brg.term -> 'a
+val push: (context -> 'a) -> context -> Brg.bind -> 'a
+
+val get: (Brg.bind -> 'a) -> context -> int -> 'a
-val get: (Brg.bind * Brg.term -> 'a) -> context -> int -> 'a
+val iter: (unit -> 'a) -> ((unit -> 'a) -> Brg.bind -> 'a) -> context -> 'a
val are_convertible: (bool -> 'a) -> context -> Brg.term -> Brg.term -> 'a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module L = Log
module B = Brg
+module O = BrgOutput
module E = BrgEnvironment
module R = BrgReduction
-exception TypeError of string Lazy.t
+exception TypeError of (R.context, B.term) Log.item list
(* Internal functions *******************************************************)
-let error msg = raise (TypeError (lazy msg))
+let error1 s c t =
+ raise (TypeError (L.ct_items1 s c t))
+
+let error2 s1 c1 t1 s2 c2 t2 =
+ raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2))
+
+let are_convertible f c t1 t2 =
+ L.log O.specs 4 (L.ct_items2 "Now converting" c t1 "and" c t2);
+ R.are_convertible f c t1 t2
(* Interface functions ******************************************************)
-let rec type_of f g c = function
- | B.Sort h -> f (B.Sort (g h))
- | B.LRef i ->
+let rec type_of f g c x =
+ L.log O.specs 5 (L.ct_items1 "now checking" c x);
+ match x with
+ | B.Sort h -> f (B.Sort (g h))
+ | B.LRef i ->
let f = function
- | B.Abst, w -> f w
- | B.Abbr, B.Cast (w, v) -> f w
- | B.Abbr, _ -> error "lref"
+ | B.Abst w -> f w
+ | B.Abbr (B.Cast (w, v)) -> f w
+ | B.Abbr _ -> assert false
+ | B.Void -> assert false
in
R.get f c i
- | B.GRef uri ->
+ | B.GRef uri ->
let f = function
- | _, _, B.Abst, w -> f w
- | _, _, B.Abbr, B.Cast (w, v) -> f w
- | _, _, B.Abbr, _ -> error "gref"
+ | _, _, B.Abst w -> f w
+ | _, _, B.Abbr (B.Cast (w, v)) -> f w
+ | _, _, B.Abbr _ -> assert false
+ | _, _, B.Void -> assert false
in
E.get_obj f uri
- | B.Bind (id, b, u, t) ->
- let f uu tt = match b, t with
- | B.Abst, _
- | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
- | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt))
+ | B.Bind (id, B.Abbr u, t) ->
+ let f tt = f (B.Bind (id, B.Abbr u, tt)) in
+ let f cc = type_of f g cc t in
+ let f u = R.push f c (B.Abbr u) in
+ let f uu = match u with
+ | B.Cast _ -> f u
+ | _ -> f (B.Cast (uu, u))
in
- let f uu cc = type_of (f uu) g cc t in
- let f uu = R.push (f uu) c b u in
type_of f g c u
- | B.Appl (v, t) ->
+ | B.Bind (id, B.Abst u, t) ->
+ let f tt = f (B.Bind (id, B.Abst u, tt)) in
+ let f cc = type_of f g cc t in
+ let f _ = R.push f c (B.Abst u) in
+ type_of f g c u
+ | B.Bind (id, B.Void, t) ->
+ let f tt = f (B.Bind (id, B.Void, tt)) in
+ let f cc = type_of f g cc t in
+ R.push f c B.Void
+ | B.Appl (v, t) ->
let f tt cc = function
- | R.Sort _ -> error "appl"
+ | R.Sort _ -> error1 "not a function" c t
| R.Abst w ->
- let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in
- type_of (R.are_convertible f cc w) g c v
+ let f b =
+ if b then f (B.Appl (v, tt)) else
+ error2 "the term" c v "must be of type" cc w
+ in
+ type_of (are_convertible f cc w) g c v
in
let f tt = R.ho_whd (f tt) c t in
type_of f g c t
- | B.Cast (u, t) ->
- let f b = if b then f u else error "cast" in
- let f _ = type_of (R.are_convertible f c u) g c t in
+ | B.Cast (u, t) ->
+ let f b =
+ if b then f u else
+ error2 "the term" c t "must be of type" c u
+ in
+ let f _ = type_of (are_convertible f c u) g c t in
type_of f g c u
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-exception TypeError of string Lazy.t
+exception TypeError of (BrgReduction.context, Brg.term) Log.item list
val type_of: (Brg.term -> 'a) ->
Brg.hierarchy -> BrgReduction.context -> Brg.term -> 'a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module B = Brg
module E = BrgEnvironment
module R = BrgReduction
module T = BrgType
(* Interface functions ******************************************************)
let type_check f g = function
- | None -> f None
- | Some ((_, _, _, t) as obj) ->
+ | None -> f None
+ | Some ((_, _, B.Abst t) as obj)
+ | Some ((_, _, B.Abbr t) as obj) ->
let f tt obj = f (Some (tt, obj)) in
let f tt = E.set_obj (f tt) obj in
T.type_of f g R.empty_context t
+ | Some (_, _, B.Void) -> assert false
let list_map f =
list_rev_map (list_rev f)
+let list_iter f map l =
+ let map f () x = map f x in
+ list_fold_left f map () l
V_______________________________________________________________ *)
module P = Printf
+module F = Format
+module C = Cps
+
+type ('a, 'b) item = Term of 'a * 'b
+ | Context of 'a
+ | Warn of string
+ | String of string
+
+type ('a, 'b) specs = {
+ pp_term : F.formatter -> 'a -> 'b -> unit;
+ pp_context: F.formatter -> 'a -> unit
+}
+
+let level = ref 0
+
+(* Internal functions *******************************************************)
let init =
let started = ref false in
if !started then () else
begin P.printf "\n"; started := true end
+let pp_items frm st l items =
+ let pp_item = function
+ | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t
+ | Context c -> st.pp_context frm c
+ | Warn s -> F.fprintf frm "@[%s\n@]" s
+ | String s -> F.fprintf frm "@[%s @]" s
+ in
+ if !level >= l then List.iter pp_item items
+
+(* Interface functions ******************************************************)
+
let warn msg =
init (); P.printf " %s\n" msg; flush stdout
+
+let log st l items = pp_items F.std_formatter st l items
+
+let error st items = pp_items F.err_formatter st 0 items
+
+let items1 s = [Warn s]
+
+let ct_items1 s c t =
+ [Warn s; Term (c, t)]
+
+let ct_items2 s1 c1 t1 s2 c2 t2 =
+ [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+type ('a, 'b) item = Term of 'a * 'b
+ | Context of 'a
+ | Warn of string
+ | String of string
+
+type ('a, 'b) specs = {
+ pp_term : Format.formatter -> 'a -> 'b -> unit;
+ pp_context: Format.formatter -> 'a -> unit
+}
+
+val level: int ref
+
val warn: string -> unit
+
+val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit
+
+val error: ('a, 'b) specs -> ('a, 'b) item list -> unit
+
+val items1: string -> ('a, 'b) item list
+
+val ct_items1: string -> 'a -> 'b -> ('a, 'b) item list
+
+val ct_items2: string -> 'a -> 'b -> string -> 'a -> 'b -> ('a, 'b) item list
let sh a b =
if a == b then a else b
-
-let sh2 a1 b1 a2 b2 c1 c2 =
+
+let sh1 a1 a2 b1 b2 =
+ if a1 == a2 then b1 else b2 (sh a1 a2)
+
+let sh2 a1 a2 b1 b2 c1 c2 =
if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)
let map_args f t v = f (B.Appl (v, t))
-let map_pars f t (id, w) = f (B.Bind (id, B.Abst, w, t))
+let map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t))
let rec xlate_term f = function
| M.Sort s ->
let f h = f (B.Sort h) in
if s then f 0 else f 1
| M.LRef (l, i) ->
- f (B.LRef (l - i))
+ f (B.LRef (l - succ i))
| M.GRef (_, uri, vs) ->
let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in
- Cps.list_rev_map f xlate_term vs
+ Cps.list_map f xlate_term vs
| M.Appl (v, t) ->
let f v t = f (B.Appl (v, t)) in
let f v = xlate_term (f v) t in
xlate_term f v
| M.Abst (id, w, t) ->
- let f w t = f (B.Bind (id, B.Abst, w, t)) in
+ let f w t = f (B.Bind (id, B.Abst w, t)) in
let f w = xlate_term (f w) t in
xlate_term f w
let xlate_entry f = function
| e, pars, uri, u, None ->
- let f u = f (e, uri, B.Abst, u) in
+ let f u = f (e, uri, B.Abst u) in
let f pars = map_fold_left f xlate_term map_pars u pars in
- Cps.list_rev_map f xlate_pars pars
+ Cps.list_map f xlate_pars pars
| e, pars, uri, u, Some (_, t) ->
- let f u t = f (e, uri, B.Abbr, (B.Cast (u, t))) in
+ let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in
let f pars u = map_fold_left (f u) xlate_term map_pars t pars in
let f pars = map_fold_left (f pars) xlate_term map_pars u pars in
- Cps.list_rev_map f xlate_pars pars
+ Cps.list_map f xlate_pars pars
let xlate_item f = function
| None -> f None
in
if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
+let pp_rev_list pp opend sep closed frm l =
+ pp_list pp opend sep closed frm (List.rev l)
+
let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
and pp_term frm = function
let pp_par frm (id, w) =
F.fprintf frm "%s:%a" id pp_term w
-let pp_pars = pp_list pp_par "[" "," "]"
+let pp_pars = pp_rev_list pp_par "[" "," "]"
let pp_body frm = function
| None -> ()
V_______________________________________________________________ *)
module P = Printf
+module U = NUri
module L = Log
module AO = AutOutput
module MA = MetaAut
module BrgU = BrgUntrusted
type status = {
- summary: int;
mst : MA.status;
ac : AO.counters;
mc : MO.counters;
brgc: BrgO.counters
}
-let initial_status summary = {
- summary = summary;
+let initial_status = {
ac = AO.initial_counters;
mc = MO.initial_counters;
brgc= BrgO.initial_counters;
mst = MA.initial_status
}
-let count st count_fun c item =
- if st.summary > 2 then count_fun Cps.start c item else c
+let count count_fun c item =
+ if !L.level > 2 then count_fun Cps.start c item else c
+
+let brg_error s msg =
+ L.error BrgO.specs (L.Warn s :: msg)
let main =
+try
let version_string = "Helena Checker 0.8.0 M - December 2008" in
- let summary = ref 0 in
let stage = ref 3 in
let meta_file = ref None in
let hierarchy = ref (fun h -> h + 2) in
- let set_summary i = summary := i in
+ let set_summary i = L.level := i in
let print_version () = L.warn version_string; exit 0 in
let set_stage i = stage := i in
let close = function
meta_file := Some (och, frm)
in
let read_file name =
- if !summary > 0 then Time.gmtime version_string;
- if !summary > 1 then
+ if !L.level > 0 then Time.gmtime version_string;
+ if !L.level > 1 then
L.warn (P.sprintf "Processing file: %s" name);
- if !summary > 0 then Time.utime_stamp "started";
+ if !L.level > 0 then Time.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 !summary > 0 then Time.utime_stamp "parsed";
+ if !L.level > 0 then Time.utime_stamp "parsed";
let rec aux st = function
| [] -> st
| item :: tl ->
(* stage 3 *)
let f st = function
- | None -> st
- | Some (_, (i, _, _, _)) ->
- Log.warn (string_of_int i); st
+ | None -> st
+ | Some (_, (i, u, _)) ->
+ Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st
in
(* stage 2 *)
let f st item =
- let st = {st with brgc = count st BrgO.count_item st.brgc item} in
+ let st = {st with brgc = count BrgO.count_item st.brgc item} in
if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st
in
(* stage 1 *)
let f mst item =
let st = {st with
- mst = mst; mc = count st MO.count_item st.mc item
+ mst = mst; mc = count MO.count_item st.mc item
} in
begin match !meta_file with
| None -> ()
if !stage > 1 then MBrg.brg_of_meta (f st) item else st
in
(* stage 0 *)
- let st = {st with ac = count st AO.count_item st.ac item} in
+ 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
in
aux st tl
in
- let st = aux (initial_status !summary) book in
- if !summary > 0 then Time.utime_stamp "processed";
- if !summary > 2 then AO.print_counters Cps.start st.ac;
- if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
- if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
+ let st = aux initial_status book in
+ if !L.level > 0 then Time.utime_stamp "processed";
+ if !L.level > 2 then AO.print_counters Cps.start st.ac;
+ if !L.level > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
+ if !L.level > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
in
let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
let help_S = "<number> Set summary level" in
("-m", Arg.String set_meta_file, help_m);
("-s", Arg.Int set_stage, help_s);
] read_file help;
- if !summary > 0 then Time.utime_stamp "at exit"
+ if !L.level > 0 then Time.utime_stamp "at exit"
+with BrgType.TypeError msg -> brg_error "Type Error" msg
projects / helm.git / commitdiff