From 3270d5e228bbcd3dfe7350e59416b843a5149e3b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Apr 2008 08:20:24 +0000 Subject: [PATCH] do not use an implicit but a sort as a neutral term for positivity check --- .../components/ng_kernel/nCicTypeChecker.ml | 27 ++++++++++--------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 334ab8622..26e2163ea 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -417,29 +417,30 @@ let does_not_occur ~subst context n nn t = (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) let rec weakly_positive ~subst context n nn uri te = (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) - let dummy_mutind = C.Implicit `Hole in + let dummy = C.Sort (C.Type ~-1) in (*CSC: mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_mutind _ = function - | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind - | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri -> - dummy_mutind - | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t + let rec subst_inductive_type_with_dummy _ = function + | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy + | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) + when NUri.eq uri' uri -> dummy + | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t in match R.whd context te with | C.Const (Ref.Ref (_,uri',Ref.Ind _)) - | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true + | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) + when NUri.eq uri' uri -> true | C.Prod (name,source,dest) when does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive ~subst context n nn - (subst_inductive_type_with_dummy_mutind () source) && - weakly_positive ~subst ((name,C.Decl source)::context) - (n + 1) (nn + 1) uri dest + (subst_inductive_type_with_dummy () source) && + weakly_positive ~subst ((name,C.Decl source)::context) + (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) -> does_not_occur ~subst context n nn - (subst_inductive_type_with_dummy_mutind () source)&& - weakly_positive ~subst ((name,C.Decl source)::context) - (n + 1) (nn + 1) uri dest + (subst_inductive_type_with_dummy () source)&& + weakly_positive ~subst ((name,C.Decl source)::context) + (n + 1) (nn + 1) uri dest | _ -> raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) -- 2.39.2