helm/software/components/ng_kernel/nCicPp.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 let ppterm =
  15   ref (fun ~context ~subst ~metasenv ?inside_fix t -> "Please, set a pp callback")
  16 ;;
  17
  18 let set_ppterm f = ppterm := f;;
  19
  20 let ppterm ~context ~subst ~metasenv ?inside_fix t =
  21   !ppterm ~context ~subst ~metasenv ?inside_fix t
  22 ;;
  23
  24 module C = NCic
  25 module R = NReference
  26
  27 let r2s pp_fix_name r =
  28   try
  29     match r with
  30     | R.Ref (u,R.Ind (_,i)) ->
  31         (match NCicLibrary.get_obj u with
  32         | _,_,_,_, C.Inductive (_,_,itl,_) ->
  33             let _,name,_,_ = List.nth itl i in name
  34         | _ -> assert false)
  35     | R.Ref (u,R.Con (i,j)) ->
  36         (match NCicLibrary.get_obj u with
  37         | _,_,_,_, C.Inductive (_,_,itl,_) ->
  38             let _,_,_,cl = List.nth itl i in
  39             let _,name,_ = List.nth cl (j-1) in name
  40         | _ -> assert false)
  41     | R.Ref (u,(R.Decl | R.Def _)) ->
  42         (match NCicLibrary.get_obj u with
  43         | _,_,_,_, C.Constant (_,name,_,_,_) -> name
  44         | _ -> assert false)
  45     | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
  46         (match NCicLibrary.get_obj u with
  47         | _,_,_,_, C.Fixpoint (_,fl,_) ->
  48             if pp_fix_name then
  49               let _,name,_,_,_ = List.nth fl i in name
  50             else
  51               NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
  52         | _ -> assert false)
  53   with exn -> R.string_of_reference r
  54 ;;
  55
  56 let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t =
  57   let buff = Buffer.create 100 in
  58   let f = Format.formatter_of_buffer buff in
  59   let module F = Format in
  60   let rec aux ?(toplevel=false) ctx = function
  61    | C.Rel m ->
  62          (try
  63             let name = List.nth ctx (m-1) in
  64             F.fprintf f "%s" (if name = "_" then "__"^string_of_int m else name)
  65          with Failure _ -> F.fprintf f " -%d" (m - List.length ctx))
  66    | C.Const r -> F.fprintf f "%s" (r2s inside_fix r)
  67    | C.Prod ("_",s,t) ->
  68        if not toplevel then F.fprintf f "(";
  69        F.fprintf f "@[<hov 1>";
  70        (match s with
  71        | C.Prod ("_",_,_) -> aux ~toplevel:false ctx s
  72        | _ -> aux ~toplevel:true ctx s);
  73        F.fprintf f "@;→ ";
  74        aux ~toplevel:true ("_"::ctx) t;
  75        F.fprintf f "@]";
  76        if not toplevel then F.fprintf f ")";
  77    | C.Prod (name,s,t) ->
  78        if not toplevel then F.fprintf f "(";
  79        F.fprintf f "@[<hov 1>";
  80        F.fprintf f "@[<hov 2>∀%s:@;" name;
  81        aux ~toplevel:true ctx s;
  82        F.fprintf f "@].@;";
  83        aux ~toplevel:true (name::ctx) t;
  84        F.fprintf f "@]";
  85        if not toplevel then F.fprintf f ")";
  86    | C.Lambda (name,s,t) ->
  87        if not toplevel then F.fprintf f "(";
  88        F.fprintf f "@[<hov 1>";
  89        F.fprintf f "λ%s:" name;
  90        aux ~toplevel:true ctx s;
  91        F.fprintf f ".@;";
  92        aux ~toplevel:true (name::ctx) t;
  93        F.fprintf f "@]";
  94        if not toplevel then F.fprintf f ")";
  95    | C.LetIn (name,ty,t,b) ->
  96        if not toplevel then F.fprintf f "(";
  97        F.fprintf f "@[<hov 1>";
  98        F.fprintf f "let %s:@;" name;
  99        aux ~toplevel:true ctx ty;
 100        F.fprintf f "@;≝ ";
 101        aux ~toplevel:true ctx t;
 102        F.fprintf f "@;in@;";
 103        (aux ~toplevel:true (name::ctx) b);
 104        F.fprintf f "@]";
 105        if not toplevel then F.fprintf f ")";
 106    | C.Match (r,oty,t,pl) ->
 107        F.fprintf f "@[<hov>match ";
 108        aux ~toplevel:true ctx t;
 109        F.fprintf f "@;return ";
 110        aux ~toplevel:true ctx oty;
 111        F.fprintf f "@; @[<v>[ ";
 112        if pl <> [] then
 113          begin
 114            F.fprintf f "@[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r));
 115            aux ~toplevel:true ctx (List.hd pl);
 116            F.fprintf f "@]";
 117            ignore(List.fold_left
 118              (fun i t ->
 119               F.fprintf f "@;| @[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor i r));
 120               aux ~toplevel:true ctx t;
 121               F.fprintf f "@]";
 122               i+1)
 123              2 (List.tl pl));
 124          end;
 125       F.fprintf f "]@] @]";
 126    | C.Appl l ->
 127        F.fprintf f "@[<hov 2>";
 128        if not toplevel then F.fprintf f "(";
 129        aux ctx (List.hd l);
 130        List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l);
 131        if not toplevel then F.fprintf f ")";
 132        F.fprintf f "@]"
 133    | C.Implicit _ -> F.fprintf f "?"
 134    | C.Meta (n,_) -> F.fprintf f "?%d" n
 135    | C.Sort C.Prop -> F.fprintf f "Prop"
 136    | C.Sort C.CProp -> F.fprintf f "CProp"
 137    | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
 138    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
 139    | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
 140    | C.Sort (C.Type l) ->
 141        F.fprintf f "Max(";
 142        aux ctx (C.Sort (C.Type [List.hd l]));
 143        List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
 144         (List.tl l);
 145        F.fprintf f ")"
 146   in
 147   aux ~toplevel:true (List.map fst context) t;
 148   F.fprintf f "@?";
 149   Buffer.contents buff
 150 ;;
 151
 152 let ppobj = function
 153   | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
 154       "{"^NUri.string_of_uri u^"}\n"^
 155       (if b then "let rec " else "let corec ") ^
 156        String.concat "\nand "
 157         (List.map (fun (_,name,n,ty,bo) ->
 158           name^ " on " ^ string_of_int n ^ " : " ^
 159           ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
 160           ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
 161   | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) ->
 162       "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
 163       "inductive "^
 164       String.concat "\nand "
 165         (List.map (fun (_,name,ty,cl) ->
 166           name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
 167           String.concat "\n"
 168           (List.map (fun (_,name,ty) ->
 169            "  | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
 170            cl)) tyl) ^ "."
 171   | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
 172       "{"^NUri.string_of_uri u^"}\n"^
 173         "axiom " ^ name ^ " : " ^
 174           ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
 175   | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
 176       "{"^NUri.string_of_uri u^"}\n"^
 177         "definition " ^ name ^ " : " ^
 178           ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
 179           ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
 180 ;;
 181
 182 let rec ppcontext ~subst ~metasenv = function
 183   | [] -> ""
 184   | (name, NCic.Decl t) :: tl ->
 185       ppcontext ~subst ~metasenv tl ^
 186       name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl t ^ "\n"
 187   | (name, NCic.Def (bo,ty)) :: tl->
 188       ppcontext ~subst ~metasenv tl ^
 189       name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl ty ^
 190       " := " ^ ppterm ~subst ~metasenv ~context:tl bo ^ "\n"
 191 ;;