From 576d7a815174106f337fca2f19ad7f26a7e87cc4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 11:24:16 +0200 Subject: Add a flag to deactivate guard checking in the kernel. --- pretyping/inductiveops.ml | 4 ++-- pretyping/pretyping.ml | 6 +++--- pretyping/typing.ml | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index dfdc24d480..efea4bec89 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix e cofix + Inductive.check_cofix ~chk:true e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix e fix + Inductive.check_fix ~chk:true e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 03fe2122c0..d9f490ba55 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env fix + (try check_fix env ~chk:true fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env fix; raise (Found indexes) + try check_fix env ~chk:true fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env ~chk:true cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb5927dbf7..0bb2979c2a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env fix; + check_fix env ~chk:true fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix env ~chk:true cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> -- cgit v1.2.3 From 9f4e67a7c9f22ca853e76f4837a276a6111bf159 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Sep 2015 09:27:50 +0200 Subject: Prevent pretyping from checking well-guardedness unnecessarily. The `search_guard` function is called to infer the recursive argument of fixpoints. For each potential argument, it tests whether it is called structurally, calling the kernel test. When a single argument is available either because `{struct x}` was specified, or because there is a single inductive argument, the kernel test is performed, despite the fact that the kernel will do it later, and the kernel error reraised. It is unnecessary. --- pretyping/pretyping.ml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d9f490ba55..94749648e0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -73,14 +73,9 @@ let search_guard loc env possible_indexes fixdefs = (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then - let indexes = Array.of_list (List.map List.hd possible_indexes) in - let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~chk:true fix - with reraise -> - let (e, info) = Errors.push reraise in - let info = Loc.add_loc info loc in - iraise (e, info)); - indexes + (* in this case, errors are delegated to the kernel, which will + check well-guardedness if required. *) + Array.of_list (List.map List.hd possible_indexes) else (* we now search recursively among all combinations *) (try -- cgit v1.2.3 From 64e94267cb80adc1b4df782cc83a579ee521b59b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 5 Apr 2016 09:25:54 +0200 Subject: Revert "Prevent pretyping from checking well-guardedness unnecessarily." This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159. --- pretyping/pretyping.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 94749648e0..d9f490ba55 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -73,9 +73,14 @@ let search_guard loc env possible_indexes fixdefs = (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then - (* in this case, errors are delegated to the kernel, which will - check well-guardedness if required. *) - Array.of_list (List.map List.hd possible_indexes) + let indexes = Array.of_list (List.map List.hd possible_indexes) in + let fix = ((indexes, 0),fixdefs) in + (try check_fix env ~chk:true fix + with reraise -> + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); + indexes else (* we now search recursively among all combinations *) (try -- cgit v1.2.3 From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 7 Jun 2016 09:52:43 +0200 Subject: Assume totality: dedicated type rather than bool The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument --- pretyping/inductiveops.ml | 4 ++-- pretyping/pretyping.ml | 6 +++--- pretyping/typing.ml | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index efea4bec89..930b0413e5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix ~chk:true e cofix + Inductive.check_cofix ~flags:{check_guarded=true} e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix ~chk:true e fix + Inductive.check_fix ~flags:{check_guarded=true} e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d9f490ba55..8fbcc8e5e7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~chk:true fix + (try check_fix env ~flags:{Declarations.check_guarded=true} fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env ~chk:true fix; raise (Found indexes) + try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~chk:true cofix + (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0bb2979c2a..fa6fd9677b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env ~chk:true fix; + check_fix env ~flags:{Declarations.check_guarded=true} fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env ~chk:true cofix; + check_cofix env ~flags:{Declarations.check_guarded=true} cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> -- cgit v1.2.3 From 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 15 Jun 2016 19:19:58 +0200 Subject: Allow `Pretyping.search_guard` to not check guard This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper. --- pretyping/pretyping.ml | 21 +++++++++++++++++---- pretyping/pretyping.mli | 2 +- 2 files changed, 18 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8fbcc8e5e7..c86a4e3e48 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,14 +68,17 @@ open Inductiveops exception Found of int array -let search_guard loc env possible_indexes fixdefs = +(* spiwack: I chose [tflags] rather than [flags], like in the rest of + the code, for the argument name to avoid interference with the + argument for [inference_flags] also used in this module. *) +let search_guard ~tflags loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~flags:{Declarations.check_guarded=true} fix + (try check_fix env ~flags:tflags fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -87,7 +90,13 @@ let search_guard loc env possible_indexes fixdefs = List.iter (fun l -> let indexes = Array.of_list l in - let fix = ((indexes, 0),fixdefs) in + let fix = ((indexes, 0),fixdefs) in + (* spiwack: We search for a unspecified structural + argument under the assumption that we need to check the + guardedness condition (otherwise the first inductive argument + will be chosen). A more robust solution may be to raise an + error when totality is assumed but the strutural argument is + not specified. *) try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); @@ -533,7 +542,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var vn) in let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in + let indexes = + search_guard + ~tflags:{Declarations.check_guarded=true} + loc env possible_indexes fixdecls + in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513e..1ef3da1509 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) -val search_guard : +val search_guard : tflags:Declarations.typing_flags -> Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -- cgit v1.2.3