urimanager removed

[helm.git] / matita / components / ng_cic_content / nTermCicContent.ml

diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml
index 5cfda009c26bb564af3a45205860d931c320befb..5d91cee284a7ab0e73c9e08d1ef1b7ed3de63db9 100644 (file)
--- a/matita/components/ng_cic_content/nTermCicContent.ml
+++ b/matita/components/ng_cic_content/nTermCicContent.ml
@@ -27,13 +27,15 @@
 
 open Printf
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 type id = string
 
+let hide_coercions = ref true;;
+
 (*
 type interpretation_id = int
 
@@ -41,12 +43,6 @@ type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, UriManager.uri) Hashtbl.t;
   }
-
-let get_types uri =
-  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
-    match o with
-      | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno 
-      | _ -> assert false
 *)
 
 let idref register_ref =
@@ -87,7 +83,7 @@ let destroy_nat =
 (* CODICE c&p da NCicPp *)
 let nast_of_cic0 status
  ~(idref:
-    ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+    ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
  ~output_type ~metasenv ~subst k ~context =
   function
     | NCic.Rel n ->
@@ -143,7 +139,7 @@ let nast_of_cic0 status
          | Some n -> idref (Ast.Num (string_of_int n, -1))
          | None ->
             let args =
-             if not !Acic2content.hide_coercions then args
+             if not !hide_coercions then args
              else
               match
                NCicCoercion.match_coercion status ~metasenv ~context ~subst t
@@ -275,7 +271,7 @@ let instantiate32 idrefs env symbol args =
         in
         let rec add_lambda t n =
           if n > 0 then
-            let name = CicNotationUtil.fresh_name () in
+            let name = NotationUtil.fresh_name () in
             Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
               Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
           else
@@ -303,7 +299,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
            idref
             ~reference:
               (match term with NCic.Const nref -> nref | _ -> assert false)
-           (CicNotationPt.Ident ("dummy",None))
+           (NotationPt.Ident ("dummy",None))
           in
            match attrterm with
               Ast.AttributedTerm (`IdRef id, _) -> id
@@ -320,7 +316,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
       in
       let _, symbol, args, _ =
         try
-          TermAcicContent.find_level2_patterns32 pid
+          Interpretations.find_level2_patterns32 pid
         with Not_found -> assert false
       in
       let ast = instantiate32 idrefs env symbol args in
@@ -333,19 +329,11 @@ let load_patterns32 t =
  in
   set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
 in
- TermAcicContent.add_load_patterns32 load_patterns32;
- TermAcicContent.init ()
+ Interpretations.add_load_patterns32 load_patterns32;
+ Interpretations.init ()
 ;;
 
 (*
-let ast_of_acic ~output_type id_to_sort annterm =
-  debug_print (lazy ("ast_of_acic <- "
-    ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
-  let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
-  let ast = ast_of_acic1 ~output_type term_info annterm in
-  debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
-  ast, term_info.uri
-
 let fresh_id =
   fun () ->
     incr counter;
@@ -601,7 +589,7 @@ in
   let res =
    match kind with
     | NCic.Fixpoint (is_rec, ifl, _) -> 
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
                 K.joint_kind = 
@@ -611,7 +599,7 @@ in
                 K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
               }) 
     | NCic.Inductive (is_ind, lno, itl, _) ->
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
                 K.joint_kind = 
@@ -621,12 +609,12 @@ in
     | NCic.Constant (_,_,Some bo,ty,_) ->
        let ty = nast_of_cic ~context:[] ty in
        let bo = nast_of_cic ~context:[] bo in
-        (gen_id object_prefix seed, [], conjectures,
+        (gen_id object_prefix seed, conjectures,
           `Def (K.Const,ty,
             build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
     | NCic.Constant (_,_,None,ty,_) ->
        let ty = nast_of_cic ~context:[] ty in
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
            `Decl (K.Const,
              (*CSC: ??? get_id ty here used to be the id of the axiom! *)
              build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))