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