helm/software/components/ng_kernel/nCicPp.ml

   1 let ppterm =
   2   ref (fun ~context ~subst ~metasenv t -> "Please, set a pp callback")
   3 ;;
   4
   5 let set_ppterm f = ppterm := f;;
   6
   7 let ppterm ~context ~subst ~metasenv t =
   8   !ppterm ~context ~subst ~metasenv t
   9 ;;
  10
  11 module C = NCic
  12 module R = NReference
  13
  14 let r2s = function
  15   | R.Ref (_,u,R.Ind i) ->
  16       (match snd(NCicEnvironment.get_obj u) with
  17       | _,_,_,_, C.Inductive (_,_,itl,_) ->
  18           let _,name,_,_ = List.nth itl i in name
  19       | _ -> assert false)
  20   | R.Ref (_,u,R.Con (i,j)) ->
  21       (match snd(NCicEnvironment.get_obj u) with
  22       | _,_,_,_, C.Inductive (_,_,itl,_) ->
  23           let _,_,_,cl = List.nth itl i in
  24           let _,name,_ = List.nth cl (j-1) in name
  25       | _ -> assert false)
  26   | R.Ref (_,u,(R.Decl | R.Def )) ->
  27       (match snd(NCicEnvironment.get_obj u) with
  28       | _,_,_,_, C.Constant (_,name,_,_,_) -> name
  29       | _ -> assert false)
  30   | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
  31       (match snd(NCicEnvironment.get_obj u) with
  32       | _,_,_,_, C.Fixpoint (_,fl,_) ->
  33           let name = NUri.string_of_uri u in
  34           let name = Filename.basename name in
  35           let name = Filename.chop_extension name in
  36           name ^"("^ string_of_int i ^ ")"
  37       | _ -> assert false)
  38 ;;
  39
  40 let trivial_pp_term ~context ~subst ~metasenv t =
  41   let buff = Buffer.create 100 in
  42   let f = Format.formatter_of_buffer buff in
  43   let module F = Format in
  44   let rec aux ctx = function
  45    | C.Rel m ->
  46        (try F.fprintf f "%s" (List.nth ctx (m-1))
  47        with Failure _ -> F.fprintf f " -%d" (m - List.length context))
  48    | C.Const r -> F.fprintf f "%s" (r2s r)
  49    | C.Prod ("_",s,t) ->
  50        F.fprintf f "@[<hov 1>";
  51        aux ctx s;
  52        F.fprintf f "@;→ ";
  53        aux ("_"::ctx) t;
  54        F.fprintf f "@]";
  55    | C.Prod (name,s,t) ->
  56        F.fprintf f "@[<hov 1>";
  57        F.fprintf f "∀%s:" name;
  58        aux ctx s;
  59        F.fprintf f ".@;";
  60        aux (name::ctx) t;
  61        F.fprintf f "@]";
  62    | C.Lambda (name,s,t) ->
  63        F.fprintf f "@[<hov 1>";
  64        F.fprintf f "λ%s:" name;
  65        aux ctx s;
  66        F.fprintf f ".@;";
  67        aux (name::ctx) t;
  68        F.fprintf f "@]";
  69    | C.LetIn (name,ty,t,b) ->
  70        F.fprintf f "let %s:" name;
  71        aux ctx ty;
  72        F.fprintf f "≝@;";
  73        aux ctx t;
  74        F.fprintf f "in@;";
  75        (aux (name::ctx) b)
  76    | C.Match (r,oty,t,pl) ->
  77        F.fprintf f "@[<hov>match ";
  78        aux ctx t;
  79        F.fprintf f "@;return ";
  80        aux ctx oty;
  81        F.fprintf f "@; @[<v>[ ";
  82        if pl <> [] then
  83          begin
  84            F.fprintf f "%s ⇒ " (r2s (R.mk_constructor 1 r));
  85            aux ctx (List.hd pl);
  86            ignore(List.fold_left
  87              (fun i t ->
  88               F.fprintf f "@;| %s ⇒ " (r2s (R.mk_constructor i r));
  89               aux ctx t; i+1)
  90              2 (List.tl pl));
  91          end;
  92       F.fprintf f "]@] @]";
  93    | C.Appl l ->
  94        F.fprintf f "@[<h 2>(";
  95        aux ctx (List.hd l);
  96        List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l);
  97        F.fprintf f ")@]"
  98    | C.Implicit _ -> F.fprintf f "?"
  99    | C.Meta (n,_) -> F.fprintf f "?%d" n
 100    | C.Sort C.Prop -> F.fprintf f "Prop"
 101    | C.Sort C.CProp -> F.fprintf f "CProp"
 102    | C.Sort (C.Type n) -> F.fprintf f "Type%d" n
 103   in
 104   aux (List.map fst context) t;
 105   F.fprintf f "@?";
 106   Buffer.contents buff
 107 ;;
 108
 109 let ppobj = function
 110   | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
 111        "let rec "^
 112        String.concat "\nand " (fst
 113         (List.fold_right (fun (_,name,n,ty,bo) (l,i) ->
 114           ((Filename.chop_extension (Filename.basename (NUri.string_of_uri u))^
 115           "("^string_of_int (i-1) ^") aka "^name^
 116           " on " ^ string_of_int n ^ " : " ^
 117           ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
 118           ppterm ~metasenv ~subst ~context:[] bo) :: l),i-1) fl
 119            ([],List.length fl)))
 120   | (u,_,_,_,NCic.Inductive (b, _,tyl, _)) -> "inductive"
 121   | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
 122         "axiom " ^ name ^ " : " ^
 123           ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
 124   | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
 125         "definition " ^ name ^ " : " ^
 126           ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
 127           ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
 128 ;;