X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=62d708a7fdfcce6797bff7e0fa07926a3e128a1e;hb=7a490593a8c798ac35007ddcc61da3b9153ac619;hp=c8376078285100419e9ba228cadce6fc60170de7;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml
index c83760782..62d708a7f 100644
--- a/matitaB/components/disambiguation/disambiguate.ml
+++ b/matitaB/components/disambiguation/disambiguate.ml
@@ -124,11 +124,6 @@ let domain_size = ref 0
 let choices_avg = ref 0.
 *)
 
-let descr_of_domain_item = function
- | Id s -> s
- | Symbol (s, _) -> s
- | Num i -> string_of_int i
-
 type ('term,'metasenv,'subst,'graph) test_result =
   | Ok of 'term * 'metasenv * 'subst * 'graph
   | Ko of (Stdpp.location * string) Lazy.t
@@ -156,7 +151,7 @@ let find_in_context name context =
 
 let string_of_name =
  function
-  | Ast.Ident (n, None) -> Some n
+  | Ast.Ident (n, _) -> Some n
   | _ -> assert false
 ;;
 
@@ -165,11 +160,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
      domain_of_term ~loc ~context term
   | Ast.AttributedTerm (_, term) ->
       domain_of_term ~loc ~context term
-  | Ast.Symbol (symbol, instance) ->
-      [ Node ([loc], Symbol (symbol, instance), []) ]
+  | Ast.Symbol (name, attr) ->
+      [ Node ([loc], Symbol (name,attr), []) ]
       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
-  | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
-  | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+  | Ast.Appl (Ast.Symbol (name, attr)  as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args)
      ->
       let args_dom =
         List.fold_right
@@ -180,9 +175,13 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
           Ast.AttributedTerm (`Loc loc,_)  -> loc
         | _ -> loc
       in
-       [ Node ([loc], Symbol (symbol, instance), args_dom) ]
-  | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
-  | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+       [ Node ([loc], Symbol (name,attr), args_dom) ]
+  | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
+      let uri = match uri with
+        | `Uri u -> Some u
+        | _ -> None
+      in
       let args_dom =
         List.fold_right
           (fun term acc -> domain_of_term ~loc ~context term @ acc)
@@ -194,22 +193,10 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
       in
       (try
         (* the next line can raise Not_found *)
-        ignore(find_in_context name context);
-        if subst <> None then
-          Ast.fail loc "Explicit substitutions not allowed here"
-        else
+        ignore(find_in_context id context);
           args_dom
       with Not_found ->
-        (match subst with
-        | None -> [ Node ([loc], Id name, args_dom) ]
-        | Some subst ->
-            let terms =
-              List.fold_left
-                (fun dom (_, term) ->
-                  let dom' = domain_of_term ~loc ~context term in
-                  dom @ dom')
-                [] subst in
-            [ Node ([loc], Id name, terms @ args_dom) ]))
+        [ Node ([loc], Id (id,uri), args_dom) ] )
   | Ast.Appl terms ->
       List.fold_right
         (fun term acc -> domain_of_term ~loc ~context term @ acc)
@@ -220,14 +207,17 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
         domain_of_term ~loc
           ~context:(string_of_name var :: context) body in
       (match kind with
-      | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+      | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ]
       | _ -> type_dom @ body_dom)
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in
       let rec get_first_constructor = function
         | [] -> []
