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