(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *)
let rec weakly_positive ~subst context n nn uri te =
(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
- let dummy_mutind = C.Implicit `Hole in
+ let dummy = C.Sort (C.Type ~-1) in
(*CSC: mettere in cicSubstitution *)
- let rec subst_inductive_type_with_dummy_mutind _ = function
- | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind
- | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri ->
- dummy_mutind
- | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t
+ let rec subst_inductive_type_with_dummy _ = function
+ | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
+ | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl)
+ when NUri.eq uri' uri -> dummy
+ | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
in
match R.whd context te with
| C.Const (Ref.Ref (_,uri',Ref.Ind _))
- | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true
+ | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_)
+ when NUri.eq uri' uri -> true
| C.Prod (name,source,dest) when
- does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+ does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
(* dummy abstraction, so we behave as in the anonimous case *)
strictly_positive ~subst context n nn
- (subst_inductive_type_with_dummy_mutind () source) &&
- weakly_positive ~subst ((name,C.Decl source)::context)
- (n + 1) (nn + 1) uri dest
+ (subst_inductive_type_with_dummy () source) &&
+ weakly_positive ~subst ((name,C.Decl source)::context)
+ (n + 1) (nn + 1) uri dest
| C.Prod (name,source,dest) ->
does_not_occur ~subst context n nn
- (subst_inductive_type_with_dummy_mutind () source)&&
- weakly_positive ~subst ((name,C.Decl source)::context)
- (n + 1) (nn + 1) uri dest
+ (subst_inductive_type_with_dummy () source)&&
+ weakly_positive ~subst ((name,C.Decl source)::context)
+ (n + 1) (nn + 1) uri dest
| _ ->
raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
(* the inductive type indexes are s.t. n < x <= nn *)
and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
match R.whd context te with
- | C.Appl ((C.Rel m)::tl) when m = i ->
+ | C.Appl ((C.Rel m)::tl) as reduct when m = i ->
let last =
List.fold_left
(fun k x ->
else
match R.whd context x with
| C.Rel m when m = n - (indparamsno - k) -> k - 1
- | _ -> raise (TypeCheckerFailure (lazy
- ("Non-positive occurence in mutual inductive definition(s) [1]" ^
- NUri.string_of_uri uri))))
+ | y -> raise (TypeCheckerFailure (lazy
+ ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+ string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+ "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct))))
indparamsno tl
in
if last = 0 then
(lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
NUri.string_of_uri uri)))
| C.Prod (name,source,dest) when
- does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+ does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
strictly_positive ~subst context n nn source &&
are_all_occurrences_positive ~subst
((name,C.Decl source)::context) uri indparamsno
(i+1) (n + 1) (nn + 1) dest
| C.Prod (name,source,dest) ->
- does_not_occur ~subst context n nn source &&
+ if not (does_not_occur ~subst context n nn source) then
+ raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
+ NCicPp.ppterm ~context ~metasenv:[] ~subst te)));
are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
uri indparamsno (i+1) (n + 1) (nn + 1) dest
| _ ->
and guarded_by_destructors ~subst ~metasenv context recfuns t =
let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
- let rec aux (context, recfuns, x, safes as k) = function
+ let rec aux (context, recfuns, x, safes as k) t =
+ match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*)
| C.Rel m as t when List.mem_assoc m recfuns ->
raise (NotGuarded (lazy
(NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
raise (NotGuarded (lazy
(NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller")));
List.iter (aux k) tl
+ (*
+ | C.Appl (C.Const ((Ref.Ref (_,_,Ref.Fix (i,j))) as r)::args) ->
+ List.iter (aux k) args;
+ let fixes,_,_ = E.get_checked_fixes r in
+ let _,_,_,_,bo = List.nth fixes i in
+ let bo_wout_lam, context = eat_lambdas ~subst ~metasenv context j in
+ (* debruijna body..... *) assert false
+*)
| C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
(match R.whd ~subst context term with
| C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x ->
and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
match R.whd ~subst context te with
| C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd"))
- | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _
- | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) ->
- raise (AssertFailure (lazy "not a constructor"))
- | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl"))
+ | C.Lambda (name, s, t) ->
+ is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
| C.Appl (he::_) ->
- (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
- (*CSC: solo perche' non abbiamo trovato controesempi *)
- (*TASSI: da capire soprattutto se he รจ un altro fix che non ha ridotto...*)
- is_really_smaller ~subst ~metasenv k he
+ is_really_smaller ~subst ~metasenv k he
+ | C.Appl _
+ | C.Rel _
| C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
| C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
(*| C.Fix (_, fl) ->
is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
x_plus_len safes' bo
) fl true*)
- | C.Meta _ ->
- true (* XXX if this check is repeated when the user completes the
- definition *)
+ | C.Meta _ -> true
| C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
(match term with
| C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
is_really_smaller ~subst ~metasenv k e)
pl cl
| _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl)
+ | _ -> assert false
and returns_a_coinductive ~subst context ty =
match R.whd ~subst context ty with
projects / helm.git / blobdiff