| t -> t
in
match CicReduction.whd context te with
+(*
C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
+*)
+ C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
| C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
| C.Prod (C.Anonymous,source,dest) ->
strictly_positive context n nn
(* dummy abstraction, so we behave as in the anonimous case *)
strictly_positive context n nn
(subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
+ weakly_positive ((Some (name,(C.Decl source)))::context)
(n + 1) (nn + 1) uri dest
| C.Prod (name,source,dest) ->
- does_not_occur context n nn
- (subst_inductive_type_with_dummy_mutind source)&&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
+ does_not_occur context n nn
+ (subst_inductive_type_with_dummy_mutind source)&&
+ weakly_positive ((Some (name,(C.Decl source)))::context)
+ (n + 1) (nn + 1) uri dest
| _ ->
raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
let module C = Cic in
let module U = UriManager in
match CicReduction.whd context te with
- C.Rel _ -> true
+ | t when does_not_occur context n nn t -> true
+ | C.Rel _ -> true
| C.Cast (te,ty) ->
(*CSC: bisogna controllare ty????*)
strictly_positive context n nn te
| C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
let (ok,paramsno,ity,cl,name) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let (name,_,ity,cl) = List.nth tl i in
- (List.length tl = 1, paramsno, ity, cl, name)
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
- in
- let (params,arguments) = split tl paramsno in
- let lifted_params = List.map (CicSubstitution.lift 1) params in
- let cl' =
+ match o with
+ C.InductiveDefinition (tl,_,paramsno,_) ->
+ let (name,_,ity,cl) = List.nth tl i in
+ (List.length tl = 1, paramsno, ity, cl, name)
+ (* (true, paramsno, ity, cl, name) *)
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
+ in
+ let (params,arguments) = split tl paramsno in
+ let lifted_params = List.map (CicSubstitution.lift 1) params in
+ let cl' =
List.map
- (fun (_,te) ->
- instantiate_parameters lifted_params
- (CicSubstitution.subst_vars exp_named_subst te)
- ) cl
- in
+ (fun (_,te) ->
+ instantiate_parameters lifted_params
+ (CicSubstitution.subst_vars exp_named_subst te)
+ ) cl
+ in
ok &&
- List.fold_right
+ List.fold_right
(fun x i -> i && does_not_occur context n nn x)
arguments true &&
(*CSC: MEGAPATCH3 (sara' quella giusta?)*)
- List.fold_right
+ List.fold_right
(fun x i ->
- i &&
- weakly_positive
- ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
- x
+ i &&
+ weakly_positive
+ ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+ x
) cl' true
- | t -> does_not_occur context n nn t
-
+ | t -> false
+
(* the inductive type indexes are s.t. n < x <= nn *)
and are_all_occurrences_positive context uri indparamsno i n nn te =
let module C = Cic in
(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 &&
+ let b = strictly_positive context n nn source in
+ b &&
are_all_occurrences_positive
((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
(i+1) (n + 1) (nn + 1) dest
(are_all_occurrences_positive tys uri indparamsno i 0 len
debrujinedte)
then
+ begin
+ prerr_endline (UriManager.string_of_uri uri);
+ prerr_endline (string_of_int (List.length tys));
raise
(TypeCheckerFailure
- (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
+ (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end
else
ugraph'
) ugraph cl in
| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
C.Rel m when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
| C.MutCase (uri,i,outtype,term,pl) ->
(match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let debrujinedty = debrujin_constructor uri len ty in
(id, snd (split_prods ~subst tys paramsno ty),
snd (split_prods ~subst tys paramsno debrujinedty)
- )) cl
+ )) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,len,isinductive,paramsno,cl')
+ (tys@lefts,len,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun (p,(_,c,brujinedc)) i ->
- let rl' = recursive_args tys 0 len brujinedc in
+ let rl' = recursive_args lefts_and_tys 0 len brujinedc in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
guarded_by_destructors ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (tys,len,isinductive,paramsno,cl) =
+ let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno,_) ->
let cl' =
List.map
(fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl
+ (id, snd (split_prods ~subst tys paramsno ty))) cl in
+ let lefts =
+ match tl with
+ [] -> assert false
+ | (_,_,ty,_)::_ ->
+ fst (split_prods ~subst [] paramsno ty)
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ (tys@lefts,List.length tl,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
+ recursive_args lefts_and_tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonymous,so,type_of_branch ~subst
+ C.Prod (name,so,type_of_branch ~subst
((Some (name,(C.Decl so)))::context) argsno need_dummy
(CicSubstitution.lift 1 outtype) term' de)
- | _ -> raise (AssertFailure (lazy "20"))
+ | _ -> raise (AssertFailure (lazy "20"))
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_gt t' t ugraph in
(C.Sort (C.Type t')),ugraph1
- (* TASSI: CONSTRAINTS *)
| C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
- | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+ | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
| C.Cast (te,ty) as t ->
let _,ugraph1 = type_of_aux ~logger context ty ugraph in
let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
type_of_aux ~logger
((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
in
- (CicSubstitution.subst s ty1),ugraph2
+ (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
let tlbody_and_type,ugraph2 =
R.are_convertible
~subst ~metasenv context ty_p ty_branch ugraph3
in
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
if not b1 then
debug_print (lazy
("#### " ^ CicPp.ppterm ty_p ^
begin
CicReduction.fdebug := -1 ;
eat_prods ~subst context
- (CicSubstitution.subst hete t) tl ugraph1
+ (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+ tl ugraph1
(*TASSI: not sure *)
end
else
(** wrappers which instantiate fresh loggers *)
+let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
+
let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
- type_of_aux' ~logger ~subst metasenv context t ugraph
+ profiler.HExtlib.profile
+ (type_of_aux' ~logger ~subst metasenv context t) ugraph
let typecheck_obj uri obj =
let logger = new CicLogger.logger in
projects / helm.git / blobdiff