X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=1a793b92fde5db51b370c46eac38a5343f188058;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=bd5b7f206a4bd1f02404249e5d85d7f35430cbfe;hpb=105236d275296be7ab2561f83ec539a1d166b445;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index bd5b7f206..1a793b92f 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -18,45 +18,49 @@ module F = Format let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);; let set_head_beta_reduce = (:=) head_beta_reduce;; +let get_obj = ref (fun _ -> assert false);; +let set_get_obj f = get_obj := f;; + let r2s pp_fix_name r = try match r with | R.Ref (u,R.Ind (_,i,_)) -> - (match NCicLibrary.get_obj u with + (match !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 NCicLibrary.get_obj u with + (match !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 NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Constant (_,name,_,_,_) -> name | _ -> assert false) | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) -> - (match NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Fixpoint (_,fl,_) -> 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 - | NCicLibrary.ObjectNotFound _ + | 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 -> "…" ;; let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = @@ -131,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 @@ -164,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 = @@ -191,30 +195,53 @@ 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 + | `IsTerm -> "term" + | `IsType -> "type" + | `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 -> - let name = match name with Some n -> "("^n^")" | _ -> "" in + | (i,(attrs, ctx, ty)) :: tl -> + F.fprintf formatter "@["; 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"; + F.fprintf formatter "@]@\n"; ppmetasenv ~formatter ~subst metasenv tl ;; @@ -224,10 +251,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; @@ -235,8 +261,38 @@ let rec ppsubst ~formatter ~subst ~metasenv = function ppsubst ~formatter ~subst ~metasenv tl ;; -let ppsubst ~formatter ~metasenv subst = - ppsubst ~formatter ~metasenv ~subst subst +let ppsubst ~formatter ~metasenv ?(use_subst=true) subst = + let ssubst = if use_subst then subst else [] in + ppsubst ~formatter ~metasenv ~subst:ssubst 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) = @@ -247,40 +303,47 @@ 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, _) -> - 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 ~sep:(fun ()->F.fprintf formatter "\nand ") + | 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 + ~sep:(fun () -> F.fprintf formatter "@\n@[and ") (fun (_,name,n,ty,bo) -> - F.fprintf formatter "%s on %d : " name n; + F.fprintf formatter "%s on %d :@;" name n; ppterm ~formatter ~metasenv ~subst ~context:[] ty; - F.fprintf formatter " :=\n"; - ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl + F.fprintf formatter "@]@;@[:=@;"; + ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo; + F.fprintf formatter "@]") fl; + 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" + F.fprintf formatter "{%s} with %d fixed params@\n@[@[%s" (NUri.string_of_uri u) leftno (if b then "inductive " else "coinductive "); - HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ") + HExtlib.list_iter_sep + ~sep:(fun () -> F.fprintf formatter "@\n@[and ") (fun (_,name,ty,cl) -> - F.fprintf formatter "%s: " name; + F.fprintf formatter "%s:@;" name; ppterm ~formatter ~metasenv ~subst ~context:[] ty; - F.fprintf formatter " :=\n"; - HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "\n") + F.fprintf formatter "@]@;@[:=@;"; + HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "@;") (fun (_,name,ty) -> - F.fprintf formatter " | %s: " name; - ppterm ~formatter ~metasenv ~subst ~context:[] ty) - cl - ) tyl + F.fprintf formatter "| %s: " name; + ppterm ~formatter ~metasenv ~subst ~context:[] ty;) + cl; + F.fprintf formatter "@]" + ) tyl ; + F.fprintf formatter "@]" | NCic.Constant (_,name,None,ty, _) -> - F.fprintf formatter "{%s}\naxiom %s : " (NUri.string_of_uri u) name; + F.fprintf formatter "{%s}@\n@[axiom %s :@;" (NUri.string_of_uri u) name; ppterm ~formatter ~metasenv ~subst ~context:[] ty; - F.fprintf formatter "\n" + F.fprintf formatter "@]@\n" | NCic.Constant (_,name,Some bo,ty, _) -> - F.fprintf formatter "{%s}\ndefinition %s : " (NUri.string_of_uri u) name; + F.fprintf formatter "{%s}@\n@[@[definition %s :@;" (NUri.string_of_uri u) name; ppterm ~formatter ~metasenv ~subst ~context:[] ty; - F.fprintf formatter " := \n"; + F.fprintf formatter "@]@;@[:=@;"; ppterm ~formatter ~metasenv ~subst ~context:[] bo; - F.fprintf formatter "\n" + F.fprintf formatter "@]@\n@]" ;; let ppterm ~context ~subst ~metasenv ?margin ?inside_fix t = @@ -293,7 +356,9 @@ let ppcontext ?sep ~subst ~metasenv ctx = let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;; -let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;; +let ppsubst ~metasenv ?use_subst subst = + on_buffer (ppsubst ~metasenv ?use_subst) subst +;; let ppobj obj = on_buffer ppobj obj;;