From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 May 2011 08:49:10 +0000 (+0000)
Subject: Simplified rendering
X-Git-Tag: make_still_working~2505
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53d4524b2dbe23f5b48f00099d8ff39efb00941d;p=helm.git

Simplified rendering
---

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 5f41a1fe5..598c93af7 100644
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -85,15 +85,6 @@ class virtual status =
     interp_db <- Some (initial_db self)
  end
 
-let idref register_ref =
- let id = ref 0 in
-  fun ?reference t ->
-   incr id;
-   let id = "i" ^ string_of_int !id in
-    (match reference with None -> () | Some r -> register_ref id r);
-    Ast.AttributedTerm (`IdRef id, t)
-;;
-
 let level_of_uri u = 
   let name = NUri.name_of_uri u in
   assert(String.length name > String.length "Type");
@@ -103,10 +94,7 @@ let level_of_uri u =
 let find_level2_patterns32 status pid =
  IntMap.find pid status#interp_db.level2_patterns32
 
-let add_idrefs =
-  List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
-
-let instantiate32 idrefs env symbol args =
+let instantiate32 env symbol args =
   let rec instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = 
@@ -129,16 +117,13 @@ let instantiate32 idrefs env symbol args =
         in
         add_lambda t (n - count_lambda t)
   in
-  let head =
-    let symbol = Ast.Symbol (symbol, None) in
-    add_idrefs idrefs symbol
-  in
+  let head = Ast.Symbol (symbol, None) in
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
 let fresh_id status =
-  let counter = status#interp_db.counter+1 in
-   status#set_interp_db ({ status#interp_db with counter = counter  }), counter
+  let counter = status#interp_db.counter + 1 in
+    status#set_interp_db {status#interp_db with counter = counter},counter
 
 let load_patterns32 status t =
  let t =
@@ -226,53 +211,51 @@ let destroy_nat =
   in
    aux 0
 
-(* CODICE c&p da NCicPp *)
 let nast_of_cic0 status
- ~(idref:
-    ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
  ~output_type ~metasenv ~subst k ~context =
   function
     | NCic.Rel n ->
        (try 
          let name,_ = List.nth context (n-1) in
          let name = if name = "_" then "__"^string_of_int n else name in
-          idref (Ast.Ident (name,`Ambiguous))
+          Ast.Ident (name,`Ambiguous)
         with Failure "nth" | Invalid_argument "List.nth" -> 
-         idref (Ast.Ident ("-" ^ string_of_int (n - List.length
-         context),`Ambiguous)))
-    | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous))
+         Ast.Ident ("-" ^ string_of_int (n - List.length context),`Ambiguous))
+    | NCic.Const r -> 
+	let uri = `Uri (NReference.string_of_reference r) in
+	Ast.Ident (NCicPp.r2s status true r, uri)
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ~context (NCicSubstitution.subst_meta status lc t)
     | NCic.Meta (n,(s,l)) ->
        (* CSC: qua non dovremmo espandere *)
        let l = NCicUtils.expand_local_context l in
-        idref (Ast.Meta
-         (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l))
-    | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
-    | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set)
+       Ast.Meta
+         (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l)
+    | NCic.Sort NCic.Prop -> Ast.Sort `Prop
+    | NCic.Sort NCic.Type [] -> Ast.Sort `Set
     | NCic.Sort NCic.Type ((`Type,u)::_) -> 
-              idref(Ast.Sort (`NType (level_of_uri u)))
+              Ast.Sort (`NType (level_of_uri u))
     | NCic.Sort NCic.Type ((`CProp,u)::_) -> 
