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