- (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
- let ugraph1 =
- (match uobj with
- 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
- if not b then
- raise (TypeCheckerFailure
- ("Unknown constant:" ^ U.string_of_uri uri))
- else
- ugraph3
- | 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,_,_) ->
- let _,ugraph1 =
- List.fold_left
- (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
- let _,ugraph1 =
- type_of_aux' ~logger metasenv context ty ugraph
- in
- metasenv @ [conj],ugraph1
- ) ([],ugraph) conjs
- in
- let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
- let type_of_te,ugraph3 =
- type_of_aux' ~logger conjs [] te ugraph2
- in
- let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in
- if not b then
- raise (TypeCheckerFailure (sprintf
- "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
- (U.string_of_uri uri) (CicPp.ppterm type_of_te)
- (CicPp.ppterm ty)))
- else
- ugraph4
- | C.Variable (_,bo,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph1 = type_of ~logger ty ugraph in
- (match bo with
- None -> ugraph1
- | Some bo ->
- let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in
- let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in
- if not b then
- raise (TypeCheckerFailure
- ("Unknown variable:" ^ U.string_of_uri uri))
- else
- ugraph3
- )
- | C.InductiveDefinition _ ->
- check_mutual_inductive_defs ~logger uri uobj ugraph
- ) in