From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Apr 2009 13:19:11 +0000 (+0000)
Subject: The sequent viewer now considers the context to render the Rels.
X-Git-Tag: make_still_working~4090
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6abf435197c2bc37fadc0b3bd5925cd9cbe112e2;p=helm.git

The sequent viewer now considers the context to render the Rels.
---

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index b98f95634..b1bc38758 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -107,8 +107,7 @@ let sequent2pres ~ids_to_inner_sorts =
 
 let nsequent2pres ~subst =
   sequent2pres0
-    (fun term ->
-      let ast = NTermCicContent.nast_of_cic ~subst term in
-       CicNotationPres.box_of_mpres
-        (CicNotationPres.render (Hashtbl.create 1)
-          (TermContentPres.pp_ast ast)))
+    (fun ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render (Hashtbl.create 1)
+         (TermContentPres.pp_ast ast)))
diff --git a/helm/software/components/content_pres/sequent2pres.mli b/helm/software/components/content_pres/sequent2pres.mli
index 03b528783..6866cd3ae 100644
--- a/helm/software/components/content_pres/sequent2pres.mli
+++ b/helm/software/components/content_pres/sequent2pres.mli
@@ -38,5 +38,5 @@ val sequent2pres :
     CicNotationPres.boxml_markup
 
 val nsequent2pres :
- subst:NCic.substitution -> NCic.term Content.conjecture ->
+ subst:NCic.substitution -> CicNotationPt.term Content.conjecture ->
   CicNotationPres.boxml_markup
diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 3253e7908..b3c827f92 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -73,66 +73,57 @@ let left_params_no_of_inductive_type uri =
 *)
 
 (* CODICE c&p da NCicPp *)
-let r2s pp_fix_name r = 
-  try
-    match r with
-    | NReference.Ref (u,NReference.Ind (_,i,_)) -> 
-        (match NCicLibrary.get_obj u with
-        | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
-            let _,name,_,_ = List.nth itl i in name
-        | _ -> assert false)
-    | NReference.Ref (u,NReference.Con (i,j,_)) -> 
-        (match NCicLibrary.get_obj u with
-        | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
-            let _,_,_,cl = List.nth itl i in
-            let _,name,_ = List.nth cl (j-1) in name
-        | _ -> assert false)
-    | NReference.Ref (u,(NReference.Decl | NReference.Def _)) -> 
-        (match NCicLibrary.get_obj u with
-        | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name
-        | _ -> assert false)
-    | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) ->
-        (match NCicLibrary.get_obj u with
-        | _,_,_,_, NCic.Fixpoint (_,fl,_) -> 
-            if pp_fix_name then
-              let _,name,_,_,_ = List.nth fl i in name
-            else 
-              NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
-        | _ -> assert false)
-  with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r
-;;
-
-let nast_of_cic ~subst =
-  let rec k = function
-    | NCic.Rel n -> Ast.Ident ("-" ^ string_of_int n, None)
-    | NCic.Const r -> Ast.Ident (r2s true r, None)
+let nast_of_cic ~subst ~context =
+  let rec k ctx = function
+    | NCic.Rel n ->
+       (try 
+         let name,_ = List.nth ctx (n-1) in
+         let name = if name = "_" then "__"^string_of_int n else name in
+          Ast.Ident (name,None)
+        with Failure "nth" | Invalid_argument "List.nth" -> 
+          Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None))
+    | NCic.Const r -> Ast.Ident (NCicPp.r2s false r, None)
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
-         k (*ctx*) (NCicSubstitution.subst_meta lc t)
-    | NCic.Meta (n,l) -> Ast.Meta (n, [](*aux_context l*))
+         k ctx (NCicSubstitution.subst_meta lc t)
+    | NCic.Meta (n,(s,l)) ->
+       (* CSC: qua non dovremmo espandere *)
+       let l = NCicUtils.expand_local_context l in
+        Ast.Meta
+         (n, List.map (fun x -> Some (k ctx (NCicSubstitution.lift s x))) l)
     | NCic.Sort NCic.Prop -> Ast.Sort `Prop
     | NCic.Sort NCic.Type _ -> Ast.Sort `Set
