From 21d58ec6efaf1969c42eb3929475b638cdd0ce2e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Apr 2009 17:50:35 +0000
Subject: [PATCH] The substitution is now taken in account when printing
 sequents in the sequent viewer. Context is not yet taken in account.

---
 .../components/content_pres/sequent2pres.ml     |  4 ++--
 .../components/content_pres/sequent2pres.mli    |  4 +++-
 .../ng_cic_content/nTermCicContent.ml           | 17 ++++++++++++++---
 .../ng_cic_content/nTermCicContent.mli          |  4 ++--
 helm/software/matita/applyTransformation.ml     |  4 ++--
 5 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index 41683b94f..b98f95634 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -105,10 +105,10 @@ let sequent2pres ~ids_to_inner_sorts =
         (CicNotationPres.render ids_to_uris
           (TermContentPres.pp_ast ast)))
 
-let nsequent2pres =
+let nsequent2pres ~subst =
   sequent2pres0
     (fun term ->
-      let ast = NTermCicContent.nast_of_cic term in
+      let ast = NTermCicContent.nast_of_cic ~subst term in
        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 b49263136..03b528783 100644
--- a/helm/software/components/content_pres/sequent2pres.mli
+++ b/helm/software/components/content_pres/sequent2pres.mli
@@ -37,4 +37,6 @@ val sequent2pres :
   Cic.annterm Content.conjecture ->
     CicNotationPres.boxml_markup
 
-val nsequent2pres : NCic.term Content.conjecture -> CicNotationPres.boxml_markup
+val nsequent2pres :
+ subst:NCic.substitution -> NCic.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 d770837bc..3253e7908 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -102,10 +102,13 @@ let r2s pp_fix_name r =
   with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r
 ;;
 
-let nast_of_cic =
+let nast_of_cic ~subst =
   let rec k = function
-    | NCic.Rel n -> Ast.Ident (string_of_int n, None)
+    | NCic.Rel n -> Ast.Ident ("-" ^ string_of_int n, None)
     | NCic.Const r -> Ast.Ident (r2s true 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*))
     | NCic.Sort NCic.Prop -> Ast.Sort `Prop
     | NCic.Sort NCic.Type _ -> Ast.Sort `Set
@@ -118,6 +121,14 @@ let nast_of_cic =
         Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t)
     | NCic.LetIn (n,s,ty,t) ->
         Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k 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*)
+         (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;
@@ -168,7 +179,7 @@ let nast_of_cic =
    k
 ;;
 
-let map_sequent (i,(n,context,ty):int * NCic.conjecture) =
+let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
  let module K = Content in
  let context' =
   List.map
diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli
index 2f2acb077..6381e7f48 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.mli
+++ b/helm/software/components/ng_cic_content/nTermCicContent.mli
@@ -76,5 +76,5 @@ val push: unit -> unit
 val pop: unit -> unit
 *)
 
-val nast_of_cic : NCic.term -> CicNotationPt.term
-val map_sequent : int * NCic.conjecture -> NCic.term Content.conjecture
+val nast_of_cic : subst:NCic.substitution -> NCic.term -> CicNotationPt.term
+val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> NCic.term Content.conjecture
diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 27725882e..c504996e0 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -65,9 +65,9 @@ let mml_of_cic_sequent metasenv sequent =
     (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
 
 let nmml_of_cic_sequent metasenv subst sequent =
-  let content_sequent = NTermCicContent.map_sequent sequent in 
+  let content_sequent = NTermCicContent.nmap_sequent ~subst sequent in 
   let pres_sequent = 
-   Sequent2pres.nsequent2pres content_sequent in
+   Sequent2pres.nsequent2pres subst content_sequent in
   let xmlpres = mpres_document pres_sequent in
    Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
 
-- 
2.39.2