Benchmarking integrated in folding/unfolding.

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4ea6e5ac3e4dd3ee47655f62a2ac1ed05254dc8f..f221a2b05a57a31596ab767c2a8438f1d40a919c 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -22,6 +22,9 @@ module NRef = NReference
 let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
 
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
   | _ -> assert false
@@ -325,12 +328,17 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
+         NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
+    | CicNotationPt.NCic t -> 
+           let context = (* to make metas_of_term happy *)
+             List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
+           assert(NCicUntrusted.metas_of_term [] context t = []); t
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+    | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -434,7 +442,7 @@ let interpretate_obj
    interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
  let uri = match uri with | None -> assert false | Some u -> u in
  match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
      let ty' = 
        interpretate_term 
          ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
@@ -443,11 +451,11 @@ let interpretate_obj
      uri, height, [], [], 
      (match bo,flavour with
       | None,`Axiom -> 
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,None,ty',attrs)
       | Some _,`Axiom -> assert false
       | None,_ ->
-          let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
         (match bo with
@@ -484,14 +492,14 @@ let interpretate_obj
                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
                  defs
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
              NCic.Fixpoint (inductive,inductiveFuns,attrs)
          | bo -> 
              let bo = 
                interpretate_term 
                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
              NCic.Constant ([],name,Some bo,ty',attrs)))
  | CicNotationPt.Inductive (params,tyl) ->
     let context,params =