helm/gTopLevel/testlibrary.ml

   1
   2 let mqi_debug_fun = ignore
   3 let mqi_flags = []
   4 let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
   5
   6 let verbose = false
   7
   8 exception Failure of string
   9 let fail msg = raise (Failure msg)
  10
  11 module DisambiguateCallbacks =
  12  struct
  13   let output_html ?(append_NL = true) msg =
  14     if verbose then
  15       (if append_NL then print_string else print_endline)
  16         (Ui_logger.string_of_html_msg msg)
  17
  18   let interactive_user_uri_choice
  19    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id =
  20      List.filter
  21       (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
  22
  23   let interactive_interpretation_choice _ = fail "Multiple interpretations"
  24   let input_or_locate_uri ~title = fail "Unknown identifier"
  25  end
  26
  27 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
  28
  29 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
  30
  31 let main () =
  32   let uri = UriManager.uri_of_string (Sys.argv.(1)) in
  33   let obj = CicCache.get_obj uri in
  34   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
  35     Cic2acic.acic_object_of_cic_object obj
  36   in
  37   let ids_to_uris = Hashtbl.create 1023 in
  38   let round_trip annterm =
  39     debug_print "(1) acic -> ast";
  40     let (ast, _) =
  41       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
  42     in
  43     debug_print ("ast: " ^ CicAstPp.pp_term ast);
  44     let (_, _, term) =
  45       Disambiguate'.disambiguate_term mqi_handle [] [] ast
  46         DisambiguateTypes.Environment.empty
  47     in
  48     debug_print ("term: " ^ CicPp.ppterm term)
  49   in
  50   match annobj with
  51   | Cic.AConstant (_, _, _, None, ty, _) ->
  52       debug_print "Cic.AConstant (ty)";
  53       round_trip ty
  54   | Cic.AConstant (_, _, _, Some bo, ty, _) ->
  55       debug_print "Cic.AConstant (bo)";
  56       round_trip bo;
  57       debug_print "Cic.AConstant (ty)";
  58       round_trip ty
  59   | Cic.AVariable (_, _, None, ty, _) ->
  60       debug_print "Cic.AVariable (ty)";
  61       round_trip ty
  62   | Cic.AVariable (_, _, Some bo, ty, _) ->
  63       debug_print "Cic.AVariable (bo)";
  64       round_trip bo;
  65       debug_print "Cic.AVariable (ty)";
  66       round_trip ty
  67   | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
  68       debug_print "Cic.ACurrentProof (proof)";
  69       round_trip proof;
  70       debug_print "Cic.ACurrentProof (ty)";
  71       round_trip ty
  72   | Cic.AInductiveDefinition _ ->
  73       debug_print "AInductiveDefinition: boh ..."
  74
  75 let _ = main ()
  76