-              idref(Ast.Sort (`NCProp (level_of_uri u)))
+              Ast.Sort (`NCProp (level_of_uri u))
     | NCic.Sort NCic.Type ((`Succ,u)::_) -> 
-              idref(Ast.Sort (`NType (level_of_uri u ^ "+1")))
-    | NCic.Implicit `Hole -> idref (Ast.UserInput)
-    | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
-    | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
+              Ast.Sort (`NType (level_of_uri u ^ "+1"))
+    | NCic.Implicit `Hole -> Ast.UserInput
+    | NCic.Implicit `Vector -> Ast.Implicit `Vector
+    | NCic.Implicit _ -> Ast.Implicit `JustOne
     | NCic.Prod (n,s,t) ->
         let n = if n.[0] = '_' then "_" else n in
         let binder_kind = `Forall in
-         idref (Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
-          k ~context:((n,NCic.Decl s)::context) t))
+          Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
+          k ~context:((n,NCic.Decl s)::context) t)
     | NCic.Lambda (n,s,t) ->
-        idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
-         k ~context:((n,NCic.Decl s)::context) t))
+        Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
+		    k ~context:((n,NCic.Decl s)::context) t)
     | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
-        idref (Ast.Cast (k ~context ty, k ~context s))
+        Ast.Cast (k ~context ty, k ~context s)
     | NCic.LetIn (n,s,ty,t) ->
-        idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
-          ty, k ~context:((n,NCic.Decl s)::context) t))
+        Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
+          ty, k ~context:((n,NCic.Decl s)::context) t)
     | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> 
        let _,_,t,_ = List.assoc n subst in
        let hd = NCicSubstitution.subst_meta status lc t in
@@ -283,7 +266,7 @@ let nast_of_cic0 status
            | _ -> NCic.Appl (hd :: args)))
     | NCic.Appl args as t ->
        (match destroy_nat t with
-         | Some n -> idref (Ast.Num (string_of_int n, None))
+         | Some n -> Ast.Num (string_of_int n, None)
          | None ->
             let args =
              if not !hide_coercions then args
@@ -303,20 +286,12 @@ let nast_of_cic0 status
                    args
             in
              (match args with
-                 [arg] -> idref (k ~context arg)
-               | _ -> idref (Ast.Appl (List.map (k ~context) args))))
+                 [arg] -> k ~context arg
+               | _ -> Ast.Appl (List.map (k ~context) args)))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
         let name = NUri.name_of_uri uri in
-(* CSC
-        let uri_str = UriManager.string_of_uri uri in
-        let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
-        let ctor_puri j =
-          UriManager.uri_of_string
-            (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
-        in
-*)
         let case_indty =
-         name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in
+         name, Some r in
         let constructors, leftno =
          let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
          let _,_,_,cl  = List.nth tys n in
@@ -351,34 +326,20 @@ let nast_of_cic0 status
             `Pattern -> None
           | `Term -> Some case_indty
         in
-         idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+         Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)
 ;;
 
-let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
+let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term =
   match Lazy.force status#interp_db.compiled32 term with
   | None ->
-     nast_of_cic0 status ~idref ~output_type ~metasenv ~subst
-      (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term 
+     nast_of_cic0 status ~output_type ~metasenv ~subst
+      (nast_of_cic1 status ~output_type ~metasenv ~subst) ~context term 
   | Some (env, ctors, pid) -> 
-      let idrefs =
-       List.map
-        (fun term ->
-          let attrterm =
-           idref
-            ~reference:
-              (match term with NCic.Const nref -> nref | _ -> assert false)
-           (NotationPt.Ident ("dummy",`Ambiguous))
-          in
-           match attrterm with
-              Ast.AttributedTerm (`IdRef id, _) -> id
-            | _ -> assert false
-        ) ctors
-      in
       let env =
        List.map
         (fun (name, term) ->
           name,
-           nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context
+           nast_of_cic1 status ~output_type ~subst ~metasenv ~context
             term
         ) env
       in
@@ -387,50 +348,32 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
          find_level2_patterns32 status pid
         with Not_found -> assert false
       in
-      let ast = instantiate32 idrefs env symbol args in
-      idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*)
+      instantiate32 env symbol args 
 ;;
 
-let nmap_context0 status ~idref ~metasenv ~subst context =
- let module K = Content in
+let nmap_context0 status ~metasenv ~subst context =
  let nast_of_cic =
-  nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst
+  nast_of_cic1 status ~output_type:`Term ~metasenv ~subst
  in
  fst (
   List.fold_right
    (fun item (res,context) ->
      match item with
       | name,NCic.Decl t ->
-         Some
-          (* We should call build_decl_item, but we have not computed *)
-          (* the inner-types ==> we always produce a declaration      *)
-          (`Declaration
-            { K.dec_name = (Some name);
-              K.dec_id = "-1"; 
-              K.dec_inductive = false;
-              K.dec_aref = "-1";
-              K.dec_type = nast_of_cic ~context t
-            })::res,item::context
+          (name, Ast.Decl (nast_of_cic ~context t))::res,
+          item::context
       | name,NCic.Def (t,ty) ->
-         Some
-          (* We should call build_def_item, but we have not computed *)
-          (* the inner-types ==> we always produce a declaration     *)
-          (`Definition
-             { K.def_name = (Some name);
-               K.def_id = "-1"; 
-               K.def_aref = "-1";
-               K.def_term = nast_of_cic ~context t;
-               K.def_type = nast_of_cic ~context ty
-             })::res,item::context
+          (name, Ast.Def (nast_of_cic ~context t, 
+			   nast_of_cic ~context ty))::res,
+           item::context
    ) context ([],[]))
 ;;
 
-let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
- let module K = Content in
+let nmap_sequent0 status ~metasenv ~subst (i,(n,context,ty)) =
  let nast_of_cic =
-  nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
- let context' = nmap_context0 status ~idref ~metasenv ~subst context in
-  ("-1",i,context',nast_of_cic ~context ty)
+  nast_of_cic1 status ~output_type:`Term ~metasenv ~subst in
+ let context' = nmap_context0 status ~metasenv ~subst context in
+  (i,context',nast_of_cic ~context ty)
 ;;
 
 let object_prefix = "obj:";;
@@ -439,6 +382,7 @@ let definition_prefix = "def:";;
 let inductive_prefix = "ind:";;
 let joint_prefix = "joint:";;
 
+(*
 let get_id =
  function
     Ast.AttributedTerm (`IdRef id, _) -> id
@@ -451,58 +395,6 @@ let gen_id prefix seed =
   res
 ;;
 
-let build_def_item seed context metasenv id n t ty =
- let module K = Content in
-(*
-  try
-   let sort = Hashtbl.find ids_to_inner_sorts id in
-   if sort = `Prop then
-       (let p = 
-        (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
-       in 
-        `Proof p;)
-   else 
-*)
-      `Definition
-        { K.def_name = Some n;
-          K.def_id = gen_id definition_prefix seed; 
-          K.def_aref = id;
-          K.def_term = t;
-          K.def_type = ty
-        }
-(*
-  with
-   Not_found -> assert false
-*)
-
-let build_decl_item seed id n s =
- let module K = Content in
-(*
- let sort =
-   try
-    Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
-   with Not_found -> None
- in
- match sort with
- | Some `Prop ->
-    `Hypothesis
-      { K.dec_name = name_of n;
-        K.dec_id = gen_id declaration_prefix seed; 
-        K.dec_inductive = false;
-        K.dec_aref = id;
-        K.dec_type = s
-      }
- | _ ->
-*)
-    `Declaration
-      { K.dec_name = Some n;
-        K.dec_id = gen_id declaration_prefix seed; 
-        K.dec_inductive = false;
-        K.dec_aref = id;
-        K.dec_type = s
-      }
-;;
-
 let nmap_obj0 status ~idref (uri,_,metasenv,subst,kind) =
   let module K = Content in
   let nast_of_cic =
