let rec aux k =
let module C = Cic in
function
- C.Rel _ as t -> t
+ C.Rel n as t when n <= k -> t
+ | C.Rel _ ->
+ raise (NotWellTyped ("Debrujin: open term found"))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
Logger.log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
let _ = type_of ty in ()
| C.CurrentProof (_,conjs,te,ty,_) ->
- (*CSC: bisogna controllare anche il metasenv!!! *)
- let _ = type_of_aux' conjs [] ty in
- if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
- then
- raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+ let _ =
+ List.fold_left
+ (fun metasenv ((_,context,ty) as conj) ->
+ ignore (type_of_aux' metasenv context ty) ;
+ metasenv @ [conj]
+ ) [] conjs
+ in
+ let _ = type_of_aux' conjs [] ty in
+ if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
+ then
+ raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
| _ -> raise (WrongUriToConstant (U.string_of_uri uri))
) ;
CicEnvironment.set_type_checking_info uri ;
Logger.log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
in
let module R = CicReduction in
let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
| CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
Logger.log (`Start_type_checking uri) ;
| _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
(* Main function to checks the correctness of a mutual *)
-(* inductive block definition. *)
-and check_mutual_inductive_defs uri =
+(* inductive block definition. This is the function *)
+(* exported to the proof-engine. *)
+and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
let module U = UriManager in
- function
- Cic.InductiveDefinition (itl, _, indparamsno) ->
- (* let's check if the arity of the inductive types are well *)
- (* formed *)
- List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
+ (* let's check if the arity of the inductive types are well *)
+ (* formed *)
+ List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
- (* let's check if the types of the inductive constructors *)
- (* are well formed. *)
- (* In order not to use type_of_aux we put the types of the *)
- (* mutual inductive types at the head of the types of the *)
- (* constructors using Prods *)
- let len = List.length itl in
- let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
- let _ =
- List.fold_right
- (fun (_,_,_,cl) i ->
- List.iter
- (fun (name,te) ->
- let debrujinedte = debrujin_constructor uri len te in
- let augmented_term =
- List.fold_right
- (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
- itl debrujinedte
- in
- let _ = type_of augmented_term in
- (* let's check also the positivity conditions *)
- if
- not
- (are_all_occurrences_positive tys uri indparamsno i 0 len
- debrujinedte)
- then
- raise (NotPositiveOccurrences (U.string_of_uri uri))
- ) cl ;
- (i + 1)
- ) itl 1
- in
- ()
- | _ ->
- raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ (* let's check if the types of the inductive constructors *)
+ (* are well formed. *)
+ (* In order not to use type_of_aux we put the types of the *)
+ (* mutual inductive types at the head of the types of the *)
+ (* constructors using Prods *)
+ let len = List.length itl in
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
+ let _ =
+ List.fold_right
+ (fun (_,_,_,cl) i ->
+ List.iter
+ (fun (name,te) ->
+ let debrujinedte = debrujin_constructor uri len te in
+ let augmented_term =
+ List.fold_right
+ (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
+ itl debrujinedte
+ in
+ let _ = type_of augmented_term in
+ (* let's check also the positivity conditions *)
+ if
+ not
+ (are_all_occurrences_positive tys uri indparamsno i 0 len
+ debrujinedte)
+ then
+ raise (NotPositiveOccurrences (U.string_of_uri uri))
+ ) cl ;
+ (i + 1)
+ ) itl 1
+ in
+ ()
+
+(* Main function to checks the correctness of a mutual *)
+(* inductive block definition. *)
+and check_mutual_inductive_defs uri =
+ function
+ Cic.InductiveDefinition (itl, params, indparamsno) ->
+ typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri))
and type_of_mutual_inductive_defs uri i =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
Logger.log (`Start_type_checking uri) ;
check_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
Logger.log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked uri with
+ (match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
)
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
Logger.log (`Start_type_checking uri) ;
check_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
Logger.log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked uri with
+ (match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
)
let cl' =
List.map
(fun (id,ty) ->
- (id, ty, snd (split_prods tys paramsno ty))) cl
+ (id, snd (split_prods tys paramsno ty))) cl
in
(tys,List.length tl,isinductive,paramsno,cl')
| _ ->
pl true
else
List.fold_right
- (fun (p,(_,te,c)) i ->
+ (fun (p,(_,c)) i ->
let rl' =
- let debrujinedte = debrujin_constructor uri len te in
+ let debrujinedte = debrujin_constructor uri len c in
recursive_args tys 0 len debrujinedte
in
let (e,safes',n',nn',x',context') =
let cl' =
List.map
(fun (id,ty) ->
- (id, ty, snd (split_prods tys paramsno ty))) cl
+ (id, snd (split_prods tys paramsno ty))) cl
in
(tys,List.length tl,isinductive,paramsno,cl')
| _ ->
(*CSC: supponiamo come prima che nessun controllo sia necessario*)
(*CSC: sugli argomenti di una applicazione *)
List.fold_right
- (fun (p,(_,te,c)) i ->
+ (fun (p,(_,c)) i ->
let rl' =
- let debrujinedte = debrujin_constructor uri len te in
+ let debrujinedte = debrujin_constructor uri len c in
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
let cl' =
List.map
(fun (id,ty) ->
- (id, ty, snd (split_prods tys paramsno ty))) cl
+ (id, snd (split_prods tys paramsno ty))) cl
in
(tys,List.length tl,isinductive,paramsno,cl')
| _ ->
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
- (fun (p,(_,te,c)) i ->
+ (fun (p,(_,c)) i ->
let rl' =
- let debrujinedte = debrujin_constructor uri len te in
+ let debrujinedte = debrujin_constructor uri len c in
recursive_args tys 0 len debrujinedte
in
let (e,safes',n',nn',x',context') =
let cl' =
List.map
(fun (id,ty) ->
- (id, ty, snd (split_prods tys paramsno ty))) cl
+ (id, snd (split_prods tys paramsno ty))) cl
in
(tys,List.length tl,isinductive,paramsno,cl')
| _ ->
i && guarded_by_destructors context n nn kl x safes t)
tl true &&
List.fold_right
- (fun (p,(_,te,c)) i ->
+ (fun (p,(_,c)) i ->
let rl' =
- let debrujinedte = debrujin_constructor uri len te in
+ let debrujinedte = debrujin_constructor uri len c in
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
| C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
let consty =
- match CicEnvironment.get_cooked_obj uri with
+ match CicEnvironment.get_cooked_obj ~trust:false uri with
C.InductiveDefinition (itl,_,_) ->
let (_,_,_,cl) = List.nth itl i in
let (_,cons) = List.nth cl (j - 1) in
(* let's check if the type of branches are right *)
let parsno =
- match CicEnvironment.get_cooked_obj uri with
+ match CicEnvironment.get_cooked_obj ~trust:false uri with
C.InductiveDefinition (_,_,parsno) -> parsno
| _ ->
raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
| ((uri,t) as subst)::tl ->
let typeofvar =
CicSubstitution.subst_vars substs (type_of_variable uri) in
- (match CicEnvironment.get_cooked_obj uri with
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
(NotWellTyped
match CicReduction.whd context ty with
C.MutInd (uri,i,_) ->
(*CSC: definire una funzioncina per questo codice sempre replicato *)
- (match CicEnvironment.get_cooked_obj uri with
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
C.InductiveDefinition (itl,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
if is_inductive then None else (Some uri)
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- match CicEnvironment.is_type_checked uri with
+ match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj _ -> ()
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
(* only to check that ty is well-typed *)
let _ = type_of ty in ()
| C.CurrentProof (_,conjs,te,ty,_) ->
- (*CSC: bisogna controllare anche il metasenv!!! *)
+ let _ =
+ List.fold_left
+ (fun metasenv ((_,context,ty) as conj) ->
+ ignore (type_of_aux' metasenv context ty) ;
+ metasenv @ [conj]
+ ) [] conjs
+ in
let _ = type_of_aux' conjs [] ty in
- debug (type_of_aux' conjs [] te) [] ;
- if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
+ if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
+ then
raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
| C.Variable (_,bo,ty,_) ->
(* only to check that ty is well-typed *)
projects / helm.git / blobdiff