From 186c1171d37f5d1cde9bb6f38a863be16debf3f0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 13 Jul 2008 11:06:20 +0000 Subject: [PATCH] cicUtil : we added a context to is_sober to check for consistancy of RELS (not implemented yet) doubleTypeInference: the inferred name of an anonymous lambda must be the name of the expected prod :) acic2Procedural : we added a consistancy check that was missing --- .../acic_procedural/acic2Procedural.ml | 12 ++++-- helm/software/components/cic/cicUtil.ml | 43 ++++++++++--------- helm/software/components/cic/cicUtil.mli | 2 +- .../cic_acic/doubleTypeInference.ml | 13 +++--- 4 files changed, 38 insertions(+), 32 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index dd59d1f6e..a6e0667b0 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -202,8 +202,8 @@ let mk_convert st ?name sty ety note = [T.Note note] else [] in - assert (Ut.is_sober csty); - assert (Ut.is_sober cety); + assert (Ut.is_sober st.context csty); + assert (Ut.is_sober st.context cety); if Ut.alpha_equivalence csty cety then script else let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in match name with @@ -266,11 +266,14 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = in if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then {st with context = Cn.clear st.context premise}, script name - else + else begin + assert (Ut.is_sober st.context (H.cic ity)); + let ity = H.acic_bc st.context ity in let br1 = [T.Id ""] in let br2 = List.rev (T.Apply (w, "assumption") :: script None) in let text = "non linear rewrite" in st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)] + end | _ -> assert false let mk_rewrite st dtext where qs tl direction t = @@ -305,8 +308,9 @@ and proc_letin st what name v w t = | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl -> mk_fwd_rewrite st dtext intro tl false v t ity | v -> + assert (Ut.is_sober st.context (H.cic ity)); + let ity = H.acic_bc st.context ity in let qs = [proc_proof (next st) v; [T.Id ""]] in - let ity = H.acic_bc st.context ity in st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in st, C.Decl (H.cic ity), rqv diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 75b7fd2cc..8c42aed61 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -557,43 +557,44 @@ let alpha_equivalence = in aux -let is_sober t = - let rec sober_term g = function +let is_sober c t = + let rec sober_term c 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.MutInd (_, _, xnss) -> sober_xnss c g xnss + | C.Meta (_, xss) -> sober_xss c g xss | C.Lambda (_, v, t) | C.Prod (_, v, t) - | C.Cast (t, v) -> sober_term (sober_term g t) v - | C.LetIn (_, v, ty, t) -> sober_term - (sober_term (sober_term g t) ty) v + | C.Cast (t, v) -> + sober_term c (sober_term c g t) v + | C.LetIn (_, v, ty, t) -> + sober_term c (sober_term c (sober_term c g t) ty) v | C.Appl [] | C.Appl [_] -> fun b -> false - | C.Appl ts -> sober_terms g ts + | C.Appl ts -> sober_terms c 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 + sober_terms c (sober_term c (sober_term c g t) v) ts + | C.Fix (_, ifs) -> sober_ifs c g ifs + | C.CoFix (_, cifs) -> sober_cifs c g cifs + and sober_terms c g = List.fold_left (sober_term c) g + and sober_xnss c g = + let map g (_, t) = sober_term c g t in List.fold_left map g - and sober_xss g = + and sober_xss c g = let map g = function | None -> g - | Some t -> sober_term g t + | Some t -> sober_term c 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 + and sober_ifs c g = + let map g (_, _, t, v) = sober_term c (sober_term c 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 + and sober_cifs c g = + let map g (_, t, v) = sober_term c (sober_term c g t) v in List.fold_left map g in - sober_term (fun b -> b) t true + sober_term c (fun b -> b) t true diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli index 9977d1864..54a0a9bea 100644 --- a/helm/software/components/cic/cicUtil.mli +++ b/helm/software/components/cic/cicUtil.mli @@ -70,4 +70,4 @@ val alpha_equivalence: Cic.term -> Cic.term -> bool (* FG: Consistency Check * detects applications without arguments *) -val is_sober: Cic.term -> bool +val is_sober: Cic.context -> Cic.term -> bool diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 1671b98d2..7f93716b2 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -339,17 +339,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | C.Lambda (n,s,t) -> (* Let's visit all the subterms that will not be visited later *) let _ = type_of_aux context s None in - let expected_target_type = + let n, expected_target_type = match expectedty with - None -> None + | None -> n, None | Some expectedty' -> - let ty = + let n, ty = match R.whd context expectedty' with - C.Prod (_,_,expected_target_type) -> - beta_reduce expected_target_type + | C.Prod (n',_,expected_target_type) -> + let xtt = beta_reduce expected_target_type in + if n <> C.Anonymous then n, xtt else n', xtt | _ -> assert false in - Some ty + n, Some ty in let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type -- 2.39.2