-        | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+        | (Ast.Pattern (head, Some r, _), _) :: _ -> 
+             [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
+        | (Ast.Pattern (head, None, _), _) :: _ -> 
+             [ Node ([loc], Id (head,None), []) ]
         | _ :: tl -> get_first_constructor tl in
       let do_branch =
        function
@@ -249,7 +239,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
       (match indty_ident with
        | None -> get_first_constructor branches
-       | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+       | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ]
+       | Some (ident, Some r) -> 
+           [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
       @ term_dom @ outtype_dom @ branches_dom
   | Ast.Cast (term, ty) ->
       let term_dom = domain_of_term ~loc ~context term in
@@ -289,15 +281,16 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
           ) [] defs
       in
       defs_dom @ where_dom
-  | Ast.Ident (name, subst) ->
+  | Ast.Ident (name, x) ->
+      let x = match x with
+        | `Uri u -> Some u
+        | _ -> None
+      in
       (try
         (* the next line can raise Not_found *)
-        ignore(find_in_context name context);
-        if subst <> None then
-          Ast.fail loc "Explicit substitutions not allowed here"
-        else
-          []
+        ignore(find_in_context name context); []
       with Not_found ->
+        (*
         (match subst with
         | None -> [ Node ([loc], Id name, []) ]
         | Some subst ->
@@ -307,8 +300,8 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   let dom' = domain_of_term ~loc ~context term in
                   dom @ dom')
                 [] subst in
-            [ Node ([loc], Id name, terms) ]))
-  | Ast.Uri _ -> []
+            [ Node ([loc], Id name, terms) ]))*)
+        [ Node ([loc], Id (name,x), []) ])
   | Ast.NRef _ -> []
   | Ast.NCic _ -> []
   | Ast.Implicit _ -> []
@@ -386,11 +379,11 @@ let domain_diff dom1 dom2 =
   let is_in_dom2 elt =
     List.exists
      (function
-       | Symbol (symb, 0) ->
+       | Symbol (symb,None) ->
           (match elt with
               Symbol (symb',_) when symb = symb' -> true
             | _ -> false)
-       | Num i ->
+       | Num _ ->
           (match elt with
               Num _ -> true
             | _ -> false)
@@ -407,6 +400,368 @@ let domain_diff dom1 dom2 =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
+(* generic function lifting splitting from type T to type (T list) *) 
+let rec list_split item_split ctx pre post =
+  match post with
+  | [] -> []
+  | x :: post' ->
+      (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+        list_split item_split ctx (pre@[x]) post'
+;;
+
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+  | (_,None) -> []
+  | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
+
+let ity_split ctx (n,isind,ty,cl) = 
+  [(fun x -> ctx (n,isind,x,cl)),ty]@
+  list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty]) 
+    (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+        [(fun x -> ctx (n,x,b,m)),ty]
+;;
+
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+        list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+        var_split (fun x -> ctx (args,x,bo,n)) f@
+        [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+  | Ast.Wildcard -> []
+  | Ast.Pattern (s,href,pl) -> 
+     let rec auxpatt pre = function
+     | [] -> []
+     | (x,Some y as x')::post' ->
+         ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+         ::auxpatt (pre@[x']) post'
+     | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+     in auxpatt [] pl
+;;
+
+  (* this function is used to get the children of a given node, together with
+   * their context 
+   * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
+let rec split ctx = function
+  | Ast.AttributedTerm (attr,t) -> 
+     [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
+  | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
+  | Ast.Binder (k,((n,None) as n'),body) -> 
+     [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
+  | Ast.Binder (k,((n,Some ty) as n'),body) -> 
+     [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty 
+     ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
+  | Ast.Case (t,ity,outty,pl) -> 
+     let outty_split = match outty with
+     | None -> []
+     | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+     in
+     ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+       outty_split@list_split
+         (fun ctx0 (p,x) -> 
+            ((fun y -> ctx0 (p,y)),x)::pattern_split 
+              (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+              [] pl
+  | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
+                  ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+  | Ast.LetIn ((n,None) as n',u,v) ->
+                  [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
+                  ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+  | Ast.LetIn ((n,Some t) as n',u,v) ->
+                  [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
+                  ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
+                  ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+  | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+      list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+  | _ -> [] (* leaves *)
+;;
+
+
+(* top_split : 'a -> ((term -> 'a) * term) list
+ * returns all the possible top-level (ctx,t) for its input *)
+let bfvisit ~pp_term top_split test t = 
+  let rec aux = function
+  | [] -> None
+  | (ctx0,t0 as hd)::tl ->
+(*      prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+      prerr_endline ("t0 = " ^ pp_term t0); 
+      if test t0 then (prerr_endline "caso 1"; Some hd)
+      else 
+              let t0' = split ctx0 t0 in
+              (prerr_endline ("caso 2: length t0' = " ^ string_of_int
+              (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+  (* in aux [(fun x -> x),t] *)
+  in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+  | Ast.Inductive (ls,itl) -> 
+      list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+      list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl 
+  | Ast.Theorem (flav,n,ty,None,p) ->
+      [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
+  | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+      [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
+      ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+  | Ast.Record (ls,n,ty,fl) ->
+      list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+      [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+      list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl 
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
+
+(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
+  let mk_alias = function
+    | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+    | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+    | Ast.Num _ -> DisambiguateTypes.Num None
+    | _ -> assert false
+  in
+  let lookup_choices =
+     fun item ->
+      (*match universe with
+      | None -> 
+          lookup_in_library 
+            interactive_user_uri_choice 
+            input_or_locate_uri item
+      | Some e ->
+          (try Environment.find item e
+          with Not_found -> [])
+*)
+          (try Environment.find item universe
+          with Not_found -> [])
+   in
+   match t with
+   | Ast.Ident (_,None)
+   | Ast.Num (_,None) 
+   | Ast.Symbol (_,None) -> 
+       let choices = lookup_choices (mk_alias t) in
+       if List.length choices <> 1 then t
+       else List.hd choices
+     (* but we lose info on closedness *)
+   | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
+;;
+*)
+
+let domain_item_of_ast = function
+  | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+  | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+  | Ast.Num (n,_) -> DisambiguateTypes.Num None
+  | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+  | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+  | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+  | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) -> 
+      Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+  | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+  | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+  | _ -> assert false
+;;
+
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri 
+  ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+  try
+   let localization_tbl = mk_localization_tbl 503 in
+    let cic_thing =
+      interpretate_thing ~context ~env
+       ~uri ~is_path:false t ~localization_tbl
+    in
+    let foo () =
+           refine_thing metasenv subst context uri
+            ~use_coercions cic_thing expty ugraph ~localization_tbl
+    in match (refine_profiler.HExtlib.profile foo ()) with
+    | Ko _ -> false
+    | _ -> true
+  with
+     (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+     | Invalid_choice loc_msg -> Ko loc_msg*)
+     | Invalid_choice _ -> false
+     | _ -> true
+;;
+
+let rec disambiguate_list
+  ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+  ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
+  let disambiguate_list = 
+    disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+      ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+      ~mk_localization_tbl ~pp_thing ~pp_term
+  in
+  let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
+    ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+  in
+  let find_choices item = 
+    let a2s = function
+    | GrafiteAst.Ident_alias (id,_)
+    | GrafiteAst.Symbol_alias (id,_,_) -> id
+    | GrafiteAst.Number_alias _ -> "NUM"
+    in
+    let d2s = function
+    | Id (id,_)
+    | Symbol (id,_) -> id
+    | Num _ -> "NUM"
+    in
+    let res =
+      Environment.find item universe 
+    in
+    prerr_endline (Printf.sprintf "choices for %s :\n%s"
+      (d2s item) (String.concat ", " (List.map a2s res)));
+    res
+  in
+
+  let get_instances ctx t = 
+    try 
+      let choices = find_choices (domain_item_of_ast t) in
+      List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
+    with
+    | Not_found -> []
+  in
+
+  match ts with
+  | [] -> None
+  | t0 :: tl ->
+      prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); 
+      let is_ambiguous = function
+      | Ast.Ident (_,`Ambiguous)
+      | Ast.Num (_,None)
+      | Ast.Symbol (_,None) -> true
+      | Ast.Case (_,Some (ity,None),_,_) -> 
+          (prerr_endline ("ambiguous case" ^ ity);true)
+      | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
+      | Ast.Case (_,Some (ity,Some r),_,_) -> 
+          (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
+      | Ast.Ident (n,`Uri u) -> 
+          (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+      | _ -> false
+      in
+      let astpp = function
+              | Ast.Ident (id,_) -> "ID " ^ id
+              | Ast.Num _ -> "NUM"
+              | Ast.Symbol (sym,_) -> "SYM " ^ sym
+              | _ -> "ERROR!"
+      in
+      (* get first ambiguous subterm (or return disambiguated term) *)
+      match visit ~pp_term is_ambiguous t0 with
+      | None -> 
+          prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
+          Some (t0,tl)
+      | Some (ctx, t) -> 
+        prerr_endline ("disambiguating node " ^ astpp t ^
+        "\nin " ^ pp_thing (ctx t));
+        (* get possible instantiations of t *)
+        let instances = get_instances ctx t in
+        (* perforate ambiguous subterms and test refinement *)
+        let survivors = List.filter test_interpr instances in
+        disambiguate_list (survivors@tl) 
+;;
+
+
+(*  let rec aux l =
+    match l with
+    | [] -> None
+    | (ctx,u)::vl -> 
+        if test u 
+          then (ctx,u)
+          else aux (vl@split ctx u)
+  in aux [t]
+;;*) 
+
+(* let rec instantiate_ast = function
+  | Ident (n,Some _)
+  | Symbol (s,Some _)
+  | Num (n,Some _) as t -> []
+  | Ident (n,None) -> (* output: all possible instantiations of n *)
+  | Symbol (s,None) ->
+  | Num (n,None) -> 
+
+
+  | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+  | Appl tl -> Appl (List.map f tl)
+  | Binder (k,n,body) -> Binder (k,n,f body)
+  | Case (t,ity,oty,pl) -> 
+      let pl' = List.map (fun (p,u) -> p,f u) pl in 
+      Case (f t,ity,map_option f oty,pl')
+  | Cast (u,v) -> Cast (f u,f v)
+  | LetIn (n,u,v) -> LetIn (n,f u,f v)
+  | LetRec -> ada (* TODO *)
+  | t -> t
+*)
+
+let disambiguate_thing 
+  ~context ~metasenv ~subst ~use_coercions
+  ~string_context_of_context
+  ~initial_ugraph:base_univ ~expty
+  ~mk_implicit ~description_of_alias ~fix_instance
+  ~aliases ~universe ~lookup_in_library 
+  ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing 
+  ~visit ~mk_localization_tbl
+  (thing_txt,thing_txt_prefix_len,thing)
+=
+(* XXX: will be thrown away *)
+  let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing 
+  in
+  let rec aux_env env = function
+   | [] -> env
+   | Node (_, item, l) :: tl ->
+       let env =
+         Environment.add item
+          (mk_implicit
+            (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+          env in
+       aux_env (aux_env env l) tl in
+  let env = aux_env aliases todo_dom in
+
+  let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
+    ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+  in
+(* real function *)
+  let rec aux tl =
+    match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+      ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+      ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+      ~pp_term tl with
+    | None -> []
+    | Some (t,tl') -> t::aux tl'
+  in
+
+  let refine t = 
+    let localization_tbl = mk_localization_tbl 503 in
+    match refine_thing metasenv subst context uri
+      ~use_coercions
+      (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
+      expty base_univ ~localization_tbl with
+    | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+    | Uncertain x ->
+        let _,err = Lazy.force x in
+        prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+        assert false
+    | _ -> assert false
+  in
+  if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
+  else
+    let res = aux [thing] in
+    let res =
+      HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
+    in
+    match res with
+    | [] -> raise (NoWellTypedInterpretation (0,[]))
+    | [t] -> res,false
+    | _ -> res,true
+;;
+
+(*
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
@@ -702,3 +1057,4 @@ in refine_profiler.HExtlib.profile foo ()
           true
     in
      res
+     *)