let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+ CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
;;
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
let rec split l n =
match (l,n) with
let ugraph_dust =
(match uobj with
- C.Constant (_,Some te,ty,_) ->
+ C.Constant (_,Some te,ty,_,_) ->
let _,ugraph = type_of ~logger ty ugraph in
let type_of_te,ugraph' = type_of ~logger te ugraph in
let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
(CicPp.ppterm ty)))
else
ugraph'
- | C.Constant (_,None,ty,_) ->
+ | C.Constant (_,None,ty,_,_) ->
(* only to check that ty is well-typed *)
let _,ugraph' = type_of ~logger ty ugraph in
ugraph'
- | C.CurrentProof (_,conjs,te,ty,_) ->
+ | C.CurrentProof (_,conjs,te,ty,_,_) ->
let _,ugraph1 =
List.fold_left
(fun (metasenv,ugraph) ((_,context,ty) as conj) ->
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph_dust
in
match cobj,ugraph with
- (C.Constant (_,_,ty,_)),g -> ty,g
- | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g
+ (C.Constant (_,_,ty,_,_)),g -> ty,g
+ | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
| _ ->
raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
match CicEnvironment.is_type_checked ~trust:true ugraph uri with
- CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph'
- | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
+ CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+ | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
logger#log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
let _,ugraph1 = type_of ~logger ty ugraph in
CicEnvironment.set_type_checking_info uri ;
logger#log (`Type_checking_completed uri) ;
match CicEnvironment.is_type_checked ~trust:false ugraph uri with
- CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') ->
+ CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
ty,ugraph'
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
ty,ugraph2)
| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
let (ok,paramsno,ity,cl,name) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (name,_,ity,cl) = List.nth tl i in
(List.length tl = 1, paramsno, ity, cl, name)
| _ ->
(* inductive block definition. *)
and check_mutual_inductive_defs uri obj ugraph =
match obj with
- Cic.InductiveDefinition (itl, params, indparamsno) ->
+ Cic.InductiveDefinition (itl, params, indparamsno, _) ->
typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
| _ ->
raise (TypeCheckerFailure (
)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,arity,_) = List.nth dl i in
arity,ugraph1
| _ ->
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty,ugraph1
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let tys =
List.map
(fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
List.map (fun (n,_,ty,_) ->
(fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
exp_named_subst true
| C.MutCase (uri,i,outtype,term,pl) ->
- (match term with
+ (match CicReduction.whd context term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let len = List.length tl in
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
List.map
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,_,_,cl) = List.nth itl i in
let (_,cons) = List.nth cl (j - 1) in
CicSubstitution.subst_vars exp_named_subst cons
(*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,_,_) ->
+ 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
when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,paramsno) ->
+ C.InductiveDefinition (itl,_,paramsno,_) ->
let tys =
List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
in
| (C.Sort C.Set | C.Sort C.CProp) ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,_,_,cl) = List.nth itl i in
(* is a singleton definition? *)
List.length cl = 1,ugraph1
(* TASSI: da verificare *)
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,paramsno) ->
+ C.InductiveDefinition (itl,_,paramsno,_) ->
let (_,_,_,cl) = List.nth itl i in
let tys =
List.map
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
in
aux 1 canonical_context
in
~subst metasenv context canonical_context l ugraph
in
(* assuming subst is well typed !!!!! *)
- ((CicSubstitution.lift_meta l ty), ugraph1)
- (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+ ((CicSubstitution.subst_meta l ty), ugraph1)
+ (* type_of_aux context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let ugraph1 =
check_metasenv_consistency ~logger
~subst metasenv context canonical_context l ugraph
in
- ((CicSubstitution.lift_meta l ty),ugraph1))
+ ((CicSubstitution.subst_meta l ty),ugraph1))
(* TASSI: CONSTRAINTS *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
else raise
(TypeCheckerFailure
(sprintf
- ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
- (CicPp.ppterm typ) (U.string_of_uri uri) i))
+ ("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' ->
if U.eq uri uri' && i = i' then
else raise
(TypeCheckerFailure
(sprintf
- "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
- (CicPp.ppterm typ') (U.string_of_uri uri) i))
+ ("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))
| _ ->
raise
(TypeCheckerFailure
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (_,_,parsno) -> parsno
+ C.InductiveDefinition (_,_,parsno,_) -> parsno
| _ ->
raise (TypeCheckerFailure
("Unknown mutual inductive definition:" ^
with Not_found -> assert false
in
(match obj with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
if is_inductive then None else (Some uri)
| _ ->
| C.Appl ((C.MutInd (uri,i,_))::_) ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
if is_inductive then None else (Some uri)
| _ ->
(* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') ->
- (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+ (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking uri) ;
- (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+ (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
let ugraph1 =
(match uobj with
- C.Constant (_,Some te,ty,_) ->
+ C.Constant (_,Some te,ty,_,_) ->
let _,ugraph1 = type_of ~logger ty ugraph in
let ty_te,ugraph2 = type_of ~logger te ugraph1 in
let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
("Unknown constant:" ^ U.string_of_uri uri))
else
ugraph3
- | C.Constant (_,None,ty,_) ->
+ | C.Constant (_,None,ty,_,_) ->
(* only to check that ty is well-typed *)
let _,ugraph1 = type_of ~logger ty ugraph in
ugraph1
- | C.CurrentProof (_,conjs,te,ty,_) ->
+ | C.CurrentProof (_,conjs,te,ty,_,_) ->
let _,ugraph1 =
List.fold_left
(fun (metasenv,ugraph) ((_,context,ty) as conj) ->
(CicPp.ppterm ty)))
else
ugraph4
- | C.Variable (_,bo,ty,_) ->
+ | C.Variable (_,bo,ty,_,_) ->
(* only to check that ty is well-typed *)
let _,ugraph1 = type_of ~logger ty ugraph in
(match bo with
object.
*)
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1
;;