helm/interface/theoryTypeChecker.ml

   1 exception NotWellTyped of string;;
   2
   3 let typecheck uri =
   4   let rec typecheck_term curi t =
   5   let module T = Theory in
   6   let module P = CicTypeChecker in
   7   let module C = CicCache in
   8   let module U = UriManager in
   9   let obj_typecheck uri =
  10    try
  11     P.typecheck (U.uri_of_string uri)
  12    with
  13     P.NotWellTyped s ->
  14      raise (NotWellTyped
  15       ("Type Checking was NOT successfull due to an error during " ^
  16        "type-checking of term " ^ uri ^ ":\n\n" ^ s))
  17   in
  18     match t with
  19        T.Theorem uri -> obj_typecheck (curi ^ "/" ^ uri)
  20      | T.Definition uri -> obj_typecheck (curi ^ "/" ^ uri)
  21      | T.Axiom uri -> obj_typecheck (curi ^ "/" ^ uri)
  22      | T.Variable uri -> obj_typecheck (curi ^ "/" ^ uri)
  23      | T.Section (uri,l) -> typecheck_theory l (curi ^ "/" ^ uri)
  24  and typecheck_theory l curi =
  25   List.iter (typecheck_term curi) l
  26  in
  27   let (uri, l) = TheoryCache.get_theory uri in
  28    typecheck_theory l uri
  29 ;;