matita/components/ng_kernel/nCicExtraction.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 let fix_sorts t = t;;
  29 let apply_subst subst t = assert (subst=[]); t;;
  30
  31 type typformerreference = NReference.reference
  32 type reference = NReference.reference
  33
  34 type kind =
  35    Type
  36  | KArrow of kind * kind
  37  | KSkip of kind (* dropped abstraction *)
  38
  39 type typ =
  40    Var of int
  41  | Top
  42  | TConst of typformerreference
  43  | Arrow of typ * typ
  44  | Skip of typ
  45  | Forall of string * kind * typ
  46  | TAppl of typ list
  47
  48 type term =
  49    Rel of int
  50  | Const of reference
  51  | Lambda of string * (* typ **) term
  52  | Appl of term list
  53  | LetIn of string * (* typ **) term * term
  54  | Match of reference * term * term list
  55  | TLambda of (* string **) term
  56  | Inst of (*typ_former **) term
  57
  58 let unitty =
  59  NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
  60
  61 (* None = dropped abstraction *)
  62 type typ_context = (string * kind) option list
  63 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
  64
  65 type typ_former_decl = typ_context * kind
  66 type typ_former_def = typ_former_decl * typ
  67
  68 type term_former_decl = term_context * typ
  69 type term_former_def = term_former_decl * term
  70
  71 type obj_kind =
  72    TypeDeclaration of typ_former_decl
  73  | TypeDefinition of typ_former_def
  74  | TermDeclaration of term_former_decl
  75  | TermDefinition of term_former_def
  76  | LetRec of (string * typ * term) list
  77  (* inductive and records missing *)
  78
  79 type obj = NUri.uri * obj_kind
  80
  81 exception NotInFOmega
  82
  83 let rec classify_not_term status no_dep_prods context t =
  84  match NCicReduction.whd status ~subst:[] context t with
  85   | NCic.Sort s ->
  86      (match s with
  87          NCic.Prop
  88        | NCic.Type [`CProp,_] -> `PropKind
  89        | NCic.Type [`Type,_] ->
  90           if no_dep_prods then `Kind
  91           else
  92            raise NotInFOmega (* ?? *)
  93        | NCic.Type _ -> assert false)
  94   | NCic.Prod (b,s,t) ->
  95      (*CSC: using invariant on "_" *)
  96      classify_not_term status (no_dep_prods && b.[0] = '_')
  97       ((b,NCic.Decl s)::context) t
  98   | NCic.Implicit _
  99   | NCic.LetIn _
 100   | NCic.Lambda _
 101   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 102   | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
 103   | NCic.Match _
 104   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 105      (* be aware: we can be the head of an application *)
 106      assert false (* TODO *)
 107   | NCic.Meta _ -> assert false (* TODO *)
 108   | NCic.Appl (he::_) -> classify_not_term status no_dep_prods context he
 109   | NCic.Rel _ -> `KindOrType
 110   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 111      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 112       (match classify_not_term status true [] ty with
 113         | `Proposition
 114         | `Type -> assert false (* IMPOSSIBLE *)
 115         | `Kind
 116         | `KindOrType -> `KindOrType
 117         | `PropKind -> `Proposition)
 118   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 119      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 120      let _,_,arity,_ = List.nth ityl i in
 121       (match classify_not_term status true [] arity with
 122         | `Proposition
 123         | `Type
 124         | `KindOrType -> assert false (* IMPOSSIBLE *)
 125         | `Kind -> `Type
 126         | `PropKind -> `Proposition)
 127   | NCic.Const (NReference.Ref (_,NReference.Con _))
 128   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 129      assert false (* IMPOSSIBLE *)
 130 ;;
 131
 132 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 133
 134 let classify status ~metasenv context t =
 135  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 136   | NCic.Sort _ ->
 137      (classify_not_term status true context t : not_term :> [> not_term])
 138   | ty ->
 139      let ty = fix_sorts ty in
 140       `Term
 141         (match classify_not_term status true context ty with
 142           | `Proposition -> `Proof
 143           | `Type -> `Term
 144           | `KindOrType -> `TypeFormerOrTerm
 145           | `Kind -> `TypeFormer
 146           | `PropKind -> `PropFormer)
 147 ;;
 148
 149
 150 let rec kind_of status ~metasenv context k =
 151  match NCicReduction.whd status ~subst:[] context k with
 152   | NCic.Sort _ -> Type
 153   | NCic.Prod (b,s,t) ->
 154      (* CSC: non-invariant assumed here about "_" *)
 155      (match classify status ~metasenv context s with
 156        | `Kind
 157        | `KindOrType -> (* KindOrType OK?? *)
 158            KArrow (kind_of status ~metasenv context s,
 159             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 160        | `Type
 161        | `Proposition
 162        | `PropKind ->
 163            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 164        | `Term _ -> assert false (* IMPOSSIBLE *))
 165   | NCic.Implicit _
 166   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 167   | NCic.Lambda _
 168   | NCic.Rel _
 169   | NCic.Const _ -> assert false (* NOT A KIND *)
 170   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 171                                    otherwise NOT A KIND *)
 172   | NCic.Meta _
 173   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 174 ;;
 175
 176 let rec skip_args status ~metasenv context =
 177  function
 178   | _,[] -> []
 179   | [],_ -> assert false (* IMPOSSIBLE *)
 180   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 181   | _::tl1,arg::tl2 ->
 182      match classify status ~metasenv context arg with
 183       | `KindOrType
 184       | `Type
 185       | `Term `TypeFormer -> arg::skip_args status ~metasenv context (tl1,tl2)
 186       | `Kind
 187       | `Proposition
 188       | `PropKind -> unitty::skip_args status ~metasenv context (tl1,tl2)
 189       | `Term _ -> assert false (* IMPOSSIBLE *)
 190 ;;
 191
 192 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 193
 194 type db = typ_context ReferenceMap.t
 195
 196 class type g_status =
 197  object
 198   method extraction_db: db
 199  end
 200
 201 class virtual status =
 202  object
 203   inherit NCic.status
 204   val extraction_db = ReferenceMap.empty
 205   method extraction_db = extraction_db
 206   method set_extraction_db v = {< extraction_db = v >}
 207   method set_extraction_status
 208    : 'status. #g_status as 'status -> 'self
 209    = fun o -> {< extraction_db = o#extraction_db >}
 210  end
 211
 212 let rec split_kind_prods context =
 213  function
 214   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 215   | KSkip ta -> split_kind_prods (None::context) ta
 216   | Type -> context,Type
 217 ;;
 218
 219 let rec split_typ_prods context =
 220  function
 221   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 222   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 223   | Skip ta -> split_typ_prods (None::context) ta
 224   | _ as t -> context,t
 225 ;;
 226
 227 let rec glue_ctx_typ ctx typ =
 228  match ctx with
 229   | [] -> typ
 230   | Some (_,`OfType so)::ctx -> Arrow (so,glue_ctx_typ ctx typ)
 231   | Some (name,`OfKind so)::ctx -> Forall (name,so,glue_ctx_typ ctx typ)
 232   | None::ctx -> Skip (glue_ctx_typ ctx typ)
 233 ;;
 234
 235 let rec split_typ_lambdas status n ~metasenv context typ =
 236  if n = 0 then context,typ
 237  else
 238   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 239    | NCic.Lambda (name,s,t) ->
 240       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 241    | t ->
 242       (* eta-expansion required *)
 243       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 244       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 245        | NCic.Prod (name,typ,_) ->
 246           split_typ_lambdas status (n-1) ~metasenv
 247            ((name,NCic.Decl typ)::context)
 248            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 249        | _ -> assert false (* IMPOSSIBLE *)
 250 ;;
 251
 252
 253 let context_of_typformer status ~metasenv context =
 254  function
 255     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 256   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 257   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 258   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 259      (try ReferenceMap.find ref status#extraction_db
 260       with
 261        Not_found -> assert false (* IMPOSSIBLE *))
 262   | NCic.Match _ -> assert false (* TODO ???? *)
 263   | NCic.Rel n ->
 264      let typ =
 265       match List.nth context (n-1) with
 266          _,NCic.Decl typ -> typ
 267        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 268      let typ_ctx = snd (HExtlib.split_nth n context) in
 269      let typ = kind_of status ~metasenv typ_ctx typ in
 270       fst (split_kind_prods [] typ)
 271   | NCic.Meta _ -> assert false (* TODO *)
 272   | NCic.Const (NReference.Ref (_,NReference.Con _))
 273   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 274   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 275   | NCic.Appl _ | NCic.Prod _ ->
 276      assert false (* IMPOSSIBLE *)
 277
 278 let rec typ_of status ~metasenv context k =
 279  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 280   | NCic.Prod (b,s,t) ->
 281      (* CSC: non-invariant assumed here about "_" *)
 282      (match classify status ~metasenv context s with
 283        | `Kind ->
 284            Forall (b, kind_of status ~metasenv context s,
 285             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 286        | `Type
 287        | `KindOrType -> (* ??? *)
 288            Arrow (typ_of status ~metasenv context s,
 289             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 290        | `PropKind
 291        | `Proposition ->
 292            Skip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 293        | `Term _ -> assert false (* IMPOSSIBLE *))
 294   | NCic.Sort _
 295   | NCic.Implicit _
 296   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 297   | NCic.Lambda _ -> assert false (* NOT A TYPE *)
 298   | NCic.Rel n -> Var n
 299   | NCic.Const ref -> TConst ref
 300   | NCic.Appl (he::args) ->
 301      let he_context = context_of_typformer status ~metasenv context he in
 302      TAppl (typ_of status ~metasenv context he ::
 303       List.map (typ_of status ~metasenv context)
 304        (skip_args status ~metasenv context (List.rev he_context,args)))
 305   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 306                                    otherwise NOT A TYPE *)
 307   | NCic.Meta _
 308   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 309 ;;
 310
 311 let rec term_of status ~metasenv context =
 312  function
 313   | NCic.Implicit _
 314   | NCic.Sort _
 315   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 316   | NCic.Lambda (b,ty,bo) ->
 317      (* CSC: non-invariant assumed here about "_" *)
 318      (match classify status ~metasenv context ty with
 319        | `Kind ->
 320            TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 321        | `KindOrType (* ??? *)
 322        | `Type ->
 323            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 324        | `PropKind
 325        | `Proposition ->
 326            (* CSC: LAZY ??? *)
 327            term_of status ~metasenv ((b,NCic.Decl ty)::context) bo
 328        | `Term _ -> assert false (* IMPOSSIBLE *))
 329   | NCic.LetIn (b,ty,t,bo) ->
 330      (match classify status ~metasenv context t with
 331        | `Term `Term ->
 332           LetIn (b,term_of status ~metasenv context t,
 333            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 334        | `Kind
 335        | `Type
 336        | `KindOrType
 337        | `PropKind
 338        | `Proposition
 339        | `Term `PropFormer
 340        | `Term `TypeFormer
 341        | `Term `TypeFormerOrTerm
 342        | `Term `Proof -> assert false (* NOT IN PROGRAMMING LANGUAGES? EXPAND IT ??? *))
 343   | NCic.Rel n -> Rel n
 344   | NCic.Const ref -> Const ref
 345   | NCic.Appl (he::args) ->
 346      assert false (* TODO
 347      let he_context = context_of_typformer status ~metasenv context he in
 348      TAppl (typ_of status ~metasenv context he ::
 349       List.map (typ_of status ~metasenv context)
 350        (skip_args status ~metasenv context (List.rev he_context,args)))*)
 351   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 352                                    otherwise NOT A TYPE *)
 353   | NCic.Meta _ -> assert false (* TODO *)
 354   | NCic.Match (ref,_,t,pl) ->
 355      Match (ref,term_of status ~metasenv context t,
 356       List.map (term_of status ~metasenv context) pl)
 357 ;;
 358
 359 let obj_of status (uri,height,metasenv,subst,obj_kind) =
 360  let obj_kind = apply_subst subst obj_kind in
 361  try
 362   match obj_kind with
 363    | NCic.Constant (_,_,None,ty,_) ->
 364       (match classify status ~metasenv [] ty with
 365         | `Kind ->
 366             let ty = kind_of status ~metasenv [] ty in
 367             let ctx,_ as res = split_kind_prods [] ty in
 368             let ref = NReference.reference_of_spec uri NReference.Decl in
 369              status#set_extraction_db
 370               (ReferenceMap.add ref ctx status#extraction_db),
 371              Some (uri, TypeDeclaration res)
 372         | `KindOrType -> assert false (* TODO ??? *)
 373         | `PropKind
 374         | `Proposition -> status, None
 375         | `Type ->
 376             let ty = typ_of status ~metasenv [] ty in
 377              status,
 378              Some (uri, TermDeclaration (split_typ_prods [] ty))
 379         | `Term _ -> assert false (* IMPOSSIBLE *))
 380    | NCic.Constant (_,_,Some bo,ty,_) ->
 381       (match classify status ~metasenv [] ty with
 382         | `Kind ->
 383             let ty = kind_of status ~metasenv [] ty in
 384             let ctx0,res = split_kind_prods [] ty in
 385             let ctx,bo =
 386              split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 387             (match classify status ~metasenv ctx bo with
 388               | `Type
 389               | `KindOrType -> (* ?? no kind formers in System F_omega *)
 390                   let nicectx =
 391                    List.map2
 392                     (fun p1 n ->
 393                       HExtlib.map_option (fun (_,k) ->
 394                        (*CSC: BUG here, clashes*)
 395                        String.uncapitalize (fst n),k) p1)
 396                     ctx0 ctx
 397                   in
 398                   let ref =
 399                    NReference.reference_of_spec uri (NReference.Def height) in
 400                    status#set_extraction_db
 401                     (ReferenceMap.add ref ctx0 status#extraction_db),
 402                    Some (uri,TypeDefinition((nicectx,res),typ_of status ~metasenv ctx bo))
 403               | `Kind -> status, None
 404               | `PropKind
 405               | `Proposition -> status, None
 406               | `Term _ -> assert false (* IMPOSSIBLE *))
 407         | `PropKind
 408         | `Proposition -> status, None
 409         | `KindOrType (* ??? *)
 410         | `Type ->
 411            (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 412            let ty = typ_of status ~metasenv [] ty in
 413             status,
 414             Some (uri, TermDefinition (split_typ_prods [] ty,
 415              term_of status ~metasenv [](* BAD! *) bo))
 416         | `Term _ -> assert false (* IMPOSSIBLE *))
 417  with
 418   NotInFOmega ->
 419    prerr_endline "NOT IN F_omega";
 420    status, None
 421
 422 (************************ HASKELL *************************)
 423
 424 (*CSC: code to be changed soon when we implement constructors and
 425   we fix the code for term application *)
 426 let classify_reference status ref =
 427  if ReferenceMap.mem ref status#extraction_db then
 428   `TypeName
 429  else
 430   `FunctionName
 431
 432 let capitalize classification name =
 433   match classification with
 434      `Constructor
 435    | `TypeName -> String.capitalize name
 436    | `FunctionName -> String.uncapitalize name
 437
 438 let pp_ref status ref =
 439  capitalize (classify_reference status ref)
 440   (NCicPp.r2s status false ref)
 441
 442 let name_of_uri classification uri =
 443  capitalize classification (NUri.name_of_uri uri)
 444
 445 (* cons avoid duplicates *)
 446 let rec (@::) name l =
 447  if name <> "" (* propositional things *) && name.[0] = '_' then
 448   let name = String.sub name 1 (String.length name - 1) in
 449   let name = if name = "" then "a" else name in
 450    name @:: l
 451  else if List.mem name l then (name ^ "'") @:: l
 452  else name::l
 453 ;;
 454
 455 let rec pp_kind =
 456  function
 457    Type -> "*"
 458  | KArrow (k1,k2) -> "(" ^ pp_kind k1 ^ ") -> " ^ pp_kind k2
 459  | KSkip k -> pp_kind k
 460
 461 let rec pp_typ status ctx =
 462  function
 463    Var n -> List.nth ctx (n-1)
 464  | Top -> assert false (* ??? *)
 465  | TConst ref -> pp_ref status ref
 466  | Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2
 467  | Skip t -> pp_typ status ("_"::ctx) t
 468  | Forall (name,_,t) ->
 469     (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 470     let name = String.uncapitalize name in
 471     "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")"
 472  | TAppl tl -> "(" ^ String.concat " " (List.map (pp_typ status ctx) tl) ^ ")"
 473
 474 let rec pp_term status ctx =
 475  function
 476    Rel n -> List.nth ctx (n-1)
 477  | Const ref -> pp_ref status ref
 478  | Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")"
 479  | Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")"
 480  | LetIn (name,s,t) ->
 481     "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
 482     ")"
 483  | Match _ -> assert false (* TODO of reference * term * term list *)
 484  | TLambda t -> pp_term status ctx t
 485  | Inst t -> pp_term status ctx t
 486
 487 (*
 488 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 489
 490 type term_former_def = term_context * term * typ
 491 type term_former_decl = term_context * typ
 492 *)
 493
 494 let pp_obj status (uri,obj_kind) =
 495  let pp_ctx ctx =
 496   String.concat " " (List.rev
 497    (List.fold_right (fun (x,_) l -> x@::l)
 498      (HExtlib.filter_map (fun x -> x) ctx) [])) in
 499  let namectx_of_ctx ctx =
 500   List.fold_right (@::)
 501    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 502  match obj_kind with
 503    TypeDeclaration (ctx,_) ->
 504     (* data?? unsure semantics: inductive type without constructor, but
 505        not matchable apparently *)
 506     "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx
 507  | TypeDefinition ((ctx,_),ty) ->
 508     let namectx = namectx_of_ctx ctx in
 509     "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
 510        pp_typ status namectx ty
 511  | TermDeclaration (ctx,ty) ->
 512     (* Implemented with undefined, the best we can do *)
 513     let name = name_of_uri `FunctionName uri in
 514     name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 515     name ^ " = undefined"
 516  | TermDefinition ((ctx,ty),bo) ->
 517     let name = name_of_uri `FunctionName uri in
 518     let namectx = namectx_of_ctx ctx in
 519     name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 520     name ^ " = " ^ pp_term status namectx bo
 521  | LetRec _ -> assert false (* TODO
 522  (* inductive and records missing *)*)
 523
 524 let haskell_of_obj status obj =
 525  let status, obj = obj_of status obj in
 526   status,HExtlib.map_option (pp_obj status) obj
 527
 528 (*
 529 let rec typ_of context =
 530  function
 531 (*
 532     C.Rel n ->
 533        begin
 534         try
 535          (match get_nth context n with
 536              Some (C.Name s,_) -> ppid s
 537            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 538            | None -> "_hidden_" ^ string_of_int n
 539          )
 540         with
 541          NotEnoughElements -> string_of_int (List.length context - n)
 542        end
 543     | C.Meta (n,l1) ->
 544        (match metasenv with
 545            None ->
 546             "?" ^ (string_of_int n) ^ "[" ^
 547              String.concat " ; "
 548               (List.rev_map
 549                 (function
 550                     None -> "_"
 551                   | Some t -> pp ~in_type:false t context) l1) ^
 552              "]"
 553          | Some metasenv ->
 554             try
 555              let _,context,_ = CicUtil.lookup_meta n metasenv in
 556               "?" ^ (string_of_int n) ^ "[" ^
 557                String.concat " ; "
 558                 (List.rev
 559                   (List.map2
 560                     (fun x y ->
 561                       match x,y with
 562                          _, None
 563                        | None, _ -> "_"
 564                        | Some _, Some t -> pp ~in_type:false t context
 565                     ) context l1)) ^
 566                "]"
 567             with
 568               CicUtil.Meta_not_found _
 569             | Invalid_argument _ ->
 570               "???" ^ (string_of_int n) ^ "[" ^
 571                String.concat " ; "
 572                 (List.rev_map (function None -> "_" | Some t ->
 573                   pp ~in_type:false t context) l1) ^
 574                "]"
 575        )
 576     | C.Sort s ->
 577        (match s with
 578            C.Prop  -> "Prop"
 579          | C.Set   -> "Set"
 580          | C.Type _ -> "Type"
 581          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 582          | C.CProp _ -> "CProp"
 583        )
 584     | C.Implicit (Some `Hole) -> "%"
 585     | C.Implicit _ -> "?"
 586     | C.Prod (b,s,t) ->
 587        (match b, is_term s with
 588            _, true -> typ_of (None::context) t
 589          | "_",_ -> Arrow (typ_of context s) (typ_of (Some b::context) t)
 590          | _,_ -> Forall (b,typ_of (Some b::context) t)
 591     | C.Lambda (b,s,t) ->
 592        (match analyze_type context s with
 593            `Sort _
 594          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 595          | `Optimize -> prerr_endline "XXX lambda";assert false
 596          | `Type ->
 597             "(function " ^ ppname b ^ " -> " ^
 598              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 599     | C.LetIn (b,s,ty,t) ->
 600        (match analyze_term context s with
 601          | `Type
 602          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 603          | `Optimize
 604          | `Term ->
 605             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 606             " = " ^ pp ~in_type:false s context ^ " in " ^
 607              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 608     | C.Appl (he::tl) when in_type ->
 609        let hes = pp ~in_type he context in
 610        let stl = String.concat "," (clean_args_for_ty context tl) in
 611         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 612     | C.Appl (C.MutInd _ as he::tl) ->
 613        let hes = pp ~in_type he context in
 614        let stl = String.concat "," (clean_args_for_ty context tl) in
 615         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 616     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 617        let nparams =
 618         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 619            C.InductiveDefinition (_,_,nparams,_) -> nparams
 620          | _ -> assert false in
 621        let hes = pp ~in_type he context in
 622        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
 623         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
 624     | C.Appl li ->
 625        "(" ^ String.concat " " (clean_args context li) ^ ")"
 626     | C.Const (uri,exp_named_subst) ->
 627        qualified_name_of_uri status current_module_uri uri ^
 628         pp_exp_named_subst exp_named_subst context
 629     | C.MutInd (uri,n,exp_named_subst) ->
 630        (try
 631          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 632             C.InductiveDefinition (dl,_,_,_) ->
 633              let (name,_,_,_) = get_nth dl (n+1) in
 634               qualified_name_of_uri status current_module_uri
 635                (UriManager.uri_of_string
 636                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
 637               pp_exp_named_subst exp_named_subst context
 638           | _ -> raise CicExportationInternalError
 639         with
 640            Sys.Break as exn -> raise exn
 641          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
 642        )
 643     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
 644        (try
 645          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 646             C.InductiveDefinition (dl,_,_,_) ->
 647              let _,_,_,cons = get_nth dl (n1+1) in
 648               let id,_ = get_nth cons n2 in
 649                qualified_name_of_uri status current_module_uri ~capitalize:true
 650                 (UriManager.uri_of_string
 651                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
 652                pp_exp_named_subst exp_named_subst context
 653           | _ -> raise CicExportationInternalError
 654         with
 655            Sys.Break as exn -> raise exn
 656          | _ ->
 657           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
 658            string_of_int n2
 659        )
 660     | C.MutCase (uri,n1,ty,te,patterns) ->
 661        if in_type then
 662         "unit (* TOO POLYMORPHIC TYPE *)"
 663        else (
 664        let rec needs_obj_magic ty =
 665         match CicReduction.whd context ty with
 666          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
 667          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
 668          | _ -> false (* it can be a Rel, e.g. in *_rec *)
 669        in
 670        let needs_obj_magic = needs_obj_magic ty in
 671        (match analyze_term context te with
 672            `Type -> assert false
 673          | `Proof ->
 674              (match patterns with
 675                  [] -> "assert false"   (* empty type elimination *)
 676                | [he] ->
 677                   pp ~in_type:false he context  (* singleton elimination *)
 678                | _ -> assert false)
 679          | `Optimize
 680          | `Term ->
 681             if patterns = [] then "assert false"
 682             else
 683              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
 684                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 685                    C.InductiveDefinition (dl,_,paramsno,_) ->
 686                     let (_,_,_,cons) = get_nth dl (n1+1) in
 687                     let rc =
 688                      List.map
 689                       (fun (id,ty) ->
 690                         (* this is just an approximation since we do not have
 691                            reduction yet! *)
 692                         let rec count_prods toskip =
 693                          function
 694                             C.Prod (_,_,bo) when toskip > 0 ->
 695                              count_prods (toskip - 1) bo
 696                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
 697                           | _ -> 0
 698                         in
 699                          qualified_name_of_uri status current_module_uri
 700                           ~capitalize:true
 701                           (UriManager.uri_of_string
 702                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
 703                          count_prods paramsno ty
 704                       ) cons
 705                     in
 706                     if not (is_mcu_type uri) then rc, "","","",""
 707                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
 708                  | _ -> raise CicExportationInternalError
 709                )
 710               in
 711                let connames_and_argsno_and_patterns =
 712                 let rec combine =
 713                    function
 714                       [],[] -> []
 715                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
 716                     | _,_ -> assert false
 717                 in
 718                  combine (connames_and_argsno,patterns)
 719                in
 720                 go_up ^
 721                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
 722                  (String.concat "\n | "
 723                   (List.map
 724                    (fun (x,argsno,y) ->
 725                      let rec aux argsno context =
 726                       function
 727                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
 728                           let name =
 729                            match name with
 730                               Cic.Anonymous -> Cic.Anonymous
 731                             | Cic.Name n -> Cic.Name (ppid n) in
 732                           let args,res =
 733                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
 734                             bo
 735                           in
 736                            (match analyze_type context ty with
 737                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
 738                              | `Statement
 739                              | `Sort _ -> args,res
 740                              | `Type ->
 741                                  (match name with
 742                                      C.Anonymous -> "_"
 743                                    | C.Name s -> s)::args,res)
 744                        | t when argsno = 0 -> [],pp ~in_type:false t context
 745                        | t ->
 746                           ["{" ^ string_of_int argsno ^ " args missing}"],
 747                            pp ~in_type:false t context
 748                      in
 749                       let pattern,body =
 750                        if argsno = 0 then x,pp ~in_type:false y context
 751                        else
 752                         let args,body = aux argsno context y in
 753                         let sargs = String.concat "," args in
 754                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
 755                           body
 756                       in
 757                        pattern ^ " -> " ^ go_down ^
 758                         (if needs_obj_magic then
 759                          "Obj.magic (" ^ body ^ ")"
 760                         else
 761                          body) ^ go_nwod
 762                    ) connames_and_argsno_and_patterns)) ^
 763                  ")\n"^go_pu)))
 764     | C.Fix (no, funs) ->
 765        let names,_ =
 766         List.fold_left
 767          (fun (types,len) (n,_,ty,_) ->
 768             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 769              len+1)
 770          ) ([],0) funs
 771        in
 772          "let rec " ^
 773          List.fold_right
 774           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
 775             pp ~in_type:false bo (names@context) ^ i)
 776           funs "" ^
 777          " in " ^
 778          (match get_nth names (no + 1) with
 779              Some (Cic.Name n,_) -> n
 780            | _ -> assert false)
 781     | C.CoFix (no,funs) ->
 782        let names,_ =
 783         List.fold_left
 784          (fun (types,len) (n,ty,_) ->
 785             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 786              len+1)
 787          ) ([],0) funs
 788        in
 789          "\nCoFix " ^ " {" ^
 790          List.fold_right
 791           (fun (name,ty,bo) i -> "\n" ^ name ^
 792             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
 793             pp ~in_type:false bo (names@context) ^ i)
 794           funs "" ^
 795          "}\n"
 796 *)
 797
 798 (*
 799 exception CicExportationInternalError;;
 800 exception NotEnoughElements;;
 801
 802 (* *)
 803
 804 let is_mcu_type u =
 805   UriManager.eq (UriManager.uri_of_string
 806   "cic:/matita/freescale/opcode/mcu_type.ind") u
 807 ;;
 808
 809 (* Utility functions *)
 810
 811 let analyze_term context t =
 812  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
 813   | Cic.Sort _ -> `Type
 814   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 815   | ty ->
 816      match
 817       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
 818      with
 819      | Cic.Sort Cic.Prop -> `Proof
 820      | _ -> `Term
 821 ;;
 822
 823 let analyze_type context t =
 824  let rec aux =
 825   function
 826      Cic.Sort s -> `Sort s
 827    | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 828    | Cic.Prod (_,_,t) -> aux t
 829    | _ -> `SomethingElse
 830  in
 831  match aux t with
 832     `Sort _ | `Optimize as res -> res
 833   | `SomethingElse ->
 834       match
 835        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
 836       with
 837           Cic.Sort Cic.Prop -> `Statement
 838        | _ -> `Type
 839 ;;
 840
 841 let ppid =
 842  let reserved =
 843   [ "to";
 844     "mod";
 845     "val";
 846     "in";
 847     "function"
 848   ]
 849  in
 850   function n ->
 851    let n = String.uncapitalize n in
 852     if List.mem n reserved then n ^ "_" else n
 853 ;;
 854
 855 let ppname =
 856  function
 857     Cic.Name s     -> ppid s
 858   | Cic.Anonymous  -> "_"
 859 ;;
 860
 861 (* get_nth l n   returns the nth element of the list l if it exists or *)
 862 (* raises NotEnoughElements if l has less than n elements             *)
 863 let rec get_nth l n =
 864  match (n,l) with
 865     (1, he::_) -> he
 866   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
 867   | (_,_) -> raise NotEnoughElements
 868 ;;
 869
 870 let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
 871  let name =
 872   if capitalize then
 873    String.capitalize (UriManager.name_of_uri status uri)
 874   else
 875    ppid (UriManager.name_of_uri status uri) in
 876   let filename =
 877    let suri = UriManager.buri_of_uri uri in
 878    let s = String.sub suri 5 (String.length suri - 5) in
 879    let s = Pcre.replace ~pat:"/" ~templ:"_" s in
 880     String.uncapitalize s in
 881   if current_module_uri = UriManager.buri_of_uri uri then
 882    name
 883   else
 884    String.capitalize filename ^ "." ^ name
 885 ;;
 886
 887 let current_go_up = ref "(.!(";;
 888 let at_level2 f x =
 889   try
 890     current_go_up := "(.~(";
 891     let rc = f x in
 892     current_go_up := "(.!(";
 893     rc
 894   with exn ->
 895     current_go_up := "(.!(";
 896     raise exn
 897 ;;
 898
 899 let pp current_module_uri ?metasenv ~in_type =
 900 let rec pp ~in_type t context =
 901  let module C = Cic in
 902    match t with
 903       C.Rel n ->
 904        begin
 905         try
 906          (match get_nth context n with
 907              Some (C.Name s,_) -> ppid s
 908            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 909            | None -> "_hidden_" ^ string_of_int n
 910          )
 911         with
 912          NotEnoughElements -> string_of_int (List.length context - n)
 913        end
 914     | C.Var (uri,exp_named_subst) ->
 915         qualified_name_of_uri status current_module_uri uri ^
 916          pp_exp_named_subst exp_named_subst context
 917     | C.Meta (n,l1) ->
 918        (match metasenv with
 919            None ->
 920             "?" ^ (string_of_int n) ^ "[" ^
 921              String.concat " ; "
 922               (List.rev_map
 923                 (function
 924                     None -> "_"
 925                   | Some t -> pp ~in_type:false t context) l1) ^
 926              "]"
 927          | Some metasenv ->
 928             try
 929              let _,context,_ = CicUtil.lookup_meta n metasenv in
 930               "?" ^ (string_of_int n) ^ "[" ^
 931                String.concat " ; "
 932                 (List.rev
 933                   (List.map2
 934                     (fun x y ->
 935                       match x,y with
 936                          _, None
 937                        | None, _ -> "_"
 938                        | Some _, Some t -> pp ~in_type:false t context
 939                     ) context l1)) ^
 940                "]"
 941             with
 942               CicUtil.Meta_not_found _
 943             | Invalid_argument _ ->
 944               "???" ^ (string_of_int n) ^ "[" ^
 945                String.concat " ; "
 946                 (List.rev_map (function None -> "_" | Some t ->
 947                   pp ~in_type:false t context) l1) ^
 948                "]"
 949        )
 950     | C.Sort s ->
 951        (match s with
 952            C.Prop  -> "Prop"
 953          | C.Set   -> "Set"
 954          | C.Type _ -> "Type"
 955          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 956          | C.CProp _ -> "CProp"
 957        )
 958     | C.Implicit (Some `Hole) -> "%"
 959     | C.Implicit _ -> "?"
 960     | C.Prod (b,s,t) ->
 961        (match b with
 962           C.Name n ->
 963            let n = "'" ^ String.uncapitalize n in
 964             "(" ^ pp ~in_type:true s context ^ " -> " ^
 965             pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
 966         | C.Anonymous ->
 967            "(" ^ pp ~in_type:true s context ^ " -> " ^
 968            pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
 969     | C.Cast (v,t) -> pp ~in_type v context
 970     | C.Lambda (b,s,t) ->
 971        (match analyze_type context s with
 972            `Sort _
 973          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 974          | `Optimize -> prerr_endline "XXX lambda";assert false
 975          | `Type ->
 976             "(function " ^ ppname b ^ " -> " ^
 977              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 978     | C.LetIn (b,s,ty,t) ->
 979        (match analyze_term context s with
 980          | `Type
 981          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 982          | `Optimize
 983          | `Term ->
 984             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 985             " = " ^ pp ~in_type:false s context ^ " in " ^
 986              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 987     | C.Appl (he::tl) when in_type ->
 988        let hes = pp ~in_type he context in
 989        let stl = String.concat "," (clean_args_for_ty context tl) in
 990         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 991     | C.Appl (C.MutInd _ as he::tl) ->
 992        let hes = pp ~in_type he context in
 993        let stl = String.concat "," (clean_args_for_ty context tl) in
 994         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 995     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 996        let nparams =
 997         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 998            C.InductiveDefinition (_,_,nparams,_) -> nparams
 999          | _ -> assert false in
1000        let hes = pp ~in_type he context in
1001        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
1002         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
1003     | C.Appl li ->
1004        "(" ^ String.concat " " (clean_args context li) ^ ")"
1005     | C.Const (uri,exp_named_subst) ->
1006        qualified_name_of_uri status current_module_uri uri ^
1007         pp_exp_named_subst exp_named_subst context
1008     | C.MutInd (uri,n,exp_named_subst) ->
1009        (try
1010          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1011             C.InductiveDefinition (dl,_,_,_) ->
1012              let (name,_,_,_) = get_nth dl (n+1) in
1013               qualified_name_of_uri status current_module_uri
1014                (UriManager.uri_of_string
1015                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
1016               pp_exp_named_subst exp_named_subst context
1017           | _ -> raise CicExportationInternalError
1018         with
1019            Sys.Break as exn -> raise exn
1020          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
1021        )
1022     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
1023        (try
1024          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1025             C.InductiveDefinition (dl,_,_,_) ->
1026              let _,_,_,cons = get_nth dl (n1+1) in
1027               let id,_ = get_nth cons n2 in
1028                qualified_name_of_uri status current_module_uri ~capitalize:true
1029                 (UriManager.uri_of_string
1030                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
1031                pp_exp_named_subst exp_named_subst context
1032           | _ -> raise CicExportationInternalError
1033         with
1034            Sys.Break as exn -> raise exn
1035          | _ ->
1036           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
1037            string_of_int n2
1038        )
1039     | C.MutCase (uri,n1,ty,te,patterns) ->
1040        if in_type then
1041         "unit (* TOO POLYMORPHIC TYPE *)"
1042        else (
1043        let rec needs_obj_magic ty =
1044         match CicReduction.whd context ty with
1045          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
1046          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
1047          | _ -> false (* it can be a Rel, e.g. in *_rec *)
1048        in
1049        let needs_obj_magic = needs_obj_magic ty in
1050        (match analyze_term context te with
1051            `Type -> assert false
1052          | `Proof ->
1053              (match patterns with
1054                  [] -> "assert false"   (* empty type elimination *)
1055                | [he] ->
1056                   pp ~in_type:false he context  (* singleton elimination *)
1057                | _ -> assert false)
1058          | `Optimize
1059          | `Term ->
1060             if patterns = [] then "assert false"
1061             else
1062              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
1063                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1064                    C.InductiveDefinition (dl,_,paramsno,_) ->
1065                     let (_,_,_,cons) = get_nth dl (n1+1) in
1066                     let rc =
1067                      List.map
1068                       (fun (id,ty) ->
1069                         (* this is just an approximation since we do not have
1070                            reduction yet! *)
1071                         let rec count_prods toskip =
1072                          function
1073                             C.Prod (_,_,bo) when toskip > 0 ->
1074                              count_prods (toskip - 1) bo
1075                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
1076                           | _ -> 0
1077                         in
1078                          qualified_name_of_uri status current_module_uri
1079                           ~capitalize:true
1080                           (UriManager.uri_of_string
1081                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
1082                          count_prods paramsno ty
1083                       ) cons
1084                     in
1085                     if not (is_mcu_type uri) then rc, "","","",""
1086                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
1087                  | _ -> raise CicExportationInternalError
1088                )
1089               in
1090                let connames_and_argsno_and_patterns =
1091                 let rec combine =
1092                    function
1093                       [],[] -> []
1094                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
1095                     | _,_ -> assert false
1096                 in
1097                  combine (connames_and_argsno,patterns)
1098                in
1099                 go_up ^
1100                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
1101                  (String.concat "\n | "
1102                   (List.map
1103                    (fun (x,argsno,y) ->
1104                      let rec aux argsno context =
1105                       function
1106                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
1107                           let name =
1108                            match name with
1109                               Cic.Anonymous -> Cic.Anonymous
1110                             | Cic.Name n -> Cic.Name (ppid n) in
1111                           let args,res =
1112                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
1113                             bo
1114                           in
1115                            (match analyze_type context ty with
1116                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
1117                              | `Statement
1118                              | `Sort _ -> args,res
1119                              | `Type ->
1120                                  (match name with
1121                                      C.Anonymous -> "_"
1122                                    | C.Name s -> s)::args,res)
1123                        | t when argsno = 0 -> [],pp ~in_type:false t context
1124                        | t ->
1125                           ["{" ^ string_of_int argsno ^ " args missing}"],
1126                            pp ~in_type:false t context
1127                      in
1128                       let pattern,body =
1129                        if argsno = 0 then x,pp ~in_type:false y context
1130                        else
1131                         let args,body = aux argsno context y in
1132                         let sargs = String.concat "," args in
1133                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
1134                           body
1135                       in
1136                        pattern ^ " -> " ^ go_down ^
1137                         (if needs_obj_magic then
1138                          "Obj.magic (" ^ body ^ ")"
1139                         else
1140                          body) ^ go_nwod
1141                    ) connames_and_argsno_and_patterns)) ^
1142                  ")\n"^go_pu)))
1143     | C.Fix (no, funs) ->
1144        let names,_ =
1145         List.fold_left
1146          (fun (types,len) (n,_,ty,_) ->
1147             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1148              len+1)
1149          ) ([],0) funs
1150        in
1151          "let rec " ^
1152          List.fold_right
1153           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
1154             pp ~in_type:false bo (names@context) ^ i)
1155           funs "" ^
1156          " in " ^
1157          (match get_nth names (no + 1) with
1158              Some (Cic.Name n,_) -> n
1159            | _ -> assert false)
1160     | C.CoFix (no,funs) ->
1161        let names,_ =
1162         List.fold_left
1163          (fun (types,len) (n,ty,_) ->
1164             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1165              len+1)
1166          ) ([],0) funs
1167        in
1168          "\nCoFix " ^ " {" ^
1169          List.fold_right
1170           (fun (name,ty,bo) i -> "\n" ^ name ^
1171             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
1172             pp ~in_type:false bo (names@context) ^ i)
1173           funs "" ^
1174          "}\n"
1175 and pp_exp_named_subst exp_named_subst context =
1176  if exp_named_subst = [] then "" else
1177   "\\subst[" ^
1178    String.concat " ; " (
1179     List.map
1180      (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
1181      exp_named_subst
1182    ) ^ "]"
1183 and clean_args_for_constr nparams context =
1184  let nparams = ref nparams in
1185  HExtlib.filter_map
1186   (function t ->
1187     decr nparams;
1188     match analyze_term context t with
1189        `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
1190      | `Optimize
1191      | `Term
1192      | `Type
1193      | `Proof -> None)
1194 and clean_args context =
1195  function
1196  | [] | [_] -> assert false
1197  | he::arg1::tl as l ->
1198     let head_arg1, rest =
1199        match analyze_term context arg1 with
1200       | `Optimize ->
1201          !current_go_up :: pp ~in_type:false he context ::
1202                  pp ~in_type:false arg1 context :: ["))"], tl
1203       | _ -> [], l
1204     in
1205     head_arg1 @
1206     HExtlib.filter_map
1207      (function t ->
1208        match analyze_term context t with
1209         | `Term -> Some (pp ~in_type:false t context)
1210         | `Optimize ->
1211             prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
1212         | `Type
1213         | `Proof -> None) rest
1214 and clean_args_for_ty context =
1215  HExtlib.filter_map
1216   (function t ->
1217     match analyze_term context t with
1218        `Type -> Some (pp ~in_type:true t context)
1219      | `Optimize -> None
1220      | `Proof -> None
1221      | `Term -> None)
1222 in
1223  pp ~in_type
1224 ;;
1225
1226 let ppty current_module_uri =
1227  (* nparams is the number of left arguments
1228     left arguments should either become parameters or be skipped altogether *)
1229  let rec args nparams context =
1230   function
1231      Cic.Prod (n,s,t) ->
1232       let n =
1233        match n with
1234           Cic.Anonymous -> Cic.Anonymous
1235         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1236       in
1237        (match analyze_type context s with
1238          | `Optimize
1239          | `Statement
1240          | `Sort Cic.Prop ->
1241              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1242          | `Type when nparams > 0 ->
1243              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1244          | `Type ->
1245              let abstr,args =
1246               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
1247                abstr,pp ~in_type:true current_module_uri s context::args
1248          | `Sort _ when nparams <= 0 ->
1249              let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
1250               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1251          | `Sort _ ->
1252              let n =
1253               match n with
1254                  Cic.Anonymous -> Cic.Anonymous
1255                | Cic.Name name -> Cic.Name ("'" ^ name) in
1256              let abstr,args =
1257               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1258              in
1259               (match n with
1260                   Cic.Anonymous -> abstr
1261                 | Cic.Name name -> name::abstr),
1262               args)
1263    | _ -> [],[]
1264  in
1265   args
1266 ;;
1267
1268 exception DoNotExtract;;
1269
1270 let pp_abstracted_ty current_module_uri =
1271  let rec args context =
1272   function
1273      Cic.Lambda (n,s,t) ->
1274       let n =
1275        match n with
1276           Cic.Anonymous -> Cic.Anonymous
1277         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1278       in
1279        (match analyze_type context s with
1280          | `Optimize
1281          | `Statement
1282          | `Type
1283          | `Sort Cic.Prop ->
1284              args ((Some (n,Cic.Decl s))::context) t
1285          | `Sort _ ->
1286              let n =
1287               match n with
1288                  Cic.Anonymous -> Cic.Anonymous
1289                | Cic.Name name -> Cic.Name ("'" ^ name) in
1290              let abstr,res =
1291               args ((Some (n,Cic.Decl s))::context) t
1292              in
1293               (match n with
1294                   Cic.Anonymous -> abstr
1295                 | Cic.Name name -> name::abstr),
1296               res)
1297    | ty ->
1298      match analyze_type context ty with
1299       | `Optimize ->
1300            prerr_endline "XXX abstracted l2 ty"; assert false
1301       | `Sort _
1302       | `Statement -> raise DoNotExtract
1303       | `Type ->
1304           (* BUG HERE: this can be a real System F type *)
1305           let head = pp ~in_type:true current_module_uri ty context in
1306           [],head
1307  in
1308   args
1309 ;;
1310
1311
1312 (* ppinductiveType (typename, inductive, arity, cons)                       *)
1313 (* pretty-prints a single inductive definition                              *)
1314 (* (typename, inductive, arity, cons)                                       *)
1315 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
1316 =
1317  match analyze_type [] arity with
1318     `Sort Cic.Prop -> ""
1319   | `Optimize
1320   | `Statement
1321   | `Type -> assert false
1322   | `Sort _ ->
1323     if cons = [] then
1324      "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
1325     else (
1326      let abstr,scons =
1327       List.fold_right
1328        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
1329           let abstr',sargs = ppty current_module_uri nparams [] ty in
1330           let sargs = String.concat " * " sargs in
1331            abstr',
1332            String.capitalize id ^
1333             (if sargs = "" then "" else " of " ^ sargs) ^
1334             (if i = "" then "" else "\n | ") ^ i)
1335        cons ([],"")
1336       in
1337        let abstr =
1338         let s = String.concat "," abstr in
1339         if s = "" then "" else "(" ^ s ^ ") "
1340        in
1341        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
1342 ;;
1343
1344 let ppobj current_module_uri obj =
1345  let module C = Cic in
1346  let module U = UriManager in
1347   let pp ~in_type = pp ~in_type current_module_uri in
1348   match obj with
1349     C.Constant (name, Some t1, t2, params, _) ->
1350       (match analyze_type [] t2 with
1351         | `Sort Cic.Prop
1352         | `Statement -> ""
1353         | `Optimize
1354         | `Type ->
1355             (match t1 with
1356             | Cic.Lambda (Cic.Name arg, s, t) ->
1357                             (match analyze_type [] s with
1358                 | `Optimize ->
1359
1360                     "let " ^ ppid name ^ "__1 = function " ^ ppid arg
1361                     ^ " -> .< " ^
1362                     at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)]
1363                     ^ " >. ;;\n"
1364                     ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
1365                     ^ "let " ^ ppid name ^ " = function " ^ ppid arg
1366                     ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic  !"^ppid name
1367                     ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
1368                     ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
1369                     ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
1370                     ^ppid name^"__2)) >.\n;;\n"
1371                     ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
1372                     name^" Matita_freescale_opcode.HCS08)"
1373                 | _ ->
1374                    "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1375             | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1376         | `Sort _ ->
1377             match analyze_type [] t1 with
1378                `Sort Cic.Prop -> ""
1379              | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
1380              | _ ->
1381                (try
1382                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
1383                  let abstr =
1384                   let s = String.concat "," abstr in
1385                   if s = "" then "" else "(" ^ s ^ ") "
1386                  in
1387                   "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
1388                 with
1389                  DoNotExtract -> ""))
1390    | C.Constant (name, None, ty, params, _) ->
1391       (match analyze_type [] ty with
1392           `Sort Cic.Prop
1393         | `Optimize -> prerr_endline "XXX axiom l2"; assert false
1394         | `Statement -> ""
1395         | `Sort _ -> "type " ^ ppid name ^ "\n"
1396         | `Type -> "let " ^ ppid name ^ " = assert false\n")
1397    | C.Variable (name, bo, ty, params, _) ->
1398       "Variable " ^ name ^
1399        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1400        ")" ^ ":\n" ^
1401        pp ~in_type:true ty [] ^ "\n" ^
1402        (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
1403    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
1404       "Current Proof of " ^ name ^
1405        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1406        ")" ^ ":\n" ^
1407       let separate s = if s = "" then "" else s ^ " ; " in
1408        List.fold_right
1409         (fun (n, context, t) i ->
1410           let conjectures',name_context =
1411                  List.fold_right
1412                   (fun context_entry (i,name_context) ->
1413                     (match context_entry with
1414                         Some (n,C.Decl at) ->
1415                          (separate i) ^
1416                            ppname n ^ ":" ^
1417                             pp ~in_type:true ~metasenv:conjectures
1418                             at name_context ^ " ",
1419                             context_entry::name_context
1420                       | Some (n,C.Def (at,aty)) ->
1421                          (separate i) ^
1422                            ppname n ^ ":" ^
1423                             pp ~in_type:true ~metasenv:conjectures
1424                             aty name_context ^
1425                            ":= " ^ pp ~in_type:false
1426                             ~metasenv:conjectures at name_context ^ " ",
1427                             context_entry::name_context
1428                       | None ->
1429                          (separate i) ^ "_ :? _ ", context_entry::name_context)
1430             ) context ("",[])
1431           in
1432            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
1433             pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
1434         ) conjectures "" ^
1435         "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
1436           pp ~in_type:true ~metasenv:conjectures ty []
1437    | C.InductiveDefinition (l, params, nparams, _) ->
1438       List.fold_right
1439        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
1440 ;;
1441
1442 let ppobj current_module_uri obj =
1443  let res = ppobj current_module_uri obj in
1444   if res = "" then "" else res ^ ";;\n\n"
1445 ;;
1446 *)
1447 *)