X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=1058a48cca4a0faaa09ee2609d4f10a9dc522b08;hb=d40ad33ad3d075c5dd74b6a67131683b0ebe32d6;hp=a7b6559a6520300c108b3167272264bce37f70cc;hpb=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index a7b6559a6..1058a48cc 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -45,22 +45,22 @@ let r2s pp_fix_name r = if pp_fix_name then let _,name,_,_,_ = List.nth fl i in name else - NUri.name_of_uri u ^"("^ string_of_int i ^ ")" + NUri.name_of_uri u (*^"("^ string_of_int i ^ ")"*) | _ -> assert false) with | NCicEnvironment.ObjectNotFound _ | Failure "nth" | Invalid_argument "List.nth" -> R.string_of_reference r - ;; let string_of_implicit_annotation = function | `Closed -> "▪" | `Type -> "" | `Hole -> "□" + | `Tagged s -> "[\"" ^ s ^ "\"]" | `Term -> "Term" | `Typeof x -> "Ty("^string_of_int x^")" - | `Vector -> "..." + | `Vector -> "…" ;; let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = @@ -135,8 +135,14 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = 2 (List.tl pl)); end; F.fprintf f "]@] @]"; - | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> - F.fprintf f "BAD APPLICATION" + | C.Appl [] -> + F.fprintf f "BAD APPLICATION: empty list" + | C.Appl [x] -> + F.fprintf f "BAD APPLICATION: just the head: "; + aux ctx x + | C.Appl (C.Appl _ as x::_) -> + F.fprintf f "BAD APPLICATION: appl of appl with head: "; + aux ctx x | 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 @@ -168,26 +174,20 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = (List.map (NCicSubstitution.lift shift) (List.tl l)); end; F.fprintf f "])" - | C.Sort C.Prop -> F.fprintf f "Prop" - | C.Sort (C.Type []) -> F.fprintf f "Type0" - | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) - | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) - | C.Sort (C.Type l) -> - F.fprintf f "Max("; - aux ctx (C.Sort (C.Type [List.hd l])); - List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) - (List.tl l); - F.fprintf f ")" + | C.Sort s -> NCicEnvironment.ppsort f s in aux ~toplevel:true (List.map fst context) t ;; let on_buffer f t = + try let buff = Buffer.create 100 in let formatter = F.formatter_of_buffer buff in f ~formatter:formatter t; F.fprintf formatter "@?"; Buffer.contents buff + with Failure m -> + "[[Unprintable: " ^ m ^ "]]" ;; let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = @@ -195,29 +195,49 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t ;; -let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function +let rec ppcontext ~formatter ?(sep="; ") ~subst ~metasenv = function | [] -> () | (name, NCic.Decl t) :: tl -> ppcontext ~formatter ~sep ~subst ~metasenv tl; F.fprintf formatter "%s: " name; ppterm ~formatter ~subst ~metasenv ~context:tl t; - F.fprintf formatter "%s" sep + F.fprintf formatter "%s@;" sep | (name, NCic.Def (bo,ty)) :: tl-> ppcontext ~formatter ~sep ~subst ~metasenv tl; F.fprintf formatter "%s: " name; ppterm ~formatter ~subst ~metasenv ~context:tl ty; F.fprintf formatter " := "; ppterm ~formatter ~subst ~metasenv ~context:tl bo; - F.fprintf formatter "%s" sep + F.fprintf formatter "%s@;" sep +;; +let ppcontext ~formatter ?sep ~subst ~metasenv c = + F.fprintf formatter "@["; + ppcontext ~formatter ?sep ~subst ~metasenv c; + F.fprintf formatter "@]"; +;; + +let ppmetaattrs = + function + [] -> "" + | attrs -> + "(" ^ + String.concat "," + (List.map + (function + `IsSort -> "sort" + | `Name n -> "name=" ^ n + | `InScope -> "in_scope" + | `OutScope n -> "out_scope:" ^ string_of_int n + ) attrs) ^ + ")" ;; let rec ppmetasenv ~formatter ~subst metasenv = function | [] -> () - | (i,(name, ctx, ty)) :: tl -> + | (i,(attrs, ctx, ty)) :: tl -> F.fprintf formatter "@["; - let name = match name with Some n -> "("^n^")" | _ -> "" in ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; - F.fprintf formatter "@;⊢@;?%d%s :@;" i name; + F.fprintf formatter "@;⊢@;?%d%s :@;" i (ppmetaattrs attrs); ppterm ~formatter ~metasenv ~subst ~context:ctx ty; F.fprintf formatter "@]@\n"; ppmetasenv ~formatter ~subst metasenv tl @@ -229,10 +249,9 @@ let ppmetasenv ~formatter ~subst metasenv = let rec ppsubst ~formatter ~subst ~metasenv = function | [] -> () - | (i,(name, ctx, t, ty)) :: tl -> - let name = match name with Some n -> "("^n^")" | _ -> "" in + | (i,(attrs, ctx, t, ty)) :: tl -> ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; - F.fprintf formatter " ⊢ ?%d%s := " i name; + F.fprintf formatter " ⊢ ?%d%s := " i (ppmetaattrs attrs); ppterm ~formatter ~metasenv ~subst ~context:ctx t; F.fprintf formatter " : "; ppterm ~formatter ~metasenv ~subst ~context:ctx ty; @@ -244,6 +263,35 @@ let ppsubst ~formatter ~metasenv subst = ppsubst ~formatter ~metasenv ~subst subst ;; +let string_of_generated = function + | `Generated -> "Generated" + | `Provided -> "Provided" +;; + +let string_of_flavour = function + | `Definition -> "Definition" + | `Fact -> "Fact" + | `Lemma -> "Lemma" + | `Theorem -> "Theorem" + | `Corollary -> "Corollary" + | `Example -> "Example" +;; + +let string_of_pragma = function + | `Coercion _arity -> "Coercion _" + | `Elim _sort -> "Elim _" + | `Projection -> "Projection" + | `InversionPrinciple -> "InversionPrinciple" + | `Variant -> "Variant" + | `Local -> "Local" + | `Regular -> "Regular" +;; + +let string_of_fattrs (g,f,p) = + String.concat "," + [ string_of_generated g; string_of_flavour f; string_of_pragma p ] +;; + let ppobj ~formatter (u,_,metasenv, subst, o) = F.fprintf formatter "metasenv:\n"; ppmetasenv ~formatter ~subst metasenv; @@ -252,7 +300,7 @@ let ppobj ~formatter (u,_,metasenv, subst, o) = (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "..."; F.fprintf formatter "\n"; match o with - | NCic.Fixpoint (b, fl, _) -> + | NCic.Fixpoint (b, fl, attrs) -> F.fprintf formatter "{%s}@\n@[" (NUri.string_of_uri u); F.fprintf formatter "@[%s"(if b then "let rec " else "let corec "); HExtlib.list_iter_sep @@ -263,7 +311,8 @@ let ppobj ~formatter (u,_,metasenv, subst, o) = F.fprintf formatter "@]@;@[:=@;"; ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo; F.fprintf formatter "@]") fl; - F.fprintf formatter "@]" + F.fprintf formatter "@; %s" (string_of_fattrs attrs); + F.fprintf formatter "@]" | NCic.Inductive (b, leftno,tyl, _) -> F.fprintf formatter "{%s} with %d fixed params@\n@[@[%s" (NUri.string_of_uri u) leftno