lib/log.cmx: lib/cps.cmx lib/log.cmi
lib/time.cmo: lib/log.cmi
lib/time.cmx: lib/log.cmx
+lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi
+lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi
automath/autOutput.cmi: automath/aut.cmx
automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \
automath/autOutput.cmi
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.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx basic_rg/brg.cmx \
- basic_rg/brgOutput.cmi
-basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx basic_rg/brg.cmx \
- basic_rg/brgOutput.cmi
+basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \
+ lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
+basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \
+ lib/cps.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 lib/log.cmi basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
basic_rg/brgReduction.cmx: lib/share.cmx lib/log.cmx lib/cps.cmx \
basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
basic_rg/brgReduction.cmi
-basic_rg/brgType.cmi: basic_rg/brg.cmx
-basic_rg/brgType.cmo: lib/log.cmi 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.cmi
-basic_rg/brgType.cmx: lib/log.cmx basic_rg/brgReduction.cmx \
+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.cmi
-basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx
+basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx
basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \
basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgEnvironment.cmx \
toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
toplevel/metaBrg.cmi
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/metaBrg.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 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
+ toplevel/metaBrg.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 automath/autParser.cmx automath/autOutput.cmx \
+ automath/autLexer.cmx
meta: $(MAIN).opt
@echo " HELENA -m meta.txt automath/*.aut"
$(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 automath/*.aut > /dev/null
+ $(H)$(GZIP) meta.txt
ifeq ($(MAKECMDGOALS), test)
include .depend.opt
OCAMLDEP = ocamlfind ocamldep -native $(INCLUDES)
OCAMLOPT = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES)
-OCAMLLEX = ocamllex
+OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
TAR = tar -czf $(MAIN:%=%.tgz)
+GZIP = gzip
define DIR_TEMPLATE
MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make))
type message = (context, term) Log.item list
-type hierarchy = int -> int
-
(* Currified constructors ***************************************************)
let abst w = Abst w
module U = NUri
module C = Cps
module L = Log
+module H = Hierarchy
module B = Brg
type counters = {
f ()
let rec pp_term c frm = function
- | B.Sort h -> F.fprintf frm "@[*%u@]" h
+ | B.Sort h ->
+ let f = function
+ | Some s -> F.fprintf frm "@[%s@]" s
+ | None -> F.fprintf frm "@[*%u@]" h
+ in
+ H.get_sort f h
| B.LRef i ->
let f = function
| Some (id, _) -> F.fprintf frm "@[%s@]" id
V_______________________________________________________________ *)
module L = Log
+module H = Hierarchy
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
let rec type_of f g c x =
L.log O.specs level (L.ct_items1 "now checking" c x);
match x with
- | B.Sort h -> f (B.Sort (g h))
+ | B.Sort h ->
+ let f h = f (B.Sort h) in H.apply f g h
| B.LRef i ->
let f = function
| Some (_, B.Abst w) -> f w
exception TypeError of Brg.message
val type_of:
- (Brg.term -> 'a) -> Brg.hierarchy -> Brg.context -> Brg.term -> 'a
+ (Brg.term -> 'a) -> Hierarchy.graph -> Brg.context -> Brg.term -> 'a
V_______________________________________________________________ *)
val type_check:
- ((Brg.term * Brg.obj) option -> 'a) -> Brg.hierarchy -> Brg.item -> 'a
+ ((Brg.term * Brg.obj) option -> 'a) -> Hierarchy.graph -> Brg.item -> 'a
-nUri cps share log time
+nUri cps share log time hierarchy
--- /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 H = Hashtbl
+module S = Scanf
+module C = Cps
+
+type graph = string * (int -> int)
+
+let sorts = 2
+let sort = H.create sorts
+let index = ref 0
+
+(* Internal functions *******************************************************)
+
+let set_sort f (h:int) (s:string) =
+ H.add sort h s; f (succ h)
+
+(* Interface functions ******************************************************)
+
+let set_new_sorts f ss =
+ let f i = index := i; f i in
+ C.list_fold_left f set_sort !index ss
+
+let get_sort f h =
+ try f (Some (H.find sort h))
+ with Not_found -> f None
+
+let string_of_graph f (s, _) = f s
+
+let apply f (_, g) h = f (g h)
+
+let graph_of_string f s =
+ try
+ let x = S.sscanf s "Z%u" C.start in
+ if x > 0 then f (Some (s, fun h -> x + h)) else f None
+ with
+ S.Scan_failure _ | Failure _ | End_of_file -> f None
+
+let graph =
+ ref (graph_of_string (function Some g -> g | None -> assert false) "Z2")
--- /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 graph
+
+val set_new_sorts: (int -> 'a) -> string list -> 'a
+
+val get_sort: (string option -> 'a) -> int -> 'a
+
+val graph_of_string: (graph option -> 'a) -> string -> 'a
+
+val string_of_graph: (string -> 'a) -> graph -> 'a
+
+val apply: (int -> 'a) -> graph -> int -> 'a
+
+val graph: graph ref
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module C = Cps
module B = Brg
module M = Meta
(* Internal functions *******************************************************)
let map_fold_left f map1 map2 a l =
- let f a = Cps.list_fold_left f map2 a l in
+ let f a = C.list_fold_left f map2 a l in
map1 f a
let map_args f t v = f (B.Appl (v, t))
| M.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_map f xlate_term vs
+ let f vs = map_fold_left f C.id map_args (B.GRef uri) vs in
+ C.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
| e, pars, uri, u, None ->
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_map f xlate_pars pars
+ C.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 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_map f xlate_pars pars
+ C.list_map f xlate_pars pars
let xlate_item f = function
| None -> f None
module P = Printf
module U = NUri
+module C = Cps
module L = Log
+module H = Hierarchy
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
}
let count count_fun c item =
- if !L.level > 2 then count_fun Cps.start c item else c
+ if !L.level > 2 then count_fun C.start c item else c
let brg_error s msg =
L.error BrgO.specs (L.Warn s :: msg)
let version_string = "Helena Checker 0.8.0 M - December 2008" in
let stage = ref 3 in
let meta_file = ref None in
- let hierarchy = ref (fun h -> h + 2) in
+ let set_hierarchy s =
+ let f = function
+ | Some g -> H.graph := g
+ | None -> L.warn (P.sprintf "Unknown type hierarchy: %s" s)
+ in
+ H.graph_of_string f s
+ 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
(* stage 2 *)
let f st item =
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
+ if !stage > 2 then BrgU.type_check (f st) !H.graph item else st
in
(* stage 1 *)
let f mst item =
} in
begin match !meta_file with
| None -> ()
- | Some (_, frm) -> MO.pp_item Cps.start frm item
+ | Some (_, frm) -> MO.pp_item C.start frm item
end;
if !stage > 1 then MBrg.brg_of_meta (f st) item else st
in
in
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;
+ if !L.level > 2 then AO.print_counters C.start st.ac;
+ if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
+ if !L.level > 2 && !stage > 1 then BrgO.print_counters C.start st.brgc;
in
let help =
- "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ...\n\n" ^
+ "Usage: helena [ -V | -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_h = "<string> set type hierarchy" in
let help_m = "<file> output intermediate representation" in
let help_s = "<number> Set translation stage" in
+ 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);
("-m", Arg.String set_meta_file, help_m);
("-s", Arg.Int set_stage, help_s);
] read_file help;
projects / helm.git / commitdiff