@@ -589,12 +481,12 @@ let with_idrefs foo status obj =
 ;;
 
 let nmap_obj status = with_idrefs nmap_obj0 status
+*)
+
+let nmap_obj = assert false
 
-let nmap_sequent status ~metasenv ~subst =
- with_idrefs (nmap_sequent0 ~metasenv ~subst) status
+let nmap_sequent = nmap_sequent0 
 
-let nmap_term status ~metasenv ~subst ~context =
- with_idrefs (nast_of_cic1 ~output_type:`Term ~metasenv ~subst ~context) status
+let nmap_term = nast_of_cic1 ~output_type:`Term 
 
-let nmap_context status ~metasenv ~subst =
- with_idrefs (nmap_context0 ~metasenv ~subst) status
+let nmap_context = nmap_context0
diff --git a/matitaB/components/ng_cic_content/interpretations.mli b/matitaB/components/ng_cic_content/interpretations.mli
index 71732cc7d..b2c59b9c9 100644
--- a/matitaB/components/ng_cic_content/interpretations.mli
+++ b/matitaB/components/ng_cic_content/interpretations.mli
@@ -79,21 +79,17 @@ val nmap_term:
  #status ->
   metasenv:NCic.metasenv -> subst:NCic.substitution -> context:NCic.context ->
   NCic.term ->
-   NotationPt.term *
-   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+   NotationPt.term 
 
 val nmap_context:
  #status ->
   metasenv:NCic.metasenv -> subst:NCic.substitution ->
-  NCic.context ->
-   NotationPt.term Content.context *
-   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+  NCic.context -> NotationPt.context 
 
 val nmap_sequent:
  #status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   int * NCic.conjecture ->
-   NotationPt.term Content.conjecture *
-    (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+   NotationPt.sequent 
 
 val nmap_obj:
  #status -> NCic.obj ->