helm/software/components/cic_exportation/cicExportation.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
  27
  28 exception CicExportationInternalError;;
  29 exception NotEnoughElements;;
  30
  31 (* *)
  32
  33 let is_mcu_type u =
  34   UriManager.eq (UriManager.uri_of_string
  35   "cic:/matita/freescale/opcode/mcu_type.ind") u
  36 ;;
  37
  38 (* Utility functions *)
  39
  40 let analyze_term context t =
  41  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
  42   | Cic.Sort _ -> `Type
  43   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
  44   | ty ->
  45      match
  46       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
  47      with
  48      | Cic.Sort Cic.Prop -> `Proof
  49      | _ -> `Term
  50 ;;
  51
  52 let analyze_type context t =
  53  let rec aux =
  54   function
  55      Cic.Sort s -> `Sort s
  56    | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
  57    | Cic.Prod (_,_,t) -> aux t
  58    | _ -> `SomethingElse
  59  in
  60  match aux t with
  61     `Sort _ | `Optimize as res -> res
  62   | `SomethingElse ->
  63       match
  64        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
  65       with
  66           Cic.Sort Cic.Prop -> `Statement
  67        | _ -> `Type
  68 ;;
  69
  70 let ppid =
  71  let reserved =
  72   [ "to";
  73     "mod";
  74     "val";
  75     "in";
  76     "function"
  77   ]
  78  in
  79   function n ->
  80    let n = String.uncapitalize n in
  81     if List.mem n reserved then n ^ "_" else n
  82 ;;
  83
  84 let ppname =
  85  function
  86     Cic.Name s     -> ppid s
  87   | Cic.Anonymous  -> "_"
  88 ;;
  89
  90 (* get_nth l n   returns the nth element of the list l if it exists or *)
  91 (* raises NotEnoughElements if l has less than n elements             *)
  92 let rec get_nth l n =
  93  match (n,l) with
  94     (1, he::_) -> he
  95   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
  96   | (_,_) -> raise NotEnoughElements
  97 ;;
  98
  99 let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
 100  let name =
 101   if capitalize then
 102    String.capitalize (UriManager.name_of_uri uri)
 103   else
 104    ppid (UriManager.name_of_uri uri) in
 105   let filename =
 106    let suri = UriManager.buri_of_uri uri in
 107    let s = String.sub suri 5 (String.length suri - 5) in
 108    let s = Pcre.replace ~pat:"/" ~templ:"_" s in
 109     String.uncapitalize s in
 110   if current_module_uri = UriManager.buri_of_uri uri then
 111    name
 112   else
 113    String.capitalize filename ^ "." ^ name
 114 ;;
 115
 116 let current_go_up = ref "(.!(";;
 117 let at_level2 f x =
 118   try
 119     current_go_up := "(.~(";
 120     let rc = f x in
 121     current_go_up := "(.!(";
 122     rc
 123   with exn ->
 124     current_go_up := "(.!(";
 125     raise exn
 126 ;;
 127
 128 let pp current_module_uri ?metasenv ~in_type =
 129 let rec pp ~in_type t context =
 130  let module C = Cic in
 131    match t with
 132       C.Rel n ->
 133        begin
 134         try
 135          (match get_nth context n with
 136              Some (C.Name s,_) -> ppid s
 137            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 138            | None -> "_hidden_" ^ string_of_int n
 139          )
 140         with
 141          NotEnoughElements -> string_of_int (List.length context - n)
 142        end
 143     | C.Var (uri,exp_named_subst) ->
 144         qualified_name_of_uri current_module_uri uri ^
 145          pp_exp_named_subst exp_named_subst context
 146     | C.Meta (n,l1) ->
 147        (match metasenv with
 148            None ->
 149             "?" ^ (string_of_int n) ^ "[" ^
 150              String.concat " ; "
 151               (List.rev_map
 152                 (function
 153                     None -> "_"
 154                   | Some t -> pp ~in_type:false t context) l1) ^
 155              "]"
 156          | Some metasenv ->
 157             try
 158              let _,context,_ = CicUtil.lookup_meta n metasenv in
 159               "?" ^ (string_of_int n) ^ "[" ^
 160                String.concat " ; "
 161                 (List.rev
 162                   (List.map2
 163                     (fun x y ->
 164                       match x,y with
 165                          _, None
 166                        | None, _ -> "_"
 167                        | Some _, Some t -> pp ~in_type:false t context
 168                     ) context l1)) ^
 169                "]"
 170             with
 171               CicUtil.Meta_not_found _
 172             | Invalid_argument _ ->
 173               "???" ^ (string_of_int n) ^ "[" ^
 174                String.concat " ; "
 175                 (List.rev_map (function None -> "_" | Some t ->
 176                   pp ~in_type:false t context) l1) ^
 177                "]"
 178        )
 179     | C.Sort s ->
 180        (match s with
 181            C.Prop  -> "Prop"
 182          | C.Set   -> "Set"
 183          | C.Type _ -> "Type"
 184          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 185          | C.CProp _ -> "CProp"
 186        )
 187     | C.Implicit (Some `Hole) -> "%"
 188     | C.Implicit _ -> "?"
 189     | C.Prod (b,s,t) ->
 190        (match b with
 191           C.Name n ->
 192            let n = "'" ^ String.uncapitalize n in
 193             "(" ^ pp ~in_type:true s context ^ " -> " ^
 194             pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
 195         | C.Anonymous ->
 196            "(" ^ pp ~in_type:true s context ^ " -> " ^
 197            pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
 198     | C.Cast (v,t) -> pp ~in_type v context
 199     | C.Lambda (b,s,t) ->
 200        (match analyze_type context s with
 201            `Sort _
 202          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 203          | `Optimize -> prerr_endline "XXX lambda";assert false
 204          | `Type ->
 205             "(function " ^ ppname b ^ " -> " ^
 206              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 207     | C.LetIn (b,s,ty,t) ->
 208        (match analyze_term context s with
 209          | `Type
 210          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 211          | `Optimize
 212          | `Term ->
 213             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 214             " = " ^ pp ~in_type:false s context ^ " in " ^
 215              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 216     | C.Appl (he::tl) when in_type ->
 217        let hes = pp ~in_type he context in
 218        let stl = String.concat "," (clean_args_for_ty context tl) in
 219         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 220     | C.Appl (C.MutInd _ as he::tl) ->
 221        let hes = pp ~in_type he context in
 222        let stl = String.concat "," (clean_args_for_ty context tl) in
 223         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 224     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 225        let nparams =
 226         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 227            C.InductiveDefinition (_,_,nparams,_) -> nparams
 228          | _ -> assert false in
 229        let hes = pp ~in_type he context in
 230        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
 231         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
 232     | C.Appl li ->
 233        "(" ^ String.concat " " (clean_args context li) ^ ")"
 234     | C.Const (uri,exp_named_subst) ->
 235        qualified_name_of_uri current_module_uri uri ^
 236         pp_exp_named_subst exp_named_subst context
 237     | C.MutInd (uri,n,exp_named_subst) ->
 238        (try
 239          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 240             C.InductiveDefinition (dl,_,_,_) ->
 241              let (name,_,_,_) = get_nth dl (n+1) in
 242               qualified_name_of_uri current_module_uri
 243                (UriManager.uri_of_string
 244                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
 245               pp_exp_named_subst exp_named_subst context
 246           | _ -> raise CicExportationInternalError
 247         with
 248            Sys.Break as exn -> raise exn
 249          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
 250        )
 251     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
 252        (try
 253          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 254             C.InductiveDefinition (dl,_,_,_) ->
 255              let _,_,_,cons = get_nth dl (n1+1) in
 256               let id,_ = get_nth cons n2 in
 257                qualified_name_of_uri current_module_uri ~capitalize:true
 258                 (UriManager.uri_of_string
 259                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
 260                pp_exp_named_subst exp_named_subst context
 261           | _ -> raise CicExportationInternalError
 262         with
 263            Sys.Break as exn -> raise exn
 264          | _ ->
 265           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
 266            string_of_int n2
 267        )
 268     | C.MutCase (uri,n1,ty,te,patterns) ->
 269        if in_type then
 270         "unit (* TOO POLYMORPHIC TYPE *)"
 271        else (
 272        let rec needs_obj_magic ty =
 273         match CicReduction.whd context ty with
 274          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
 275          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
 276          | _ -> false (* it can be a Rel, e.g. in *_rec *)
 277        in
 278        let needs_obj_magic = needs_obj_magic ty in
 279        (match analyze_term context te with
 280            `Type -> assert false
 281          | `Proof ->
 282              (match patterns with
 283                  [] -> "assert false"   (* empty type elimination *)
 284                | [he] ->
 285                   pp ~in_type:false he context  (* singleton elimination *)
 286                | _ -> assert false)
 287          | `Optimize
 288          | `Term ->
 289             if patterns = [] then "assert false"
 290             else
 291              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
 292                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 293                    C.InductiveDefinition (dl,_,paramsno,_) ->
 294                     let (_,_,_,cons) = get_nth dl (n1+1) in
 295                     let rc =
 296                      List.map
 297                       (fun (id,ty) ->
 298                         (* this is just an approximation since we do not have
 299                            reduction yet! *)
 300                         let rec count_prods toskip =
 301                          function
 302                             C.Prod (_,_,bo) when toskip > 0 ->
 303                              count_prods (toskip - 1) bo
 304                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
 305                           | _ -> 0
 306                         in
 307                          qualified_name_of_uri current_module_uri
 308                           ~capitalize:true
 309                           (UriManager.uri_of_string
 310                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
 311                          count_prods paramsno ty
 312                       ) cons
 313                     in
 314                     if not (is_mcu_type uri) then rc, "","","",""
 315                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
 316                  | _ -> raise CicExportationInternalError
 317                )
 318               in
 319                let connames_and_argsno_and_patterns =
 320                 let rec combine =
 321                    function
 322                       [],[] -> []
 323                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
 324                     | _,_ -> assert false
 325                 in
 326                  combine (connames_and_argsno,patterns)
 327                in
 328                 go_up ^
 329                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
 330                  (String.concat "\n | "
 331                   (List.map
 332                    (fun (x,argsno,y) ->
 333                      let rec aux argsno context =
 334                       function
 335                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
 336                           let name =
 337                            match name with
 338                               Cic.Anonymous -> Cic.Anonymous
 339                             | Cic.Name n -> Cic.Name (ppid n) in
 340                           let args,res =
 341                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
 342                             bo
 343                           in
 344                            (match analyze_type context ty with
 345                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
 346                              | `Statement
 347                              | `Sort _ -> args,res
 348                              | `Type ->
 349                                  (match name with
 350                                      C.Anonymous -> "_"
 351                                    | C.Name s -> s)::args,res)
 352                        | t when argsno = 0 -> [],pp ~in_type:false t context
 353                        | t ->
 354                           ["{" ^ string_of_int argsno ^ " args missing}"],
 355                            pp ~in_type:false t context
 356                      in
 357                       let pattern,body =
 358                        if argsno = 0 then x,pp ~in_type:false y context
 359                        else
 360                         let args,body = aux argsno context y in
 361                         let sargs = String.concat "," args in
 362                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
 363                           body
 364                       in
 365                        pattern ^ " -> " ^ go_down ^
 366                         (if needs_obj_magic then
 367                          "Obj.magic (" ^ body ^ ")"
 368                         else
 369                          body) ^ go_nwod
 370                    ) connames_and_argsno_and_patterns)) ^
 371                  ")\n"^go_pu)))
 372     | C.Fix (no, funs) ->
 373        let names,_ =
 374         List.fold_left
 375          (fun (types,len) (n,_,ty,_) ->
 376             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 377              len+1)
 378          ) ([],0) funs
 379        in
 380          "let rec " ^
 381          List.fold_right
 382           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
 383             pp ~in_type:false bo (names@context) ^ i)
 384           funs "" ^
 385          " in " ^
 386          (match get_nth names (no + 1) with
 387              Some (Cic.Name n,_) -> n
 388            | _ -> assert false)
 389     | C.CoFix (no,funs) ->
 390        let names,_ =
 391         List.fold_left
 392          (fun (types,len) (n,ty,_) ->
 393             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 394              len+1)
 395          ) ([],0) funs
 396        in
 397          "\nCoFix " ^ " {" ^
 398          List.fold_right
 399           (fun (name,ty,bo) i -> "\n" ^ name ^
 400             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
 401             pp ~in_type:false bo (names@context) ^ i)
 402           funs "" ^
 403          "}\n"
 404 and pp_exp_named_subst exp_named_subst context =
 405  if exp_named_subst = [] then "" else
 406   "\\subst[" ^
 407    String.concat " ; " (
 408     List.map
 409      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
 410      exp_named_subst
 411    ) ^ "]"
 412 and clean_args_for_constr nparams context =
 413  let nparams = ref nparams in
 414  HExtlib.filter_map
 415   (function t ->
 416     decr nparams;
 417     match analyze_term context t with
 418        `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
 419      | `Optimize
 420      | `Term
 421      | `Type
 422      | `Proof -> None)
 423 and clean_args context =
 424  function
 425  | [] | [_] -> assert false
 426  | he::arg1::tl as l ->
 427     let head_arg1, rest =
 428        match analyze_term context arg1 with
 429       | `Optimize ->
 430          !current_go_up :: pp ~in_type:false he context ::
 431                  pp ~in_type:false arg1 context :: ["))"], tl
 432       | _ -> [], l
 433     in
 434     head_arg1 @
 435     HExtlib.filter_map
 436      (function t ->
 437        match analyze_term context t with
 438         | `Term -> Some (pp ~in_type:false t context)
 439         | `Optimize ->
 440             prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
 441         | `Type
 442         | `Proof -> None) rest
 443 and clean_args_for_ty context =
 444  HExtlib.filter_map
 445   (function t ->
 446     match analyze_term context t with
 447        `Type -> Some (pp ~in_type:true t context)
 448      | `Optimize -> None
 449      | `Proof -> None
 450      | `Term -> None)
 451 in
 452  pp ~in_type
 453 ;;
 454
 455 let ppty current_module_uri =
 456  (* nparams is the number of left arguments
 457     left arguments should either become parameters or be skipped altogether *)
 458  let rec args nparams context =
 459   function
 460      Cic.Prod (n,s,t) ->
 461       let n =
 462        match n with
 463           Cic.Anonymous -> Cic.Anonymous
 464         | Cic.Name n -> Cic.Name (String.uncapitalize n)
 465       in
 466        (match analyze_type context s with
 467          | `Optimize
 468          | `Statement
 469          | `Sort Cic.Prop ->
 470              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
 471          | `Type when nparams > 0 ->
 472              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
 473          | `Type ->
 474              let abstr,args =
 475               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
 476                abstr,pp ~in_type:true current_module_uri s context::args
 477          | `Sort _ when nparams <= 0 ->
 478              let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
 479               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
 480          | `Sort _ ->
 481              let n =
 482               match n with
 483                  Cic.Anonymous -> Cic.Anonymous
 484                | Cic.Name name -> Cic.Name ("'" ^ name) in
 485              let abstr,args =
 486               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
 487              in
 488               (match n with
 489                   Cic.Anonymous -> abstr
 490                 | Cic.Name name -> name::abstr),
 491               args)
 492    | _ -> [],[]
 493  in
 494   args
 495 ;;
 496
 497 exception DoNotExtract;;
 498
 499 let pp_abstracted_ty current_module_uri =
 500  let rec args context =
 501   function
 502      Cic.Lambda (n,s,t) ->
 503       let n =
 504        match n with
 505           Cic.Anonymous -> Cic.Anonymous
 506         | Cic.Name n -> Cic.Name (String.uncapitalize n)
 507       in
 508        (match analyze_type context s with
 509          | `Optimize
 510          | `Statement
 511          | `Type
 512          | `Sort Cic.Prop ->
 513              args ((Some (n,Cic.Decl s))::context) t
 514          | `Sort _ ->
 515              let n =
 516               match n with
 517                  Cic.Anonymous -> Cic.Anonymous
 518                | Cic.Name name -> Cic.Name ("'" ^ name) in
 519              let abstr,res =
 520               args ((Some (n,Cic.Decl s))::context) t
 521              in
 522               (match n with
 523                   Cic.Anonymous -> abstr
 524                 | Cic.Name name -> name::abstr),
 525               res)
 526    | ty ->
 527      match analyze_type context ty with
 528       | `Optimize ->
 529            prerr_endline "XXX abstracted l2 ty"; assert false
 530       | `Sort _
 531       | `Statement -> raise DoNotExtract
 532       | `Type ->
 533           (* BUG HERE: this can be a real System F type *)
 534           let head = pp ~in_type:true current_module_uri ty context in
 535           [],head
 536  in
 537   args
 538 ;;
 539
 540
 541 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 542 (* pretty-prints a single inductive definition                              *)
 543 (* (typename, inductive, arity, cons)                                       *)
 544 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
 545 =
 546  match analyze_type [] arity with
 547     `Sort Cic.Prop -> ""
 548   | `Optimize
 549   | `Statement
 550   | `Type -> assert false
 551   | `Sort _ ->
 552     if cons = [] then
 553      "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
 554     else (
 555      let abstr,scons =
 556       List.fold_right
 557        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
 558           let abstr',sargs = ppty current_module_uri nparams [] ty in
 559           let sargs = String.concat " * " sargs in
 560            abstr',
 561            String.capitalize id ^
 562             (if sargs = "" then "" else " of " ^ sargs) ^
 563             (if i = "" then "" else "\n | ") ^ i)
 564        cons ([],"")
 565       in
 566        let abstr =
 567         let s = String.concat "," abstr in
 568         if s = "" then "" else "(" ^ s ^ ") "
 569        in
 570        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
 571 ;;
 572
 573 let ppobj current_module_uri obj =
 574  let module C = Cic in
 575  let module U = UriManager in
 576   let pp ~in_type = pp ~in_type current_module_uri in
 577   match obj with
 578     C.Constant (name, Some t1, t2, params, _) ->
 579       (match analyze_type [] t2 with
 580         | `Sort Cic.Prop
 581         | `Statement -> ""
 582         | `Optimize
 583         | `Type ->
 584             (match t1 with
 585             | Cic.Lambda (Cic.Name arg, s, t) ->
 586                             (match analyze_type [] s with
 587                 | `Optimize ->
 588
 589                     "let " ^ ppid name ^ "__1 = function " ^ ppid arg
 590                     ^ " -> .< " ^
 591                     at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)]
 592                     ^ " >. ;;\n"
 593                     ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
 594                     ^ "let " ^ ppid name ^ " = function " ^ ppid arg
 595                     ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic  !"^ppid name
 596                     ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
 597                     ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
 598                     ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
 599                     ^ppid name^"__2)) >.\n;;\n"
 600                     ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
 601                     name^" Matita_freescale_opcode.HCS08)"
 602                 | _ ->
 603                    "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
 604             | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
 605         | `Sort _ ->
 606             match analyze_type [] t1 with
 607                `Sort Cic.Prop -> ""
 608              | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
 609              | _ ->
 610                (try
 611                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
 612                  let abstr =
 613                   let s = String.concat "," abstr in
 614                   if s = "" then "" else "(" ^ s ^ ") "
 615                  in
 616                   "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
 617                 with
 618                  DoNotExtract -> ""))
 619    | C.Constant (name, None, ty, params, _) ->
 620       (match analyze_type [] ty with
 621           `Sort Cic.Prop
 622         | `Optimize -> prerr_endline "XXX axiom l2"; assert false
 623         | `Statement -> ""
 624         | `Sort _ -> "type " ^ ppid name ^ "\n"
 625         | `Type -> "let " ^ ppid name ^ " = assert false\n")
 626    | C.Variable (name, bo, ty, params, _) ->
 627       "Variable " ^ name ^
 628        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
 629        ")" ^ ":\n" ^
 630        pp ~in_type:true ty [] ^ "\n" ^
 631        (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
 632    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
 633       "Current Proof of " ^ name ^
 634        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
 635        ")" ^ ":\n" ^
 636       let separate s = if s = "" then "" else s ^ " ; " in
 637        List.fold_right
 638         (fun (n, context, t) i ->
 639           let conjectures',name_context =
 640                  List.fold_right
 641                   (fun context_entry (i,name_context) ->
 642                     (match context_entry with
 643                         Some (n,C.Decl at) ->
 644                          (separate i) ^
 645                            ppname n ^ ":" ^
 646                             pp ~in_type:true ~metasenv:conjectures
 647                             at name_context ^ " ",
 648                             context_entry::name_context
 649                       | Some (n,C.Def (at,aty)) ->
 650                          (separate i) ^
 651                            ppname n ^ ":" ^
 652                             pp ~in_type:true ~metasenv:conjectures
 653                             aty name_context ^
 654                            ":= " ^ pp ~in_type:false
 655                             ~metasenv:conjectures at name_context ^ " ",
 656                             context_entry::name_context
 657                       | None ->
 658                          (separate i) ^ "_ :? _ ", context_entry::name_context)
 659             ) context ("",[])
 660           in
 661            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
 662             pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
 663         ) conjectures "" ^
 664         "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
 665           pp ~in_type:true ~metasenv:conjectures ty []
 666    | C.InductiveDefinition (l, params, nparams, _) ->
 667       List.fold_right
 668        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
 669 ;;
 670
 671 let ppobj current_module_uri obj =
 672  let res = ppobj current_module_uri obj in
 673   if res = "" then "" else res ^ ";;\n\n"
 674 ;;