From 9a913a2aa1834704908ec829d5326d214fd68e88 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 21 Mar 2000 18:16:19 +0000 Subject: Modification de type_of_case, type_case_branches, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/typeops.ml | 59 +++++++++++++++++++++++++++++++------------------------ 1 file changed, 33 insertions(+), 26 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c7496554c..5c4b5e41c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -242,18 +242,18 @@ let is_correct_arity env sigma kelim (c,p) = in error_elim_arity CCI env ind listarity c p pt kinds in - srec + srec let find_case_dep_nparams env sigma (c,p) (mind,largs) typP = - let mis = lookup_mind_specif mind env in + let mis = lookup_mind_specif mind env in let nparams = mis_nparams mis - and kelim = mis_kelim mis + and kelim = mis_kelim mis and t = body_of_type (instantiate_arity mis) in let (globargs,la) = list_chop nparams largs in let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in let arity = applist(mkMutInd mind,globargs) in let (dep,_) = is_correct_arity env sigma kelim (c,p) arity (typP,glob_t) in - (dep, (nparams, globargs,la)) + dep let type_one_branch_dep env sigma (nparams,globargs,p) co t = let rec typrec n c = @@ -277,6 +277,19 @@ let type_one_branch_nodep env sigma (nparams,globargs,p) t = in typrec 0 (hnf_prod_applist env sigma "type_case" t globargs) +(* [p] is the predicate and [cs] a constructor summary *) +let mytype_one_branch dep env p cs = + if dep then + let n = cs.cs_nargs in + let ci = + applist + (mkMutConstruct cs.cs_cstr, + (List.map (lift n) cs.cs_params)@(rel_list 0 n)) in + it_prod_name env (applist (appvect (lift n p,cs.cs_concl_realargs), [ci])) + cs.cs_args + else + prod_it (appvect (lift cs.cs_nargs p,cs.cs_concl_realargs)) cs.cs_args + (* type_case_branches type un

Case c of ... end ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc pt = sorte de p @@ -284,26 +297,17 @@ let type_one_branch_nodep env sigma (nparams,globargs,p) t = attendus dans les branches du Case; lr est le type attendu du resultat *) -let type_case_branches env sigma ct pt p c = - try - let (mind,largs) = find_mrectype env sigma ct in - let (dep,(nparams,globargs,la)) = - find_case_dep_nparams env sigma (c,p) (mind,largs) pt - in - let (lconstruct,ltypconstr) = type_mconstructs env sigma mind in - let mI = mkMutInd mind in - if dep then - (mI, - array_map2 (type_one_branch_dep env sigma (nparams,globargs,p)) - lconstruct ltypconstr, - beta_applist (p,(la@[c]))) - else - (mI, - Array.map (type_one_branch_nodep env sigma (nparams,globargs,p)) - ltypconstr, - beta_applist (p,la)) - with Induc -> - error_case_not_inductive CCI env c ct +let type_case_branches env sigma indspec pt p c = + let dep = + find_case_dep_nparams env sigma (c,p) + (indspec.mind,indspec.params@indspec.realargs) pt in + let constructs = get_constructors env sigma indspec in + let lc = Array.map (mytype_one_branch dep env p) constructs in + let la = indspec.realargs in + if dep then + (lc, beta_applist (p,(la@[c]))) + else + (lc, beta_applist (p,la)) let check_branches_message env sigma (c,ct) (explft,lft) = let n = Array.length explft @@ -317,8 +321,11 @@ let check_branches_message env sigma (c,ct) (explft,lft) = let type_of_case env sigma ci pj cj lfj = let lft = Array.map (fun j -> j.uj_type) lfj in - let (mind,bty,rslty) = - type_case_branches env sigma cj.uj_type pj.uj_type pj.uj_val cj.uj_val in + let indspec = + try try_mutind_of env sigma cj.uj_type + with Induc -> error_case_not_inductive CCI env cj.uj_val cj.uj_type in + let (bty,rslty) = + type_case_branches env sigma indspec pj.uj_type pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma pj.uj_type in check_branches_message env sigma (cj.uj_val,cj.uj_type) (bty,lft); { uj_val = mkMutCaseA ci (j_val pj) (j_val cj) (Array.map j_val lfj); -- cgit v1.2.3