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,_ as 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 ref =
 391                    NReference.reference_of_spec uri (NReference.Def height) in
 392                    status#set_extraction_db
 393                     (ReferenceMap.add ref ctx0 status#extraction_db),
 394                    Some (uri,TypeDefinition(res,typ_of status ~metasenv ctx bo))
 395               | `Kind -> status, None
 396               | `PropKind
 397               | `Proposition -> status, None
 398               | `Term _ -> assert false (* IMPOSSIBLE *))
 399         | `PropKind
 400         | `Proposition -> status, None
 401         | `KindOrType (* ??? *)
 402         | `Type ->
 403            (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 404            let ty = typ_of status ~metasenv [] ty in
 405             status,
 406             Some (uri, TermDefinition (split_typ_prods [] ty,
 407              term_of status ~metasenv [](* BAD! *) bo))
 408         | `Term _ -> assert false (* IMPOSSIBLE *))
 409  with
 410   NotInFOmega ->
 411    prerr_endline "NOT IN F_omega";
 412    status, None
 413
 414 (************************ HASKELL *************************)
 415
 416 (*CSC: code to be changed soon when we implement constructors and
 417   we fix the code for term application *)
 418 let classify_reference status ref =
 419  if ReferenceMap.mem ref status#extraction_db then
 420   `TypeName
 421  else
 422   `FunctionName
 423
 424 let capitalize classification name =
 425   match classification with
 426      `Constructor
 427    | `TypeName -> String.capitalize name
 428    | `FunctionName -> String.uncapitalize name
 429
 430 let pp_ref status ref =
 431  capitalize (classify_reference status ref)
 432   (NCicPp.r2s status false ref)
 433
 434 let name_of_uri classification uri =
 435  capitalize classification (NUri.name_of_uri uri)
 436
 437 (* cons avoid duplicates *)
 438 let rec (@::) name l =
 439  if name.[0] = '_' then "a" @:: l
 440  else if List.mem name l then (name ^ "'") @:: l
 441  else name::l
 442 ;;
 443
 444 let rec pp_kind =
 445  function
 446    Type -> "*"
 447  | KArrow (k1,k2) -> "(" ^ pp_kind k1 ^ ") -> " ^ pp_kind k2
 448  | KSkip k -> pp_kind k
 449
 450 let rec pp_typ status ctx =
 451  function
 452    Var n -> List.nth ctx (n-1)
 453  | Top -> assert false (* ??? *)
 454  | TConst ref -> pp_ref status ref
 455  | Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2
 456  | Skip t -> pp_typ status ("_"::ctx) t
 457  | Forall (name,_,t) ->
 458     let name = String.uncapitalize name in
 459     "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")"
 460  | TAppl tl -> "(" ^ String.concat " " (List.map (pp_typ status ctx) tl) ^ ")"
 461
 462 let rec pp_term status ctx =
 463  function
 464    Rel n -> List.nth ctx (n-1)
 465  | Const ref -> pp_ref status ref
 466  | Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")"
 467  | Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")"
 468  | LetIn (name,s,t) ->
 469     "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
 470     ")"
 471  | Match _ -> assert false (* TODO of reference * term * term list *)
 472  | TLambda t -> pp_term status ctx t
 473  | Inst t -> pp_term status ctx t
 474
 475 (*
 476 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 477
 478 type term_former_def = term_context * term * typ
 479 type term_former_decl = term_context * typ
 480 *)
 481
 482 let pp_obj status (uri,obj_kind) =
 483  let pp_ctx ctx =
 484   String.concat " " (List.rev
 485    (List.fold_right (fun (x,_) l -> x@::l)
 486      (HExtlib.filter_map (fun x -> x) ctx) [])) in
 487  let namectx_of_ctx ctx =
 488   List.fold_right (@::)
 489    (List.map (function None -> "_" | Some (x,_) -> x) ctx) [] in
 490  match obj_kind with
 491    TypeDeclaration (ctx,_) ->
 492     (* data?? unsure semantics: inductive type without constructor, but
 493        not matchable apparently *)
 494     "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx
 495  | TypeDefinition ((ctx,_),ty) ->
 496     let namectx = namectx_of_ctx ctx in
 497     "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
 498        pp_typ status namectx ty
 499  | TermDeclaration (ctx,ty) ->
 500     (* Implemented with undefined, the best we can do *)
 501     let name = name_of_uri `FunctionName uri in
 502     name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 503     name ^ " = undefined"
 504  | TermDefinition ((ctx,ty),bo) ->
 505     let name = name_of_uri `FunctionName uri in
 506     let namectx = namectx_of_ctx ctx in
 507     name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 508     name ^ " = " ^ pp_term status namectx bo
 509  | LetRec _ -> assert false (* TODO
 510  (* inductive and records missing *)*)
 511
 512 let haskell_of_obj status obj =
 513  let status, obj = obj_of status obj in
 514   status,HExtlib.map_option (pp_obj status) obj
 515
 516 (*
 517 let rec typ_of context =
 518  function
 519 (*
 520     C.Rel n ->
 521        begin
 522         try
 523          (match get_nth context n with
 524              Some (C.Name s,_) -> ppid s
 525            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 526            | None -> "_hidden_" ^ string_of_int n
 527          )
 528         with
 529          NotEnoughElements -> string_of_int (List.length context - n)
 530        end
 531     | C.Meta (n,l1) ->
 532        (match metasenv with
 533            None ->
 534             "?" ^ (string_of_int n) ^ "[" ^
 535              String.concat " ; "
 536               (List.rev_map
 537                 (function
 538                     None -> "_"
 539                   | Some t -> pp ~in_type:false t context) l1) ^
 540              "]"
 541          | Some metasenv ->
 542             try
 543              let _,context,_ = CicUtil.lookup_meta n metasenv in
 544               "?" ^ (string_of_int n) ^ "[" ^
 545                String.concat " ; "
 546                 (List.rev
 547                   (List.map2
 548                     (fun x y ->
 549                       match x,y with
 550                          _, None
 551                        | None, _ -> "_"
 552                        | Some _, Some t -> pp ~in_type:false t context
 553                     ) context l1)) ^
 554                "]"
 555             with
 556               CicUtil.Meta_not_found _
 557             | Invalid_argument _ ->
 558               "???" ^ (string_of_int n) ^ "[" ^
 559                String.concat " ; "
 560                 (List.rev_map (function None -> "_" | Some t ->
 561                   pp ~in_type:false t context) l1) ^
 562                "]"
 563        )
 564     | C.Sort s ->
 565        (match s with
 566            C.Prop  -> "Prop"
 567          | C.Set   -> "Set"
 568          | C.Type _ -> "Type"
 569          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 570          | C.CProp _ -> "CProp"
 571        )
 572     | C.Implicit (Some `Hole) -> "%"
 573     | C.Implicit _ -> "?"
 574     | C.Prod (b,s,t) ->
 575        (match b, is_term s with
 576            _, true -> typ_of (None::context) t
 577          | "_",_ -> Arrow (typ_of context s) (typ_of (Some b::context) t)
 578          | _,_ -> Forall (b,typ_of (Some b::context) t)
 579     | C.Lambda (b,s,t) ->
 580        (match analyze_type context s with
 581            `Sort _
 582          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 583          | `Optimize -> prerr_endline "XXX lambda";assert false
 584          | `Type ->
 585             "(function " ^ ppname b ^ " -> " ^
 586              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 587     | C.LetIn (b,s,ty,t) ->
 588        (match analyze_term context s with
 589          | `Type
 590          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 591          | `Optimize
 592          | `Term ->
 593             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 594             " = " ^ pp ~in_type:false s context ^ " in " ^
 595              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 596     | C.Appl (he::tl) when in_type ->
 597        let hes = pp ~in_type he context in
 598        let stl = String.concat "," (clean_args_for_ty context tl) in
 599         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 600     | C.Appl (C.MutInd _ as he::tl) ->
 601        let hes = pp ~in_type he context in
 602        let stl = String.concat "," (clean_args_for_ty context tl) in
 603         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 604     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 605        let nparams =
 606         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 607            C.InductiveDefinition (_,_,nparams,_) -> nparams
 608          | _ -> assert false in
 609        let hes = pp ~in_type he context in
 610        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
 611         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
 612     | C.Appl li ->
 613        "(" ^ String.concat " " (clean_args context li) ^ ")"
 614     | C.Const (uri,exp_named_subst) ->
 615        qualified_name_of_uri status current_module_uri uri ^
 616         pp_exp_named_subst exp_named_subst context
 617     | C.MutInd (uri,n,exp_named_subst) ->
 618        (try
 619          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 620             C.InductiveDefinition (dl,_,_,_) ->
 621              let (name,_,_,_) = get_nth dl (n+1) in
 622               qualified_name_of_uri status current_module_uri
 623                (UriManager.uri_of_string
 624                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
 625               pp_exp_named_subst exp_named_subst context
 626           | _ -> raise CicExportationInternalError
 627         with
 628            Sys.Break as exn -> raise exn
 629          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
 630        )
 631     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
 632        (try
 633          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 634             C.InductiveDefinition (dl,_,_,_) ->
 635              let _,_,_,cons = get_nth dl (n1+1) in
 636               let id,_ = get_nth cons n2 in
 637                qualified_name_of_uri status current_module_uri ~capitalize:true
 638                 (UriManager.uri_of_string
 639                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
 640                pp_exp_named_subst exp_named_subst context
 641           | _ -> raise CicExportationInternalError
 642         with
 643            Sys.Break as exn -> raise exn
 644          | _ ->
 645           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
 646            string_of_int n2
 647        )
 648     | C.MutCase (uri,n1,ty,te,patterns) ->
 649        if in_type then
 650         "unit (* TOO POLYMORPHIC TYPE *)"
 651        else (
 652        let rec needs_obj_magic ty =
 653         match CicReduction.whd context ty with
 654          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
 655          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
 656          | _ -> false (* it can be a Rel, e.g. in *_rec *)
 657        in
 658        let needs_obj_magic = needs_obj_magic ty in
 659        (match analyze_term context te with
 660            `Type -> assert false
 661          | `Proof ->
 662              (match patterns with
 663                  [] -> "assert false"   (* empty type elimination *)
 664                | [he] ->
 665                   pp ~in_type:false he context  (* singleton elimination *)
 666                | _ -> assert false)
 667          | `Optimize
 668          | `Term ->
 669             if patterns = [] then "assert false"
 670             else
 671              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
 672                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 673                    C.InductiveDefinition (dl,_,paramsno,_) ->
 674                     let (_,_,_,cons) = get_nth dl (n1+1) in
 675                     let rc =
 676                      List.map
 677                       (fun (id,ty) ->
 678                         (* this is just an approximation since we do not have
 679                            reduction yet! *)
 680                         let rec count_prods toskip =
 681                          function
 682                             C.Prod (_,_,bo) when toskip > 0 ->
 683                              count_prods (toskip - 1) bo
 684                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
 685                           | _ -> 0
 686                         in
 687                          qualified_name_of_uri status current_module_uri
 688                           ~capitalize:true
 689                           (UriManager.uri_of_string
 690                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
 691                          count_prods paramsno ty
 692                       ) cons
 693                     in
 694                     if not (is_mcu_type uri) then rc, "","","",""
 695                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
 696                  | _ -> raise CicExportationInternalError
 697                )
 698               in
 699                let connames_and_argsno_and_patterns =
 700                 let rec combine =
 701                    function
 702                       [],[] -> []
 703                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
 704                     | _,_ -> assert false
 705                 in
 706                  combine (connames_and_argsno,patterns)
 707                in
 708                 go_up ^
 709                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
 710                  (String.concat "\n | "
 711                   (List.map
 712                    (fun (x,argsno,y) ->
 713                      let rec aux argsno context =
 714                       function
 715                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
 716                           let name =
 717                            match name with
 718                               Cic.Anonymous -> Cic.Anonymous
 719                             | Cic.Name n -> Cic.Name (ppid n) in
 720                           let args,res =
 721                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
 722                             bo
 723                           in
 724                            (match analyze_type context ty with
 725                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
 726                              | `Statement
 727                              | `Sort _ -> args,res
 728                              | `Type ->
 729                                  (match name with
 730                                      C.Anonymous -> "_"
 731                                    | C.Name s -> s)::args,res)
 732                        | t when argsno = 0 -> [],pp ~in_type:false t context
 733                        | t ->
 734                           ["{" ^ string_of_int argsno ^ " args missing}"],
 735                            pp ~in_type:false t context
 736                      in
 737                       let pattern,body =
 738                        if argsno = 0 then x,pp ~in_type:false y context
 739                        else
 740                         let args,body = aux argsno context y in
 741                         let sargs = String.concat "," args in
 742                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
 743                           body
 744                       in
 745                        pattern ^ " -> " ^ go_down ^
 746                         (if needs_obj_magic then
 747                          "Obj.magic (" ^ body ^ ")"
 748                         else
 749                          body) ^ go_nwod
 750                    ) connames_and_argsno_and_patterns)) ^
 751                  ")\n"^go_pu)))
 752     | C.Fix (no, funs) ->
 753        let names,_ =
 754         List.fold_left
 755          (fun (types,len) (n,_,ty,_) ->
 756             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 757              len+1)
 758          ) ([],0) funs
 759        in
 760          "let rec " ^
 761          List.fold_right
 762           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
 763             pp ~in_type:false bo (names@context) ^ i)
 764           funs "" ^
 765          " in " ^
 766          (match get_nth names (no + 1) with
 767              Some (Cic.Name n,_) -> n
 768            | _ -> assert false)
 769     | C.CoFix (no,funs) ->
 770        let names,_ =
 771         List.fold_left
 772          (fun (types,len) (n,ty,_) ->
 773             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 774              len+1)
 775          ) ([],0) funs
 776        in
 777          "\nCoFix " ^ " {" ^
 778          List.fold_right
 779           (fun (name,ty,bo) i -> "\n" ^ name ^
 780             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
 781             pp ~in_type:false bo (names@context) ^ i)
 782           funs "" ^
 783          "}\n"
 784 *)
 785
 786 (*
 787 exception CicExportationInternalError;;
 788 exception NotEnoughElements;;
 789
 790 (* *)
 791
 792 let is_mcu_type u =
 793   UriManager.eq (UriManager.uri_of_string
 794   "cic:/matita/freescale/opcode/mcu_type.ind") u
 795 ;;
 796
 797 (* Utility functions *)
 798
 799 let analyze_term context t =
 800  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
 801   | Cic.Sort _ -> `Type
 802   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 803   | ty ->
 804      match
 805       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
 806      with
 807      | Cic.Sort Cic.Prop -> `Proof
 808      | _ -> `Term
 809 ;;
 810
 811 let analyze_type context t =
 812  let rec aux =
 813   function
 814      Cic.Sort s -> `Sort s
 815    | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 816    | Cic.Prod (_,_,t) -> aux t
 817    | _ -> `SomethingElse
 818  in
 819  match aux t with
 820     `Sort _ | `Optimize as res -> res
 821   | `SomethingElse ->
 822       match
 823        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
 824       with
 825           Cic.Sort Cic.Prop -> `Statement
 826        | _ -> `Type
 827 ;;
 828
 829 let ppid =
 830  let reserved =
 831   [ "to";
 832     "mod";
 833     "val";
 834     "in";
 835     "function"
 836   ]
 837  in
 838   function n ->
 839    let n = String.uncapitalize n in
 840     if List.mem n reserved then n ^ "_" else n
 841 ;;
 842
 843 let ppname =
 844  function
 845     Cic.Name s     -> ppid s
 846   | Cic.Anonymous  -> "_"
 847 ;;
 848
 849 (* get_nth l n   returns the nth element of the list l if it exists or *)
 850 (* raises NotEnoughElements if l has less than n elements             *)
 851 let rec get_nth l n =
 852  match (n,l) with
 853     (1, he::_) -> he
 854   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
 855   | (_,_) -> raise NotEnoughElements
 856 ;;
 857
 858 let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
 859  let name =
 860   if capitalize then
 861    String.capitalize (UriManager.name_of_uri status uri)
 862   else
 863    ppid (UriManager.name_of_uri status uri) in
 864   let filename =
 865    let suri = UriManager.buri_of_uri uri in
 866    let s = String.sub suri 5 (String.length suri - 5) in
 867    let s = Pcre.replace ~pat:"/" ~templ:"_" s in
 868     String.uncapitalize s in
 869   if current_module_uri = UriManager.buri_of_uri uri then
 870    name
 871   else
 872    String.capitalize filename ^ "." ^ name
 873 ;;
 874
 875 let current_go_up = ref "(.!(";;
 876 let at_level2 f x =
 877   try
 878     current_go_up := "(.~(";
 879     let rc = f x in
 880     current_go_up := "(.!(";
 881     rc
 882   with exn ->
 883     current_go_up := "(.!(";
 884     raise exn
 885 ;;
 886
 887 let pp current_module_uri ?metasenv ~in_type =
 888 let rec pp ~in_type t context =
 889  let module C = Cic in
 890    match t with
 891       C.Rel n ->
 892        begin
 893         try
 894          (match get_nth context n with
 895              Some (C.Name s,_) -> ppid s
 896            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 897            | None -> "_hidden_" ^ string_of_int n
 898          )
 899         with
 900          NotEnoughElements -> string_of_int (List.length context - n)
 901        end
 902     | C.Var (uri,exp_named_subst) ->
 903         qualified_name_of_uri status current_module_uri uri ^
 904          pp_exp_named_subst exp_named_subst context
 905     | C.Meta (n,l1) ->
 906        (match metasenv with
 907            None ->
 908             "?" ^ (string_of_int n) ^ "[" ^
 909              String.concat " ; "
 910               (List.rev_map
 911                 (function
 912                     None -> "_"
 913                   | Some t -> pp ~in_type:false t context) l1) ^
 914              "]"
 915          | Some metasenv ->
 916             try
 917              let _,context,_ = CicUtil.lookup_meta n metasenv in
 918               "?" ^ (string_of_int n) ^ "[" ^
 919                String.concat " ; "
 920                 (List.rev
 921                   (List.map2
 922                     (fun x y ->
 923                       match x,y with
 924                          _, None
 925                        | None, _ -> "_"
 926                        | Some _, Some t -> pp ~in_type:false t context
 927                     ) context l1)) ^
 928                "]"
 929             with
 930               CicUtil.Meta_not_found _
 931             | Invalid_argument _ ->
 932               "???" ^ (string_of_int n) ^ "[" ^
 933                String.concat " ; "
 934                 (List.rev_map (function None -> "_" | Some t ->
 935                   pp ~in_type:false t context) l1) ^
 936                "]"
 937        )
 938     | C.Sort s ->
 939        (match s with
 940            C.Prop  -> "Prop"
 941          | C.Set   -> "Set"
 942          | C.Type _ -> "Type"
 943          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 944          | C.CProp _ -> "CProp"
 945        )
 946     | C.Implicit (Some `Hole) -> "%"
 947     | C.Implicit _ -> "?"
 948     | C.Prod (b,s,t) ->
 949        (match b with
 950           C.Name n ->
 951            let n = "'" ^ String.uncapitalize n in
 952             "(" ^ pp ~in_type:true s context ^ " -> " ^
 953             pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
 954         | C.Anonymous ->
 955            "(" ^ pp ~in_type:true s context ^ " -> " ^
 956            pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
 957     | C.Cast (v,t) -> pp ~in_type v context
 958     | C.Lambda (b,s,t) ->
 959        (match analyze_type context s with
 960            `Sort _
 961          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 962          | `Optimize -> prerr_endline "XXX lambda";assert false
 963          | `Type ->
 964             "(function " ^ ppname b ^ " -> " ^
 965              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 966     | C.LetIn (b,s,ty,t) ->
 967        (match analyze_term context s with
 968          | `Type
 969          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 970          | `Optimize
 971          | `Term ->
 972             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 973             " = " ^ pp ~in_type:false s context ^ " in " ^
 974              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 975     | C.Appl (he::tl) when in_type ->
 976        let hes = pp ~in_type he context in
 977        let stl = String.concat "," (clean_args_for_ty context tl) in
 978         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 979     | C.Appl (C.MutInd _ as he::tl) ->
 980        let hes = pp ~in_type he context in
 981        let stl = String.concat "," (clean_args_for_ty context tl) in
 982         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 983     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 984        let nparams =
 985         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 986            C.InductiveDefinition (_,_,nparams,_) -> nparams
 987          | _ -> assert false in
 988        let hes = pp ~in_type he context in
 989        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
 990         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
 991     | C.Appl li ->
 992        "(" ^ String.concat " " (clean_args context li) ^ ")"
 993     | C.Const (uri,exp_named_subst) ->
 994        qualified_name_of_uri status current_module_uri uri ^
 995         pp_exp_named_subst exp_named_subst context
 996     | C.MutInd (uri,n,exp_named_subst) ->
 997        (try
 998          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 999             C.InductiveDefinition (dl,_,_,_) ->
1000              let (name,_,_,_) = get_nth dl (n+1) in
1001               qualified_name_of_uri status current_module_uri
1002                (UriManager.uri_of_string
1003                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
1004               pp_exp_named_subst exp_named_subst context
1005           | _ -> raise CicExportationInternalError
1006         with
1007            Sys.Break as exn -> raise exn
1008          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
1009        )
1010     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
1011        (try
1012          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1013             C.InductiveDefinition (dl,_,_,_) ->
1014              let _,_,_,cons = get_nth dl (n1+1) in
1015               let id,_ = get_nth cons n2 in
1016                qualified_name_of_uri status current_module_uri ~capitalize:true
1017                 (UriManager.uri_of_string
1018                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
1019                pp_exp_named_subst exp_named_subst context
1020           | _ -> raise CicExportationInternalError
1021         with
1022            Sys.Break as exn -> raise exn
1023          | _ ->
1024           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
1025            string_of_int n2
1026        )
1027     | C.MutCase (uri,n1,ty,te,patterns) ->
1028        if in_type then
1029         "unit (* TOO POLYMORPHIC TYPE *)"
1030        else (
1031        let rec needs_obj_magic ty =
1032         match CicReduction.whd context ty with
1033          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
1034          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
1035          | _ -> false (* it can be a Rel, e.g. in *_rec *)
1036        in
1037        let needs_obj_magic = needs_obj_magic ty in
1038        (match analyze_term context te with
1039            `Type -> assert false
1040          | `Proof ->
1041              (match patterns with
1042                  [] -> "assert false"   (* empty type elimination *)
1043                | [he] ->
1044                   pp ~in_type:false he context  (* singleton elimination *)
1045                | _ -> assert false)
1046          | `Optimize
1047          | `Term ->
1048             if patterns = [] then "assert false"
1049             else
1050              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
1051                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1052                    C.InductiveDefinition (dl,_,paramsno,_) ->
1053                     let (_,_,_,cons) = get_nth dl (n1+1) in
1054                     let rc =
1055                      List.map
1056                       (fun (id,ty) ->
1057                         (* this is just an approximation since we do not have
1058                            reduction yet! *)
1059                         let rec count_prods toskip =
1060                          function
1061                             C.Prod (_,_,bo) when toskip > 0 ->
1062                              count_prods (toskip - 1) bo
1063                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
1064                           | _ -> 0
1065                         in
1066                          qualified_name_of_uri status current_module_uri
1067                           ~capitalize:true
1068                           (UriManager.uri_of_string
1069                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
1070                          count_prods paramsno ty
1071                       ) cons
1072                     in
1073                     if not (is_mcu_type uri) then rc, "","","",""
1074                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
1075                  | _ -> raise CicExportationInternalError
1076                )
1077               in
1078                let connames_and_argsno_and_patterns =
1079                 let rec combine =
1080                    function
1081                       [],[] -> []
1082                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
1083                     | _,_ -> assert false
1084                 in
1085                  combine (connames_and_argsno,patterns)
1086                in
1087                 go_up ^
1088                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
1089                  (String.concat "\n | "
1090                   (List.map
1091                    (fun (x,argsno,y) ->
1092                      let rec aux argsno context =
1093                       function
1094                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
1095                           let name =
1096                            match name with
1097                               Cic.Anonymous -> Cic.Anonymous
1098                             | Cic.Name n -> Cic.Name (ppid n) in
1099                           let args,res =
1100                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
1101                             bo
1102                           in
1103                            (match analyze_type context ty with
1104                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
1105                              | `Statement
1106                              | `Sort _ -> args,res
1107                              | `Type ->
1108                                  (match name with
1109                                      C.Anonymous -> "_"
1110                                    | C.Name s -> s)::args,res)
1111                        | t when argsno = 0 -> [],pp ~in_type:false t context
1112                        | t ->
1113                           ["{" ^ string_of_int argsno ^ " args missing}"],
1114                            pp ~in_type:false t context
1115                      in
1116                       let pattern,body =
1117                        if argsno = 0 then x,pp ~in_type:false y context
1118                        else
1119                         let args,body = aux argsno context y in
1120                         let sargs = String.concat "," args in
1121                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
1122                           body
1123                       in
1124                        pattern ^ " -> " ^ go_down ^
1125                         (if needs_obj_magic then
1126                          "Obj.magic (" ^ body ^ ")"
1127                         else
1128                          body) ^ go_nwod
1129                    ) connames_and_argsno_and_patterns)) ^
1130                  ")\n"^go_pu)))
1131     | C.Fix (no, funs) ->
1132        let names,_ =
1133         List.fold_left
1134          (fun (types,len) (n,_,ty,_) ->
1135             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1136              len+1)
1137          ) ([],0) funs
1138        in
1139          "let rec " ^
1140          List.fold_right
1141           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
1142             pp ~in_type:false bo (names@context) ^ i)
1143           funs "" ^
1144          " in " ^
1145          (match get_nth names (no + 1) with
1146              Some (Cic.Name n,_) -> n
1147            | _ -> assert false)
1148     | C.CoFix (no,funs) ->
1149        let names,_ =
1150         List.fold_left
1151          (fun (types,len) (n,ty,_) ->
1152             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1153              len+1)
1154          ) ([],0) funs
1155        in
1156          "\nCoFix " ^ " {" ^
1157          List.fold_right
1158           (fun (name,ty,bo) i -> "\n" ^ name ^
1159             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
1160             pp ~in_type:false bo (names@context) ^ i)
1161           funs "" ^
1162          "}\n"
1163 and pp_exp_named_subst exp_named_subst context =
1164  if exp_named_subst = [] then "" else
1165   "\\subst[" ^
1166    String.concat " ; " (
1167     List.map
1168      (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
1169      exp_named_subst
1170    ) ^ "]"
1171 and clean_args_for_constr nparams context =
1172  let nparams = ref nparams in
1173  HExtlib.filter_map
1174   (function t ->
1175     decr nparams;
1176     match analyze_term context t with
1177        `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
1178      | `Optimize
1179      | `Term
1180      | `Type
1181      | `Proof -> None)
1182 and clean_args context =
1183  function
1184  | [] | [_] -> assert false
1185  | he::arg1::tl as l ->
1186     let head_arg1, rest =
1187        match analyze_term context arg1 with
1188       | `Optimize ->
1189          !current_go_up :: pp ~in_type:false he context ::
1190                  pp ~in_type:false arg1 context :: ["))"], tl
1191       | _ -> [], l
1192     in
1193     head_arg1 @
1194     HExtlib.filter_map
1195      (function t ->
1196        match analyze_term context t with
1197         | `Term -> Some (pp ~in_type:false t context)
1198         | `Optimize ->
1199             prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
1200         | `Type
1201         | `Proof -> None) rest
1202 and clean_args_for_ty context =
1203  HExtlib.filter_map
1204   (function t ->
1205     match analyze_term context t with
1206        `Type -> Some (pp ~in_type:true t context)
1207      | `Optimize -> None
1208      | `Proof -> None
1209      | `Term -> None)
1210 in
1211  pp ~in_type
1212 ;;
1213
1214 let ppty current_module_uri =
1215  (* nparams is the number of left arguments
1216     left arguments should either become parameters or be skipped altogether *)
1217  let rec args nparams context =
1218   function
1219      Cic.Prod (n,s,t) ->
1220       let n =
1221        match n with
1222           Cic.Anonymous -> Cic.Anonymous
1223         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1224       in
1225        (match analyze_type context s with
1226          | `Optimize
1227          | `Statement
1228          | `Sort Cic.Prop ->
1229              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1230          | `Type when nparams > 0 ->
1231              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1232          | `Type ->
1233              let abstr,args =
1234               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
1235                abstr,pp ~in_type:true current_module_uri s context::args
1236          | `Sort _ when nparams <= 0 ->
1237              let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
1238               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1239          | `Sort _ ->
1240              let n =
1241               match n with
1242                  Cic.Anonymous -> Cic.Anonymous
1243                | Cic.Name name -> Cic.Name ("'" ^ name) in
1244              let abstr,args =
1245               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1246              in
1247               (match n with
1248                   Cic.Anonymous -> abstr
1249                 | Cic.Name name -> name::abstr),
1250               args)
1251    | _ -> [],[]
1252  in
1253   args
1254 ;;
1255
1256 exception DoNotExtract;;
1257
1258 let pp_abstracted_ty current_module_uri =
1259  let rec args context =
1260   function
1261      Cic.Lambda (n,s,t) ->
1262       let n =
1263        match n with
1264           Cic.Anonymous -> Cic.Anonymous
1265         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1266       in
1267        (match analyze_type context s with
1268          | `Optimize
1269          | `Statement
1270          | `Type
1271          | `Sort Cic.Prop ->
1272              args ((Some (n,Cic.Decl s))::context) t
1273          | `Sort _ ->
1274              let n =
1275               match n with
1276                  Cic.Anonymous -> Cic.Anonymous
1277                | Cic.Name name -> Cic.Name ("'" ^ name) in
1278              let abstr,res =
1279               args ((Some (n,Cic.Decl s))::context) t
1280              in
1281               (match n with
1282                   Cic.Anonymous -> abstr
1283                 | Cic.Name name -> name::abstr),
1284               res)
1285    | ty ->
1286      match analyze_type context ty with
1287       | `Optimize ->
1288            prerr_endline "XXX abstracted l2 ty"; assert false
1289       | `Sort _
1290       | `Statement -> raise DoNotExtract
1291       | `Type ->
1292           (* BUG HERE: this can be a real System F type *)
1293           let head = pp ~in_type:true current_module_uri ty context in
1294           [],head
1295  in
1296   args
1297 ;;
1298
1299
1300 (* ppinductiveType (typename, inductive, arity, cons)                       *)
1301 (* pretty-prints a single inductive definition                              *)
1302 (* (typename, inductive, arity, cons)                                       *)
1303 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
1304 =
1305  match analyze_type [] arity with
1306     `Sort Cic.Prop -> ""
1307   | `Optimize
1308   | `Statement
1309   | `Type -> assert false
1310   | `Sort _ ->
1311     if cons = [] then
1312      "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
1313     else (
1314      let abstr,scons =
1315       List.fold_right
1316        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
1317           let abstr',sargs = ppty current_module_uri nparams [] ty in
1318           let sargs = String.concat " * " sargs in
1319            abstr',
1320            String.capitalize id ^
1321             (if sargs = "" then "" else " of " ^ sargs) ^
1322             (if i = "" then "" else "\n | ") ^ i)
1323        cons ([],"")
1324       in
1325        let abstr =
1326         let s = String.concat "," abstr in
1327         if s = "" then "" else "(" ^ s ^ ") "
1328        in
1329        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
1330 ;;
1331
1332 let ppobj current_module_uri obj =
1333  let module C = Cic in
1334  let module U = UriManager in
1335   let pp ~in_type = pp ~in_type current_module_uri in
1336   match obj with
1337     C.Constant (name, Some t1, t2, params, _) ->
1338       (match analyze_type [] t2 with
1339         | `Sort Cic.Prop
1340         | `Statement -> ""
1341         | `Optimize
1342         | `Type ->
1343             (match t1 with
1344             | Cic.Lambda (Cic.Name arg, s, t) ->
1345                             (match analyze_type [] s with
1346                 | `Optimize ->
1347
1348                     "let " ^ ppid name ^ "__1 = function " ^ ppid arg
1349                     ^ " -> .< " ^
1350                     at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)]
1351                     ^ " >. ;;\n"
1352                     ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
1353                     ^ "let " ^ ppid name ^ " = function " ^ ppid arg
1354                     ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic  !"^ppid name
1355                     ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
1356                     ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
1357                     ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
1358                     ^ppid name^"__2)) >.\n;;\n"
1359                     ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
1360                     name^" Matita_freescale_opcode.HCS08)"
1361                 | _ ->
1362                    "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1363             | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1364         | `Sort _ ->
1365             match analyze_type [] t1 with
1366                `Sort Cic.Prop -> ""
1367              | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
1368              | _ ->
1369                (try
1370                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
1371                  let abstr =
1372                   let s = String.concat "," abstr in
1373                   if s = "" then "" else "(" ^ s ^ ") "
1374                  in
1375                   "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
1376                 with
1377                  DoNotExtract -> ""))
1378    | C.Constant (name, None, ty, params, _) ->
1379       (match analyze_type [] ty with
1380           `Sort Cic.Prop
1381         | `Optimize -> prerr_endline "XXX axiom l2"; assert false
1382         | `Statement -> ""
1383         | `Sort _ -> "type " ^ ppid name ^ "\n"
1384         | `Type -> "let " ^ ppid name ^ " = assert false\n")
1385    | C.Variable (name, bo, ty, params, _) ->
1386       "Variable " ^ name ^
1387        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1388        ")" ^ ":\n" ^
1389        pp ~in_type:true ty [] ^ "\n" ^
1390        (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
1391    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
1392       "Current Proof of " ^ name ^
1393        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1394        ")" ^ ":\n" ^
1395       let separate s = if s = "" then "" else s ^ " ; " in
1396        List.fold_right
1397         (fun (n, context, t) i ->
1398           let conjectures',name_context =
1399                  List.fold_right
1400                   (fun context_entry (i,name_context) ->
1401                     (match context_entry with
1402                         Some (n,C.Decl at) ->
1403                          (separate i) ^
1404                            ppname n ^ ":" ^
1405                             pp ~in_type:true ~metasenv:conjectures
1406                             at name_context ^ " ",
1407                             context_entry::name_context
1408                       | Some (n,C.Def (at,aty)) ->
1409                          (separate i) ^
1410                            ppname n ^ ":" ^
1411                             pp ~in_type:true ~metasenv:conjectures
1412                             aty name_context ^
1413                            ":= " ^ pp ~in_type:false
1414                             ~metasenv:conjectures at name_context ^ " ",
1415                             context_entry::name_context
1416                       | None ->
1417                          (separate i) ^ "_ :? _ ", context_entry::name_context)
1418             ) context ("",[])
1419           in
1420            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
1421             pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
1422         ) conjectures "" ^
1423         "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
1424           pp ~in_type:true ~metasenv:conjectures ty []
1425    | C.InductiveDefinition (l, params, nparams, _) ->
1426       List.fold_right
1427        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
1428 ;;
1429
1430 let ppobj current_module_uri obj =
1431  let res = ppobj current_module_uri obj in
1432   if res = "" then "" else res ^ ";;\n\n"
1433 ;;
1434 *)
1435 *)