* 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
;;
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 _ ->
let itl_len = List.length itl in
let (name,_,ty,cl) = List.nth itl i in
let cl_len = List.length cl in
- if (itl_len = 1 && cl_len <= 1) then
+ 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 a singleton or empty non recursive and non informative
+ (* is it a singleton or empty non recursive and non informative
definition? *)
non_informative, ugraph
else
- false,ugraph
+ false,ugraph
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(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)
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,_,_) ->