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