-let refine metasenv context term =
- let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
- debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
- try
- let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
- Ok (term', metasenv')
- with
- | CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
- (* TODO remove this case as soon as refine is fully implemented *)
- (try
- debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term));
- let term' = CicTypeChecker.type_of_aux' metasenv context term in
- Ok (term',metasenv)
-(* with _ -> Ko) *)
- with _ -> Uncertain)
- | CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
- Uncertain
- | _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
- Ko
-
-let indtyuri_of_uri uri =
- let index_sharp = String.index uri '#' in
- let index_num = index_sharp + 3 in
- (UriManager.uri_of_string (String.sub uri 0 index_sharp),
- int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
-
-let indconuri_of_uri uri =
- let index_sharp = String.index uri '#' in
- let index_div = String.rindex uri '/' in
- let index_con = index_div + 1 in
- (UriManager.uri_of_string (String.sub uri 0 index_sharp),
- int_of_string
- (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
- int_of_string
- (String.sub uri index_con (String.length uri - index_con)))
-
- (* TODO move it to Cic *)
-let term_of_uri uri =
- try
- (* Constant *)
- (* TODO explicit substitutions? *)
- let len = String.length uri in
- if String.sub uri (len - 4) 4 = ".con" then
- Cic.Const (uri_of_string uri, [])
- else if String.sub uri (len - 4) 4 = ".var" then
- Cic.Var (uri_of_string uri, [])
- else
- (try
- (* Inductive Type *)
- let uri',typeno = indtyuri_of_uri uri in
- Cic.MutInd (uri', typeno, [])
- with
- | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
- (* Constructor of an Inductive Type *)
- let uri',typeno,consno = indconuri_of_uri uri in
- Cic.MutConstruct (uri', typeno, consno, []))
- with
- | Invalid_argument _ -> raise (UriManager.IllFormedUri uri)
+let refine metasenv context term ugraph =
+(* if benchmark then incr actual_refinements; *)
+ let metasenv, term =
+ CicMkImplicit.expand_implicits metasenv [] context term in
+ debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
+ try
+ let term', _, metasenv',ugraph1 =
+ CicRefine.type_of_aux' metasenv context term ugraph in
+ (Ok (term', metasenv')),ugraph1
+ with
+ | CicRefine.Uncertain _ ->
+ debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ Uncertain,ugraph
+ | CicRefine.RefineFailure msg ->
+ debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) msg);
+ Ko,ugraph
+ | CicUnification.UnificationFailure s ->
+ prerr_endline ("PASSADI QUI: " ^ s);
+ raise ( CicUnification.UnificationFailure s )