From 9f1f0cb1ae2665a495db930f1561e381e64f5137 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Apr 2009 10:50:23 +0000 Subject: [PATCH] added analyse_indty --- .../components/ng_tactics/nTactics.ml | 25 ++++++++++++------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 87be3279f..49daed849 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -531,19 +531,26 @@ let intro_tac name = (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit))) ;; -let case status goal = - let _,ctx,_ = get_goal status goal in - let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in - let ref = - match whd status (`Ctx ctx) ty with - _,_,NCic.Const ref - | _,_,NCic.Appl (NCic.Const ref :: _) -> ref +let analyse_indty status ty = + let ref, args = + match whd status (`Term ty) ty with + | _,_,NCic.Const ref -> ref, [] + | _,_,NCic.Appl (NCic.Const ref :: args) -> ref, args | _,_,_ -> fail (lazy ("not an inductive type")) in - let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in + let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in let _,_,_,cl = List.nth tl i in let consno = List.length cl in + let left, right = HExtlib.split_nth lno args in + ref, consno, left, right +;; + +let case status goal = + let _,ctx,_ = get_goal status goal in + let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in + let ref, consno, left, right = analyse_indty status ty in let t = - NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno) + NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1, + HExtlib.mk_list (NCic.Implicit `Term) consno) in let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in instantiate status goal t -- 2.39.2