cicUtil : new test function "is_sober" to test the integrity of a term

                 now fails when fake applications are detected
acic_procedural: some bug fix

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index f39aa18bd96ee3a162baa10fa6da07ca3b6f8805..cc4ec10a340e9793999d5b09bbd3d12b4dcd40c8 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -198,6 +198,8 @@ let mk_convert st ?name sty ety note =
    let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
       note (Pp.ppterm csty) (Pp.ppterm cety)
    in
+   assert (Ut.is_sober csty); 
+   assert (Ut.is_sober cety);
    if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else 
    match name with
       | None         -> [T.Change (sty, ety, None, e, ""(*note*))]
@@ -266,7 +268,7 @@ let mk_rewrite st dtext where qs tl direction t =
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
-      | None          -> true
+      | None          -> false
       | Some (it, et) -> 
          DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 755176e5c50cc4d4d280fcee4b373089ebbcb485..489feb4b66aa54385f1e3f102ecdc5381cb1d9c8 100644 (file)
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -82,8 +82,9 @@ try
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
+      let isf = argsno > 0 || H.is_sort v in
       let iu = H.is_unsafe h (List.hd vs) in
-      (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h
+      (I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
    in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in

diff --git a/components/acic_procedural/proceduralHelpers.ml b/components/acic_procedural/proceduralHelpers.ml
index 94ef413c1042207a4058f6429e7cc02e4c8f4e72..bfffb11ba21ab846bb26a51d46f891246d7ff0e6 100644 (file)
--- a/components/acic_procedural/proceduralHelpers.ml
+++ b/components/acic_procedural/proceduralHelpers.ml
@@ -106,6 +106,10 @@ let is_proof c t =
       | C.Sort _      -> false
       | _             -> assert false 
 
+let is_sort = function
+   | C.Sort _ -> true
+   | _        -> false 
+
 let is_unsafe h (c, t) = true
 
 let is_not_atomic = function

diff --git a/components/acic_procedural/proceduralHelpers.mli b/components/acic_procedural/proceduralHelpers.mli
index 97b637d70b126cc21f0c1b80ec28e5faefcf6bbd..a7dfcc957dc8a04ef54beb88a9425acd085f9f50 100644 (file)
--- a/components/acic_procedural/proceduralHelpers.mli
+++ b/components/acic_procedural/proceduralHelpers.mli
@@ -39,6 +39,8 @@ val get_type:
    Cic.context -> Cic.term -> Cic.term
 val is_proof:
    Cic.context -> Cic.term -> bool
+val is_sort:
+   Cic.term -> bool
 val is_unsafe:
    int -> Cic.context * Cic.term -> bool
 val is_not_atomic:

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index d26d422d526318b3efedb7786ea0e7e2bc90ca62..dd165219694c2f1bbf1f0dc361f952e709e74532 100644 (file)
--- a/components/cic/cicUtil.ml
+++ b/components/cic/cicUtil.ml
@@ -484,7 +484,7 @@ let alpha_equivalence =
         aux s s' && aux t t'
      | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
         aux s s' && aux t t'
-     | C.Appl l, C.Appl l' ->
+     | C.Appl l, C.Appl l' when List.length l = List.length l' ->
         (try
           List.fold_left2
            (fun b t1 t2 -> b && aux t1 t2) true l l'
@@ -535,7 +535,8 @@ let alpha_equivalence =
             | _               -> b
            ) true subst subst'
          with
-          Invalid_argument _ -> false)     
+          Invalid_argument _ -> false)
+     | C.Appl [t], t' | t, C.Appl [t'] -> assert false
 (* FG: are we _really_ sure of these?      
      | C.Sort (C.Type u), C.Sort (C.Type u') -> u = u' 
      | C.Implicit a, C.Implicit a' -> a = a'
@@ -552,3 +553,43 @@ let alpha_equivalence =
      Invalid_argument _ -> false
   in
    aux
+
+let is_sober t =
+   let rec sober_term g = function
+      | C.Rel _ 
+      | C.Sort _  
+      | C.Implicit _                    -> g      
+      | C.Const (_, xnss) 
+      | C.Var (_, xnss) 
+      | C.MutConstruct (_, _, _, xnss)
+      | C.MutInd (_, _, xnss)           -> sober_xnss g xnss
+      | C.Meta (_, xss)                 -> sober_xss g xss
+      | C.LetIn (_, v, t)
+      | C.Lambda (_, v, t)
+      | C.Prod (_, v, t)
+      | C.Cast (t, v)                   -> sober_term (sober_term g t) v
+      | C.Appl []                       
+      | C.Appl [_]                      -> fun b -> false
+      | C.Appl ts                       -> sober_terms g ts
+      | C.MutCase (_, _, t, v, ts)      -> 
+         sober_terms (sober_term (sober_term g t) v) ts
+      | C.Fix (_, ifs)                  -> sober_ifs g ifs
+      | C.CoFix (_, cifs)               -> sober_cifs g cifs
+   and sober_terms g = List.fold_left sober_term g
+   and sober_xnss g =
+      let map g (_, t) = sober_term g t in
+      List.fold_left map g
+   and sober_xss g =
+      let map g = function 
+         | None   -> g
+        | Some t -> sober_term g t
+      in
+      List.fold_left map g
+   and sober_ifs g =
+      let map g (_, _, t, v) = sober_term (sober_term g t) v in
+      List.fold_left map g
+   and sober_cifs g =
+      let map g (_, t, v) = sober_term (sober_term g t) v in
+      List.fold_left map g
+   in 
+   sober_term (fun b -> b) t true

diff --git a/components/cic/cicUtil.mli b/components/cic/cicUtil.mli
index de8c020952ac0262d774ef6c7ad2fff39d5d543a..9977d186465c24e245e4ea404a8ae6bf1c4ca812 100644 (file)
--- a/components/cic/cicUtil.mli
+++ b/components/cic/cicUtil.mli
@@ -66,3 +66,8 @@ val rehash_term: Cic.term -> Cic.term
 val rehash_obj: Cic.obj -> Cic.obj
 
 val alpha_equivalence: Cic.term -> Cic.term -> bool
+
+(* FG: Consistency Check 
+ * detects applications without arguments
+ *)
+val is_sober: Cic.term -> bool