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 (r,matched,pl) ->
 595     let constructors, leftno =
 596      let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
 597      let _,_,_,cl  = List.nth tys n in
 598       cl,leftno
 599     in
 600     let rec eat_branch n ty pat =
 601       match (ty, pat) with
 602       | NCic.Prod (_, _, t), _ when n > 0 ->
 603          eat_branch (pred n) t pat
 604       | NCic.Prod (_, _, t), Lambda (name, t') ->
 605           (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
 606           let cv, rhs = eat_branch 0 t t' in
 607           name :: cv, rhs
 608       | _, _ -> [], pat
 609     in
 610     let j = ref 0 in
 611     let patterns =
 612       try
 613         List.map2
 614           (fun (_, name, ty) pat ->
 615             incr j;
 616             name, eat_branch leftno ty pat
 617           ) constructors pl
 618       with Invalid_argument _ -> assert false
 619     in
 620    "case " ^ pp_term status ctx matched ^ " of\n" ^
 621    String.concat "\n"
 622     (List.map
 623       (fun (name,(bound_names,rhs)) ->
 624         let pattern,body =
 625          (*CSC: BUG avoid name clashes *)
 626          String.concat " " (String.capitalize name::bound_names),
 627          pp_term status (bound_names@ctx) rhs
 628         in
 629          "  " ^ pattern ^ " -> " ^ body
 630      ) patterns)
 631  | TLambda t -> pp_term status ctx t
 632  | Inst t -> pp_term status ctx t
 633
 634 (*
 635 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 636
 637 type term_former_def = term_context * term * typ
 638 type term_former_decl = term_context * typ
 639 *)
 640
 641 let rec pp_obj status (uri,obj_kind) =
 642  let pp_ctx ctx =
 643   String.concat " " (List.rev
 644    (List.fold_right (fun (x,_) l -> x@::l)
 645      (HExtlib.filter_map (fun x -> x) ctx) [])) in
 646  let namectx_of_ctx ctx =
 647   List.fold_right (@::)
 648    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 649  match obj_kind with
 650    TypeDeclaration (ctx,_) ->
 651     (* data?? unsure semantics: inductive type without constructor, but
 652        not matchable apparently *)
 653     "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx
 654  | TypeDefinition ((ctx,_),ty) ->
 655     let namectx = namectx_of_ctx ctx in
 656     "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
 657        pp_typ status namectx ty
 658  | TermDeclaration (ctx,ty) ->
 659     (* Implemented with undefined, the best we can do *)
 660     let name = name_of_uri `FunctionName uri in
 661     name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 662     name ^ " = undefined"
 663  | TermDefinition ((ctx,ty),bo) ->
 664     let name = name_of_uri `FunctionName uri in
 665     let namectx = namectx_of_ctx ctx in
 666     name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^
 667     name ^ " = " ^ pp_term status namectx bo
 668  | LetRec l ->
 669     (*CSC: BUG always uses the name of the URI *)
 670     String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
 671  (* inductive and records missing *)
 672
 673 let haskell_of_obj status obj =
 674  let status, obj = obj_of status obj in
 675   status,
 676    match obj with
 677       None -> "-- ERASED\n"
 678     | Some obj -> pp_obj status obj ^ "\n"
 679
 680 (*
 681 let rec typ_of context =
 682  function
 683 (*
 684     C.Rel n ->
 685        begin
 686         try
 687          (match get_nth context n with
 688              Some (C.Name s,_) -> ppid s
 689            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
 690            | None -> "_hidden_" ^ string_of_int n
 691          )
 692         with
 693          NotEnoughElements -> string_of_int (List.length context - n)
 694        end
 695     | C.Meta (n,l1) ->
 696        (match metasenv with
 697            None ->
 698             "?" ^ (string_of_int n) ^ "[" ^
 699              String.concat " ; "
 700               (List.rev_map
 701                 (function
 702                     None -> "_"
 703                   | Some t -> pp ~in_type:false t context) l1) ^
 704              "]"
 705          | Some metasenv ->
 706             try
 707              let _,context,_ = CicUtil.lookup_meta n metasenv in
 708               "?" ^ (string_of_int n) ^ "[" ^
 709                String.concat " ; "
 710                 (List.rev
 711                   (List.map2
 712                     (fun x y ->
 713                       match x,y with
 714                          _, None
 715                        | None, _ -> "_"
 716                        | Some _, Some t -> pp ~in_type:false t context
 717                     ) context l1)) ^
 718                "]"
 719             with
 720               CicUtil.Meta_not_found _
 721             | Invalid_argument _ ->
 722               "???" ^ (string_of_int n) ^ "[" ^
 723                String.concat " ; "
 724                 (List.rev_map (function None -> "_" | Some t ->
 725                   pp ~in_type:false t context) l1) ^
 726                "]"
 727        )
 728     | C.Sort s ->
 729        (match s with
 730            C.Prop  -> "Prop"
 731          | C.Set   -> "Set"
 732          | C.Type _ -> "Type"
 733          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 734          | C.CProp _ -> "CProp"
 735        )
 736     | C.Implicit (Some `Hole) -> "%"
 737     | C.Implicit _ -> "?"
 738     | C.Prod (b,s,t) ->
 739        (match b, is_term s with
 740            _, true -> typ_of (None::context) t
 741          | "_",_ -> Arrow (typ_of context s) (typ_of (Some b::context) t)
 742          | _,_ -> Forall (b,typ_of (Some b::context) t)
 743     | C.Lambda (b,s,t) ->
 744        (match analyze_type context s with
 745            `Sort _
 746          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
 747          | `Optimize -> prerr_endline "XXX lambda";assert false
 748          | `Type ->
 749             "(function " ^ ppname b ^ " -> " ^
 750              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
 751     | C.LetIn (b,s,ty,t) ->
 752        (match analyze_term context s with
 753          | `Type
 754          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
 755          | `Optimize
 756          | `Term ->
 757             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
 758             " = " ^ pp ~in_type:false s context ^ " in " ^
 759              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
 760     | C.Appl (he::tl) when in_type ->
 761        let hes = pp ~in_type he context in
 762        let stl = String.concat "," (clean_args_for_ty context tl) in
 763         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 764     | C.Appl (C.MutInd _ as he::tl) ->
 765        let hes = pp ~in_type he context in
 766        let stl = String.concat "," (clean_args_for_ty context tl) in
 767         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
 768     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
 769        let nparams =
 770         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 771            C.InductiveDefinition (_,_,nparams,_) -> nparams
 772          | _ -> assert false in
 773        let hes = pp ~in_type he context in
 774        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
 775         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
 776     | C.Appl li ->
 777        "(" ^ String.concat " " (clean_args context li) ^ ")"
 778     | C.Const (uri,exp_named_subst) ->
 779        qualified_name_of_uri status current_module_uri uri ^
 780         pp_exp_named_subst exp_named_subst context
 781     | C.MutInd (uri,n,exp_named_subst) ->
 782        (try
 783          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 784             C.InductiveDefinition (dl,_,_,_) ->
 785              let (name,_,_,_) = get_nth dl (n+1) in
 786               qualified_name_of_uri status current_module_uri
 787                (UriManager.uri_of_string
 788                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
 789               pp_exp_named_subst exp_named_subst context
 790           | _ -> raise CicExportationInternalError
 791         with
 792            Sys.Break as exn -> raise exn
 793          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
 794        )
 795     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
 796        (try
 797          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 798             C.InductiveDefinition (dl,_,_,_) ->
 799              let _,_,_,cons = get_nth dl (n1+1) in
 800               let id,_ = get_nth cons n2 in
 801                qualified_name_of_uri status current_module_uri ~capitalize:true
 802                 (UriManager.uri_of_string
 803                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
 804                pp_exp_named_subst exp_named_subst context
 805           | _ -> raise CicExportationInternalError
 806         with
 807            Sys.Break as exn -> raise exn
 808          | _ ->
 809           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
 810            string_of_int n2
 811        )
 812     | C.MutCase (uri,n1,ty,te,patterns) ->
 813        if in_type then
 814         "unit (* TOO POLYMORPHIC TYPE *)"
 815        else (
 816        let rec needs_obj_magic ty =
 817         match CicReduction.whd context ty with
 818          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
 819          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
 820          | _ -> false (* it can be a Rel, e.g. in *_rec *)
 821        in
 822        let needs_obj_magic = needs_obj_magic ty in
 823        (match analyze_term context te with
 824            `Type -> assert false
 825          | `Proof ->
 826              (match patterns with
 827                  [] -> "assert false"   (* empty type elimination *)
 828                | [he] ->
 829                   pp ~in_type:false he context  (* singleton elimination *)
 830                | _ -> assert false)
 831          | `Optimize
 832          | `Term ->
 833             if patterns = [] then "assert false"
 834             else
 835              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
 836                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 837                    C.InductiveDefinition (dl,_,paramsno,_) ->
 838                     let (_,_,_,cons) = get_nth dl (n1+1) in
 839                     let rc =
 840                      List.map
 841                       (fun (id,ty) ->
 842                         (* this is just an approximation since we do not have
 843                            reduction yet! *)
 844                         let rec count_prods toskip =
 845                          function
 846                             C.Prod (_,_,bo) when toskip > 0 ->
 847                              count_prods (toskip - 1) bo
 848                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
 849                           | _ -> 0
 850                         in
 851                          qualified_name_of_uri status current_module_uri
 852                           ~capitalize:true
 853                           (UriManager.uri_of_string
 854                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
 855                          count_prods paramsno ty
 856                       ) cons
 857                     in
 858                     if not (is_mcu_type uri) then rc, "","","",""
 859                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
 860                  | _ -> raise CicExportationInternalError
 861                )
 862               in
 863                let connames_and_argsno_and_patterns =
 864                 let rec combine =
 865                    function
 866                       [],[] -> []
 867                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
 868                     | _,_ -> assert false
 869                 in
 870                  combine (connames_and_argsno,patterns)
 871                in
 872                 go_up ^
 873                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
 874                  (String.concat "\n | "
 875                   (List.map
 876                    (fun (x,argsno,y) ->
 877                      let rec aux argsno context =
 878                       function
 879                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
 880                           let name =
 881                            match name with
 882                               Cic.Anonymous -> Cic.Anonymous
 883                             | Cic.Name n -> Cic.Name (ppid n) in
 884                           let args,res =
 885                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
 886                             bo
 887                           in
 888                            (match analyze_type context ty with
 889                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
 890                              | `Statement
 891                              | `Sort _ -> args,res
 892                              | `Type ->
 893                                  (match name with
 894                                      C.Anonymous -> "_"
 895                                    | C.Name s -> s)::args,res)
 896                        | t when argsno = 0 -> [],pp ~in_type:false t context
 897                        | t ->
 898                           ["{" ^ string_of_int argsno ^ " args missing}"],
 899                            pp ~in_type:false t context
 900                      in
 901                       let pattern,body =
 902                        if argsno = 0 then x,pp ~in_type:false y context
 903                        else
 904                         let args,body = aux argsno context y in
 905                         let sargs = String.concat "," args in
 906                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
 907                           body
 908                       in
 909                        pattern ^ " -> " ^ go_down ^
 910                         (if needs_obj_magic then
 911                          "Obj.magic (" ^ body ^ ")"
 912                         else
 913                          body) ^ go_nwod
 914                    ) connames_and_argsno_and_patterns)) ^
 915                  ")\n"^go_pu)))
 916     | C.Fix (no, funs) ->
 917        let names,_ =
 918         List.fold_left
 919          (fun (types,len) (n,_,ty,_) ->
 920             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 921              len+1)
 922          ) ([],0) funs
 923        in
 924          "let rec " ^
 925          List.fold_right
 926           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
 927             pp ~in_type:false bo (names@context) ^ i)
 928           funs "" ^
 929          " in " ^
 930          (match get_nth names (no + 1) with
 931              Some (Cic.Name n,_) -> n
 932            | _ -> assert false)
 933     | C.CoFix (no,funs) ->
 934        let names,_ =
 935         List.fold_left
 936          (fun (types,len) (n,ty,_) ->
 937             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 938              len+1)
 939          ) ([],0) funs
 940        in
 941          "\nCoFix " ^ " {" ^
 942          List.fold_right
 943           (fun (name,ty,bo) i -> "\n" ^ name ^
 944             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
 945             pp ~in_type:false bo (names@context) ^ i)
 946           funs "" ^
 947          "}\n"
 948 *)
 949
 950 (*
 951 exception CicExportationInternalError;;
 952 exception NotEnoughElements;;
 953
 954 (* *)
 955
 956 let is_mcu_type u =
 957   UriManager.eq (UriManager.uri_of_string
 958   "cic:/matita/freescale/opcode/mcu_type.ind") u
 959 ;;
 960
 961 (* Utility functions *)
 962
 963 let analyze_term context t =
 964  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
 965   | Cic.Sort _ -> `Type
 966   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 967   | ty ->
 968      match
 969       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
 970      with
 971      | Cic.Sort Cic.Prop -> `Proof
 972      | _ -> `Term
 973 ;;
 974
 975 let analyze_type context t =
 976  let rec aux =
 977   function
 978      Cic.Sort s -> `Sort s
 979    | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
 980    | Cic.Prod (_,_,t) -> aux t
 981    | _ -> `SomethingElse
 982  in
 983  match aux t with
 984     `Sort _ | `Optimize as res -> res
 985   | `SomethingElse ->
 986       match
 987        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
 988       with
 989           Cic.Sort Cic.Prop -> `Statement
 990        | _ -> `Type
 991 ;;
 992
 993 let ppid =
 994  let reserved =
 995   [ "to";
 996     "mod";
 997     "val";
 998     "in";
 999     "function"
1000   ]
1001  in
1002   function n ->
1003    let n = String.uncapitalize n in
1004     if List.mem n reserved then n ^ "_" else n
1005 ;;
1006
1007 let ppname =
1008  function
1009     Cic.Name s     -> ppid s
1010   | Cic.Anonymous  -> "_"
1011 ;;
1012
1013 (* get_nth l n   returns the nth element of the list l if it exists or *)
1014 (* raises NotEnoughElements if l has less than n elements             *)
1015 let rec get_nth l n =
1016  match (n,l) with
1017     (1, he::_) -> he
1018   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
1019   | (_,_) -> raise NotEnoughElements
1020 ;;
1021
1022 let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
1023  let name =
1024   if capitalize then
1025    String.capitalize (UriManager.name_of_uri status uri)
1026   else
1027    ppid (UriManager.name_of_uri status uri) in
1028   let filename =
1029    let suri = UriManager.buri_of_uri uri in
1030    let s = String.sub suri 5 (String.length suri - 5) in
1031    let s = Pcre.replace ~pat:"/" ~templ:"_" s in
1032     String.uncapitalize s in
1033   if current_module_uri = UriManager.buri_of_uri uri then
1034    name
1035   else
1036    String.capitalize filename ^ "." ^ name
1037 ;;
1038
1039 let current_go_up = ref "(.!(";;
1040 let at_level2 f x =
1041   try
1042     current_go_up := "(.~(";
1043     let rc = f x in
1044     current_go_up := "(.!(";
1045     rc
1046   with exn ->
1047     current_go_up := "(.!(";
1048     raise exn
1049 ;;
1050
1051 let pp current_module_uri ?metasenv ~in_type =
1052 let rec pp ~in_type t context =
1053  let module C = Cic in
1054    match t with
1055       C.Rel n ->
1056        begin
1057         try
1058          (match get_nth context n with
1059              Some (C.Name s,_) -> ppid s
1060            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
1061            | None -> "_hidden_" ^ string_of_int n
1062          )
1063         with
1064          NotEnoughElements -> string_of_int (List.length context - n)
1065        end
1066     | C.Var (uri,exp_named_subst) ->
1067         qualified_name_of_uri status current_module_uri uri ^
1068          pp_exp_named_subst exp_named_subst context
1069     | C.Meta (n,l1) ->
1070        (match metasenv with
1071            None ->
1072             "?" ^ (string_of_int n) ^ "[" ^
1073              String.concat " ; "
1074               (List.rev_map
1075                 (function
1076                     None -> "_"
1077                   | Some t -> pp ~in_type:false t context) l1) ^
1078              "]"
1079          | Some metasenv ->
1080             try
1081              let _,context,_ = CicUtil.lookup_meta n metasenv in
1082               "?" ^ (string_of_int n) ^ "[" ^
1083                String.concat " ; "
1084                 (List.rev
1085                   (List.map2
1086                     (fun x y ->
1087                       match x,y with
1088                          _, None
1089                        | None, _ -> "_"
1090                        | Some _, Some t -> pp ~in_type:false t context
1091                     ) context l1)) ^
1092                "]"
1093             with
1094               CicUtil.Meta_not_found _
1095             | Invalid_argument _ ->
1096               "???" ^ (string_of_int n) ^ "[" ^
1097                String.concat " ; "
1098                 (List.rev_map (function None -> "_" | Some t ->
1099                   pp ~in_type:false t context) l1) ^
1100                "]"
1101        )
1102     | C.Sort s ->
1103        (match s with
1104            C.Prop  -> "Prop"
1105          | C.Set   -> "Set"
1106          | C.Type _ -> "Type"
1107          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
1108          | C.CProp _ -> "CProp"
1109        )
1110     | C.Implicit (Some `Hole) -> "%"
1111     | C.Implicit _ -> "?"
1112     | C.Prod (b,s,t) ->
1113        (match b with
1114           C.Name n ->
1115            let n = "'" ^ String.uncapitalize n in
1116             "(" ^ pp ~in_type:true s context ^ " -> " ^
1117             pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
1118         | C.Anonymous ->
1119            "(" ^ pp ~in_type:true s context ^ " -> " ^
1120            pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
1121     | C.Cast (v,t) -> pp ~in_type v context
1122     | C.Lambda (b,s,t) ->
1123        (match analyze_type context s with
1124            `Sort _
1125          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
1126          | `Optimize -> prerr_endline "XXX lambda";assert false
1127          | `Type ->
1128             "(function " ^ ppname b ^ " -> " ^
1129              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
1130     | C.LetIn (b,s,ty,t) ->
1131        (match analyze_term context s with
1132          | `Type
1133          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
1134          | `Optimize
1135          | `Term ->
1136             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
1137             " = " ^ pp ~in_type:false s context ^ " in " ^
1138              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
1139     | C.Appl (he::tl) when in_type ->
1140        let hes = pp ~in_type he context in
1141        let stl = String.concat "," (clean_args_for_ty context tl) in
1142         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
1143     | C.Appl (C.MutInd _ as he::tl) ->
1144        let hes = pp ~in_type he context in
1145        let stl = String.concat "," (clean_args_for_ty context tl) in
1146         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
1147     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
1148        let nparams =
1149         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1150            C.InductiveDefinition (_,_,nparams,_) -> nparams
1151          | _ -> assert false in
1152        let hes = pp ~in_type he context in
1153        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
1154         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
1155     | C.Appl li ->
1156        "(" ^ String.concat " " (clean_args context li) ^ ")"
1157     | C.Const (uri,exp_named_subst) ->
1158        qualified_name_of_uri status current_module_uri uri ^
1159         pp_exp_named_subst exp_named_subst context
1160     | C.MutInd (uri,n,exp_named_subst) ->
1161        (try
1162          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1163             C.InductiveDefinition (dl,_,_,_) ->
1164              let (name,_,_,_) = get_nth dl (n+1) in
1165               qualified_name_of_uri status current_module_uri
1166                (UriManager.uri_of_string
1167                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
1168               pp_exp_named_subst exp_named_subst context
1169           | _ -> raise CicExportationInternalError
1170         with
1171            Sys.Break as exn -> raise exn
1172          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
1173        )
1174     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
1175        (try
1176          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1177             C.InductiveDefinition (dl,_,_,_) ->
1178              let _,_,_,cons = get_nth dl (n1+1) in
1179               let id,_ = get_nth cons n2 in
1180                qualified_name_of_uri status current_module_uri ~capitalize:true
1181                 (UriManager.uri_of_string
1182                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
1183                pp_exp_named_subst exp_named_subst context
1184           | _ -> raise CicExportationInternalError
1185         with
1186            Sys.Break as exn -> raise exn
1187          | _ ->
1188           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
1189            string_of_int n2
1190        )
1191     | C.MutCase (uri,n1,ty,te,patterns) ->
1192        if in_type then
1193         "unit (* TOO POLYMORPHIC TYPE *)"
1194        else (
1195        let rec needs_obj_magic ty =
1196         match CicReduction.whd context ty with
1197          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
1198          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
1199          | _ -> false (* it can be a Rel, e.g. in *_rec *)
1200        in
1201        let needs_obj_magic = needs_obj_magic ty in
1202        (match analyze_term context te with
1203            `Type -> assert false
1204          | `Proof ->
1205              (match patterns with
1206                  [] -> "assert false"   (* empty type elimination *)
1207                | [he] ->
1208                   pp ~in_type:false he context  (* singleton elimination *)
1209                | _ -> assert false)
1210          | `Optimize
1211          | `Term ->
1212             if patterns = [] then "assert false"
1213             else
1214              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
1215                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1216                    C.InductiveDefinition (dl,_,paramsno,_) ->
1217                     let (_,_,_,cons) = get_nth dl (n1+1) in
1218                     let rc =
1219                      List.map
1220                       (fun (id,ty) ->
1221                         (* this is just an approximation since we do not have
1222                            reduction yet! *)
1223                         let rec count_prods toskip =
1224                          function
1225                             C.Prod (_,_,bo) when toskip > 0 ->
1226                              count_prods (toskip - 1) bo
1227                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
1228                           | _ -> 0
1229                         in
1230                          qualified_name_of_uri status current_module_uri
1231                           ~capitalize:true
1232                           (UriManager.uri_of_string
1233                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
1234                          count_prods paramsno ty
1235                       ) cons
1236                     in
1237                     if not (is_mcu_type uri) then rc, "","","",""
1238                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
1239                  | _ -> raise CicExportationInternalError
1240                )
1241               in
1242                let connames_and_argsno_and_patterns =
1243                 let rec combine =
1244                    function
1245                       [],[] -> []
1246                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
1247                     | _,_ -> assert false
1248                 in
1249                  combine (connames_and_argsno,patterns)
1250                in
1251                 go_up ^
1252                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
1253                  (String.concat "\n | "
1254                   (List.map
1255                    (fun (x,argsno,y) ->
1256                      let rec aux argsno context =
1257                       function
1258                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
1259                           let name =
1260                            match name with
1261                               Cic.Anonymous -> Cic.Anonymous
1262                             | Cic.Name n -> Cic.Name (ppid n) in
1263                           let args,res =
1264                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
1265                             bo
1266                           in
1267                            (match analyze_type context ty with
1268                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
1269                              | `Statement
1270                              | `Sort _ -> args,res
1271                              | `Type ->
1272                                  (match name with
1273                                      C.Anonymous -> "_"
1274                                    | C.Name s -> s)::args,res)
1275                        | t when argsno = 0 -> [],pp ~in_type:false t context
1276                        | t ->
1277                           ["{" ^ string_of_int argsno ^ " args missing}"],
1278                            pp ~in_type:false t context
1279                      in
1280                       let pattern,body =
1281                        if argsno = 0 then x,pp ~in_type:false y context
1282                        else
1283                         let args,body = aux argsno context y in
1284                         let sargs = String.concat "," args in
1285                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
1286                           body
1287                       in
1288                        pattern ^ " -> " ^ go_down ^
1289                         (if needs_obj_magic then
1290                          "Obj.magic (" ^ body ^ ")"
1291                         else
1292                          body) ^ go_nwod
1293                    ) connames_and_argsno_and_patterns)) ^
1294                  ")\n"^go_pu)))
1295     | C.Fix (no, funs) ->
1296        let names,_ =
1297         List.fold_left
1298          (fun (types,len) (n,_,ty,_) ->
1299             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1300              len+1)
1301          ) ([],0) funs
1302        in
1303          "let rec " ^
1304          List.fold_right
1305           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
1306             pp ~in_type:false bo (names@context) ^ i)
1307           funs "" ^
1308          " in " ^
1309          (match get_nth names (no + 1) with
1310              Some (Cic.Name n,_) -> n
1311            | _ -> assert false)
1312     | C.CoFix (no,funs) ->
1313        let names,_ =
1314         List.fold_left
1315          (fun (types,len) (n,ty,_) ->
1316             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1317              len+1)
1318          ) ([],0) funs
1319        in
1320          "\nCoFix " ^ " {" ^
1321          List.fold_right
1322           (fun (name,ty,bo) i -> "\n" ^ name ^
1323             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
1324             pp ~in_type:false bo (names@context) ^ i)
1325           funs "" ^
1326          "}\n"
1327 and pp_exp_named_subst exp_named_subst context =
1328  if exp_named_subst = [] then "" else
1329   "\\subst[" ^
1330    String.concat " ; " (
1331     List.map
1332      (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
1333      exp_named_subst
1334    ) ^ "]"
1335 and clean_args_for_constr nparams context =
1336  let nparams = ref nparams in
1337  HExtlib.filter_map
1338   (function t ->
1339     decr nparams;
1340     match analyze_term context t with
1341        `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
1342      | `Optimize
1343      | `Term
1344      | `Type
1345      | `Proof -> None)
1346 and clean_args context =
1347  function
1348  | [] | [_] -> assert false
1349  | he::arg1::tl as l ->
1350     let head_arg1, rest =
1351        match analyze_term context arg1 with
1352       | `Optimize ->
1353          !current_go_up :: pp ~in_type:false he context ::
1354                  pp ~in_type:false arg1 context :: ["))"], tl
1355       | _ -> [], l
1356     in
1357     head_arg1 @
1358     HExtlib.filter_map
1359      (function t ->
1360        match analyze_term context t with
1361         | `Term -> Some (pp ~in_type:false t context)
1362         | `Optimize ->
1363             prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
1364         | `Type
1365         | `Proof -> None) rest
1366 and clean_args_for_ty context =
1367  HExtlib.filter_map
1368   (function t ->
1369     match analyze_term context t with
1370        `Type -> Some (pp ~in_type:true t context)
1371      | `Optimize -> None
1372      | `Proof -> None
1373      | `Term -> None)
1374 in
1375  pp ~in_type
1376 ;;
1377
1378 let ppty current_module_uri =
1379  (* nparams is the number of left arguments
1380     left arguments should either become parameters or be skipped altogether *)
1381  let rec args nparams context =
1382   function
1383      Cic.Prod (n,s,t) ->
1384       let n =
1385        match n with
1386           Cic.Anonymous -> Cic.Anonymous
1387         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1388       in
1389        (match analyze_type context s with
1390          | `Optimize
1391          | `Statement
1392          | `Sort Cic.Prop ->
1393              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1394          | `Type when nparams > 0 ->
1395              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1396          | `Type ->
1397              let abstr,args =
1398               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
1399                abstr,pp ~in_type:true current_module_uri s context::args
1400          | `Sort _ when nparams <= 0 ->
1401              let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
1402               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1403          | `Sort _ ->
1404              let n =
1405               match n with
1406                  Cic.Anonymous -> Cic.Anonymous
1407                | Cic.Name name -> Cic.Name ("'" ^ name) in
1408              let abstr,args =
1409               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1410              in
1411               (match n with
1412                   Cic.Anonymous -> abstr
1413                 | Cic.Name name -> name::abstr),
1414               args)
1415    | _ -> [],[]
1416  in
1417   args
1418 ;;
1419
1420 exception DoNotExtract;;
1421
1422 let pp_abstracted_ty current_module_uri =
1423  let rec args context =
1424   function
1425      Cic.Lambda (n,s,t) ->
1426       let n =
1427        match n with
1428           Cic.Anonymous -> Cic.Anonymous
1429         | Cic.Name n -> Cic.Name (String.uncapitalize n)
1430       in
1431        (match analyze_type context s with
1432          | `Optimize
1433          | `Statement
1434          | `Type
1435          | `Sort Cic.Prop ->
1436              args ((Some (n,Cic.Decl s))::context) t
1437          | `Sort _ ->
1438              let n =
1439               match n with
1440                  Cic.Anonymous -> Cic.Anonymous
1441                | Cic.Name name -> Cic.Name ("'" ^ name) in
1442              let abstr,res =
1443               args ((Some (n,Cic.Decl s))::context) t
1444              in
1445               (match n with
1446                   Cic.Anonymous -> abstr
1447                 | Cic.Name name -> name::abstr),
1448               res)
1449    | ty ->
1450      match analyze_type context ty with
1451       | `Optimize ->
1452            prerr_endline "XXX abstracted l2 ty"; assert false
1453       | `Sort _
1454       | `Statement -> raise DoNotExtract
1455       | `Type ->
1456           (* BUG HERE: this can be a real System F type *)
1457           let head = pp ~in_type:true current_module_uri ty context in
1458           [],head
1459  in
1460   args
1461 ;;
1462
1463
1464 (* ppinductiveType (typename, inductive, arity, cons)                       *)
1465 (* pretty-prints a single inductive definition                              *)
1466 (* (typename, inductive, arity, cons)                                       *)
1467 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
1468 =
1469  match analyze_type [] arity with
1470     `Sort Cic.Prop -> ""
1471   | `Optimize
1472   | `Statement
1473   | `Type -> assert false
1474   | `Sort _ ->
1475     if cons = [] then
1476      "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
1477     else (
1478      let abstr,scons =
1479       List.fold_right
1480        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
1481           let abstr',sargs = ppty current_module_uri nparams [] ty in
1482           let sargs = String.concat " * " sargs in
1483            abstr',
1484            String.capitalize id ^
1485             (if sargs = "" then "" else " of " ^ sargs) ^
1486             (if i = "" then "" else "\n | ") ^ i)
1487        cons ([],"")
1488       in
1489        let abstr =
1490         let s = String.concat "," abstr in
1491         if s = "" then "" else "(" ^ s ^ ") "
1492        in
1493        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
1494 ;;
1495
1496 let ppobj current_module_uri obj =
1497  let module C = Cic in
1498  let module U = UriManager in
1499   let pp ~in_type = pp ~in_type current_module_uri in
1500   match obj with
1501     C.Constant (name, Some t1, t2, params, _) ->
1502       (match analyze_type [] t2 with
1503         | `Sort Cic.Prop
1504         | `Statement -> ""
1505         | `Optimize
1506         | `Type ->
1507             (match t1 with
1508             | Cic.Lambda (Cic.Name arg, s, t) ->
1509                             (match analyze_type [] s with
1510                 | `Optimize ->
1511
1512                     "let " ^ ppid name ^ "__1 = function " ^ ppid arg
1513                     ^ " -> .< " ^
1514                     at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)]
1515                     ^ " >. ;;\n"
1516                     ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
1517                     ^ "let " ^ ppid name ^ " = function " ^ ppid arg
1518                     ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic  !"^ppid name
1519                     ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
1520                     ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
1521                     ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
1522                     ^ppid name^"__2)) >.\n;;\n"
1523                     ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
1524                     name^" Matita_freescale_opcode.HCS08)"
1525                 | _ ->
1526                    "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1527             | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1528         | `Sort _ ->
1529             match analyze_type [] t1 with
1530                `Sort Cic.Prop -> ""
1531              | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
1532              | _ ->
1533                (try
1534                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
1535                  let abstr =
1536                   let s = String.concat "," abstr in
1537                   if s = "" then "" else "(" ^ s ^ ") "
1538                  in
1539                   "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
1540                 with
1541                  DoNotExtract -> ""))
1542    | C.Constant (name, None, ty, params, _) ->
1543       (match analyze_type [] ty with
1544           `Sort Cic.Prop
1545         | `Optimize -> prerr_endline "XXX axiom l2"; assert false
1546         | `Statement -> ""
1547         | `Sort _ -> "type " ^ ppid name ^ "\n"
1548         | `Type -> "let " ^ ppid name ^ " = assert false\n")
1549    | C.Variable (name, bo, ty, params, _) ->
1550       "Variable " ^ name ^
1551        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1552        ")" ^ ":\n" ^
1553        pp ~in_type:true ty [] ^ "\n" ^
1554        (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
1555    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
1556       "Current Proof of " ^ name ^
1557        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1558        ")" ^ ":\n" ^
1559       let separate s = if s = "" then "" else s ^ " ; " in
1560        List.fold_right
1561         (fun (n, context, t) i ->
1562           let conjectures',name_context =
1563                  List.fold_right
1564                   (fun context_entry (i,name_context) ->
1565                     (match context_entry with
1566                         Some (n,C.Decl at) ->
1567                          (separate i) ^
1568                            ppname n ^ ":" ^
1569                             pp ~in_type:true ~metasenv:conjectures
1570                             at name_context ^ " ",
1571                             context_entry::name_context
1572                       | Some (n,C.Def (at,aty)) ->
1573                          (separate i) ^
1574                            ppname n ^ ":" ^
1575                             pp ~in_type:true ~metasenv:conjectures
1576                             aty name_context ^
1577                            ":= " ^ pp ~in_type:false
1578                             ~metasenv:conjectures at name_context ^ " ",
1579                             context_entry::name_context
1580                       | None ->
1581                          (separate i) ^ "_ :? _ ", context_entry::name_context)
1582             ) context ("",[])
1583           in
1584            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
1585             pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
1586         ) conjectures "" ^
1587         "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
1588           pp ~in_type:true ~metasenv:conjectures ty []
1589    | C.InductiveDefinition (l, params, nparams, _) ->
1590       List.fold_right
1591        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
1592 ;;
1593
1594 let ppobj current_module_uri obj =
1595  let res = ppobj current_module_uri obj in
1596   if res = "" then "" else res ^ ";;\n\n"
1597 ;;
1598 *)
1599 *)