* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
* ...") *)
raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) "")))
;;
-let debug_print = fun _ -> () ;;
+let debug_print = fun _ -> ();;
let rec split l n =
match (l,n) with
raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
;;
-let debrujin_constructor uri number_of_types =
- let rec aux k =
+let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+ let rec aux k t =
let module C = Cic in
- function
+ let res =
+ match t with
C.Rel n as t when n <= k -> t
| C.Rel _ ->
raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
C.Var (uri,exp_named_subst')
| C.Meta (i,l) ->
let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
- C.Meta (i,l)
+ C.Meta (i,l')
| C.Sort _
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
fl
in
C.CoFix (i, liftedfl)
+ in
+ cb t res;
+ res
in
aux 0
;;
C.Rel m when m = n - (indparamsno - k) -> k - 1
| _ ->
raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+ (lazy
+ ("Non-positive occurence in mutual inductive definition(s) [1]" ^
UriManager.string_of_uri uri)))
) indparamsno tl
in
List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
else
raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+ (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
UriManager.string_of_uri uri)))
| C.Rel m when m = i ->
if indparamsno = 0 then
true
else
raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+ (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
UriManager.string_of_uri uri)))
| C.Prod (C.Anonymous,source,dest) ->
strictly_positive context n nn source &&
ugraph'
) ugraph cl in
(i + 1),ugraph''
- ) itl (1,ugraph)
+ ) itl (1,ugrap1)
in
ugraph2
| C.Lambda _
| C.LetIn _ ->
raise (AssertFailure (lazy "25"))(* due to type-checking *)
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty
- when uri == coInductiveTypeURI ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
guarded_by_constructors ~subst context n nn true te []
coInductiveTypeURI
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) ->
guarded_by_constructors ~subst context n nn true te tl
coInductiveTypeURI
| C.Appl _ ->
need_dummy ind arity1 arity2 ugraph =
let module C = Cic in
let module U = UriManager in
- match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with
+ let arity1 = CicReduction.whd ~subst context arity1 in
+ let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
+ match arity1, CicReduction.whd ~subst context arity2 with
(C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
let b,ugraph1 =
CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
ugraph1
else
false,ugraph1
+ | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
+ let b,ugraph1 =
+ CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
+ if not b then
+ false,ugraph1
+ else
+ check_allowed_sort_elimination_aux ugraph1
+ ((Some (name,C.Decl so))::context) ta true
| (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
| (C.Sort C.Prop, C.Sort C.Set)
| (C.Sort C.Prop, C.Sort C.CProp)
| (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
- (* TASSI: da verificare *)
-(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition or the empty proposition? *)
- (List.length cl = 1 || List.length cl = 0) , ugraph
+ C.InductiveDefinition (itl,_,paramsno,_) ->
+ let itl_len = List.length itl in
+ let (name,_,ty,cl) = List.nth itl i in
+ let cl_len = List.length cl in
+ if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
+ let non_informative,ugraph =
+ if cl_len = 0 then true,ugraph
+ else
+ is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
+ paramsno (snd (List.nth cl 0)) ugraph
+ in
+ (* is it a singleton or empty non recursive and non informative
+ definition? *)
+ non_informative, ugraph
+ else
+ false,ugraph
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
| (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
| (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
| ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
- (* TASSI: da verificare *)
when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
UriManager.string_of_uri uri)))
)
| (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
- (* TASSI: da verificare *)
- | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop -> true,ugraph1
- | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition or the empty proposition? *)
- (List.length cl = 1 || List.length cl = 0),ugraph1
- | _ ->
- raise (TypeCheckerFailure
- (lazy
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))))
- | _ -> false,ugraph1)
- | ((C.Sort C.Set, C.Prod (name,so,ta))
- | (C.Sort C.CProp, C.Prod (name,so,ta)))
- when not need_dummy ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop
- | C.Sort C.Set -> true,ugraph1
- | C.Sort C.CProp -> true,ugraph1
- | C.Sort (C.Type _) ->
- (* TASSI: da verificare *)
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,paramsno,_) ->
- let (_,_,_,cl) = List.nth itl i in
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
- in
- (List.fold_right
- (fun (_,x) (i,ugraph) ->
- if i then
- is_small ~logger tys paramsno x ugraph
- else
- false,ugraph
- ) cl (true,ugraph1))
- | _ ->
- raise (TypeCheckerFailure (lazy
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- )
- | _ -> raise (AssertFailure (lazy "19"))
- )
- | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
- (* TASSI: da verificare *)
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
| (_,_) -> false,ugraph
+ in
+ check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
and type_of_branch ~subst context argsno need_dummy outtype term constype =
let module C = Cic in
(lazy (sprintf
("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
(CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
- | C.Appl
- ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+ | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
if U.eq uri uri' && i = i' then
let params,args =
split tl (List.length tl - k)
(* is a small constructor? *)
(*CSC: ottimizzare calcolando staticamente *)
-and is_small ~logger context paramsno c ugraph =
- let rec is_small_aux ~logger context c ugraph =
+and is_small_or_non_informative ~condition ~logger context paramsno c ugraph =
+ let rec is_small_or_non_informative_aux ~logger context c ugraph =
let module C = Cic in
match CicReduction.whd context c with
C.Prod (n,so,de) ->
let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
- let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
+ let b = condition s in
if b then
- is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
+ is_small_or_non_informative_aux
+ ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
else
false,ugraph1
| _ -> true,ugraph (*CSC: we trust the type-checker *)
in
let (context',dx) = split_prods ~subst:[] context paramsno c in
- is_small_aux ~logger context' dx ugraph
+ is_small_or_non_informative_aux ~logger context' dx ugraph
+
+and is_small ~logger =
+ is_small_or_non_informative
+ ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set)
+ ~logger
+
+and is_non_informative ~logger =
+ is_small_or_non_informative
+ ~condition:(fun s -> s=Cic.Sort Cic.Prop)
+ ~logger
and type_of ~logger t ugraph =
(*CSC
let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
if not b then
raise (TypeCheckerFailure
- (lazy "the type of the body is not the one expected"))
+ (lazy
+ ("the type of the body is not the one expected:\n" ^
+ CicPp.ppterm ty_te ^ "\nvs\n" ^
+ CicPp.ppterm ty)))
else
ugraph
| C.Constant (_,None,ty,_,_) ->
let logger = new CicLogger.logger in
typecheck_obj ~logger uri obj
+(* check_allowed_sort_elimination uri i s1 s2
+ This function is used outside the kernel to determine in advance whether
+ a MutCase will be allowed or not.
+ [uri,i] is the type of the term to match
+ [s1] is the sort of the term to eliminate (i.e. the head of the arity
+ of the inductive type [uri,i])
+ [s2] is the sort of the goal (i.e. the head of the type of the outtype
+ of the MutCase) *)
+let check_allowed_sort_elimination uri i s1 s2 =
+ fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
+ ~logger:(new CicLogger.logger) [] uri i true
+ (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
+ CicUniv.empty_ugraph)
projects / helm.git / blobdiff