From: Ferruccio Guidi Date: Thu, 19 Jul 2007 18:00:55 +0000 (+0000) Subject: cicUtil : new test function "is_sober" to test the integrity of a term X-Git-Tag: make_still_working~6150 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=468ee32f0fc7de271454ed94643b4dd7c9578e5f;p=helm.git 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/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index f39aa18bd..cc4ec10a3 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 755176e5c..489feb4b6 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 94ef413c1..bfffb11ba 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 97b637d70..a7dfcc957 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/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/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index d26d422d5..dd1652196 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/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/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli index de8c02095..9977d1864 100644 --- a/helm/software/components/cic/cicUtil.mli +++ b/helm/software/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