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