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

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

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