diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-30 19:53:46 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-30 19:53:46 +0000 |
commit | 9518675fafc27d3af2a62a5201244f5b5dfaf47f (patch) | |
tree | 860892242d34bda1e923f697f571765a71638789 /checker/indtypes.ml | |
parent | 707e6ebc87d88e0e6a5cb5060837dbc0fce3b6a1 (diff) |
adpated the checker to handle coomutative cuts and lazyness
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/indtypes.ml')
-rw-r--r-- | checker/indtypes.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 3ad39f1de..5de03b16d 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -392,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = +let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc = let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) let rec check_pos (env, n, ntypes, ra_env as ienv) c = @@ -494,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = with IllFormedInd err -> explain_ind_err (ntypes-i) env lparams c err) indlc - in mk_paths (Mrec i) irecargs + in mk_paths (Mrec ind) irecargs let check_subtree (t1:'a) (t2:'a) = if not (Rtree.compare_rtree (fun t1 t2 -> @@ -505,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) = failwith "bad recursive trees" (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) -let check_positivity env_ar params nrecp inds = +let check_positivity env_ar mind params nrecp inds = let ntypes = Array.length inds in - let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in + let rc = + Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = List.rev (Array.to_list rc) in let lparams = rel_context_length params in let check_one i mip = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - check_positivity_one ienv params nrecp i mip.mind_nf_lc + check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in @@ -547,7 +548,7 @@ let check_inductive env kn mib = (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check mind_nparams_rec: positivity condition *) - check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; + check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) (* Now we can add the inductive *) add_mind kn mib env |