From 3199f380051c1475c8e376f5cad44433044747e7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Apr 2008 14:37:56 +0000 Subject: [PATCH] pretty printer on steroids --- helm/software/components/ng_kernel/.depend | 6 +- helm/software/components/ng_kernel/Makefile | 2 +- helm/software/components/ng_kernel/check.ml | 2 +- helm/software/components/ng_kernel/nCicPp.ml | 119 +++++++++++++++---- helm/software/components/ng_kernel/rt.ml | 2 + 5 files changed, 103 insertions(+), 28 deletions(-) diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index dddb17c02..11b70ea0f 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,9 +1,9 @@ nReference.cmi: nUri.cmi -nCicPp.cmi: nCic.cmo oCic2NCic.cmi: nCic.cmo nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicPp.cmi: nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nCic.cmo nCic2OCic.cmi: nCic.cmo @@ -13,8 +13,6 @@ nUri.cmo: nUri.cmi nUri.cmx: nUri.cmi nReference.cmo: nUri.cmi nReference.cmi nReference.cmx: nUri.cmx nReference.cmi -nCicPp.cmo: nUri.cmi nReference.cmi nCic.cmo nCicPp.cmi -nCicPp.cmx: nUri.cmx nReference.cmx nCic.cmx nCicPp.cmi oCic2NCic.cmo: nUri.cmi nReference.cmi nCic.cmo oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCic.cmx oCic2NCic.cmi nCicUtils.cmo: nCic.cmo nCicUtils.cmi @@ -25,6 +23,8 @@ nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCic.cmo \ nCicEnvironment.cmi nCicEnvironment.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCic.cmx \ nCicEnvironment.cmi +nCicPp.cmo: nUri.cmi nReference.cmi nCicEnvironment.cmi nCic.cmo nCicPp.cmi +nCicPp.cmx: nUri.cmx nReference.cmx nCicEnvironment.cmx nCic.cmx nCicPp.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 4e78c8c14..8269534d5 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -4,11 +4,11 @@ PREDICATES = INTERFACE_FILES = \ nUri.mli \ nReference.mli \ - nCicPp.mli \ oCic2NCic.mli \ nCicUtils.mli \ nCicSubstitution.mli \ nCicEnvironment.mli \ + nCicPp.mli \ nCicReduction.mli \ nCicTypeChecker.mli \ oCicTypeChecker.mli \ diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index e98010de9..750910611 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -1,6 +1,6 @@ let _ = let indent = ref 0 in - let do_indent () = String.make !indent ' ' in +(* let do_indent () = String.make !indent ' ' in *) NCicTypeChecker.set_logger (function | `Start_type_checking s -> (); diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 57a3752fe..7573ad542 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -11,45 +11,118 @@ let ppterm ~context ~subst ~metasenv t = module C = NCic module R = NReference -let trivial_pp_term ~context ~subst ~metasenv = +let r2s = function + | R.Ref (_,u,R.Ind i) -> + (match snd(NCicEnvironment.get_obj u) with + | _,_,_,_, C.Inductive (_,_,itl,_) -> + let _,name,_,_ = List.nth itl i in name + | _ -> assert false) + | R.Ref (_,u,R.Con (i,j)) -> + (match snd(NCicEnvironment.get_obj u) with + | _,_,_,_, C.Inductive (_,_,itl,_) -> + let _,_,_,cl = List.nth itl i in + let _,name,_ = List.nth cl (j-1) in name + | _ -> assert false) + | R.Ref (_,u,(R.Decl | R.Def )) -> + (match snd(NCicEnvironment.get_obj u) with + | _,_,_,_, C.Constant (_,name,_,_,_) -> name + | _ -> assert false) + | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) -> + (match snd(NCicEnvironment.get_obj u) with + | _,_,_,_, C.Fixpoint (_,fl,_) -> + let name = NUri.string_of_uri u in + let name = Filename.basename name in + let name = Filename.chop_extension name in + name ^"("^ string_of_int i ^ ")" + | _ -> assert false) +;; + +let trivial_pp_term ~context ~subst ~metasenv t = + let buff = Buffer.create 100 in + let f = Format.formatter_of_buffer buff in + let module F = Format in let rec aux ctx = function | C.Rel m -> - (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^")" + (try F.fprintf f "%s" (List.nth ctx (m-1)) + with Failure _ -> F.fprintf f " -%d" (m - List.length context)) + | C.Const r -> F.fprintf f "%s" (r2s r) + | C.Prod ("_",s,t) -> + F.fprintf f "@["; + aux ctx s; + F.fprintf f "@;→ "; + aux ("_"::ctx) t; + F.fprintf f "@]"; + | C.Prod (name,s,t) -> + F.fprintf f "@["; + F.fprintf f "∀%s:" name; + aux ctx s; + F.fprintf f ".@;"; + aux (name::ctx) t; + F.fprintf f "@]"; | C.Lambda (name,s,t) -> - "(\lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t^")" + F.fprintf f "@["; + F.fprintf f "λ%s:" name; + aux ctx s; + F.fprintf f ".@;"; + aux (name::ctx) t; + F.fprintf f "@]"; | C.LetIn (name,ty,t,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 ^ " with\n" ^ "[" ^ - String.concat "\n|" (List.map (aux ctx) pl) ^ "]\n" - | C.Appl l -> "("^String.concat " " (List.map (aux ctx) l) ^")" - | C.Implicit _ -> "?" - | C.Meta (n,_) -> "?"^string_of_int n - | C.Sort C.Prop -> "Prop" - | C.Sort C.CProp -> "CProp" - | C.Sort (C.Type n) -> "Type"^string_of_int n + F.fprintf f "let %s:" name; + aux ctx ty; + F.fprintf f "≝@;"; + aux ctx t; + F.fprintf f "in@;"; + (aux (name::ctx) b) + | C.Match (r,oty,t,pl) -> + F.fprintf f "@[match "; + aux ctx t; + F.fprintf f "@;return "; + aux ctx oty; + F.fprintf f "@; @[[ "; + if pl <> [] then + begin + F.fprintf f "%s ⇒ " (r2s (R.mk_constructor 1 r)); + aux ctx (List.hd pl); + ignore(List.fold_left + (fun i t -> + F.fprintf f "@;| %s ⇒ " (r2s (R.mk_constructor i r)); + aux ctx t; i+1) + 2 (List.tl pl)); + end; + F.fprintf f "]@] @]"; + | C.Appl l -> + F.fprintf f "@[("; + aux ctx (List.hd l); + List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l); + F.fprintf f ")@]" + | C.Implicit _ -> F.fprintf f "?" + | C.Meta (n,_) -> F.fprintf f "?%d" n + | C.Sort C.Prop -> F.fprintf f "Prop" + | C.Sort C.CProp -> F.fprintf f "CProp" + | C.Sort (C.Type n) -> F.fprintf f "Type%d" n in - aux (List.map fst context) + aux (List.map fst context) t; + F.fprintf f "@?"; + Buffer.contents buff ;; 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 ^ " : " ^ + String.concat "\nand " (fst + (List.fold_right (fun (_,name,n,ty,bo) (l,i) -> + ((Filename.chop_extension (Filename.basename (NUri.string_of_uri u))^ + "("^string_of_int (i-1) ^") aka "^name^ + " on " ^ string_of_int n ^ " : " ^ ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ - ppterm ~metasenv ~subst ~context:[] bo) fl) + ppterm ~metasenv ~subst ~context:[] bo) :: l),i-1) fl + ([],List.length 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:[] ty ^ " := \n"^ ppterm ~metasenv ~subst ~context:[] bo ^ "\n" ;; diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_kernel/rt.ml index 89e863ffc..cc4d5dd33 100644 --- a/helm/software/components/ng_kernel/rt.ml +++ b/helm/software/components/ng_kernel/rt.ml @@ -6,6 +6,8 @@ let _ = prerr_endline "VECCHIO"; prerr_endline (CicPp.ppobj o); let l = OCic2NCic.convert_obj u o in + (* fill the new env *) + let _ = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in prerr_endline "OGGETTI:........................................."; List.iter (fun o -> prerr_endline (NCicPp.ppobj o)) l; prerr_endline "/OGGETTI:........................................."; -- 2.39.2