src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \
src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \
- src/common/options.cmx src/lib/log.cmi src/common/layer.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx \
+ src/common/options.cmx src/common/marks.cmi src/lib/log.cmi \
+ src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmx \
src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
src/basic_rg/brgOutput.cmi src/basic_rg/brgGrafite.cmi \
src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \
src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \
- src/common/options.cmx src/lib/log.cmx src/common/layer.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx \
+ src/common/options.cmx src/common/marks.cmx src/lib/log.cmx \
+ src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \
src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
src/basic_rg/brgOutput.cmx src/basic_rg/brgGrafite.cmx \
CLEAN = etc/log.txt etc/profile.txt
-TAGS = test-si-fast test-si test-si-matita profile xml-si-crg xml-si matita matitac
+TAGS = test-si-fast test-si test-si-matita test profile xml-si-crg xml-si matita matitac
include Makefile.common
@echo " HELENA -d -l -m -p -o $(INPUT)"
$(H)./$(MAIN).opt -T 2 -a n -d -l -m $(PREAMBLE) -p -o $(O) $(INPUT) > etc/log.txt
+test: $(MAIN).opt etc
+ @echo " HELENA -d -l $(INPUT)"
+ $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 2 -d -l $(INPUT) > etc/log.txt
+
profile: $(MAIN).opt etc
- @echo " HELENA -o -q $(INPUTFAST) (30 TIMES)"
+ @echo " HELENA -o -q $(INPUTFAST) (31 TIMES)"
$(H)rm -f etc/log.txt
- $(H)for T in `seq 30`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
+ $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
xml-si-crg: $(MAIN).opt etc
matitac: matita/$(MA)
@echo " MATITAC $(MA)"
$(H)cd matita && $(MATITAC) $(MA)
+
+#profile-matita: $(MAIN).opt etc
+# @echo " HELENA -o $(INPUT) (1 TIMES)"
+# $(H)rm -f etc/log.txt
+# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -a n -l -m $(PREAMBLE) -o -x $(INPUT) >> etc/log.txt; done
+# $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
+
let name = Some (name, true) in
let f aw ww =
let f at tt =
- let l = if !G.cc then match y, at.E.n_degr with
- | true, _ -> N.one
- | _ , 0 -> N.one
- | _ , 1 -> N.unknown st
- | _ , 2 -> N.two
- | _ -> assert false
+ let l =
+ if !G.cc then match y, at.E.n_degr with
+ | true, _ -> N.one
+ | _ , 0 -> N.one
+ | _ , 1 -> N.unknown st
+ | _ , 2 -> N.two
+ | _ -> assert false
else N.infinite
in
let b = D.Abst (l, ww) in
in
complete_qid f lst (name, true, [])
in
- get_cnt_relaxed (D.sta f) lst
+ get_cnt_relaxed (D.replace f N.one) lst
| A.Def (name, w, trans, v) ->
let f lenv =
let f qid =
}
let refresh_status lst = {lst with
- mk_uri = G.get_mk_uri ()
+ mk_uri = G.get_mk_uri (); line = 1;
}
let crg_of_aut = xlate_entity
| B.Appl (_, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
| B.Bind (a, B.Abst (n, w), t) ->
+ let i = tsteps m in
+ let n = if i = 0 then n else N.minus st n i in
if !G.si || N.is_not_zero st n then begin match m.s with
| [] ->
- let i = tsteps m in
if i = 0 then m, x, None else
- let n = N.minus st n i in
m, B.Bind (a, B.Abst (n, w), t), None
| (c, v) :: s ->
if !G.cc && not (N.assert_not_zero st n) then assert false;
| Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
| Unk -> "-" ^ J.string_of_mark k
+(* Note: remove assigned variables *)
let pp_table st =
- let map k n =
+ let map k n =
warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
(J.string_of_mark k) (string_of_value k n.v) n.s n.b
)
let rec generated st h i =
let default = dynamic h i in
let k = J.new_mark () in
- match resolve_key_with_default st default k with
- | k, n when n = default -> if !G.trace >= level then pp_table st; n
- | _, n when n.s = true -> generated st h i
- | _ -> assert false
+ let k, n = resolve_key_with_default st default k in
+ if n.s then generated st h i else begin
+ if n <> default then H.replace st k default;
+ if !G.trace >= level then pp_table st; default
+ end
let assert_finite st n j =
if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
if !G.trace >= level then warn "UNKNOWN";
let default = empty () in
let k = J.new_mark () in
- match resolve_key_with_default st default k with
- | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
- | _, n when n.s = true -> n
- | _ -> unknown st
-
+ let k, n = resolve_key_with_default st default k in
+ if n.s then match n.v with
+ | Inf
+ | Fin _ -> n
+ | Unk -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+ | Ref _ -> assert false
+ else unknown st
+
let minus st n j =
if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
let rec aux k n j = match n.v with
let is_not_zero st n =
let _, n = resolve_layer st n in n.v <> zero
+
let null_mark = 0
let string_of_mark i = string_of_int i
+
+let clear_marks () =
+ mark := 0
val null_mark: mark
val string_of_mark: mark -> string
+
+val clear_marks: unit -> unit
| EProj (e, _, d) ->
let err () = mem err f e b in mem err f d b
-let rec sta f = function
- | ESort -> f ESort
- | EBind (e, a, Abst (_, w)) -> sta (push_bind f a (Abst (N.one, w))) e
- | EBind (e, a, b) -> sta (push_bind f a b) e
- | EAppl (e, a, v) -> sta (push_appl f a v) e
- | EProj (e, a, d) -> let f d = sta (push_proj f a d) e in sta f d
+let replace f n0 e =
+ let rec aux f = function
+ | ESort -> f ESort
+ | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e
+ | EBind (e, a, b) -> aux (push_bind f a b) e
+ | EAppl (e, a, v) -> aux (push_appl f a v) e
+ | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d
+
+ in
+ aux f e
module L = Log
module Y = Time
module G = Options
+module J = Marks
module H = Hierarchy
module N = Layer
module E = Entity
let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in
let ok _ = st in
match k with
- | BrgEntity entity ->
- let st = BU.validate brg_err ok st.kst entity in
- begin match st.och with
- | None -> st
- | Some och ->
- if BG.output_entity st.kst och entity then st
- else begin L.warn level "Matita exportation stopped"; {st with och = None} end
- end
+ | BrgEntity entity -> BU.validate brg_err ok st.kst entity
| BagEntity _ -> st
| CrgEntity _ -> st
+let grafite st och = function
+ | BrgEntity entity ->
+ if BG.output_entity st.kst och entity then st else
+ begin L.warn level "Matita exportation stopped"; {st with och = None} end
+ | BagEntity _ -> st
+ | CrgEntity _ -> st
+
(* extended lexer ***********************************************************)
type 'token lexer = {
let process_2 st entity =
let st = if !G.summary then count_entity st entity else st in
+ let st =
+ if !G.stage >= 3 then
+ let f = if !version then validate else type_check in f st entity
+ else st
+ in
if !export then export_entity st entity;
- if !G.stage >= 3 then
- let f = if !version then validate else type_check in
- f st entity
- else st
+ match st.och with
+ | None -> st
+ | Some och -> grafite st och entity
let process_1 st entity =
if !G.trace >= 3 then pp_progress entity;
let clear_options () =
export := false; preprocess := false;
root := "";
- st := initial_status ();
G.clear (); H.clear (); O.clear_reductions ();
streaming := false;
version := true
if !G.stage <= 1 then G.kernel := G.Crg;
G.cover := cover;
if !G.ma_preamble <> "" then st := {!st with och = Some (BG.open_out base_name)};
+ J.clear_marks ();
let sst, input = process (refresh_status !st) name in
st := begin match sst.och with
| None -> sst
projects / helm.git / commitdiff