added code to print the tree

[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 4bfeab669066ad762d7a260515c8a5426ab16a69..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
@@ -64,7 +67,7 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~rdb metasenv subst context _uri 
+  ~rdb metasenv subst _context _uri 
   ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
@@ -72,7 +75,6 @@ let refine_obj
   let localise t = 
     try NCicUntrusted.NCicHash.find localization_tbl t
     with Not_found -> 
-      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
       (*assert false*)HExtlib.dummy_floc
   in
   try
@@ -322,16 +324,21 @@ let interpretate_term_and_interpretate_term_option
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
-           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
     | 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)
@@ -344,15 +351,15 @@ let interpretate_term_and_interpretate_term_option
          NCic.Meta (index, (0, NCic.Ctx cic_subst))
     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+       [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+       [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
+       [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
+       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -435,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 
@@ -444,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
@@ -485,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 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 =