From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 20 Aug 2009 09:57:51 +0000 (+0000)
Subject: - sort inclusion must be restricted to term backbone in order to avoid
X-Git-Tag: make_still_working~3531
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc9fca01f135aecc2940e7318f77fea34fd6ef30;p=helm.git

- sort inclusion must be restricted to term backbone in order to avoid
validity of non-normalizing terms (see the omega.aut example)
- command-line options -a and -p rearranged
---

diff --git a/helm/software/lambda-delta/automath/omega.aut b/helm/software/lambda-delta/automath/omega.aut
new file mode 100644
index 000000000..9a41532ce
--- /dev/null
+++ b/helm/software/lambda-delta/automath/omega.aut
@@ -0,0 +1,10 @@
+# The lambda-term \omega
+# This book is not accepted in AUT-QE because [y:'type'] is not allowed
+# This book is accepted in lambda-delta with sort inclusion but omega is not
+#    valid if sort inclusion is allowed on the term backbone only
+# This book is valid in lambda-delta with sort inclusion allowed everywhere 
+
++l 
+@ delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+  omega := <delta>delta             : 'type'
+-l
diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index b57cb552b..26663cf5f 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -64,7 +64,6 @@ let are_alpha_convertible f t1 t2 =
       | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
          let f r = if r then aux f (t1, t2) else f r in
 	 aux_bind f (b1, b2)
-      | B.Sort _ as t1, B.Bind (_, _, t2)      -> aux f (t1, t2)
       | _                                      -> f false
    and aux_bind f = function
       | B.Abbr v1, B.Abbr v2
@@ -148,11 +147,10 @@ let push f m a b =
 let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
    log2 "Now converting nfs" m1.c u m2.c t;
    match a1, u, a2, t with
-      | _, B.Sort (_, h1), 
-        _, B.Sort (_, h2)                                ->
+      | _, B.Sort (_, h1), _, B.Sort (_, h2)             ->
          if h1 = h2 then f r else f false 
       | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _   ->
-	 if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
+	 if e1 = e2 then ac_stacks f r m1 m2 else f false
       | Some (e1, B.Abbr v1), _, Some (e2, B.Abbr v2), _ ->
          if e1 = e2 then
 	    let f r = 
@@ -162,7 +160,7 @@ let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
 	          ac f ~si true m1 v1 m2 v2
 	       end
 	    in
-	    ac_stacks f ~si r m1 m2
+	    ac_stacks f r m1 m2
 	 else if e1 < e2 then begin 
             P.add ~gdelta:1 ();
 	    step (ac_nfs f ~si r m1 a1 u) m2 v2
@@ -181,7 +179,7 @@ let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
 	 let g m1 m2 = ac f ~si r m1 t1 m2 t2 in
          let g m1 = push (g m1) m2 a2 b2 in 
 	 let f r = if r then push g m1 a1 b1 else f false in
-	 ac f ~si r m1 w1 m2 w2      
+	 ac f ~si:false r m1 w1 m2 w2      
       | _, B.Sort _, _, B.Bind (a, b, t) when si         ->
 	 P.add ~si:1 ();
 	 let f m1 m2 = ac f ~si r m1 u m2 t in
@@ -196,12 +194,12 @@ and ac f ~si r m1 t1 m2 t2 =
    let g m1 a1 t1 = step (ac_nfs f ~si r m1 a1 t1) m2 t2 in 
    if r = false then f false else step g m1 t1
 
-and ac_stacks f ~si r m1 m2 =
+and ac_stacks f r m1 m2 =
 (*   L.warn "entering R.are_convertible_stacks"; *)
    if List.length m1.s <> List.length m2.s then f false else
    let map f r (c1, v1) (c2, v2) =
       let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
-      ac f ~si r m1 v1 m2 v2
+      ac f ~si:false r m1 v1 m2 v2
    in
    C.list_fold_left2 f map r m1.s m2.s
 
diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3fa3c908c..469078668 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -203,7 +203,7 @@ try
       flush ()
    in
    let help = 
-      "Usage: helena [ -Vacimpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+      "Usage: helena [ -Vcijmpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
       "Summary levels: 0 just errors (default), 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 (default)\n"
@@ -211,13 +211,13 @@ try
    let help_S = "<number>  set summary level (see above)" in
    let help_V = " show version information" in   
 
-   let help_a = " analyze source files" in
    let help_c = " disable initial segment of URI hierarchy" in
    let help_h = "<string>  set type hierarchy (default: Z2)" in
    let help_i = " show local references by index" in
+   let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in
    let help_m = " output intermediate representation (HAL)" in
-   let help_p = " activate progress indicator" in
+   let help_p = " preprocess Automath source" in
    let help_u = " activate sort inclusion" in
    let help_s = "<number>  set translation stage (see above)" in
    let help_x = " export kernel objects (XML)" in
@@ -227,13 +227,13 @@ try
    Arg.parse [
       ("-S", Arg.Int set_summary, help_S);
       ("-V", Arg.Unit print_version, help_V);
-      ("-a", Arg.Set process, help_a);      
       ("-c", Arg.Clear use_cover, help_c);
       ("-h", Arg.String set_hierarchy, help_h);
       ("-i", Arg.Set O.indexes, help_i);
+      ("-j", Arg.Set progress, help_j);      
       ("-k", Arg.String set_kernel, help_k);
       ("-m", Arg.Set meta, help_m); 
-      ("-p", Arg.Set progress, help_p);
+      ("-p", Arg.Set process, help_p);      
       ("-u", Arg.Set si, help_u);
       ("-s", Arg.Int set_stage, help_s);
       ("-x", Arg.Set export, help_x)