The substitution is now taken in account when printing sequents in the

sequent viewer. Context is not yet taken in account.

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index 41683b94f51744dbd7d615e7f82e7c40dba99e46..b98f95634a3619e0e0e8027ae3fa278155c396f8 100644 (file)
--- 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 b492631368417af175b713b36a5f99f697e089cd..03b5287835ca2eb8365a175da8d69fdf30ff2caf 100644 (file)
--- 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 d770837bc4ecd4fc4a294abdf38e31277e2926a6..3253e7908802446780ab1f6a180dea3ff0503489 100644 (file)
--- 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 2f2acb077f14c85642738b7723051e10df9b33b8..6381e7f487853af26b6816ab69c3e100ffa6a06a 100644 (file)
--- 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 27725882e8d867f6f8acbe34c31c4df7e80c1e7c..c504996e0d225e18ebe89e83e0188e680a0994eb 100644 (file)
--- 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