From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 23 Dec 2014 13:16:38 +0000 (+0000)
Subject: - bug fix in the RTM
X-Git-Tag: make_still_working~778
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd77f8898787aab4808437ee731f5c7f87cd64df;p=helm.git

- bug fix in the RTM
- we can validate the Grundlagen in lambda-delta version 3
---

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index 42463197a..bc669964b 100644
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -253,8 +253,8 @@ src/basic_ag/bagUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \
 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 \
@@ -267,8 +267,8 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.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 \
diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 09dffb04d..db940e373 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -10,7 +10,7 @@ KEEP = README
 
 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
 
@@ -40,10 +40,14 @@ test-si-matita matita/$(MA): $(MAIN).opt etc
 	@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
@@ -61,3 +65,10 @@ matita: matita/$(MA)
 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
+
diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index c38e8532c..866f38341 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -126,12 +126,13 @@ let rec xlate_term f st lst y lenv = function
       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
@@ -206,7 +207,7 @@ let xlate_entity err f st lst = function
 	 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 = 
@@ -239,7 +240,7 @@ let initial_status () =
 }
 
 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
diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index e20737ec4..6f9f5f09f 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -140,11 +140,11 @@ let rec step st m x =
    | 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;
diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index 494b39159..ed2b140e4 100644
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -44,8 +44,9 @@ let string_of_value k = function
    | 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
       )
@@ -81,10 +82,11 @@ let resolve_layer st = function
 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);
@@ -133,11 +135,14 @@ let rec unknown st =
    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
@@ -188,3 +193,4 @@ let assert_equal st n1 n2 =
 
 let is_not_zero st n  =
    let _, n = resolve_layer st n in n.v <> zero
+
diff --git a/helm/software/helena/src/common/marks.ml b/helm/software/helena/src/common/marks.ml
index dd8bdc5cf..22e1599b0 100644
--- a/helm/software/helena/src/common/marks.ml
+++ b/helm/software/helena/src/common/marks.ml
@@ -23,3 +23,6 @@ let new_mark () =
 let null_mark = 0
 
 let string_of_mark i = string_of_int i
+
+let clear_marks () =
+   mark := 0
diff --git a/helm/software/helena/src/common/marks.mli b/helm/software/helena/src/common/marks.mli
index d60fe0def..e6d1faea7 100644
--- a/helm/software/helena/src/common/marks.mli
+++ b/helm/software/helena/src/common/marks.mli
@@ -18,3 +18,5 @@ val new_mark: unit -> mark
 val null_mark: mark
 
 val string_of_mark: mark -> string
+
+val clear_marks: unit -> unit
diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index 673b3a0ba..4624e4c8c 100644
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -114,9 +114,13 @@ let rec mem err f e b = match e with
    | 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
diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index e7f9158b1..d57c2b007 100644
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -17,6 +17,7 @@ module C  = Cps
 module L  = Log
 module Y  = Time
 module G  = Options
+module J  = Marks
 module H  = Hierarchy
 module N  = Layer
 module E  = Entity
@@ -128,17 +129,17 @@ let validate st k =
    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 = {
@@ -220,11 +221,15 @@ let streaming = ref false (* parsing style (temporary) *)
 
 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;
@@ -306,7 +311,6 @@ let main =
    let clear_options () =
       export := false; preprocess := false;
       root := "";
-      st := initial_status ();
       G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
       version := true
@@ -319,6 +323,7 @@ let main =
       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