diff options
author | 2015-06-26 11:24:16 +0200 | |
---|---|---|
committer | 2015-06-26 11:24:16 +0200 | |
commit | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (patch) | |
tree | 4679e39132853febe84670f5c039fc4608418496 /kernel/inductive.ml | |
parent | 42b7e36ddb68f53ada686900e5a98435d9ff7fde (diff) |
Add a flag to deactivate guard checking in the kernel.
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r-- | kernel/inductive.ml | 54 |
1 files changed, 30 insertions, 24 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4c1614bac..532287c30 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1065,21 +1065,24 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = - let (minds, rdef) = inductive_of_mutfix env fix in - let get_tree (kn,i) = - let mib = Environ.lookup_mind kn env in - mib.mind_packets.(i).mind_recargs - in - let trees = Array.map (fun (mind,_) -> get_tree mind) minds in - for i = 0 to Array.length bodies - 1 do - let (fenv,body) = rdef.(i) in - let renv = make_renv fenv nvect.(i) trees.(i) in - try check_one_fix renv nvect trees body - with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i - (push_rec_types recdef env) (judgment_of_fixpoint recdef) - done +let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) = + if chk then + let (minds, rdef) = inductive_of_mutfix env fix in + let get_tree (kn,i) = + let mib = Environ.lookup_mind kn env in + mib.mind_packets.(i).mind_recargs + in + let trees = Array.map (fun (mind,_) -> get_tree mind) minds in + for i = 0 to Array.length bodies - 1 do + let (fenv,body) = rdef.(i) in + let renv = make_renv fenv nvect.(i) trees.(i) in + try check_one_fix renv nvect trees body + with FixGuardError (fixenv,err) -> + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) + done + else + () (* let cfkey = Profile.declare_profile "check_fix";; @@ -1190,12 +1193,15 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in - for i = 0 to nbfix-1 do - let fixenv = push_rec_types recdef env in - try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i - fixenv (judgment_of_fixpoint recdef) - done +let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) = + if chk then + let nbfix = Array.length bodies in + for i = 0 to nbfix-1 do + let fixenv = push_rec_types recdef env in + try check_one_cofix fixenv nbfix bodies.(i) types.(i) + with CoFixGuardError (errenv,err) -> + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) + done + else + () |