(* $Id$ *)
module C = NCic
-module R = NCicReduction
module Ref = NReference
+module R = NCicReduction
module S = NCicSubstitution
module U = NCicUtils
module E = NCicEnvironment
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
+(*
let raise = function
| TypeCheckerFailure s as e -> prerr_endline (Lazy.force s); raise e
| e -> raise e
;;
+*)
type recf_entry =
| Evil of int (* rno *)
if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
| C.Meta _ -> t
| C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no)))
- | C.Const (Ref.Ref (uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
+ | C.Const (Ref.Ref (uri1,Ref.Ind (_,no,_))) when NUri.eq uri uri1 ->
C.Rel (k + number_of_types - no)
| t -> U.map (fun _ k -> k+1) k aux t
in
let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
match t1, t2 with
| C.Sort s1, C.Sort C.Prop -> t2
- | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2))
+ | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2))
| C.Sort _,C.Sort (C.Type _) -> t2
- | C.Sort (C.Type _) , C.Sort C.CProp -> t1
- | C.Sort _, C.Sort C.CProp
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
| C.Sort _, C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
let specialize_inductive_type_constrs ~subst context ty_term =
match R.whd ~subst context ty_term with
- | C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref)
- | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
+ | C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref)
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref) :: _ ) as ty ->
let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
let left_args,_ = HExtlib.split_nth leftno args in
let len = List.length context in
let context_dcl =
match E.get_checked_obj r_uri with
- | _,_,_,_, NCic.Inductive (_,_,tys,_) ->
+ | _,_,_,_, C.Inductive (_,_,tys,_) ->
context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys
| _ -> assert false
in
let dummy = C.Sort C.Prop in
(*CSC: mettere in cicSubstitution *)
let rec subst_inductive_type_with_dummy _ = function
- | C.Const (Ref.Ref (uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
- | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0))))::tl)
+ | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
+ | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::tl)
when NUri.eq uri' uri -> dummy
| t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
in
strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
List.for_all (does_not_occur ~subst context n nn) tl
- | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as r)::tl) ->
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as r)::tl) ->
let _,paramsno,tyl,_,i = E.get_checked_indtys r in
let _,name,ity,cl = List.nth tyl i in
let ok = List.length tyl = 1 in
*)
eat_prods ~subst ~metasenv context he ty_he args_with_ty
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
- | C.Match (Ref.Ref (_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
+ | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,outtype,term,pl) ->
let outsort = typeof_aux context outtype in
let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
let constructorsno =
(PP.ppterm ~subst ~metasenv ~context so)
)));
(match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
- | (C.Sort (C.CProp | C.Type _), C.Sort _)
+ | (C.Sort C.Type _, C.Sort _)
| (C.Sort C.Prop, C.Sort C.Prop) -> ()
- | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+ | (C.Sort C.Prop, C.Sort C.Type _) ->
(* TODO: we should pass all these parameters since we
* have them already *)
let inductive,leftno,itl,_,i = E.get_checked_indtys r in
ignore
(List.fold_right
(fun (_,_,ty,cl) i ->
- let _,ty_sort = split_prods ~subst [] ~-1 ty in
+ let context,ty_sort = split_prods ~subst [] ~-1 ty in
+ let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
List.iter
(fun (_,name,te) ->
-(*CSC: assicurarmi che i sx siano esattamente gli stessi! *)
let te = debruijn uri len [] te in
let context,te = split_prods ~subst tys leftno te in
+ let _,chopped_context_rev =
+ HExtlib.split_nth (List.length tys) (List.rev context) in
+ let sx_context_te_rev,_ =
+ HExtlib.split_nth leftno chopped_context_rev in
+ (try
+ ignore (List.fold_left2
+ (fun context item1 item2 ->
+ let convertible =
+ match item1,item2 with
+ (n1,C.Decl ty1),(n2,C.Decl ty2) ->
+ n1 = n2 && R.are_convertible ~subst context ty1 ty2
+ | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
+ n1 = n2
+ && R.are_convertible ~subst context ty1 ty2
+ && R.are_convertible ~subst context bo1 bo2
+ | _,_ -> false
+ in
+ if not convertible then
+ raise (TypeCheckerFailure (lazy
+ ("Mismatch between the left parameters of the constructor " ^
+ "and those of its inductive type")))
+ else
+ item1::context
+ ) [] sx_context_ty_rev sx_context_te_rev)
+ with Invalid_argument _ -> assert false);
let con_sort = typeof ~subst ~metasenv context te in
(match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
(C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
" of the constructor is not included in the inductive" ^
" type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
| C.Sort _, C.Sort C.Prop
- | C.Sort C.CProp, C.Sort C.CProp
| C.Sort _, C.Sort C.Type _ -> ()
| _, _ ->
raise
) bos
in
List.iter (fun (bo,k) -> aux k bo) bos_and_ks
- | C.Match (Ref.Ref (uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
+ | C.Match (Ref.Ref (uri,Ref.Ind (true,_,_)),outtype,term,pl) as t ->
(match R.whd ~subst context term with
| C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
let ty = typeof ~subst ~metasenv context term in
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h && List.for_all (does_not_occur ~subst context n nn) tl
| C.Const (Ref.Ref (_,Ref.Con _)) -> true
- | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j)) as ref) :: tl) as t ->
- let _, paramsno, _, _, _ = E.get_checked_indtys ref in
+ | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j,paramsno))) :: tl) as t ->
let ty_t = typeof ~subst ~metasenv context t in
let dc_ctx, dcl, start, stop =
specialize_and_abstract_constrs ~subst indURI indlen context ty_t in
| C.Appl []
| C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
| C.Meta _ -> true
- | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_)),outtype,term,pl) ->
+ | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_,_)),outtype,term,pl) ->
(match term with
| C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
if not isinductive then
and returns_a_coinductive ~subst context ty =
match R.whd ~subst context ty with
- | C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)
- | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)::_) ->
+ | C.Const (Ref.Ref (uri,Ref.Ind (false,_,_)) as ref)
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_,_)) as ref)::_) ->
let _, _, itl, _, _ = E.get_checked_indtys ref in
Some (uri,List.length itl)
| C.Prod (n,so,de) ->
| _ -> None
and type_of_constant ((Ref.Ref (uri,_)) as ref) =
+ let error () =
+ raise (TypeCheckerFailure (lazy "Inconsistent cached infos in reference"))
+ in
match E.get_checked_obj uri, ref with
- | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Ind (_,i)) ->
+ | (_,_,_,_,C.Inductive(isind1,lno1,tl,_)),Ref.Ref(_,Ref.Ind (isind2,i,lno2))->
+ if isind1 <> isind2 || lno1 <> lno2 then error ();
let _,_,arity,_ = List.nth tl i in arity
- | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j)) ->
+ | (_,_,_,_,C.Inductive (_,lno1,tl,_)), Ref.Ref (_,Ref.Con (i,j,lno2)) ->
+ if lno1 <> lno2 then error ();
let _,_,_,cl = List.nth tl i in
let _,_,arity = List.nth cl (j-1) in
arity
- | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,(Ref.Fix (i,_,_)|Ref.CoFix i)) ->
+ | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.CoFix i) ->
let _,_,_,arity,_ = List.nth fl i in
arity
- | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,(Ref.Def _|Ref.Decl)) -> ty
+ | (_,h1,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.Fix (i,recno2,h2)) ->
+ let _,_,recno1,arity,_ = List.nth fl i in
+ if h1 <> h2 || recno1 <> recno2 then error ();
+ arity
+ | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Decl) -> ty
+ | (_,h1,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Def h2) ->
+ if h1 <> h2 then error ();
+ ty
| _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
;;
"the type of the definiens for %s in the context is not "^^
"convertible with the declared one.\n"^^
"inferred type:\n%s\nexpected type:\n%s")
- name
- (PP.ppterm ~subst ~metasenv ~context ty')
+ name (PP.ppterm ~subst ~metasenv ~context ty')
(PP.ppterm ~subst ~metasenv ~context ty))))
end;
d::context
typecheck_metasenv metasenv;
typecheck_subst ~metasenv subst;
match kind with
- | C.Constant (_,_,Some te,ty,_) ->
+ | C.Constant (relevance,_,Some te,ty,_) ->
let _ = typeof ~subst ~metasenv [] ty in
let ty_te = typeof ~subst ~metasenv [] te in
if not (R.are_convertible ~subst [] ty_te ty) then
"inferred type:\n%s\nexpected type:\n%s")
(PP.ppterm ~subst ~metasenv ~context:[] ty_te)
(PP.ppterm ~subst ~metasenv ~context:[] ty))))
- | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
+ | C.Constant (relevance,_,None,ty,_) ->
+ ignore (typeof ~subst ~metasenv [] ty)
| C.Inductive (is_ind, leftno, tyl, _) ->
check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
| C.Fixpoint (inductive,fl,_) ->
let types, kl =
List.fold_left
- (fun (types,kl) (_,name,k,ty,_) ->
+ (fun (types,kl) (relevance,name,k,ty,_) ->
let _ = typeof ~subst ~metasenv [] ty in
((name,C.Decl ty)::types, k::kl)
) ([],[]) fl
projects / helm.git / blobdiff