+    (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0"
+    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
+    | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
+    | C.Sort (C.Type l) -> 
+       F.fprintf f "Max(";
+       aux ctx (C.Sort (C.Type [List.hd l]));
+       List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
+        (List.tl l);
+       F.fprintf f ")"*)
+    (* CSC: qua siamo grezzi *)
     | NCic.Implicit `Hole -> Ast.UserInput
     | NCic.Implicit _ -> Ast.Implicit
     | NCic.Prod (n,s,t) ->
         let binder_kind = `Forall in
-         Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k s)), k t)
+         Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ctx s)),
+          k ((n,NCic.Decl s)::ctx) t)
     | NCic.Lambda (n,s,t) ->
-        Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t)
+        Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ctx s)),
+         k ((n,NCic.Decl s)::ctx) t)
     | NCic.LetIn (n,s,ty,t) ->
-        Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k t)
+        Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s,
+         k ((n,NCic.Decl s)::ctx) 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 lc t in
-        k (*ctx*)
+        k ctx
          (NCicReduction.head_beta_reduce ~upto:(List.length args)
            (match hd with
            | NCic.Appl l -> NCic.Appl (l@args)
            | _ -> NCic.Appl (hd :: args)))
-    | NCic.Appl args -> Ast.Appl (List.map k args)
-    (*| NCic.AConst (id,uri,substs) ->
-        register_uri id uri;
-        idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))*)
+    | NCic.Appl args -> Ast.Appl (List.map (k ctx) args)
     | NCic.Match (uri,ty,te,patterns) ->
 (*
         let name = NReference.name_of_reference uri in
@@ -174,17 +165,18 @@ let nast_of_cic ~subst =
           | `Term -> Some case_indty
         in
         idref id (Ast.Case (k te, indty, Some (k ty), patterns))
-*) Ast.Ident ("Un case",None)
+*) assert false
   in
-   k
+   k context
 ;;
 
 let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
  let module K = Content in
- let context' =
-  List.map
-   (function
-     | name,NCic.Decl t ->
+ let context',_ =
+  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      *)
@@ -193,9 +185,9 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
               K.dec_id = "-1"; 
               K.dec_inductive = false;
               K.dec_aref = "-1";
-              K.dec_type = t
-            })
-     | name,NCic.Def (t,ty) ->
+              K.dec_type = nast_of_cic ~subst ~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     *)
@@ -203,12 +195,12 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
              { K.def_name = (Some name);
                K.def_id = "-1"; 
                K.def_aref = "-1";
-               K.def_term = t;
-               K.def_type = ty
-             })
-   ) context
+               K.def_term = nast_of_cic ~subst ~context t;
+               K.def_type = nast_of_cic ~subst ~context ty
+             })::res,item::context
+   ) context ([],[])
  in
-  "-1",i,context',ty
+  "-1",i,context',nast_of_cic ~subst ~context ty
 ;;
 
 (*
diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli
index 6381e7f48..e66e2ef7a 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.mli
+++ b/helm/software/components/ng_cic_content/nTermCicContent.mli
@@ -76,5 +76,7 @@ val push: unit -> unit
 val pop: unit -> unit
 *)
 
-val nast_of_cic : subst:NCic.substitution -> NCic.term -> CicNotationPt.term
-val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> NCic.term Content.conjecture
+val nast_of_cic :
+ subst:NCic.substitution -> context:NCic.context -> NCic.term ->
+  CicNotationPt.term
+val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture
diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index e8b7c6dab..ccac8dff6 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -13,6 +13,8 @@
 
 val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
 
+val r2s: bool -> NReference.reference -> string
+
 val ppterm: 
   context:NCic.context -> 
   subst:NCic.substitution ->