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_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
basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx
basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
basic_rg/brgReduction.cmi
basic_rg/brgType.cmi: lib/hierarchy.cmi basic_rg/brg.cmx
-basic_rg/brgType.cmo: lib/log.cmi lib/hierarchy.cmi basic_rg/brgReduction.cmi \
- basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
+basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
+ lib/hierarchy.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \
+ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx automath/autItem.cmx \
basic_rg/brgType.cmi
-basic_rg/brgType.cmx: lib/log.cmx lib/hierarchy.cmx basic_rg/brgReduction.cmx \
- basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
+basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
+ lib/hierarchy.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \
+ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx automath/autItem.cmx \
basic_rg/brgType.cmi
basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx
basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \
-aut autOutput autParser autLexer
+aut autOutput autParser autLexer autItem
--- /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 bind id b t = Bind (id, b, t)
+let bind_abst id u t = Bind (id, Abst u, t)
+
+let bind_abbr id v t = Bind (id, Abbr v, t)
+
(* context handling functions ***********************************************)
let empty_context = 0, []
tabbrs: int
}
+let indexes = ref false
+
let initial_counters = {
eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
| Some (id, _) -> F.fprintf frm "@[%s@]" id
| None -> F.fprintf frm "@[#%u@]" i
in
- B.get f c i
+ if !indexes then f None else B.get f c 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.push f c id B.Void
let pp_context frm c =
- let pp_entry f = function
+ let pp_entry frm = function
| id, B.Abst w ->
- F.fprintf frm "%s : %a\n%!" id (pp_term c) w; f ()
+ F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w
| id, B.Abbr v ->
- F.fprintf frm "%s = %a\n%!" id (pp_term c) v; f ()
+ F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v
| id, B.Void ->
- F.fprintf frm "%s\n%!" id; f ()
+ F.fprintf frm "@,%s" id
in
- let f _ es = C.list_iter C.start pp_entry (List.rev es) in
+ let iter map frm l = List.iter (map frm) l in
+ let f _ es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
B.contents f 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 print_counters: (unit -> 'a) -> counters -> 'a
val specs: (Brg.context, Brg.term) Log.specs
+
+val indexes: bool ref
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module U = NUri
+module S = Share
module L = Log
module H = Hierarchy
+module I = AutItem
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
let error2 s1 c1 t1 s2 c2 t2 =
raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2))
+let mk_gref u l =
+ let map t v = B.Appl (v, t) in
+ List.fold_left map (B.GRef u) l
+
(* Interface functions ******************************************************)
-let rec type_of f g c x =
- L.log O.specs level (L.ct_items1 "now checking" c x);
+let rec b_type_of f g c x =
+ L.log O.specs level (L.ct_items1 "Now checking" c x);
match x with
| B.Sort h ->
- let f h = f (B.Sort h) in H.apply f g h
+ let f h = f x (B.Sort h) in H.apply f g h
| B.LRef i ->
let f = function
- | Some (_, B.Abst w) -> f w
- | Some (_, B.Abbr (B.Cast (w, v))) -> f w
+ | Some (_, B.Abst w) -> f x w
+ | Some (_, B.Abbr (B.Cast (w, v))) -> f x w
| Some (_, B.Abbr _) -> assert false
| Some (_, B.Void) ->
error1 "reference to excluded variable" c x
B.get f c i
| B.GRef uri ->
let f = function
- | _, _, B.Abst w -> f w
- | _, _, B.Abbr (B.Cast (w, v)) -> f w
+ | _, _, B.Abst w -> f x w
+ | _, _, B.Abbr (B.Cast (w, v)) -> f x w
| _, _, B.Abbr _ -> assert false
| _, _, B.Void ->
error1 "reference to excluded object" c x
in
- E.get_obj f uri
- | 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 = B.push f c id (B.Abbr u) in
- let f uu = match u with
- | B.Cast _ -> f u
- | _ -> f (B.Cast (uu, u))
+ E.get_obj f uri
+ | B.Bind (id, B.Abbr v, t) ->
+ let f xv xt tt =
+ f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv tt)
in
- type_of f g c u
+ let f xv cc = b_type_of (f xv) g cc t in
+ let f xv = B.push (f xv) c 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
| 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 _ = B.push f c id (B.Abst u) in
+ let f xu xt tt =
+ f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu tt)
+ in
+ let f xu cc = b_type_of (f xu) g cc t in
+ let f xu _ = B.push (f xu) c id (B.Abst xu) 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
- B.push f c id B.Void
+ let f xt tt =
+ f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void tt)
+ in
+ let f cc = b_type_of f g cc t in
+ B.push f c id B.Void
| B.Appl (v, t) ->
- let f tt cc = function
- | R.Sort _ -> error1 "not a function" c t
+ let h xv vv xt tt cc = function
+ | R.Sort _ -> error1 "not a function" c xt
| R.Abst w ->
L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
let f b =
- if b then f (B.Appl (v, tt)) else
- error2 "the term" c v "must be of type" cc w
+ if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else
+ error2 "the term" cc xv "must be of type" cc w
in
- type_of (R.are_convertible f cc w) g c v
+ R.are_convertible f cc w vv
+ in
+ let f xv vv xt = function
+(* inserting a missing "modus ponens" *)
+ | B.Appl (y2, B.Appl (y1, B.GRef u)) when U.eq u I.imp ->
+ b_type_of f g c (mk_gref I.mp [y1; y2; xv; xt])
+ | tt -> R.ho_whd (h xv vv xt tt) c tt
in
- let f tt = R.ho_whd (f tt) c t in
- type_of f g c t
+ 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 b =
- if b then f u else
- error2 "the term" c t "must be of type" c u
+ let f xu xt b =
+ if b then f (S.sh2 u xu t xt x B.cast) xu else
+ error2 "the term" c xt "must be of type" c xu
in
- let f _ = type_of (R.are_convertible f c u) g c t in
+ let f xu xt tt = R.are_convertible (f xu xt) c xu tt in
+ let f xu _ = b_type_of (f xu) g c t in
type_of f g c u
+
+and type_of f g c x =
+ let f t u = L.unbox (); f t u in
+ L.box (); b_type_of f g c x
exception TypeError of Brg.message
val type_of:
- (Brg.term -> 'a) -> Hierarchy.graph -> Brg.context -> Brg.term -> 'a
+ (Brg.term -> Brg.term -> 'a) ->
+ Hierarchy.graph -> Brg.context -> Brg.term -> 'a
(* Interface functions ******************************************************)
+(* to share *)
let type_check f g = function
- | 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 B.empty_context t
- | Some (_, _, B.Void) -> assert false
+ | 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
+ 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
+ | Some (a, uri, B.Void) ->
+ let f obj = f None (Some obj) in
+ E.set_obj f (a, uri, B.Void)
V_______________________________________________________________ *)
val type_check:
- ((Brg.term * Brg.obj) option -> 'a) -> Hierarchy.graph -> Brg.item -> 'a
+ (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a
| String of string
type ('a, 'b) specs = {
- pp_term : F.formatter -> 'a -> 'b -> unit;
+ pp_term : 'a -> F.formatter -> 'b -> unit;
pp_context: F.formatter -> 'a -> unit
}
(* Internal functions *******************************************************)
+let std = F.std_formatter
+
+let err = F.err_formatter
+
let init =
let started = ref false in
fun () ->
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
+ let pp_item frm = function
+ | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t
+ | Context c -> F.fprintf frm "%a" st.pp_context c
+ | Warn s -> F.fprintf frm "@,%s" s
+ | String s -> F.fprintf frm "%s " s
in
- if !level >= l then List.iter pp_item items
+ let iter map frm l = List.iter (map frm) l in
+ if !level >= l then F.fprintf frm "%a" (iter pp_item) items
(* Interface functions ******************************************************)
+(*
let warn msg =
init (); P.printf " %s\n" msg; flush stdout
+*)
+let box () = F.fprintf std "@,@[<v 2>%s" " "; F.pp_print_if_newline std ()
+
+let unbox () = F.fprintf std "@]"
-let log st l items = pp_items F.std_formatter st l items
+let flush () = F.fprintf std "@]@."
-let error st items = pp_items F.err_formatter st 0 items
+let box_err () = F.fprintf err "@[<v>"
+
+let flush_err () = F.fprintf err "@]@."
+
+let log st l items = pp_items std st l items
+
+let error st items = pp_items err st 0 items
let items1 s = [Warn s]
let ct_items2 s1 c1 t1 s2 c2 t2 =
[Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]
+
+let warn msg = F.fprintf std "@,%s" msg
| String of string
type ('a, 'b) specs = {
- pp_term : Format.formatter -> 'a -> 'b -> unit;
+ pp_term : 'a -> Format.formatter -> 'b -> unit;
pp_context: Format.formatter -> 'a -> unit
}
val warn: string -> unit
+val box: unit -> unit
+
+val unbox: unit -> unit
+
+val flush: unit -> unit
+
+val box_err: unit -> unit
+
+val flush_err: unit -> unit
+
val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit
val error: ('a, 'b) specs -> ('a, 'b) item list -> unit
let count count_fun c item =
if !L.level > 2 then count_fun C.start c item else c
+let flush () = L.flush (); L.flush_err ()
+
let brg_error s msg =
- L.error BrgO.specs (L.Warn s :: msg)
+ L.error BrgO.specs (L.Warn s :: msg); flush ()
let main =
try
| [] -> st
| item :: tl ->
(* stage 3 *)
- let f st = function
- | None -> st
- | Some (_, (i, u, _)) ->
+ let f st _ = function
+ | None -> st
+ | Some (i, u, _) ->
Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st
in
(* stage 2 *)
if !L.level > 2 && !stage > 1 then BrgO.print_counters C.start st.brgc;
in
let help =
- "Usage: helena [ -V | -Ss <number> | -m <file> | -h <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vi | -Ss <number> | -m <file> | -h <string> ] <file> ...\n\n" ^
"Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n"
in
- let help_S = "<number> Set summary level" in
- let help_V = " Show version information" in
+ let help_S = "<number> set summary level" in
+ let help_V = " show version information" in
let help_h = "<string> set type hierarchy" in
+ let help_i = " show local references by index" in
let help_m = "<file> output intermediate representation" in
let help_s = "<number> Set translation stage" in
+ L.box (); L.box_err ();
H.set_new_sorts ignore ["Set"; "Prop"];
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
("-h", Arg.String set_hierarchy, help_h);
+ ("-i", Arg.Set BrgO.indexes, help_i);
("-m", Arg.String set_meta_file, help_m);
("-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 Time.utime_stamp "at exit";
+ flush ()
with BrgType.TypeError msg -> brg_error "Type Error" msg
projects / helm.git / commitdiff