X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=2c46fef6f18a75874ff5486c71f2e107a96528ec;hb=c25986cdbd05f0c06d93f850453b5f82695b7814;hp=27c7fc97ef837fc06275a3b4060d6e9eeb43fb5e;hpb=79501fecaa51e1afff2ac940706b4490b368dc27;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 27c7fc97e..2c46fef6f 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -4,7 +4,7 @@ let ppterm = let set_ppterm f = ppterm := f;; -let ppterm ?(context=[]) ?(subst=[]) ?(metasenv=[]) t = +let ppterm ~context ~subst ~metasenv t = !ppterm ~context ~subst ~metasenv t ;; @@ -14,16 +14,17 @@ module R = NReference let trivial_pp_term ~context ~subst ~metasenv = let rec aux ctx = function | C.Rel m -> - (try List.nth ctx m - with Not_found -> " -" ^ string_of_int (m - List.length context)) + (try List.nth ctx (m-1) + with Failure _ -> " -" ^ string_of_int (m - List.length context)) | C.Const r -> R.string_of_reference r - | C.Prod (name,s,t) -> " \Pi "^name^":"^aux ctx s^"."^aux (name::ctx) t - | C.Lambda (name,s,t) -> " \lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t + | C.Prod (name,s,t) -> "(\Pi "^name^":"^aux ctx s^"."^aux (name::ctx) t^")" + | C.Lambda (name,s,t) -> + "(\lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t^")" | C.LetIn (name,ty,t,b) -> - " let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b + "(let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b^")" | C.Match (_,oty,t,pl) -> - " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^ - String.concat "|" (List.map (aux ctx) pl) ^ "]" + " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^ + String.concat "|" (List.map (aux ctx) pl) ^ "]" | C.Appl l -> "("^String.concat " " (List.map (aux ctx) l) ^")" | C.Implicit _ -> "?" | C.Meta (n,_) -> "?"^string_of_int n @@ -32,4 +33,23 @@ let trivial_pp_term ~context ~subst ~metasenv = | C.Sort (C.Type n) -> "Type"^string_of_int n in aux (List.map fst context) +;; +let ppobj = function + | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> + NUri.string_of_uri u^"\n"^ + "let rec "^ + String.concat "\nand " + (List.map (fun (_,name,n,ty,bo) -> + name ^ " on " ^ string_of_int n ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ + ppterm ~metasenv ~subst ~context:[] bo) fl) + | (u,_,_,_,NCic.Inductive (b, _,tyl, _)) -> "inductive" + | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) -> + "axiom " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ "\n" + | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) -> + "definition " ^ name ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ ":=\n"^ + ppterm ~metasenv ~subst ~context:[] bo ^ "\n" +;;