- Grammar for all obj commands ported to NG (let recs and inductives still need

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index c4c66374a622b59965efdf611d262aa495732bde..6a38873fc360d9b238f3ff13bbed0174fc521bd7 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -14,6 +14,9 @@
 module C = NCic
 module R = NReference
 
+let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);;
+let set_head_beta_reduce = (:=) head_beta_reduce;;
+
 let r2s pp_fix_name r = 
   try
     match r with
@@ -128,6 +131,14 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
       F.fprintf f "]@] @]";
    | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> 
        F.fprintf f "BAD APPLICATION"
+   | C.Appl (C.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
+       aux ctx 
+         (!head_beta_reduce ~upto:(List.length args)
+           (match hd with
+           | NCic.Appl l -> NCic.Appl (l@args)
+           | _ -> NCic.Appl (hd :: args)))
    | C.Appl l -> 
        F.fprintf f "@[<hov 2>";
        if not toplevel then F.fprintf f "(";
@@ -186,7 +197,7 @@ let rec ppcontext ?(sep="\n") ~subst ~metasenv = function
 let rec ppmetasenv ~subst metasenv = function
   | [] -> ""
   | (i,(name, ctx, ty)) :: tl ->
-      let name = match name with Some n -> "(\""^n^"\")" | _ -> "" in
+      let name = match name with Some n -> "("^n^")" | _ -> "" in
       ppcontext ~sep:"; " ~subst ~metasenv ctx ^
       " ⊢ ?"^string_of_int i^name^" : " ^ 
       ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^
@@ -212,6 +223,7 @@ let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
 
 let ppobj (u,_,metasenv, subst, o) = 
   "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^
+  "subst:\n" ^ ppsubst subst ~metasenv ^ "\n" ^
   match o with 
   | NCic.Fixpoint (b, fl, _) -> 
       "{"^NUri.string_of_uri u^"}\n"^